How small can a foundation be?

[Joe Shipman]

I am unmoved by discussions about ontology or about whether set theory is essential to mathematics.  What ought to be clear to everyone is:

Whatever your ontology or axiomatics or language, for any mathematical proposition you care about, there is a straightforwardly obtainable proposition of set theory that is provable in ZFC if the proposition you care about has a proof that you would accept as valid.

But do we really need to start with all of ZFC? Here’s what I don’t need:
1) I don’t need equality, I can define it given extensionality in the form “sets with the same members are members of the same sets”.
2) I don’t need foundation, because I can talk about the well-founded sets and that’s enough to accomplish the foundational purpose I described above.
3) I don’t need a scheme with infinitely many axioms, because I can interpret the membership relation as applying to classes and defining sets as those classes which are members of something, and class theories like NBG are finitely axiomatizable and prove the same theorems about sets that ZFC does.
4) I don’t need exactly ZFC’s strength. If there’s a stronger theory, for example with some large cardinal, that’s easier to formally axiomatize than ZFC I’m ok with that.

What’s the *simplest axiomatization* for the binary elementhood relation that suffices for this? (You may interpret “simplest” as either “shortest” or “easiest” as you prefer, and you’re allowed to use definitions to create new functions or relations or constants if that makes things simpler.)

Bonus criterion: it would be especially nice if the axiomatization contains an axiom of infinity such that, when you take away that axiom, the remaining ones are modeled by using the HF sets as sets and subsets of the HF sets as classes, giving something that looks like second order arithmetic.

An alternative approach is to make the axiomatization complicated but the development easy; however I’d rather do it this way first.

— JS


Sent from my iPhone