[FOM] 543: New Explicitly Pi01
Harvey Friedman
hmflogic at gmail.com
Wed Sep 10 23:17:36 EDT 2014
TYPOS IN #541, #542. In several places I wrote Q^k instead of Q^k+1 -
because later in the statements I used k+1 arguments.
We have discovered a very satisfactory new kind of explicitly finite
Pi01 independence from ZFC at the SRP level. It has advantages and
disadvantages over the explicitly Pi01 already in
https://u.osu.edu/friedman.8/foundational-adventures/downloadable-manuscripts/
#82.
This new development lets us expand into richer structures such as the
ordered group of rationals, and even the ordered ring of reals.
We will begin by focusing on (Q,<).
DEFINITION 1. Let f:Q[-n,n]^k into Q[-n,n] be partial. The t-span of f
is the set of all values of the expressions involving -n,...,n, and at
most t occurrences of f. Note that many or even all such expressions
may be undefined. Let A be a universal property of partial f:Q[-n,n]^k
into Q[-n,n]. We say that f is a t-maximal solution to A if and only
if f is a solution to A, with no proper extension of f by a k-tuple
from the t-span that is a solution to A.
PROPOSITION 1. Every universal property of partial f:Q[-k,k]^k into
Q[-k,k], using no constants, has a finite t-maximal solution with
f(0,...,k-1) < 0 implies f(0,...,k-1) = f(1,...,k).
Proposition 1 is explicitly Pi02. However, there is an obvious bound
on the size of the t-maximal solution, and so the statement becomes
Pi01 using the decision procedure for (Q,<). Alternatively, we can
directly bound the numerators and denominators needed for the
rationals used in the finite t-maximal solution, thereby giving an
explicitly Pi01 statement.
What can we do if we allow addition?
PROPOSITION 2. Let r >> k,t >= 1. Every universal property of partial
f:Q[0,r]^k into Q[0,r], using <,+, and no constants, has a finite
t-maximal solution such that f(r,r^2,...,r^k) < r implies
f(r,r^2,...,r^k) = f(r^2,...,r^k+1). It suffices to assume that r >
(8kt)!.
Proposition 2 can be put into explicitly Pi01 form using the decision
procedure for (Q,<,+).
What can we do if we allow addition and multiplication? Below,
intervals are in the real numbers.
PROPOSITION 3. Let r >> k,t >= 1. Every universal property of partial
f:[0,r]^k into [0,r], using <,+,x, and no constants, has a finite
t-maximal solution such that f(r!,(2r)!,...,(kr)!) < r! implies
f(r!,(2r)!,...,(kr)!) = f((2r)!,(3r)!,...,(kr+r)!). It suffices to
assume that r > (8kt)!!.
Proposition 3 can be put into explicitly Pi01 form using the decision
procedure for (Reals,<,+).
THEOREM 4. Propositions 1-3 are provably equivalent to Con(SRP) over
EFA. As we fix k and quantify over t, we obtain statements provable in
SRP that are cofinal in the Con(SRP[k]) over EFA.
****************************************
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 543rd 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
535: Updated Perfect Explicitly Pi01 8/30/14 2:39PM
536: Pi01 Progress 9/1/14 11:31AM
537: Pi01/Flat Pics/Testing 9/6/14 12:49AM
538: Progress Pi01 9/6/14 11:31PM
539: Absolute Perfect Naturalness 9/7/14 9:00PM
540: SRM/Comparability 9/8/14 12:03AM
541: Master Templates 9/9/14 12:41AM
542: Templates/LC shadow 9/10/14 12:44AM
Harvey Friedman
More information about the FOM
mailing list