How many axioms can you remove from ZF set theory and still have an "interesting" version of mathematics?

Question

Obviously you can remove the axiom of choice from ZFC set theory to get ZF set theory. Using ZF only you can still construct most of mathematics and proofs.

This led me to wonder how many more axioms could you remove and still form some kind of complicated quasi-mathematical structure. In the sense that one could combine the axioms together to create theorems that are non-trivial and non-predictable?

As the axioms are similar to string replacement rules, I would imagine you could create interesting theorems starting with just 2 axioms.

The list of axioms are:

1. Axiom of extensionality
2. Axiom of regularity
3. Axiom schema of specification
4. Axiom of pairing
5. Axiom of union
6. Axiom schema of replacement
7. Axiom of infinity
8. Axiom of power set
9. Well-ordering theorem OR axiom of choice.

How many could you remove and still have an intersting quasi-set theory?

I would define "interesting" in this sense as that a theorem would have a non-obvious proof.

Perhaps even some axioms are not needed in much of modern mathematics?

Answer 1

Taking the stance

I would define "interesting" in this sense as that a theorem would have a non-obvious proof

entirely seriously, one sufficient criterion for interestingness in this case would be essential incompleteness: a consistent computably axiomatizable theory is essentially incomplete iff it has no consistent computable completion. Note that this is stronger than mere incompleteness; for example, the theory of algebraically closed fields is computably axiomatizable and incomplete, but is contained in the computable consistent complete theory of algebraically closed fields of characteristic $17$.

It turns out that essential incompleteness shows up quite early on indeed! For example, Montagna and Mancini showed that we already wind up with an essentially incomplete theory once we can show that the empty set exists and that we can always adjoin new individual elements to existing sets. In fact (this really just follows from the same argument), the problem of deciding which sentences are theorems of this theory $\mathsf{N}$ is exactly as hard as the problem of deciding which sentences are theorems of $\mathsf{ZFC}$.