[FOM] 462: Improvements/Pi01 independence

[Harvey Friedman]

We have an improved presentation of the infinitary statement.

All of this material is present in an updated version of my book on my  
website. The new date of the Introduction and of Entire Book, is  
5/14/11.

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

MAXIMAL CLIQUE STRICT UPPER SPLIT THEOREM. Every order invariant graph  
on [-1,1]^k intersect Q^k has a maximal clique that contains its  
strict upper split.

The strict upper split of q in Q is q if q < 0; undefined if q = 0; q/ 
2 if q > 0.

Thus the strict upper split is partial.

The strict upper split of a set of vectors is the set of strict upper  
splits of its elements.

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

We have overhauled the finite construction statement.

Let G be a graph on {-n!,...,n!}^k, n >= 0. We now present the G  
clique construction.

Initialize the consruction by setting x_1 = (-n!,...,-n!).

Suppose a clique x_1,...,x_p in G, has been constructed, p >= 1.

1. Find the least i <= p such that there exists a clique  
{x_1,...,x_p,y} ≠ {x_1,...,x_p} in G, where every coordinate of y is  
in {0,n,...,kn}, or is a coordinate of some x_j, 1 <= j <= i.

3. If i does not exist, set x_p+1 = x_p. If i,y exist, set x_p+1 to be  
y, or some z disconnected from y, max(z) < max(y).

The clause max(z) < max(y) reflects greed.

The upper n-shift of a vector is obtained by adding n to all of its  
nonnegative coordinates.
FINITE CONSTRUCTION THEOREM. Let n > 8kr > 0. For every order  
invariant graph on {-n!,...,n!}^k, the G construction creates some  
x_1,...,x_r, which, together with their upper n-shifts, forms a clique  
in G.

In the above, we use a very crude but safe estimate. We will give more  
refined estimates in the future.

Note that the Finite Construction Theorem is explicitly Pi01.
THEOREM. The Finite Construction Theorem is provably equivalent, over  
EFA, to Con(SRP). It is provable in SRP+ but not in any consistent  
fragment of SRP that logically implies RCA_0.

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

The Finite Games are now clearer.

Let G be any finite graph and n >= 1. We define the game G[n] as  
follows.

There are two players, Alice and Bob. They alternately move, with  
Alice playing the first move. They each make a total of n moves.

All moves by both players are vertices of G. Alice can play any move  
v. Bob must respond with a vertex w which is not connected to v in G.

To comnplete the definition of G[n], we say that Bob wins the game if  
and only if the set of all of his moves forms a clique in G.

It is easy to see that Bob wins G[n] by the following easy argument.  
Bob first chooses a maximal clique S for G. When Alice plays a vertex  
v, Bob looks up whether v Î S. If v Î S then Bob copies v. If v Ï S  
then Bob plays some w Î S which is not related to v.

Now let G be a graph on [-1,1]^k intersect Q^k, and n >= 1. We let  
G[n]* be the following modified game. Alice and Bob alternately move,  
with Alice playing the first move. They each make a total of n moves.

All moves by both players must be from [-1,1]^k intersect Q^k. Alice  
can play any move v. Bob must respond with w which is not connected to  
v in G.

Bob wins if and only if the set of all of his moves, together with  
their strict upper splits, forms a clique in G.

We also consider the game G[infinity]*, where the palyers each make  
infinitely many moves.

INFINITE UPPER SPLIT GAME THEOREM. For every order invariant graph G  
on [-1,1]^k intersect Q^k, Bob wins the game G[infinity]*.

FINITE UPPER SPLIT GAME THEOREM. For every order invariant graph G on  
[-1,1]^k intersect Q^k and n >= 1, Bob wins the game G[n]*.

We let G[n]** be the same as G[n]*, except that for all 1 <= i <= n,  
Alice's i-th move uses only numerators and denominators of magnitude  
at most (8ki)!!, and Bob's i-th move uses only numerators and  
denominators of magnitude at most (16ki)!!.

ESTIMATED STRICT UPPER SPLIT GAME THEOREM. For every order invariant  
graph G on [-1,1]^k intersect Q^k and n >= 1, Bob wins the game G[n]**.

Here we use a very crude but safe estimate. We expect to give more  
refined estaimates in the future.

THEOREM. The Infinite Upper Split Game Theorem is provably equivalent,  
over WKL_0, to Con(SRP). It is provable in SRP+ but not in any  
consistent fragment of SRP that logically implies RCA_0.

THEOREM. The Finite Upper Split Game Theorem, and the Estimated Upper  
Split Game Theorem, are provably equivalent, over EFA, to Con(SRP).  
Both are provable in SRP+ but not in any consistent fragement of SRP  
that logically implies EFA.

Note that the Finite Upper Split Game Theorem can be seen to be  
immediately equivalent to an effectively given set of sentences in the  
structure (Q,+,<). Using the well known decision procedure for this  
structure, we see that Finite Upper Split Game Theorem is provably  
equivalent to a Pi01 sentence over EFA.

Also note that in the Estimated Upper Split Game Theorem, the space of  
moves G[n]** is finite - the number is a function of the dimension, k.  
Hence the Esimated Upper Split Game Theorem is explicitly Pi01.

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

I use http://www.math.ohio-state.edu/~friedman/ for downloadable
manuscripts. This is the 462nd 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

Harvey Friedman