How small can a foundation be?

[katzmik at macs.biu.ac.il]

Hi Joe,

People might have an easier time responding to your message had you formulated
your observation as a question: "Does there exist, for every mathematical
proposition you care about, 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?"

M. Katz

On Sat, February 15, 2020 06:29, Joe Shipman wrote:
> 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
>