[FOM] 479:Explicitly Pi01 Incompleteness

[Harvey Friedman]

THIS RESEARCH WAS PARTIALLY SUPPORTED BY THE JOHN TEMPLETON FOUNDATION

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

THIS POSTING IS ENTIRELY SELF CONTAINED

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

This posting presents our currently preferred explicitly Pi01  
independent sentences. Here we can work in Z+^k.

This posting by no means obsoletes the work on Invariant Maximality  
(maximal squares, maximal cliques, etc.) in http://www.cs.nyu.edu/pipermail/fom/2012-February/016165.html 
. These have a particularly strong general strategic motivation.

The infinite ones in http://www.cs.nyu.edu/pipermail/fom/2012-February/016165.html 
  are implicitly Pi01, or "explicitly Pi01 via predicate calculus", in  
the sense that they are obviously equivalent to an explicitly Pi01  
sentence by formalizing them as satisfiability of sentences in  
predicate calculus with equality.

In summary, the ones here are more combinatorial, and the ones in http://www.cs.nyu.edu/pipermail/fom/2012-February/016165.html 
  are more conceptual.

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

SUBSPACES, REDUCTIONS

We use Z+ for the set of all positive integers, with its usual order.

Z+^k has the natural subspaces of the form A^k, A contained in Z+. For  
each A contained in Z+^k, we write A# for the subspace of Z+^k  
generated by A. I.e., A# = fld(A)^k.

Let R be a binary relation on Z+^k. I.e., R containedin Z+^k x Z+^k = Z 
+^2k.

We say that B is a reduction of A (relative to R) if and only if

i. A,B are subsets of Z^k.
ii. for all x in A, there exists y in B such that x = y or (max(x) >  
max(y) and R(x,y)).

Note that A is a (uninteresting) reduction of A.

We say that B is a fine reduction of A (relative to R) if and only if  
for all x in B, there does not exist y in B such that max(x) > max(y)  
and R(x,y).

These definitions are also made for {1,...,t}^k, where Z+ is replaced  
by {1,...,t}.

THEOREM 1. In every binary relation on Z+^k, Z+^k has a unique fine  
reduction. In every binary relation on {1,...,t}^k, {1,...,t}^k has a  
unique fine reduction.

FIRST INFINITE STATEMENT

PROPOSITION 2. Let k >= 1, and R be a binary relation on Z+^k. Some  
reduction A of some infinite E^k, 1 in E, is contained in some fine  
reduction of A# + {0,1} omitting {min(E)-1}^k.

ORDER EQUIVALENCE AND ORDER INVARIANCE

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

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

In each k, there are only finitely many order invariant subsets of Z+^k.

These definitions are also made for {1,...,t}^k, where Z+ is replaced  
by {1,...,t}.

We will be using order invariant binary relations on Z+^k, and on  
{1,...,t}^k, which are order invariant subsets of Z+^2k and  
{1,...,t}^2k, respectively.

SECOND INFINITE STATEMENT

PROPOSITION 3. Let r >= (8k)!, and R be an order invariant binary  
relation on Z+^k. Some reduction A of {1,r,r^2,...}^k is contained in  
some fine reduction of A# + {0,1} omitting {r-1}^k.

FINITE STATEMENT

PROPOSITION 4. Let r >= (8kp)!, and R be an order invariant binary  
relation on {1,...,r^p}^k. Some reduction A of {1,r,r^2,...,r^p}^k is  
contained in some fine reduction of A# + {0,1} omitting {r-1}^k.

If we remove the "omitting" clause, then in Propositions 2-4 follow  
immediately from Theorem 1, where we take the two reductions to both  
be the unique fine reduction of Z+^k (or {1,...,r^p}^k). However, the  
problem is that we have no way of controlling this unique fine  
reduction: (min(E)-1,...,min(E)-1), or (r-1,...,r-1) may well appear.

THEOREM 5. Propositions 2-4 are each provably equivalent to Con(SMAH)  
over ACA'.

SMAH = ZFC + {there exists a strongly k-Mahlo cardinal}_k.

REMARK

What is the significance of (r-1,...,r-1) being omitted? This  
"follows" from the fact that r "is" a limit ordinal, and conversely is  
used to show that r "is" a limit ordinal (with an appropriate choice  
of R). You can't subtract 1 from a limit ordinal.

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

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

450: Maximal Sets and Large Cardinals II  12/6/10  12:48PM
451: Rational Graphs and Large Cardinals I  12/18/10  10:56PM
452: Rational Graphs and Large Cardinals II  1/9/11  1:36AM
453: Rational Graphs and Large Cardinals III  1/20/11  2:33AM
454: Three Milestones in Incompleteness  2/7/11  12:05AM
455: The Quantifier "most"  2/22/11  4:47PM
456: The Quantifiers "majority/minority"  2/23/11  9:51AM
457: Maximal Cliques and Large Cardinals  5/3/11  3:40AM
458: Sequential Constructions for Large Cardinals  5/5/11  10:37AM
459: Greedy CLique Constructions in the Integers  5/8/11  1:18PM
460: Greedy Clique Constructions Simplified  5/8/11  7:39PM
461: Reflections on Vienna Meeting  5/12/11  10:41AM
462: Improvements/Pi01 Independence  5/14/11  11:53AM
463: Pi01 independence/comprehensive  5/21/11  11:31PM
464: Order Invariant Split Theorem  5/30/11  11:43AM
465: Patterns in Order Invariant Graphs  6/4/11  5:51PM
466: RETURN TO 463/Dominators  6/13/11  12:15AM
467: Comment on Minimal Dominators  6/14/11  11:58AM
468: Maximal Cliques/Incompleteness  7/26/11  4:11PM
469: Invariant Maximality/Incompleteness  11/13/11  11:47AM
470: Invariant Maximal Square Theorem  11/17/11  6:58PM
471: Shift Invariant Maximal Squares/Incompleteness  11/23/11  11:37PM
472. Shift Invariant Maximal Squares/Incompleteness  11/29/11  9:15PM
473: Invariant Maximal Powers/Incompleteness 1  12/7/11  5:13AMs
474: Invariant Maximal Squares  01/12/12  9:46AM
475: Invariant Functions and Incompleteness  1/16/12  5:57PM
476: Maximality, CHoice, and Incompleteness  1/23/12  11:52AM
477: TYPO  1/23/12  4:36PM
478: Maximality, Choice, and Incompleteness  2/2/12  5:45AM

Harvey Friedman