849: Set Equation Theory/2

Harvey Friedman hmflogic at gmail.com
Thu Apr 16 16:50:26 EDT 2020


We now take S# to be the least A^k containing S union N^k. Can't
really use extensive upper shift. Also the treatment of control was


The book is now taking some additional shape.

1. Boolean Relation Theory.
2. Invariant Maximality Theory.
3. Set Equation Theory

Of course, the Brand New Tangible Incompleteness series 1-5  is in chapter
2, Invariant Maximality Theory. Boolean Relation Theory is on my
website, downloadable manuscripts, and is already about 800 pages.

There has been a major breakthrough in Tangible Incompleteness at the
HUGE level. Recall HUGE is ZFC + {there exists an n-huge cardinal}_n.
lambda is n-huge if and only if there is a nontrivial elementary
embedding from V(lambda) into V(mu) where j...j(kappa) = lambda, where
kappa is the critical point and there are k j's. (This is a
reformulation of the standard formulations that involving elementary
embeddings of V into classes).

NOTE: In the set theory literature, kappa is n-huge if and only if it
is the critical point of a nontrivial embedding where the iterated j n
times satisfies an appropriate condition. Our definition is far more
friendly for non specialists, and lhas the expositional advantage of
looking a lot like a direct kind of
approximation to I3, which is j:V(lambda) to V(lambda). This n-huge is
well known to be intertwined with the usual, through ultraproduct

We also push this to beyond I3, and land strictly between I3 and I2.


DEFINITION 1. The upper shift USH maps Q* into Q* and USH(x) results
from adding 1 to all nonnegative coordinates of x. The upper shift of
S containedin Q^k is the set of all USH(x), x in S.

DEFINITION 2. Let S containedin Q^k. S# is the least A^k containing S union N^k.
Let R containedin Q^2k and S containedin Q^k. R<[S] = {y in Q^k: there
exists x in S such that max(x) < max(y) and x R y}, S^<= = {x in S: x_1
<= ... <= x_k}.

DEFINITION 3. Let S,T containedin Q^k. A limited section of S is a set
obtained by fixing zero or more coordinates of S, and then restricting
to strictly below some p in Q. S controls T if and only if every
limited section of T is a section of S.

Note that fixing zero arguments results in S, and so if S controls T
then S contains T.

PROPOSITION 1. Let R containedin Q^2k be order invariant. There exists
S = S#\R<[S].

PROPOSITION 2. Let R containedin Q^2k be order invariant. There exists
S = S#\R<[S] containing its upper shift.

PROPOSITION 3. Let R containedin Q^2k be order invariant. There exists
S controlling its upper shift, where S^<= = S#^<=\R<[S].

THEOREM 4. Proposition 1 is provable in RCA_0. Proposition 2 is
provably equivalent to Con(SRP)
over WKL_0. It implies Con(SRP) over RCA_0. Proposition 3 is provably
equivalent to Con(HUGE) over WKL_0. It implies Con(HUGE) over RCA_0.


We have been using the upper shift. We now use a different function,
H:Q* into Q*.

DEFINITION 4. H(x) = if the positive x_i are are at most one integer,
then replace all x_i in [-1,0] by x_i/2 and all x_i > 0 by x_i + 1
then else x. .

PROPOSITION 4. Let R containedin Q^2k be order invariant. There exists
S containing H[S], where S^<= = S#^<=\R<[S].

PROPOSITION 5. Let R containedin Q^2k be order invariant. There exists
S controlling H[S], where S^<= = S#^<=\R<[S].

THEOREM 5. Proposition 4 is provably equivalent to Con(SRP) over
WKL_0. Proposition 5 implies Con(I3) over RCA_0. I1 implies
Proposition 4. WKL_0 +  Con(I1) implies Proposition 4.


So in addition to USH and USH/N of LEAD in Invariant Maximality
(chapter 2), H:Q^k into Q^k is a particularly simple definable
functions in (Q,<,+1,/2,N).

TEMPLATE A. Given: piecewise linear binary relation W on Q^k.
Statement: Let R containedin Q^2k be order invariant. There exists S =
S#\R<[S].containing H[S].

TEMPLATE B. Given: piecewise linear binary relation W on Q^k.
Statement: Let R containedin Q^2k be order invariant. There exists S
controlling H[S], where S^<= = S#^<=\R<[S].

It is natural to conjecture that Template A gives either provables in
WKL_0 + Con(SRP) or refutables in RCA_0. And Template B gives either
provables in I2 or refutables in RCA_0. We know that Con*SRP) and
Con(HUGE) are represented in A,B respectively, and well as beyond
Con(I3) is represented in B.

We can go further and try to also template the set equations, as itchy are
so simple.


My website is at https://u.osu.edu/friedman.8/ and my youtube site is at
This is the 848th 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

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
841: New Tangible Incompleteness/4 1/15/20 1:58PM
842: Gromov's "most powerful language" and set theory  2/8/20  2:53AM
843: Brand New Tangible Incompleteness/1 3/22/20 10:50PM
844: Brand New Tangible Incompleteness/2 3/24/20  12:37AM
845: Brand New Tangible Incompleteness/3 3/28/20 7:25AM
846: Brand New Tangible Incompleteness/4 4/1/20 12:32 AM
847: Brand New Tangible Incompleteness/5 4/9/20 1 34AM
848. Set Equation Theory/1 4/15 11:45PM

Harvey Friedman

More information about the FOM mailing list