[FOM] 484:Finite Choice and Incompleteness

Sun Feb 19 21:22:37 EST 2012

THIS RESEARCH WAS PARTIALLY SUPPORTED BY THE JOHN TEMPLETON FOUNDATION

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

THIS POSTING IS ENTIRELY SELF CONTAINED

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

This posting represents a breakthrough in the explicitly Pi01  
statements. It lives in the positive integers, and there are no  
partially defined functions.

If we allow infinite statements that are implicitly Pi01 relative to  
predicate calculus (the completeness theorem), then the best are in http://www.cs.nyu.edu/pipermail/fom/2012-February/016192.html 
  .

FINITE CHOICE AND INCOMPLETENESS
by
Harvey M. Friedman
February 19, 2012

1. INVARIANCE AND SPAN

We use Z+ for the set of all positive integers, and [n] for {1,...,n}.

We will be particularly focused on the spaces [nt]^k. It will be  
notationally convenient to view the points t,2t,...,nt as inherent in  
the structure of the ambient space [nt]^k.

We use Z+* for the set of all finite sequences from Z+.

We say that x,y in Z+* are order equivalent if and only if

i. x,y have the same length.
ii. For all 1 <= i,j <= lth(x), x_i < x_j iff y_i < y_j.

We say that A contained in [nt]^2k is order invariant if and only if  
for all order equivalent x,y in [nt]^2k, x in A implies y in A.

For each t in Z+, we define the function H_t:Z+* into Z+* by

H_t(x) is the result of adding t to all coordinates greater than all  
coordinates not divisible by t.

We say that F:[nt]^k into [nt]^k is H_t invariant if and only if for  
all x,H_t(x) in [nt]^2k, x in graph(F) implies H_t(x) in graph (F).

We say that F:[nt]^k into [nt]^k is completely H_t invariant if and  
only if for all x,H_t(x) in [nt]^2k, x in graph(F) iff H_t(x) in graph  
(F).

Let R be a relation on [nt]^k. A choice function (for R) is a function  
F:]nt]^k into [nt]^k whose graph is contained in R.

Obviously if R is reflexive, then there is a choice function for R -  
namely the identity function on [nt]^k.

A set is said to be detached (relative to R) if and only if no two  
elements are R related.

We can use F:[nt]^k into [nt]^k to generate elements of [nt]^k  
starting from t,2t,...,nt.

We define the 1-span of F as F[{t,2t,...,nt}^k]. The (i+1)-span of F  
is F[E^k], where E^k is the least E^k containing the 1-span,...,i-span  
of F.

2. FINITE CHOICE THEOREM

FINITE CHOICE THEOREM (ref sym). Every reflexive symmetric relation on  
[nt]^k has a choice function with detached range.

FINITE CHOICE THEOREM (ref red). Every reflexively reducing relation  
on [nt]^k has a choice function with detached range.

Here we say that R is reflexively reducing if and only if x = y  
implies R(x,y) implies (x = y or max(x) > max(y)).

Both of these Theorems are provable in EFA.

3. EXOTIC FINITE CHOICE THEOREMS

EXOTIC FINITE CHOICE THEOREM [ref sym). Let t >= (8knr)!. Every order  
invariant reflexive symmetric relation on [nt]^k has a completely H_t  
invariant choice function with detached r-span.

EXOTIC FINITE CHOICE THEOREM (ref red). Let t >= (8knr)!. Every order  
invariant reflexively reducing relation on [nt]^k has a completely H_t  
invariant choice function with detached r-span.

EXOTIC FINITE CHOICE THEOREM (ref red). Let t >= (8knr)!. Every order  
invariant reflexively reducing relation on [nt]^k has an H_t invariant  
choice function with detached r-span.

Note that these Exotic Finite Choice THeorems are explicitly Pi01.  
Here (8knr)! is a crude but safe bound. We will look into what is  
really needed in due course.

THEOREM. The Exotic Finite Choice Theorem (ref sym), and the Exotic  
Finite Choice Theorem (ref red), are provably equivalent to Con(SRP)  
over EFA. This is true even for r = 2. If we replace "completely Z+up  
invariant" with "upper integral invariant", then the same results  
hold. For k = 2, or for n = 2, the statements are provable in ZFC. We  
obtain incompleteness from ZFC if we fix k = n = 16.

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

I use http://www.math.ohio-state.edu/~friedman/ for downloadable
manuscripts. This is the 484th 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
479: Explicitly Pi01 Incompleteness  2/12/12  9:16AM
480: Order Equivalence and Incompleteness
481: Complementation and Incompleteness  2/15/12  8:40AM
482: Maximality, Choice, and Incompleteness 2  2/19/12 7:43AM
483: Invariance in Q[0,n]^k  2/19/12  7:34AM

Harvey Friedman