[FOM] 543: New Explicitly Pi01
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
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 >
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
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
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
More information about the FOM