[FOM] 255:Controlling Pi01

[Harvey Friedman]

We continue from the November 10, 2995 abstract, Pi01 Progress/more, FOM
posting #254, http://www.cs.nyu.edu/pipermail/fom/2005-November/009324.html.

Recall Proposition A, copied from
http://www.cs.nyu.edu/pipermail/fom/2005-November/009324.html.

PROPOSITION A. For all k,n >= 1 and strictly dominating order invariant R
containedin [1,n]3k x [1,n]k, there exist A containedin [1,n]k such that the
three sets RR<A'\(8k)!> containedin RR<A'> containedin RA contain the same k
tuples of powers of (8k)!+1.

Motivation in terms of a search for a common fixed point theorem is given in
http://www.cs.nyu.edu/pipermail/fom/2005-November/009324.html. Specifically,
recall that the conclusion of Proposition A follows from the doomed common
fixed point equation

R<A'\(8k)!> = R<A'> = A.

The separate fixed point equations

R<A'> = A.
R<A'\(8k)!> = A.

are just fine. 

So is, separately,

R<A'\(8k)!> containedin R<A'> containedin A contain the same k tuples of
powers of (8k)!+1.

RR<A'\(8k)!> containedin RR<A'> containedin RA contain the same k tuples of
powers of (8k)!+1.

R<A'\(8k)!> containedin R<A'> containedin A.

RR<A'\(8k)!> containedin RR<A'> containedin RA.

The necessary use of large cardinals arise by the combination (of ways to
fix the doomed common fixed point equation) represented by Proposition A.

Recall the following two theorems from
http://www.cs.nyu.edu/pipermail/fom/2005-November/009324.html.

THEOREM. MAH+ proves Proposition A. However, Proposition A is not provable
in any consistent fragment of MAH that derives Z = Zermelo set theory. In
particular, Proposition A is not provable in ZFC provided ZFC is consistent.
These facts are provable in RCA0.

THEOREM. It is provable in ACA that Proposition A is equivalent to Con(MAH).

We wish to control the strength of Proposition A by weakening it in simple
ways. This seems to be a large subject, with much to work out, and we merely
scratch the surface of it here.

PROPOSITION B. For all k,n >= 1 and strictly dominating order invariant R
containedin [1,n]3k x [1,n]k, there exist A containedin [1,n]k such that the
three sets RR<A'\(8k)!> containedin RR<A'> containedin RA contain the same k
tuples from the first three powers of (8k)!+1.

PROPOSITION C. For all k,n >= 1 and strictly dominating order invariant R
containedin [1,n]3k x [1,n]k, there exist A containedin [1,n]k such that the
three sets RR<A'\(8k)!> containedin RR<A'> containedin RA contain the same k
tuples from the first k powers of (8k)!+1.

PROPOSITION D. For all k,n >= 1 and strictly dominating order invariant R
containedin [1,n]3k x [1,n]k, there exist A containedin [1,n]k such that the
three sets RR<A'\(8k)!> containedin RR<A'> containedin RA contain the same k
tuples from the first (8k)! powers of (8k)!+1.

PROPOSITION E. For all k,n >= 1 and strictly dominating order invariant R
containedin [1,n]3k x [1,n]k, there exist A containedin [1,n]k such that the
three sets RR<A'\(8k)!> containedin RR<A'> containedin RA contain the same k
tuples from 1,(8k)!+1,...,(8k)!+p.

THEOREM 1. Propositions B,C,E are provable in ACA but not in PA. It is
provable in PRA that Propositions B,C,E are equivalent to Con(PA).

THEOREM 2. For fixed p, Proposition E is provable in PA. The set of
Propositions obtained by fixing p in Proposition D is equivalent, over PRA,
to Con(PA). For fixed p, Proposition E requires approximately p quantaifier
induction (exact calculation is being postponed).

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

I use http://www.math.ohio-state.edu/%7Efriedman/ for downloadable
manuscripts. This is the 254th 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-249 can be found at
http://www.cs.nyu.edu/pipermail/fom/2005-June/008999.html in the FOM
archives, 6/15/05, 9:18PM.

250. Extreme Cardinals/Pi01  7/31/05  8:34PM
251. Embedding Axioms  8/1/05  10:40AM
252. Pi01 Revisited  10/25/05  10:35PM
253. Pi01 Progress  10/26/05  6:32AM
254. Pi01 Progress/more  11/10/05  4:37AM

Harvey Friedman