[FOM] 533: Progress - General Theory/Perfect Pi01
Harvey Friedman
hmflogic at gmail.com
Mon Aug 25 01:17:12 EDT 2014
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>
More information about the FOM
mailing list