854: Lower R Invariant Maximal Sets/1

Thu May 14 23:32:06 EDT 2020

We are still working on the updated version of #110 in
https://u.osu.edu/friedman.8/foundational-adventures/downloadable-manuscripts/
We have finished the SRP part and am about to start with the HUGE and
higher part.

We have decided that LOWER INVARIANCE is the way to go, not the
earlier versions. Of course it is closely related. So we don't use
embeddings or upper shifts.

Here is the key definition. J stands for any rational interval.

DEFINITION 1. Let R containedin J^k x J^k = J^2k. S containedin J^k is R
invariant if and only if for all x R y, x in S implies y in S.

DEFINITiON 2. Let R containedin J^k x J^k = J^2k. S containedin J^k is
lower R invariant if and only if for all x R y, if x',y' results from
replacing one or more x_i,y_i by various p,p < min(xy), then x' in S
implies y' in S.

EXAMPLE OF LOWER REPLACEMENT: Use J^4 = Q[0,1]^4 and (2/3,1,1/3,1/3) R
(3/4,7/8,1/4,1/4), where R has other pairs. We can replace the second
and third coordinates on both sides by 1/8 and 1/9 respectively,
obtaining (2/3,1/8,1/9,1/3), (3/4,1/8,1/9,1/4).

THEOREM 1. Let R containedin J^k x J^k = J^2k be finite and order
preserving. Every order invariant E containedin J^k has an R invariant
maximal square.

 PROPOSITION 1. Let R containedin J^k x J^k = J^2k be order preserving.
Every order invariant E containedin J^k has a lower R invariant maximal
square.

THEOREM 2. Proposition 1 is provably equivalent to Con(SRP) over WKL_0
where the implication to Con(SRP) is provable in RCA_0.

Note that so far this is purely order theoretic and we don't even use
preferred rationals. Here is a closely related version that uses the
nonnegative integers as distinguished elements.

DEFINITION. S containedin Jk is N-lower invariant if and only if for
all order equivalent x,y in (J intersect N)^k, if x',y' in J^k results
from x,y by replacing one or more xi,yi by various p,p < min(xy), then
x' in S implies y' in S.

EXAMPLE OF N-LOWER REPLACEMENT: Use J4 = Q[-5,6]^4 and order equivalent
(1,5,2,3), (0,6,3,4). We can replace the second and third coordinates
on both sides by -2/3 and -5 respectively, obtaining (1,-2/3,-5,3),
(0,-2/3,-5,4).

 PROPOSITION 2. Every order invariant E containedin Jk has an N-lower
invariant maximal square.

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

IN THE INTEGERS
from section 2.7 of new unfinished #110

We now move from Q to Z to give explicitly Pi02 and Pi01 Tangible
Incompletenss. We use normal interval notation in the integers. We
choose two of our ten categories - cliques in graphs and emulators.

We work entirely in the finite spaces [-nr,nr]^k.

DEFINITION 2.7.3. A clique extender of clique S in graph G on
[-nr,nr]^k is an x such that S U. {x} is a clique in G. An emulator
extender of emulator S of x_1,...,x_m in [-nr,nr]^k is an x such that S
U. {x} is an emulator of x_1,...,x_m. A maximal clique in graph G on
[-nr,nr]^k is a clique with no clique extender. A maximal emulator in
x_1,...,x_m in [-nr,nr]^k is an emulator with no emulator extender.

DEFINITION 2.7.4. S is a weakly maximal clique in graph G on [-nr,nr]^k
if and only if S is a clique in G where there is no nonempty set of
clique extenders R[S^k x {(0,r,2r,...,nr)}], R containedin [-nr,nr]k^2 +
n + k order invariant. S is a weakly maximal emulator in x_1,...,x_m
Î[-nr,nr]^k if and only if S is an emulator in x_1,...,x_m where there is
no nonempty set of clique extenders R[S^k x {(0,r,2r,...,nr)}], R
containedin [-nr,nr]k^2 + n + k order invariant.

DEFINITION 2.7.5. S Í[-nr,nr]^k is rN-lower invariant if and only if
for all order equivalent x,y in {0,r,...,nr}^k, if x',y' in [-nr,nr]^k
results from x,y by replacing one or more x_i,y_i by various p,p <
min(xy), then x' in S implies y' in S.

INTEGER LOWER INVARIANT WEAKLY MAXIMAL CLIQUES/1. ILIWMC/1. Every
order invariant graph on [-nr,nr]k, r >> k,n, has an rN-lower
invariant weakly maximal clique.

INTEGER LOWER INVARIANT WEAKLY MAXIMAL EMULATORS/1. ILIWME/1. Every
x_1,...,x_m in [-nr,nr]^k, r >> k,n,m, has an rN-lower invariant weakly
maximal emulator.

INTEGER LOWER INVARIANT WEAKLY MAXIMAL CLIQUES/2. ILIWMC/2. Every
order invariant graph on [-nr,nr]k, r > (8kn)!, has an rN-lower
invariant weakly maximal clique.

INTEGER LOWER INVARIANT WEAKLY MAXIMAL EMULATORS/2. ILIWME/2. Every
x_1,...,x_m in [-nr,nr]^k, r > (8knm)!, has an rN-lower invariant weakly
maximal emulator.

THEOREM. All four are provably equivalent to Con(SRP) over EFA.

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

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 854th 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
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
849. Set Equation Theory/2 4/16/20 4:50PM
850: Set Equation Theory/3 4/26/20 12:06AM
851: Product Inequality Theory/1 4/29/20 12:08AM
852: Order Theoretic Maximality/1 4/30/20 7:17PM
853: Embedded Maximality (revisited)/1 5/3/20 10:19PM :

Harvey Friedman