[FOM] 533: Progress - General Theory/Perfect Pi01

[Harvey Friedman]

There has been progress on the templating of the perfect Pi01 independent
statements of
https://u.osu.edu/friedman.8/foundational-adventures/downloadable-manuscripts/
 #82.

It will be most convenient to use the interval Q[-1,1] = Q intersect
[-1,1].

The master Template is as follows:

UNIVERSALIZED ORDER THEORETIC TEMPLATE (3 forms)
UOT

Let k >= 1 and phi be a universalized order theoretic property of subsets
of Q[-1,1]^2k. Every order invariant subset of Q[-1,1]^2k has a maximal
square with phi.
Let k >= 1 and phi be a universalized order theoretic property of subsets
of Q[-1,1]^k. Every order invariant subset of Q[-1,1]^2k has a maximal root
with phi.
Let k >= 1 and phi be a universalized order theoretic property of subsets
of Q[-1,1]^k. Every order invariant graph on Q[-1,1]^k has a maximal clique
with phi.

What is a universal order theoretic property of S contained in Q[-1,1]^m?
It is what we called "universal property" in posting #532. Here is a review
of the definition in new terminology.

DEFINITION 1. The order theoretic properties of S contained in Q[-1,1]^m
are Boolean combinations of formulas s < t, (t_1,...,t_m) epsilon S, where
s,t,t_1,...,t_m are variables x_i, i >= 1, ranging over Q[-1,1], or
constant from Q[-1,1].  We allow (combinations of) not, and, or, if then,
iff. Obviously we can allow <=,=,>,>=,not=.

DEFINITION 2. The universalized order theoretic properties of S containedin
Q[-1,1]^m take the form (forall x_1,...,x_r epsilon Q[-1,1])(phi), where
phi is an order theoretic property of S contained in Q]-1,1]^m whose
variables are among x_1,...,x_r.

Here is the Conjecture from #532:

CONJECTURE. Every instance of UOT (all three versions) are provable in SRP
or refutable in RCA_0. We know that there are perfectly natural instances
that are provable in SRP but not in ZFC (assuming ZFC is consistent, which
is generally believed).

In posting #532, I claimed a proof of the Conjecture for the universalized
order theoretic properties that assert a finite set of inclusions between
lower general sections of S at constants.

In this posting I present some stronger partial result based on logically
restricted classes  of universalized order theoretic properties of subsets
of Q[-1,1]^2k.

DEFINITION 3. The lower universalized order theoretic properties of S
containedin Q[-1,1]^m take the form of a finite conjunction of formulas
(forall x_1,...,x_r epsilon Q[-1,p))(phi), where phi is an order theoretic
property of S contained in Q]-1,1]^m whose variables are among x_1,...,x_r,
and all constants in phi are at least p.

LOWER UNIVERSALIZED ORDER THEORETIC TEMPLATE (3 forms)
LUOT

Let k >= 1 and phi be a lower universalized order theoretic property of
subsets of Q[-1,1]^2k. Every order invariant subset of Q[-1,1]^2k has a
maximal square with phi.
Let k >= 1 and phi be a lower universalized order theoretic property of
subsets of Q[-1,1]^k. Every order invariant subset of Q[-1,1]^2k has a
maximal root with phi.
Let k >= 1 and phi be a lower universalized order theoretic property of
subsets of Q[-1,1]^k. Every order invariant graph on Q[-1,1]^k has a
maximal clique with phi.

We have not been able to establish the Conjecture for LUOT.

DEFINITION 4. A simple lower universalized order theoretic property of S
containedin Q[-1,1]^m, psi_1 and ... and psi_c, where in all of the psi_i,
there are at most two occurrences of S.

SIMPLE LOWER UNIVERSALIZED ORDER THEORETIC TEMPLATE (3 forms)
SLUOT

Let k >= 1 and phi be a simple lower universalized order theoretic property
of subsets of Q[-1,1]^2k. Every order invariant subset of Q[-1,1]^2k has a
maximal square with phi.
Let k >= 1 and phi be a simple lower universalized order theoretic property
of subsets of Q[-1,1]^k. Every order invariant subset of Q[-1,1]^2k has a
maximal root with phi.
Let k >= 1 and phi be a simple lower universalized order theoretic property
of subsets of Q[-1,1]^k. Every order invariant graph on Q[-1,1]^k has a
maximal clique with phi.

THEOREM 1. Every instance of SLUOT (all three versions) is provable in SRP
or refutable in RCA_0. We know that there are perfectly natural instances
that are provable in SRP but not in ZFC (assuming ZFC is consistent, which
is generally believed).

THEOREM 2. phi provides a true instance of the first form of LUOT iff every
order invariant subset of Q[0,1]^2k has phi. phi provides a true instance
of the second (third) form of LUOT iff every order invariant subset of
Q[-1,1]^k has phi. These claims are provably equivalent to Con(SRP) over
WKL_0.

Of course, all instances of all of the Templates here and in posting #532
are implicitly Pi01 via Goedel's completeness theorem.

Harvey Friedman

****************************************
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
​3​
rd
​ ​
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

​Harvey Friedman​
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20140825/4a80119e/attachment-0001.html>