[FOM] 543: New Explicitly Pi01

[Harvey Friedman]

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