[FOM] 462: Improvements/Pi01 independence

Harvey Friedman friedman at math.ohio-state.edu
Sat May 14 07:02:35 EDT 2011

```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.

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

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

```