[FOM] 369:Fixed Points and Large Cardinals/restatement

[Harvey Friedman]

1. Terminology.
2. The Unprovable Upper Shift Fixed Point Theorem.
3. The Unprovable Internal Embedding Theorem.
4. Finite Forms.
5. Template.

1. TERMINOLOGY.

Let Q be the set of all rationals. We use \ for set theoretic
difference.

Let A be contained in Q^k. We write cube(A,0) for the least set B^k  
containing A such that 0 is in B. We write fld(A) for the set of all  
coordinates of elements of A.

We say that x,y in Q^k are order equivalent if and only if for all 1  
<= i,j <= k, x_i < x_j if and only if y_i < y_j.

We say that A contained in Q^k is order invariant if and only if for  
all order equivalent x,y in Q^k, x in A iff y in A.

Let R be contained in Q^k x Q^k. We say that R is order invariant if  
and only if R is order invariant as a subset of Q^2k.

We say that R is strictly increasing if and only if for all x,y in  
Q^k, R(x,y) implies max(x) < max(y).

We write R[A] = {y: R(x,y)}, provided A is contained in Q^k.

We use the following generalization. Let R be contained in Q^k+p x  
Q^k. We say that R is order invariant if and only if R is order  
invariant as a subset of Q^2k+p.

We say that R is strictly increasing if and only if for all x in Q^k+p  
and y in Q^k, R(x,y) implies max(x) < max(y).

We say that A is R,B free if and only if A is contained in Q^k, B is  
contained in Q^p, and for no x,y in A, b in B, is R(x,b,y).

We write R[A] = {y: R(x,y)}, provided A is contained in Q^k+p.

We write SDOI(Q^k,Q^n) for the family of all strictly dominating order  
invariant R contained in Q^k x Q^n.

The upper shift of x in Q^k is obtained by adding 1 to all nonnegative  
coordinates of x.

The upper shift of A contained in Q^k is the set of all upper shifts  
of its elements. We use "us" for the upper shift.

Let A be contained in Q^k. For q in Q, define

A[q] = {y in Q^k-1: (q,y) in A}.
A|<q = {y in A: each coordinate of y is < q}.

We say that S is a self embedding of A if and only if

i. S is a function from fld(A) into fld(A).
ii. for all x_1,...,x_k in fld(A), (x_1,...,x_k) in A iff  
(S(x_1),...,S(x_k)) in A.

2. THE UNPROVABLE UPPER SHIFT FIXED POINT THEOREM.

UPPER SHIFT FIXED POINT THEOREM. For all R in SDOI(Q^k,Q^k), some A =  
cube(A,0)\R[A] contains its upper shift.

THEOREM 2.1. The Upper Shift Fixed Point Theorem can be proved in SUB+  
but not in any consistent fragment of SUB. It is provably equivalent  
to Con(SUB), in WKL_0.

Here SUB+ = ZFC + "for all k there exists a k-subtle cardinal". SUB =  
ZFC + {there exists a k-subtle cardinal}_k.

3. THE UNPROVABLE INTERNAL EMBEDDING THEOREM.

Nearly the most extreme large cardinal hypotheses are stated in
Kanamori, The Higher Infinite, page 325:

I1. For some alpha, there is a proper elementary embedding j:V(alpha +
1) into V(alpha + 1).
I2. There is a j:V into M such that V(alpha) is contained in M for
some alpha > crit(j) satisfying j(alpha) = alpha.
I3. For some alpha, there is a proper elementary embedding j:V(alpha)
into V(alpha).

INTERNAL EMBEDDING THEOREM. For all R in SDOI(Q^k+3,Q^k), there exists  
A,B such that A = cube(A,0)\R[A x B], where B[1],...,B[k] are self  
embeddings of A|<1,...,A|<k, respectively, with the same fixed points.

THEOREM 3.1. The Internal Upper Shift Theorem is an unprovable  
theorem. It can be proved in I2 but not in I3. It is provably  
equivalent to a Pi01 sentence over ACA_0. WKL_0 proves that it implies  
the consistency of ZFC + {there exist elementary embeddings from k  
different ranks into themselves, with the same critical point}_k.

4. FINITE FORMS.

SEQUENTIAL UNPROVABLE UPPER SHIFT FIXED POINT THEOREM. For all R in  
SDOI(Q^k,Q^k), there exist finite A_1,A_2,... contained in Q^k such  
that each A_i+1 = cube(A_i+1,0)\R[A_i+2] contains A_i union us(A_i).

FINITE SEQUENTIAL UNPROVABLE UPPER SHIFT FIXED POINT THEOREM. For all  
R in SDOI(Q^k,Q^k), there exist finite A_1,...,A_k contained in Q^k  
such that each A_i+1 = cube(A_i+1,0)\R[A_i+2] contains A_i union  
us(A_i).

