How small can a foundation be?

[Joe Shipman]

My observation is practically a truism, as long as their acceptable methods of proof are algorithmically formalizable then “their methods prove X” can be rendered as a statement in set theory (or even arithmetic).

I actually hold to a stronger version than I (conservatively) stated, which is that there is generally going to be a way to do this by representing the objects their proposition discusses by some standard set-theoretic equivalents, and translating the proof methods into antecedents, so that a follower of Grothendieck would agree that if his proposition is provable then ZFC proves the Grothendieck Universes axiom implies the translation of his proposition into set theory.

— JS

Sent from my iPhone

> On Feb 16, 2020, at 7:44 AM, katzmik at macs.biu.ac.il wrote:
> 
> 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
>> 
> 
>