848: Set Equation Theory/1

Harvey Friedman hmflogic at gmail.com
Wed Apr 15 23:45:53 EDT 2020

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).

DEFINITION 1. The upper shift USH maps Q* into Q* and USH(x) results
from adding 1 to all nonnegative coordinates of x. The extensive upper
shift EUSH:Q* into Q*  is defined by EUSH(x) is the result of adding 1
to all coordinates at least as large as some coordinates of x in N.
The upper shift and the extensive upper shift of S containedin Q^k is
the set of all USH(x), EUSH(x), x in S, respectively.

USH and EUSH is to be distinguished from the USH/N that we use in the
LEAD in Invariant Maximality. EUSH is more like USH/N than USH.

DEFINITION 2. Let S containedin Q^k. S# is the least A^k containing S.
Let R containedin Q^2k and S containedin Q^k. R<[S] = {y in Q^kL 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. S is a relatively order
theoretic subset of T if and only if S is the intersection of an order
theoretic subset of Q^k with T. S controls T if and only if every
bounded above relatively order theoretic subset of T is a relatively
order theoretic subset of S.

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 (extensive upper shift).

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

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

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


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

Harvey Friedman

More information about the FOM mailing list