How small can a foundation be?
joeshipman at aol.com
Sun Feb 16 08:47:15 EST 2020
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.
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
More information about the FOM