ESTIMATED SEQUENTIAL UNPROVABLE UPPER SHIFT FIXED POINT THEOREM. For  
all R in SDOI(Q^k,Q^k), there exist finite A_1,...,A_k contained in  
Q^k such that each A_i+1 = cube(A_i+1,0)\R[A_i+2] contains A_i union  
us(A_i), where the magnitudes of the numerators and denominators used  
in the A's are at most (8k)!.

Note that the Finite Sequential Unprovable Upper Shift Fixed Point  
Theorem is
explicitly Pi02, and the Estimated Finite Sequential Unprovable Upper  
Shift Fixed
Point Theorem is explicitly Pi01.

THEOREM 4.1. Theorem 2.1 applies to all three.

Note that these finite forms of the Unprovable Upper Shift Fixed Point  
Theorem are quite simple. However, the somewhat similarly constructed  
finite forms of the Unprovable Internal Embedding Theorem are not as  
simple. Rather than present them, we present a general treatment of  
finite forms of such statements.

Consider all sentences of the following form:

#) There exists A_1,...,A_n contained in Q^k such that for all 1 <= i  
<= m, P(i,A_1,...,A_n) holds.

Here k,n,m are specific positive integers, and P is a specific first  
order property of the structure (Q,<,A_1,...,A_n), where the A's act  
as k-ary relation symbols.

THEOREM 4.2. There is an effective procedure that converts any  
sentence phi of form #) into an algorithmic process Gamma, such that  
phi holds if and only if Gamma does not terminate.

Note that every instance of the Unprovable Upper Shift Fixed Point  
Theorem and the Unprovable Internal Embedding Theorem are of the above  
form. Hence by general principles (i.e., Theorem 4.2), both have  
finite forms that are Pi01.

Moreover, the P's arising from these Unprovable Theorems are of the  
form: a block of universal quantifiers followed by a block of  
existential quantifiers. This allows the conversion in Theorem 4.2 to  
the algorithmic process Gamma to be reasonably transparent.

5. TEMPLATE.

The Unprovable Upper Shift Fixed Point Theorem is, quite naturally, an  
instance
of a large family of propositions. Note that the upper shift is the
obvious lifting of the one dimensional upper shift from Q into Q to
higher dimensions.

We let PPL(Q) be the family of partial f:Q into Q given by

a_1x + b_1 if x in I_1
...
a_nx + b_n if x in I_n

where n >= 1, the a's,b's are rationals, and the I's are pairwise
disjoint nonempty intervals with rational endpoints (or +-infinity).

A PPL(Q) system consists of a finite list of elements of PPL(Q).

Let M be a PPL(Q) system. We say that V is M closed if and only if V
is f closed for all components f of M.

TEMPLATE. Let M be a PPL(Q) system. Is it the case that for all R in
SDOI(Q^k), some A = cube(A,0)\R[A] contains M[A]?

THEOREM 5.1. The Template is false for the single function f:Q into Q,
where for all x in Q, f(x) = x+1. (The shift). The Template is true for
the single function f:[0,infinity) into [0,infinity), where for all x  
= 0, f(x) = x+1. (The nonnegative shift). These statements are  
provable in RCA_0.

CONJECTURE. Every instance of the Template is refutable in RCA_0 or
provable in SUB+.

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

I use http://www.math.ohio-state.edu/~friedman/ for downloadable
manuscripts. This is the 369th 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-349 can be found at http://www.cs.nyu.edu/pipermail/fom/2009-August/014004.html
in the FOM archives.

350: one dimensional set series  7/23/09  12:11AM
351: Mapping Theorems/Mahlo/Subtle  8/6/09  10:59PM
352: Mapping Theorems/simpler  8/7/09  10:06PM
353: Function Generation 1  8/9/09  12:09PM
354: Mahlo Cardinals in HIGH SCHOOL 1  8/9/09  6:37PM
355: Mahlo Cardinals in HIGH SCHOOL 2  8/10/09  6:18PM
356: Simplified HIGH SCHOOL and Mapping Theorem  8/14/09  9:31AM
357: HIGH SCHOOL Games/Update  8/20/09  10:42AM
358: clearer statements of HIGH SCHOOL Games  8/23/09  2:42AM
359: finite two person HIGH SCHOOL games  8/24/09  1:28PM
360: Finite Linear/Limited Memory Games  8/31/09  5:43PM
361: Finite Promise Games
362: Simplest Order Invariant Game
363: Greedy Function Games/Largest Cardinals 1
364: Anticipation Function Games/Largest Cardinals/Simplified 9/7/09
11:18AM
365: Free Reductions and Large Cardinals 1  9/24/09  1:06PM
366: Free Reductions and Large Cardinals/polished  9/28/09  2:19PM
367: Upper Shift Fixed Points and Large Cardinals  10/4/09  2:44PM
368: Upper Shift Fixed Point and Large Cardinals/correction  10/6/09   
8:15PM

Harvey Friedman