[FOM] 653: Pi01 Incompleteness/SRP,HUGE

[Harvey Friedman]

THIS POSTING IS ENTIRELY SELF CONTAINED

I now have a good version of explicitly Pi01 incompleteness for HUGE,
which is ZFC extended by the huge cardinal hierarchy. HUGE is so
strong that the leading set theorists will not commit to its
consistency, because it is so far beyond the level of large cardinals
that have a known reasonable inner model theory.

Mathematically natural explicitly Pi01 incompleteness can almost
certainly be pushed even far beyond HUGE into j:V into V (without
choice) and beyond. But we will not attempt to do this here.

http://www.cs.nyu.edu/pipermail/fom/2016-February/019491.html is not
very long, and so we choose to incorporate it in this posting. The
definition of the upper shift was given only for tuples there, and we
needed it for sets of tuples. We make this trivial correction below.

Notice that for the implicitly Pi01 statement, which as expected is
the most immediately digestable of the statements we go well beyond
ZFC to SRP, which is ZFC extended with the stationary Ramsey
cardinals. Here we used the simple concept of maximal S^2.

For the explicitly Pi01 statements, we instead used what we call
reductions, bases, and the upper shift. The version in section 3
corresponds to SRP. For HUGE, the essential change is the imposition
of an equation involving sections obtained by fixing the first
argument. This appears in the final section 4.

WKL_0 and EFA are standard weak systems for reverse mathematics.

1. PRELIMINARIES

DEFINITION 1.1. N is the set of all nonnegative integers, Q is the set
of all rationals. We use i,j,k,n,m,r for positive integers, and p,q
for rationals. Q[0,n] is Q intersect [0,n].

DEFINITION 1.2. x,y in Q^k are order equivalent if and only if for all
1 <= i,j <= k, x_i < x_j iff y_i < y_j. V containedin Q^k is order
invariant if and only if for all order equivalent x,y in Q^k, x in V
iff y in V. V containedin Q[0,n]^k is order invariant if and only if
for all order equivalent x,y in Q[0,n]^k, x in V iff y in V.

THEOREM 1.1. V containedin Q^k is order invariant if and only if V is
the union of equivalence classes of Q^k under order equivalence on
Q^k. V containedin Q[0,n]^k is order invariant if and only if V is the
union of equivalence classes of Q[0,n]^k under order equivalence on
Q[0,n]^k.

DEFINITION 1.3. Let S containedin Q^k. S is partially embedded by h if
and only if

i. h is a partial function from Q into Q.
ii. For all x_1,...,x_k in Q, (x_1,...,x_k) in S iff (hx_1,...,hx_k) in S.

THEOREM 1.2. (straightforward) Every V containedin Q^k contains a
maximal S^2. I.e., an S^2 containedin V with no proper superset S'^2
containedin V. If k is odd then the unique maximal S^2 containedin V
is the empty set.

For sections 3, we  use the following three definitions. .

DEFINITION 1.4. Let R containedin Q^2k and x,y in Q^k. x R-reduces to
y in R if and only if max(x) > max(y) and (x,y) in R. B is a basis for
A in R if and only if

i. A,B containedin Q^k.
ii. No element of B R-reduces to an element of B. (independence)
ii. If every coordinate of x in Q^k is a coordinate of some element of
A, then x in B or x R-reduces to an element of B. (spanning)

THEOREM 1.3. (straightforward)  In every R containedin Q^2k, every
finite S containedin Q^k has a finite basis. We can require that every
coordinate of every element of the basis for S in R be a coordinate of
some element of S, in which case the basis in R is unique, and is a
basis in R for itself.

DEFINITION 1.5. The upper shift of S containedin Q^k, written ush(S), results
from adding 1 to all nonnegative coordinates of the elements of S.

DEFINITION 1.6. The height of finite S containedin Q^k is the largest
of the magnitudes of the denominators and numerators of the elements
of S when put in reduced form.

For section 4, we use the following two definitions.

DEFINITION 1.7. Let S containedin Q^k. S^<= = {x in S: x_1 <= ... <=
x_k}. S|<=p = S intersect (-infinity,p]. S_p = {x in Q^k-1: (p,x) in
S}.

DEFINITION 1.8. B is a <= basis for A in R if and only if

i. A,B containedin Q^k.
ii. No element of B R-reduces to an element of B. (independence)
ii. If every coordinate of x in Q^k<= is a coordinate of some element of
A, then x in B or x R-reduces to an element of B. (spanning)

2. IMPLICITLY PI01 INCOMPLETENESS

PROPOSITION 2.1. Every order invariant V containedin Q[0,n]^k contains
a maximal S^2 partially embedded by the function p if p < 1; p+1 if p
in {1,...,n-1}.

Proposition 2.1 can be seen to be implicitly Pi01 via the Goedel
Completeness Theorem.

THEOREM 2.2. Proposition 2.1 is independent of ZFC, and in fact
provably equivalent to Con(SRP) over WKL_0.

THEOREM 2.3. Proposition 2.1 is refutable in RCA_0 if we replace "if p
in {1,...,n-1}" by "p >= 1".

INFORMAL IDEA: EVERY NICE SET HAS A MAXIMAL SQUARE WITH A NICE
EXPLICIT PARTIAL EMBEDDING.

3. EXPLICITLY Pi01 INCOMPLETENESS - SRP

