[FOM] 535: Updated Perfect Explicitly Pi01

Sat Aug 30 14:39:53 EDT 2014

In #534, I proposed a Ping Pong explicitly Pi01 incompleteness largely
because of the somewhat awkward example in
https://u.osu.edu/friedman.8/foundational-adventures/downloadable-manuscripts/
 #82 involving a function from variable length tuples. There are some
subtleties I didn't account for in #534, and instead of getting to the
bottom of them, I have upgraded the ones from #82
now to use only a function on uniform length tuples, relieving this
awkwardness. I also somewhat improved the overall statement using the
notion of order invariant reduction. Here "reduction" should not be
confused with my prior use of the term.

I will be putting a new version of #82 up shortly. For inpatient readers,
see Propositions 6 and 7 below.

I use an order theoretic F:Q^2k into Q^k, and a very interesting question
is whether the statement is independent of ZFC if I instead use an order
invariant F:Q^k into Q^k. There is even the prospect of going further and
using some specific natural order invariant F:Q^k into Q^k.

DEFINITION 1. F:Q^2k into Q^k is order theoretic if and only if graph(F)
containedin Q^3k is order theoretic (boolean combination of inequalities
in variables and constants). R is a reduction on Q^k if and only if R is
reflexive and x R y implies max(x) >= max(y). A sequence is R independent
if and only if all terms lie in Q^k no two distinct terms are related by
R.

THEOREM 1. Let F:Q^2k into Q^k be order theoretic. Every order invariant
reduction R containedin Q^2k has an independent  x_1,...,x_n with each
F(x_i,x_i+1) R x_i+2, i <= n-2.

TEMPLATE A. Fix k >= 1 and T:Q^k into Q^k. Let F:Q^2k into Q^k be order
theoretic. Every order invariant reduction R containedin Q^2k has an
independent  x_1,...,x_n,T(x_n) with each F(x_i,x_i+1) R x_i+2, i <= n-2.

TEMPLATE B. Fix k >= 1 and T:Q^k into Q^k. Let F:Q^2k into Q^k be order
theoretic. Every order invariant reduction R containedin Q^2k has an
independent x_1,...,x_n,T(x_1),...,T(x_n) with each F(x_i,x_i+1) R x_i+2,
i <= n-2.

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

THEOREM 2. (EFA). 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 3. (EFA). Templates A,B hold for Nsh on any Q^k.

PROPOSITION 4. Template A holds for ush on any Q^k. Template B holds for
ush on any Q^k.

THEOREM 5. Proposition 4 (both forms) is provably equivalent to Con(SRP)
over EFA. For each fixed k, Proposition 4 (both forms) is provable in SRP.
There exists k such that Proposition 4 (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).

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

PROPOSITION 6. Let F:Q^2k into Q^k be order theoretic. Every order
invariant reduction R containedin Q^2k, has an independent
 x_1,...,x_n,ush(x_n)} with each F(x_i,x_i+1) R x_i+2, i <= n-2.

PROPOSITION 7. Let F:Q^2k into Q^k be order theoretic. Every order
invariant reduction R containedin Q^2k has an independent
 x_1,...,x_n,ush(x_1),...,ush(x_n) with each F(x_i,x_i+1) R x_i+2, i <= n-2.

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 look for such an infinitely long sequence, and the resulting
infinite forms would be provably equivalent to Con(SRP) over WKL_0.

We do not yet know the status of the following.

PROPOSITION 8. Let F:Q^k into Q^k be order theoretic. Every order
invariant reduction R containedin Q^2k has an independent
 x_1,...,x_n,ush(x_n)} with each F(x_i) R x_i+1, i <= n-1.

PROPOSITION 9. Let F:Q^k into Q^k be order theoretic. Every order
invariant reduction R containedin Q^2k has an independent
 x_1,...,x_n,ush(x_1),...,ush(x_n)} with each F(x_i) R x_i+1, i <= n-1.

****************************************
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 535th 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-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
534: Perfect Explicitly Pi01  8/27/14  10:40AM

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