[FOM] 531: General Theory/Perfect Pi01

[Harvey Friedman]

The perfect Pi01 independent statements of
https://u.osu.edu/friedman.8/foundational-adventures/downloadable-manuscripts/
#82 are special cases of a perfectly natural family of statements. We
conjecture that all of the statements in this natural family can be decided
in SRP and even in WKL_0 + Con(SRP)., or still further in WKL_0 +
{Con(SRP_k): k >= 1}.

This is going to be quite a challenge, so in the meantime we have looked at
some smaller classes of statements for which we can establish such
completeness for the SRP hierarchy.

TEMPLATE (square). Let phi be a purely universal sentence in <, with atomic
formulas t epsilon S, s < t, where s,t are either variables ranging over
Q[0,1], or constants from Q[0,1]. Let k >= 1. Every order invariant subset
of Q^2k has a maximal square obeying phi.

TEMPLATE (root). Let phi be a purely universal sentence in <, with atomic
formulas t epsilon S, s < t, where s,t are either variables ranging over
Q[0,1], or constants from Q[0,1]. Let k >= 1. Every order invariant subset
of Q^2k has a maximal root obeying phi.

TEMPLATE (clique). Let phi be a purely universal sentence in <, with atomic
formulas t epsilon S, s < t, where s,t are either variables ranging over
Q[0,1], or constants from Q[0,1]. Let k >= 1. Every order invariant graph
on Q^k has a maximal clique obeying phi.

CONJECTURE. Each instance of each of the above 3 templates is provable or
refutable in SRP and WKL_0 + {Con(SRP_k): k >= 1}. In fact, provable there
or refutable in RCA_0.

THEOREM. There are instances of each of the above 3 templates that rise in
SRP cofinally. In particular, ones that are provable in SRP but not
provable in ZFC (assuming ZFC is consistent).

It is evident that for each k,n,r, the following statement is a special
case, presented in two forms. Note that the second is taken from
https://u.osu.edu/friedman.8/foundational-adventures/downloadable-manuscripts/
#82

Every order invariant subset of Q[0,1]^2k has a maximal square (root) whose
sections at strictly increasing tuples from {1,1/2,...,1/n} agree below 1/n.

Every order invariant subset of Q[0,n]^2k has a maximal square (root) whose
sections at strictly increasing tuples of positive integers <= n agree
below 1.

and the same for the graph formulations:

Every order invariant graph on Q[0,1]^k has a maximal clique whose sections
at strictly increasing tuples from {1,1/2,...,1/n} agree below 1/n.

Every order invariant graph on Q[0,n]^k has a maximal clique whose sections
at strictly increasing tuples of positive integers <= n agree below 1.

Now what are we in a position to claim here?

We can recast our statements in terms of the inclusion between the "lower
section" at tuples. We can also use general sections, where we fix
arguments that are not necessarily in front.

DEFINITION. Let S be containedin Q[0,1]^k. The lower general sections of S
are obtained by fixing at least 1 and less than k coordinates with
rationals from [0,1], and taking the set of tuples of the remaining
arguments, provided that the arguments are less than all of the fixed
arguments.

DEFINITION. A k dimensional lower general section inclusion condition, or
k-LGSIC, is a condition on S containedin Q[0,1]^k asserting that one
particular lower general section of S is contained in another particular
lower general section of S.

THEOREM. The above Conjecture holds for the three Templates for finite sets
of k-LGCIS, k varying.

****************************************
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 53
​1st​
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

​Harvey Friedman​
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20140822/72ce22ab/attachment-0001.html>