[FOM] 841: New Tangible Incompleteness/4

Wed Jan 15 13:58:49 EST 2020

THIS POSTING IS SELF CONTAINED

In #840, we used two set equations:

S = S#\R<[S]
S = S#>= U S#<=\R<[S]

The first corresponds to SRP and the second corresponds to HUGE. But
there is an equation I prefer for HUGE:

We no longer think it is worth it to go for an S = Gamma(S) statement.
We would rather use

... some S with S^<= = S#^<=\R<[S] has its (upper) bounded order
theoretic subsets closed under the upper shift.

And we now prefer

... some S with S^+ = S#^+\R<[S] has its bounded order theoretic
subsets closed under the upper shift.

1. Set Equation for SRP
2. Set Equation for HUGE
3. Templating Set Equations

1. SET EQUATION FOR SRP

DEFINITION 1.1. Let S containedin Q^k S# is the least A^k containing S
U {0}^k. Let R containedin Q^2k. R[S] = {y: (there exists x in S)(x R
y)}. R<[S] = {y: (there exists x in S)(max(x) < max(y) and x R y)}. S
is  bounded if and only if S is contained in some [-p,p]. The upper
shift of S is the result of adding 1 to all nonnegative coordinates of
elements of S.

PROPOSITION A. For order invariant R containedin Q^2k, some S =
S#\R<[S] contains its upper shift.

THEOREM 1.1. Proposition A is implicitly Pi01 via the Goedel
Completeness Theorem using nonstandard models.

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

SRP = ZFC + {there exists a cardinal with the k-SRP}_k.

2. SET EQUATION FOR HUGE

DEFINITION 2.1. Let S containedin Q^k. B is an order theoretic subset
of S if and only if B is of the form {x in S: phi(x,y_1,...,y_n)}
where phi is a quantifier free formula over (Q,<) with parameters
y_1,...,y_n in S. S is  bounded if and only if S is contained in some
[-p,p]. S^+ = {x in S: x_1,...,x_k > 0}.

PROPOSITION B. For order invariant R containedin Q^2k, some S with S^+
= S#^+\R<[S] has its bounded order theoretic subsets closed under the
upper shift.

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

HUGE = ZFC + {there exists a k-huge cardinal}_k.

3. TEMPLATING SET EQUATIONS

TEMPLATE A. For order invariant R containedin Q^2k, some S = Gamma(S)
contains its upper shift.

Here Gamma(S) is a set theoretic expression in S.

STEP 1. Gamma(S) is a Boolean combination of S,S#,R<[S].
STEP 2. Gamma(S) is a Boolean combination of S,S#,R[S],R<[S].
STEP 3. Gamma(S) is a Boolean combination of Step 2 and R[step 2] and
R<[step 2].
STEP 4. Gamma(S) is the least set containing S and closed under # and
R[...] and R<[...].
STEP 5. Gamma(S) is the least set containing S and closed under
Boolean operations and # and R[,,,] and R<[,,,].

CONJECTURE. You get consistency of systems that are linearly ordered
and at or below SRP.

TEMPLATE B. For order invariant R containedin Q^2k, some S with
Gamma(S)  has its bounded order theoretic subsets closed  under the
upper shift.

STEP 1. Gamma(S) is a Boolean relation among S^+,S#^+,R<[S].
STEP 2. Gamma(S) is a Boolean relation among S,S#,S^+,S#^+,R<[S]..
STEP 3. Gamma(S) is a Boolean relation among S,S#,S^+,S#^+, and R of
these four and R< of these four.
STEP 4. More as for Template A.

CONJECTURE. You get consistency of systems that are linearly ordered
and 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 841th 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
840: New Tangible Incompleteness/3 1/14/20 4:50PM

Harvey Friedman