[FOM] 839: New Tangible Incompleteness/2

[Harvey Friedman]

In 838, when presenting the second Tangible Incompleteness statement
there with emulators, I wrote "finite" and should have written
"extended finite".

*****************************

I have a breakthrough in Tangible Incompleteness at the level of the
Large Large Cardinals. In particular, at the level of the HUGE
cardinal hierarchy.

This new material is to be put under chapter 3 of the Intangible
Incompleteness book contents.

3. SET EQUATIONS - in development

In 838 we were only discussing Chapter 2, EMBEDDED MAXIMALITY.

At the moment the simplest way to present this statement is to use a
set equation.

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 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. An order theoretic subset of S containedin Q^k is a set
of the form {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 with
S^<= = S#<=\R<[S] whose upper bounded order theoretic subsets are
closed under the upper shift.

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.

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

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 839th 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

Harvey Friedman