850: Set Equation Theory/3

Sun Apr 26 00:06:41 EDT 2020

We start over. This obsoletes Set Equation Theory/1,2.

SRP

DEFINITION 1. The upper shift, ush, maps Q* into Q* where ush(x) results
from adding 1 to all nonnegative coordinates of x. ush(S) = {ush(x): x
in S} is the upper shift of S containedin Q^k.

DEFINITION 2. Let S containedin Q^k. S# is the least A^k containing S
union {0}^k. Let R containedin Q^n and S containedin Q^m. R[S] = {y in
Q^n-m: there exists x in S, (x,y) in R}. R<[S] = {y in Q^n-m: there
exists x in S, (x,y) in R and max(x) < max(y)}.

PROPOSITION 1. Let R containedin Q^2k be order invariant. Some S =
S#\R<[S] containedin Q^k contains its upper shift.

THEOREM 2. Proposition 1 is provably equivalent to Con(SRP) over
WKL_0, and implies Con(SRP) over RCA_0.

HUGE

DEFINITION 3. Let S containedin Q^k. fld(S) is the set of all
coordinates of elements of S. S^<= = {x in S: x1 <= ... <= xk}. E|<p =
E interest (-infinity,p)^k.

DEFINITION 4. S containedin Q^k conjunctively contains E if and only
if every E|<p, p in fld(E), is of the form {x in S: phi(x)}, where phi
is a finite conjunction of statements S(u1,...,uk), where each ui is
either among the variables x1,...,xk or is a parameter from fld(S). S
containedin Q^k p-conjunctively contains E if and only if n conjuncts
suffice.

Let's look at the entire transition.We start with two modifications of
Proposition 1 designed to facilitate direct comparison.

PROPOSITION 1'. Let R containedin Q^2k be order invariant. Some S
containedin Q^k contains ush(S), where S = S#\R<[S].

PROPOSITION 1''. Let R containedin Q^2k be order invariant. Some S
containedin Q^k contains ush(S), where S<= = S#<=\R<[S].

PROPOSITION 2. Let R containedin Q^2k be order invariant. Some S
containedin Q^k conjunctively contains ush(S), where S<= = S#<=\R<[S].

PROPOSITION 3. Let R containedin Q^2k be order invariant. Some S
containedin Q^k 2-conjunctively contains ush(S), where S<= =
S#<=\R<[S].

THEOREM 4. Propositions 1',1'' are provably equivalent to Con(SRP)
over WKL_0 and imply Con(SRP) over RCA_0. Propositions 2,3 are
provably equivalent to Con(HUGE) over WKL_0, and imply Con(HUGE) over
RCA_0.

BETWEEN I3 AND I2

We have been using the upper shift. We now use a different function,

Note that the upper shift is simply the unary function

ush(p) = p if p < 0; p+1 otherwise

with the coordinate action.

DEFINITION 4. The modified shift is defined on Q(-infinity,0] union Z+,
where the modified shift at p is p if p < -1, p/2 if -1 <= p <= 0, p+1
if p in Z+. mush is extended to alpha::Q* into Q* by the coordinate
action.

PROPOSITION 5. Let R containedin Q^2k be order invariant. Some S
containedin Q^k conjunctively contains mush(S), where S<= =
S#<=\R<[S].

PROPOSITION 6. Let R containedin Q^2k be order invariant. Some S
containedin Q^k 2-conjunctively contains mush(S), where S<= =
S#<=\R<[S].

THEOREM 7. Propositions 5,6 are provable in WKL0 + Con(I2) and imply
Con(I3) over RCA0.

TEMPLATES

So we have two classes of statements here. One is with S containing
alpha(S) and S = S#\R<[S]. The other is with S conjunctively
containing alpha(S) and S<= = S#<=\R<[S]/.

The first of these is at the SRP level and the second of these is at
the HUGE and above level.

We can template these by considering alpha to be various fundamental
classes of partial functions from Q into Q, and use the coordinate
action to extend to Q*.

The first Template should give a wide range of Con statements well
within the large cardinals compatible with L, and also including weak
statements, such as fragments of first and second order arithmetic.
They should be well ordered under implication over WKL0.

The second Template should also incorporate weak Con statements to
very strong Con statements, likely all weaker than I2. Again we should
have well ordering under implication over WKL0.

What countable ordinals should we get here? We conjecture the provable
ordinal of large cardinals.

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

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

Harvey Friedman