[FOM] 534: Perfect Explicitly Pi01

[Harvey Friedman]

​In ​
https://u.osu.edu/friedman.8/foundational-adventures/downloadable-manuscripts/
#82.
​ we presented ​perfect mathematically natural implicitly Pi01 sentences
independent of ZFC. There was also an arguably perfect mathematically
natural explicitly Pi01 sentence independent of ZFC. Here we considerably
improve this to a perfect mathematically natural explicitly Pi01 sentence
independent of ZFC, along with a perfect mathematically natural explicitly
Pi01 template. The template is applied to a perfect mathematically natural
piecewise linear function acting on each Q^k. I will be upgrading #82
shortly.

We present the development in terms of graphs. However, it can equally well
be stated using only binary relations. We do this as an addendum.

DEFINITION
​1​
. Let G be a graph on Q^k. An independent set in G is a
​subset of Q^k ​
such that no two elements are adjacent. x G reduces to y if and only if x,y
in Q^k and (x = y or (x,y are adjacent and max(x) > max(y)).

​PING PONG THEOREM (trivial). For all x_0 in Q^k, all order invariant
graphs G,H on Q^k have respective independent sets {x_1,...,x_n},
{y_1,...,y_n}, where  x_0,...,x_n-1 respectively H reduce to y_1,...,y_n,
and y_1,...,y_n-1 respectively G reduce to x_2,...,x_n.

The above version is trivial because we can set x_1,...,x_n,y_1,...,y_n =
x_0.

PING PONG TEMPLATE A. Let k >= 1 and T:Q^k into Q^k. For all x_0 in Q^k,
all order invariant graphs G,H on Q^k have respective independent sets
{x_1,...,x_n,T(x_n)}, {y_1,...,y_n,T(y_n)}, where  x_0,...,x_n-1
respectively H reduce to y_1,...,y_n, and y_1,...,y_n-1 respectively G
reduce to x_2,...,x_n.

PING PONG TEMPLATE B. Let k >= 1 and T:Q^k into Q^k. For all x_0 in Q^k,
all order invariant graphs G,H on Q^k have respective independent sets
{x_1,...,x_n,T(x_1),...,T(x_n)}, {y_1,...,y_n,T(y_1),...,T(y_n)}, where
 x_0,...,x_n-1 respectively H reduce to y_1,...,y_n, and y_1,...,y_n-1
respectively G reduce to x_2,...,x_n.

Obviously for a given T, the statement in Ping Pong Template B immediately
implies the statement in Ping Pong Template A.

THEOREM 1. (EFA). Ping Pong Template A is false for any linear function
T:Q^k into Q^k other than the identity.

What about piecewise linear T:Q^k into Q^k?

DEFINITION 2. The N shift, Nsh, is defined on each Q^k by Nsh(x) = x+1 if x
is in N^k; x otherwise. The upper shift, ush, is defined on each Q^k by
ush(x) = the result of adding 1 to all nonnegative coordinates of x.

THEOREM 2. (EFA). Ping Pong Templates A,B hold for Nsh on any Q^k.

PROPOSITION 3. Ping Pong Template A holds for ush on any Q^k. Ping Pong
Template B holds for ush on any Q^k.

THEOREM 4. Proposition 3 (both forms) is provably equivalent to Con(SRP)
over EFA. For each fixed k, Proposition 3 (both forms) is provable in SRP.
There exists k such that Proposition 3 (for Template A) is provable in SRP
but not in ZFC (assuming ZFC is consistent). There exists n such that
Proposition 3 (for Template A) is provable in SRP but not in ZFC (assuming
ZFC is consistent).

How small can k be taken in Theorem 4? Too early for me to have
investigated this. Previous experience suggests a target of k = 4, and also
a target of n = 4.

For the record, we state the arguably perfect mathematically natural
explicitly Pi01 independence from ZFC as follows:

PING PONG A (graphs). For all x_0 in Q^k, all order invariant graphs G,H on
Q^k have respective independent sets {x_1,...,x_n,ush(x_n)},
{y_1,...,y_n,ush(y_n)}, where  x_0,...,x_n-1 respectively G reduce to
y_1,...,y_n, and y_1,...,y_n-1 respectively H reduce to x_2,...,x_n.

PING PONG B (graphs). For all x_0 in Q^k, all order invariant graphs G,H on
Q^k have respective independent sets {x_1,...,x_n,ush(x_1),...,ush(x_n)},
{y_1,...,y_n,ush(y_1),...,ush(y_n)}, where  x_0,...,x_n-1 respectively G
reduce to y_1,...,y_n, and y_1,...,y_n-1 respectively H reduce to
x_2,...,x_n.

These are written in explicitly Pi02 form, but we can apply the well known
decision procedure for (Q,<) to put it in explicitly Pi01 form,. Or we can
directly put an a priori bound on the numerators and denominators needed
for the x's and y's in terms of k,n, and the numerators and denominators
used in x_0.

We can also play this Ping Pong for infinitely many steps, and the
resulting infinite forms would be provably equivalent to Con(SRP) over
WKL_0.

ADDENDUM.

DEFINITION 3. Let R be contained in Q^2k. X is R independent if and only if
X is contained in Q^k and for all distinct x,y in X, x notR y. x R reduces
to y if and only if x,y are in Q^k and (x = y or (x R y and max(x) >
max(y)).

PING PONG A (relations). For all x_0 in Q^k, all order invariant R,S
contained in Q^2k have respective independents sets {x_1,...,x_n,ush(x_n)},
{y_1,...,y_n,ush(y_n)}, where  x_0,...,x_n-1 respectively S reduce to
y_1,...,y_n, and y_1,...,y_n-1 respectively R reduce to x_2,...,x_n.

PING PONG B (relations). For all x_0 in Q^k, all order invariant graphs R,S
contained in Q^2k have respective independent sets
 {x_1,...,x_n,ush(x_1),...,ush(x_n)}, {y_1,...,y_n,ush(y_1),...,ush(y_n)},
where  x_0,...,x_n-1 respectively S reduce to y_1,...,y_n, and
y_1,...,y_n-1 respectively R reduce to x_2,...,x_n.

****************************************
My website is at https://u.osu.edu/friedman.8/ and my youtube site is at
https://www.youtube.com/channel/UCdRdeExwKiWndBl4YOxBTEQ
This is the 534t
​​
i
​h​
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-527 can be found at the FOM posting
http://www.cs.nyu.edu/pipermail/fom/2014-August/018092.html

528: More Perfect Pi01  8/16/14  5:19AM
529: Yet more Perfect Pi01 8/18/14  5:50AM
530: Friendlier Perfect Pi01
531: General Theory/Perfect Pi01  8/22/14  5:16PM
532: More General Theory/Perfect Pi01  8/23/14  7:32AM
533: Progress - General Theory/Perfect Pi01 8/25/14  1:17AM

Harvey Friedman
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20140827/157534f2/attachment.html>