[FOM] 817: Beyond Perfectly Natural/16

Wed Jun 13 01:08:40 EDT 2018

NOTE: There has been updates, dated June 12, 2018, at

https://u.osu.edu/friedman.8/foundational-adventures/downloadable-manuscripts/
   #105, 106.

#######################

In this posting, I want to discuss the general structure of the prospective book

CONCRETE MATHEMATICAL INCOMPLETENESS

I am thinking of three Parts:

PART 1. Boolean Relation Theory.
PART 2. Emulation Theory.
PART 3. Inductive Equation Theory.

Part 1 has been stable for some time. See
https://u.osu.edu/friedman.8/foundational-adventures/boolean-relation-theory-book/

GENERAL PLAN FOR PARTS 2,3. Given the rich amount of varied material,
interlocking between parts 2,3, I have (tentatively) decided on the
following expositional plan. The actual Parts 2,3 will contain all but
the BIG PROOFS. The big proofs are of course proofs of various
statements from Con(SRP), and proofs of Con(SRP) from various
statements. Also, from and to Con(HUGE). These BIG PROOFS are put in
four Appendices:

WKL_0 + Con(SRP) implies A.
RCA_0 + B implies Con(SRP).
WKL_0 + Con(HUGE) implies C.
RCA_0 + D implies Con(HUGE).

A,B,C,D are carefully formulated so that they support all of the
claims made in Parts 2,3 about various statements. In the actual Parts
2,3, there are complete proofs of the claims made there MODULO THESE
FOUR APPENDICES.

At various places in Parts 2,3, explicitly finite statements are given
and claimed to be equivalent to Con(SRP) or Con(HUGE). I am thinking
that complete proofs of these claims will not merit additional
Appendices, expecting reasonably friendly proofs that these finite
statements are equivalent to infinite statements that are already
treated.

There may have to be another Appendix, perhaps connected with a
potentially big proofs supporting Decision Procedures. This remains to
be seen.

There are some advantages about putting them in APPENDICES.
i. The reader is not interrupted by supercharged technical proofs, and
can relax with lots of delicious information being rolled out
leisurely, and some friendly proofs.
ii. This process avoids having to do any major proofs twice. The plan
is to find one core fundamental formulations for each of these FOUR
BIG PROOFS that links naturally with both Parts 2,3.

PART 2. Emulation Theory, with its delicious notion of an emulator, is
the only place where we claim outright to have a ZFC Incompleteness
from Everybody's Mathematics, namely MES = Maximal Emulation
Stability. One of the FUTURISTIC IDEAS is that this notion makes
perfectly good sense for virtually any mathematical structure in
virtually any mathematical context. I did lay some groundwork in
anticipation of a general theory, or at least where we put some more
structure. Especially see

https://u.osu.edu/friedman.8/foundational-adventures/downloadable-manuscripts/
  #92

which is to appear in the upcoming Putnam volume, ed. R. Cook and G.
Hellman. Also see at the same link, #100, section 1, and #105, section
7.

Within Emulation Theory there will be many sections and subsections,
and these have evolved some.

2.1. Emulators in Rational Intervals.
   2.1.1. Order Equivalence, Emulators.
   2.1.2. Stability, Invariance, Embeddings.
   2.1.3. Step, Internal, Initial Maximality.
   2.1.4. Templates, Decision Procedures.
2.2. Emulators in N.
2.3. Emulators in {0,...,t}.
2.4. Finite Solitaire Games.

There is material under 2.3, 2.4 with the Finite MES = FMES material,
and Solitaire Games material, at

https://u.osu.edu/friedman.8/foundational-adventures/downloadable-manuscripts/
   #106.

PART 3. Inductive Equation Theory. Right now, the only equations I am
using are based on the upper image construction, R<[S] = {y: there
exists x < y from S with x R y}.

3.1. Upper Images in Q.
   3.1.1. Upper Shift, Order Invariance, R<[S].
   3.1.2. S = E^k\R<[S].
   3.1.3. S = S#\R<[S].
   3.1.4. Limited 1-sections.
   3.1.5. Templates, Decision Procedures.
3.2. Upper Images in N.
3.3. Upper Images in {0,...,t}.
3.4. Finite Solitaire Games.

The Set Equations based on Upper Images have a built in inductive
structure that Maximal Emulators do not have. Solutions to these Set
Equations are like very special maximal emulators. However, they
become more closely related when we deal with the Initial Maximality
of section 2.1.3.

The natural setting for our HUGE stuff is at section 3.1.4. HUGE seems
more natural in the Inductive Equation setting than in the Maximal
Emulator setting.

Section 3.4 will include Solitaire Games associated with HUGE.

NEXT ON THE AGENDA. To give a clear account as to what goes into the
above sections, without proofs. These sections are at various levels
of development. And then fix on the A,B,C,D for the four Appendices.

************************************************************************
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 817th 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

Harvey Friedman