PROPOSITION 3.1. In every order invariant R containedin Q^2k,
{0,...,k}^k has a finite basis B with a finite basis C containing B
and ush(C).

Obviously Proposiiton 3.1 is explicitly Pi02.

PROPOSITION 3.2. In every order invariant R containedin Q^2k,
{0,...,k}^k has a finite basis B with a finite basis C containing B
and ush(C), both of height at most (8k)!.

Obviously Proposition 3.2 is explicitly Pi01.

THEOREM 3.3. Propositions 3.1 and 3.2 are independent of ZFC, and in
fact provably equivalent to Con(SRP) over EFA. If we drop "and
ush(C)", these statements are provable in EFA.

4. EXPLICITLY Pi01 INCOMPLETENESS - HUGE

PROPOSITION 4.1. In every order invariant R containedin Q^2k,
{0,...,2k}^k has a finite <= basis B with a finite <= basis C containing B
and ush(C), where C_k+.5|<=k = ush(C)_k|<=k.

Obviously Proposiiton 4.1 is explicitly Pi02.

PROPOSITION 4.2. In every order invariant R containedin Q^2k,
{0,...,2k}^k has a finite <= basis B with a finite <= basis C containing B
and ush(C), both of height at most (8k)!, where C_k+.5|<=k = ush(C)_k|<=k.

Obviously Proposition 4.2 is explicitly Pi01.

THEOREM 4.3. Propositions 4.1 and 4.2 are independent of ZFC, and in
fact provably equivalent to Con(HUGE) over EFA. If we drop the where
clauses, then the statements 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 653rd 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-599 can be found at the FOM posting
http://www.cs.nyu.edu/pipermail/fom/2015-August/018887.html

600: Removing Deep Pathology 1  8/15/15  10:37PM
601: Finite Emulation Theory 1/perfect?  8/22/15  1:17AM
602: Removing Deep Pathology 2  8/23/15  6:35PM
603: Removing Deep Pathology 3  8/25/15  10:24AM
604: Finite Emulation Theory 2  8/26/15  2:54PM
605: Integer and Real Functions  8/27/15  1:50PM
606: Simple Theory of Types  8/29/15  6:30PM
607: Hindman's Theorem  8/30/15  3:58PM
608: Integer and Real Functions 2  9/1/15  6:40AM
609. Finite Continuation Theory 17  9/315  1:17PM
610: Function Continuation Theory 1  9/4/15  3:40PM
611: Function Emulation/Continuation Theory 2  9/8/15  12:58AM
612: Binary Operation Emulation and Continuation 1  9/7/15  4:35PM
613: Optimal Function Theory 1  9/13/15  11:30AM
614: Adventures in Formalization 1  9/14/15  1:43PM
615: Adventures in Formalization 2  9/14/15  1:44PM
616: Adventures in Formalization 3  9/14/15  1:45PM
617: Removing Connectives 1  9/115/15  7:47AM
618: Adventures in Formalization 4  9/15/15  3:07PM
619: Nonstandardism 1  9/17/15  9:57AM
620: Nonstandardism 2  9/18/15  2:12AM
621: Adventures in Formalization  5  9/18/15  12:54PM
622: Adventures in Formalization 6  9/29/15  3:33AM
623: Optimal Function Theory 2  9/22/15  12:02AM
624: Optimal Function Theory 3  9/22/15  11:18AM
625: Optimal Function Theory 4  9/23/15  10:16PM
626: Optimal Function Theory 5  9/2515  10:26PM
627: Optimal Function Theory 6  9/29/15  2:21AM
628: Optimal Function Theory 7  10/2/15  6:23PM
629: Boolean Algebra/Simplicity  10/3/15  9:41AM
630: Optimal Function Theory 8  10/3/15  6PM
631: Order Theoretic Optimization 1  10/1215  12:16AM
632: Rigorous Formalization of Mathematics 1  10/13/15  8:12PM
633: Constrained Function Theory 1  10/18/15 1AM
634: Fixed Point Minimization 1  10/20/15  11:47PM
635: Fixed Point Minimization 2  10/21/15  11:52PM
636: Fixed Point Minimization 3  10/22/15  5:49PM
637: Progress in Pi01 Incompleteness 1  10/25/15  8:45PM
638: Rigorous Formalization of Mathematics 2  10/25/15 10:47PM
639: Progress in Pi01 Incompleteness 2  10/27/15  10:38PM
640: Progress in Pi01 Incompleteness 3  10/30/15  2:30PM
641: Progress in Pi01 Incompleteness 4  10/31/15  8:12PM
642: Rigorous Formalization of Mathematics 3
643: Constrained Subsets of N, #1  11/3/15  11:57PM
644: Fixed Point Selectors 1  11/16/15  8:38AM
645: Fixed Point Minimizers #1  11/22/15  7:46PM
646: Philosophy of Incompleteness 1  Nov 24 17:19:46 EST 2015
647: General Incompleteness almost everywhere 1  11/30/15  6:52PM
648: Necessary Irrelevance 1  12/21/15  4:01AM
649: Necessary Irrelevance 2  12/21/15  8:53PM
650: Necessary Irrelevance 3  12/24/15  2:42AM
651: Pi01 Incompleteness Update  2/2/16  7:58AM
652: Pi01 Incompleteness Update/2  2/7/16  10:06PM

Harvey Friedman