# "Irreducible" axiomatic systems?

So I was playing with axiomatic / formal systems and wanted to look into this property about formal systems which could be called "irreducibility". It is similar to independence in that it restricts the axioms from having redundant information.

Here is how I define the property. Suppose we have a theorem $$T$$ in our system, and it can be proved using a set of axioms $$A$$, and can alternately be proved using another set of axioms $$B$$. If our system is irreducible, we demand that T can be proven using the axioms in $$A \cap B$$.

First of all, is this property even interesting? Do number theory systems like Peano arithmetic satisfy this property? (I think it would be strange if they didn't!) Irreducibility clearly implies independence, but could the converse be true?

• Commented May 23 at 7:25

$$P \land Q$$ and $$P \land R$$ both imply $$P$$ while not implying each other, and so you can easily have independence without irreducibility. Indeed, your notion of irreducibility still allows for these kinds of 'redundancies'.