[FOM] 840: New Tangible Incompleteness/3

[Harvey Friedman]

Breakthru expositionally in the HUGE cardinal level. Don't
underestimate the power of such improvements.

This also leads to the real possibility of a DECISION PROCEDURE making
the HUGE cardinal stuff very THEMATIC.

So again we are in the realm of Chapter 3 of the book, on SET EQUATIONS.

SO WE START OVER SUPERSEDING 839,
https://cs.nyu.edu/pipermail/fom/2020-January/021886.html

DEFINITION 1. Let S containedin Q^k. S# is the least A^k containing S
and (0,...,0). S^<= = {x in S: x_1 <= ... <= x_k}. S^>= = {x in S: x_1
>= ... >= x_k}. S is upper
unbounded if and only if there are arbitrary large rationals appearing
a coordinates of elements of S. Let R containedin Q^2k. R<[S] = {y in
Q^: there exists x in S such that max(x) < max(y) and x R y}.

DEFINITION 2. The upper shift of x in Q^k results from adding 1 to all
nonnegative coordinates of x. We write ush(x). The upper shift of S
containedin Q^k is {ush(x): x in S}. We write ush(S).

DEFINITION 3. B containedin Q^k is order theoretic in S containedin
Q^k if and only if B is some {x in S: phi(x)}, where phi is a
quantifier free formula over (Q,<) with parameters allowed.

The most basic set equation that we consider is

S = S#\R<[S]

where S is the unknown subset of Q^k and R containedin Q^2k.

PROPOSITION A. Every order invariant R containedin Q^2k has an S =
S#\R<[S] containing ush(S).

THEOREM 1. Proposition A is provably equivalent to Con(SRP) over
WKL_0. The implication to Con(SRP) is provable in RCA_0,

PROPOSITION B. Every order invariant R containedin Q^2k has an S =
S^>= U (S#^<=\R<[S]) where upper shifts of upper bounded order
theoretic subsets are order theoretic subsets.

THEOREM 2. Proposition B is provably equivalent to Con(HUGE) over
WKL_0. The implication to Con(HUGE) is provable in RCA_0.

It can be shown that Propositions A,B are implicitly Pi01 via the
Goedel Completeness Theorem. This a priori argument is not as
straightforward as it was for Embedded Maximality (part 2 of book),
and uses nonstandard models.

Here HUGE = ZFC + {there exists j:V(lambda) into V(mu) such that
j^k(kappa) < lambda}_k. Here kappa is the critical point of j.

Now we readily see the following general Template.

TEMPLATE. Every order invariant R containedin Q^2k has an S = Gamma(S)
where upper shifts of upper bounded order theoretic subsets are order
theoretic subsets.

Here Gamma is a simple set theoretic expression in S. The one we use
for Proposition B is a Boolean combination of

S^<=, S^>=, S#^<=, R<[S].

STEP 1. Use any Boolean combination of these four in Proposition B and
analyze what you get.

STEP 2. Expand on that list to make it more natural but of the same
style. Aim for this:

S, S#, S#^<, S#^>, S#^<=, S#^>=
R[X], R<[X], R<=[X], R>[X], R>=[X], where X is a Boolean combination
from the first line.

We will always get implicitly Pi01 sentences.

CONJECTURE. We get only consistency statements for some familiar
systems at or below HUGE.

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

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 840th 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
838: New Tangible Incompleteness/1 1/11/20 1:04PM
839: New Tangible Incompleteness/2 1/13/20 1:10 PM

Harvey Friedman