[FOM] 808: Big Foundational Issues/2

[Joe Shipman]

We have many different ways of picking out a collection of true sentences about HF, which, when augmented with a standard form of the axiom of infinity, axiomatize ZFC. The simplest way to do this starts with a theory for HF which is equivalent in a very strong sense to PA (isomorphism between HF under the membership relation “x is an element of y” and N under the relation “2^x is included when y is written as a sum of distinct powers of 2”) . Here are some questions:

What is the weakest natural subtheory of HF such that, when you adjoin the axiom of infinity to it, you get ZFC? Ditto for getting ZF.

What is the strongest natural axiomatizable subtheory of ZFC that is true when interpreted as being about HF? Can we do better than “ZFC - AxInf” while being more natural than “all propositions P such that ZFC |- (P & (HF |= P))”?

— JS

> On May 1, 2018, at 12:24 AM, Harvey Friedman <hmflogic at gmail.com> wrote:
> 
> This continues https://cs.nyu.edu/pipermail/fom/2018-April/020907.html
> 
> 1. IN PRECISELY WHAT SENSE DO WE EVEN HAVE A FOUNDATION FOR
> MATHEMATICS? I.e., WHAT DOES ZFC REALLY ACCOMPLISH?
> 
> There is a well established mathematical style of definition, theorem,
> proof that is readily recognized and readily accepted and readily used
> by mathematicians across all fields and levels of experience. Let us
> conveniently call this set theoretic foundations by the name ZFC,
> which is the standard formal system associated with it. (But as we
> will ultimately discuss, there are some important fragments and
> variants).
> 
> ZFC may not be the preferred way of doing things for many
> mathematicians. E.g., to varying extents, some may prefer rather
> abstract formulations based on category theoretic ideas. But these are
> considered very illuminating, somewhat illuminating, somewhat of a
> frill, somewhat of a nuisance, a major nuisance, an incoherent
> nuisance, and so forth, depending on the individual mathematician and
> sometimes area of expertise. And, in fact, there is a standard way to
> more or less capture advantages of such abstract formulations and
> approaches by up front definitions in terms of set theory (e.g., the
> approach taken at the beginning of Mac Lane, Categories for a Working
> Mathematician).
> 
> NEVERTHELESS, there is a commonality to the ZFC approach, that every
> competent mathematician is acceptably comfortable viewing themselves
> as working within its framework. Of course, many mathematicians are
> totally agnostic and unreflective about what "framework" they are
> working in, and either don't care, or think that mathematics itself is
> "beyond needing or resting on any kind of framework".
> 
> In contrast, for example, some people are seriously proposing some
> sort of rather abstract rethinking of the notion of equality. At this
> particular stage of research on this, the vast majority of
> mathematicians want to completely ignore this, and when confronted too
> aggressively with this, will recoil, viewing this as an unwanted
> incoherent nuisance of a particularly obnoxious character, to be
> avoided at all possible costs. The general disgust with things like
> this is far greater than the general displeasure with sets.
> 
> Of course, in this series of postings, I am aiming at organizing my
> thoughts and my results and future results in a way that adds new
> insights. So what, for example, have I or do I want to say about all
> this?
> 
> Quite a bit, and hopefully quite a bit that I have not previously said.
> 
> One thing I have worked on, announced in various talks, discussed on
> the FOM, but did not write up proofs, is that, in a certain hard nosed
> and perhaps surprising sense,
> 
> ZFC RESULTS FROM TAKING ALL TRUE STATEMENTS ABOUT THE HEREDITARILY
> FINITE SETS OF A CERTAIN NATURAL FORM AND ADDING THE AXIOM OF
> INFINITY.
> 
> I.e., ZFC naturally arises from going from the finite to the infinite.
> 
> This result(s) go back decades, but I want to revisit this with a
> fresh (older) mind.
> 
> Of course, this addresses just one of many important aspects of issue
> 1. But it does gives us the following scenario.
> 
> Pretty much all mathematicians can get on the same page with regard to
> the hereditarily finite sets. We can start with the semi formal
> intuitively clear picture:
> 
> There are no sets of rank <= 0.
> The sets of rank <= n+1 are the sets all of whose elements are sets of
> rank <= n.
> 
> Even here there are some things that need to be said especially for
> the neophyte. Specifically, here sets are extensional, and also there
> are canonical terms for sets (this requires a little thought).
> 
> So there is a pretty clear picture of a structure (HF,epsilon), the
> universe of hereditarily finite sets under the epsilon relation, and a
> lot of cute little easy theorems can be profitably proved about this
> structure and its uniqueness up to isomorphism, so that one has a kind
> of satisfying mathematical theory going.
> 
> We are so far on very solid grounds, with a completely clear and
> completely appropriate equality relation (avoiding any abstract
> fiddling), and also a completely clear and completely appropriate
> epsilon relation.
> 
> Of course, one can raise the issue: which is more fundamental, the
> nonnegative integers or the hereditarily finite sets?
> 
> That is a tricky question, and the obvious answer is that each is more
> fundamental in some important respects than the other. On a practical
> note, there is the idea of my redoing what I have done bringing in the
> nonnegative integers along with or instead of or whatever, the HF. But
> I don't want to go there right now.
> 
> NOW HERE is the main point. There are obviously plenty of sentences
> true (and very provable) about (HF,epsilon) that are false (and very
> refutable) about any of the usual extensions of (HF,epsilon) such as
> (V,epsion), whatever exactly V means.
> 
> BUT we teach all kinds of beautiful sentences about (HF,epsilon). and
> these generally lift to (V,epsilon).
> 
> WHAT are these beautiful sentences? Can we algorithmically recognize
> them? Can we axiomatize them?
> 
> So we have now pretty much caved out a little bit of a tree structure:
> 
> 1. IN PRECISELY WHAT SENSE DO WE EVEN HAVE A FOUNDATION FOR
> MATHEMATICS? I.e., WHAT DOES ZFC REALLY ACCOMPLISH?
> 1.1. FROM FINITE TO INFINITE.
> 
> ************************************************************************
> My website is at https://u.osu.edu/friedman.8/ and my youtube site is at
> https://www.youtube.com/channel/UCdRdeExwKiWndBl4YOxBTEQ
> This is the 808th in a series of self contained numbered
> postings to FOM covering a wide range of topics in f.o.m. The list of
> previous numbered postings #1-799 can be found at
> http://u.osu.edu/friedman.8/foundational-adventures/fom-email-list/
> 
> 800: Beyond Perfectly Natural/6  4/3/18  8:37PM
> 801: Big Foundational Issues/1  4/4/18  12:15AM
> 802: Systematic f.o.m./1  4/4/18  1:06AM
> 803: Perfectly Natural/7  4/11/18  1:02AM
> 804: Beyond Perfectly Natural/8  4/12/18  11:23PM
> 805: Beyond Perfectly Natural/9  4/20/18  10:47PM
> 806: Beyond Perfectly Natural/10  4/22/18  9:06PM
> 807: Beyond Perfectly Natural/11  4/29/18  9:19PM
> 
> Harvey Friedman
> _______________________________________________
> FOM mailing list
> FOM at cs.nyu.edu
> https://cs.nyu.edu/mailman/listinfo/fom