[FOM] 838: New Tangible Incompleteness/1

[Harvey Friedman]

The advances since
https://cs.nyu.edu/pipermail/fom/2019-October/021735.html have been
numerous and strong, especially expositionally, that we use the above
subject line.

As promised, #110 is now on my website
https://u.osu.edu/friedman.8/foundational-adventures/downloadable-manuscripts/

My favorite lead statements for the mathematician uses maximal
squares, where a square is a set of the form S^2. I have shifted to NQ
which is the set of all nonnegative rational numbers.

Everybody knows that every E containedin NQ^k has a maximal S^2 containedin E.

Here is a nice piece of Ramsey combinatorics:

FINITE EMBEDDED MAXIMAL SQUARES. FEMS. For strictly increasing finite
f_1,...,f_n::NQ into NQ and order invariant E containedin NQ^k, some
maximal S^2 containedin E is f_1,...,f_n embedded.

Here we use :: for partial functions.

EXTENDED FINITE EMBEDDED MAXIMAL SQUARES. FEMS. For strictly
increasing extended finite f_1,...,f_n::NQ into NQ and order invariant
E containedin NQ^k, some maximal S^2 containedin E is f_1,...,f_n
embedded.

This innocent looking change takes us from Con(PA) all the way up to Con(SRP).

Here extended means extended by the identity function to the right of
dom(f) union rng(f).

For gifted high school students, it is better to use emulators:

Every E containedin NQ^k has a maximal emulator.
FINITE EMBEDDED MAXIMAL EMULATORS. FEME. For strictly increasing
finite f_1,...,f_n:NQ into NQ and finite E containedin NQ^k, some
maximal emulator of E is f_1,...,f_n embedded.
EXTENDED FINITE EMBEDDED MAXIMAL EMULATORS. FEME. For strictly
increasing extended finite f_1,...,f_n:NQ into NQ and finite E
containedin NQ^k, some maximal emulator of E is f_1,...,f_n embedded.

For gifted high school, there is a big focus on dimension k = 2, and
the single function f that maps 0 to 1 with domain {0}. In this case,
of course we don't need to even explain what embeddings are. We have
only to state the following conditions on S containedin NQ^2:

For p > 1, (p,0) in S iff (p,1) in S.
For p > 1, (0,p) in S iff (1,p) in S.
(0,0) in S iff (1,1) in S.

There is also major advances in the explicitly finite forms, which are
now very thematic and arguably most natural with emulators.

Everything is explained clearly in #110,
https://u.osu.edu/friedman.8/foundational-adventures/downloadable-manuscripts/

#######################################
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 838th 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
808: Big Foundational Issues/2  5/1/18  12:24AM
809: Goedel's Second Reworked/1  5/20/18  3:47PM
810: Goedel's Second Reworked/2  5/23/18  10:59AM
811: Big Foundational Issues/3  5/23/18  10:06PM
812: Goedel's Second Reworked/3  5/24/18  9:57AM
813: Beyond Perfectly Natural/12  05/29/18  6:22AM
814: Beyond Perfectly Natural/13  6/3/18  2:05PM
815: Beyond Perfectly Natural/14  6/5/18  9:41PM
816: Beyond Perfectly Natural/15  6/8/18  1:20AM
817: Beyond Perfectly Natural/16  Jun 13 01:08:40
818: Beyond Perfectly Natural/17  6/13/18  4:16PM
819: Sugared ZFC Formalization/1  6/13/18  6:42PM
820: Sugared ZFC Formalization/2  6/14/18  6:45PM
821: Beyond Perfectly Natural/18  6/17/18  1:11AM
822: Tangible Incompleteness/1  7/14/18  10:56PM
823: Tangible Incompleteness/2  7/17/18  10:54PM
824: Tangible Incompleteness/3  7/18/18  11:13PM
825: Tangible Incompleteness/4  7/20/18  12:37AM
826: Tangible Incompleteness/5  7/26/18  11:37PM
827: Tangible Incompleteness Restarted/1  9/23/19  11:19PM
828: Tangible Incompleteness Restarted/2  9/23/19  11:19PM
829: Tangible Incompleteness Restarted/3  9/23/19  11:20PM
830: Tangible Incompleteness Restarted/4  9/26/19  1:17 PM
831: Tangible Incompleteness Restarted/5  9/29/19  2:54AM
832: Tangible Incompleteness Restarted/6  10/2/19  1:15PM
833: Tangible Incompleteness Restarted/7  10/5/19  2:34PM
834: Tangible Incompleteness Restarted/8  10/10/19  5:02PM
835: Tangible Incompleteness Restarted/9  10/13/19  4:50AM
836: Tangible Incompleteness Restarted/10  10/14/19  12:34PM
837: Tangible Incompleteness Restarted/11 10/18/20  02:58AM

Harvey Friedman