[FOM] 609: Finite Continuation Theory 17

[Harvey Friedman]

THIS POSTING IS SELF CONTAINED

Recall this perfect implicitly Pi01 statement:

PROPOSITiON 1. Every finite subset of Q^k|>n has a maximal nonnegative
continuation with S[1,...,n]|>n = S[0,...,n-1]|>n.

Let's review the definitions here.

DEFINITION 1. For x,y in Q^k, x,y are order equivalent if and only if
for all 1 <= i,j <= k, x_i < x_j iff y_i < y_j. Let E containedin Q^k.
S is a nonnegative continuation of E if and only if E containedin S
containedin Q^k|>=0, and for all x,y in S, there exists z,w in E, such
that xy is order equivalent to zw. (Here xy is the concatenation of
x,y). S is a maximal nonnegative continuation of E if and only if S is
a nonnegative continuation of E which is not a proper subset of any
nonnegative continuation of E. For S containedin Q^k, S[p_1,...,p_r] =
{x in S: x extends (p_1,...,p_r)}. S|>p = {x in S: x_1,...,x_k > p}.

For an explicitly Pi01 statement coming directly out of the above
proposition, we want

PROTOTYPE. Every finite subset of Q^k|>n has a finite weakly maximal
nonnegative continuation with S[1,...,n]|>n = S[0,...,n-1]|>n.

It seems that I missed a very satisfactory notion of "weakly maximal
nonnegative continuation" that makes the above Prototype work pretty
well.

DEFINITION 2. Let S containedin Q^k. S# is the least A^k containing S.
S* = {x in S#: S union {x} does not continue S}.

DEFINITION 3. S is a weakly maximal nonnegative continuation of E if
and only if S is a nonnegative continuation of E, where every element
of (S#\S)^k x {(0,1,...,k)} is order equivalent to an element of S*^k
x {(0,1,...,k)}.

PROPOSITION 2. Every finite subset of Q^k|>n has a finite weakly
maximal nonnegative continuation with S[1,...,n]|>n = S[0,...,n-1]|>n.

Proposition 2 is obviously explicitly Pi02. However, there is an
obvious a priori upper bound on the size of the continuation, making
the statement explicitly Pi01 via the decision procedure for (Q,<). We
can also bound the numerators and denominators in the continuation in
terms of this in the given finite set.

THEOREM 3. Proposition 2 is provably equivalent to Con(SRP) over EFA.

There are some stronger forms of Propositions 1 and 2 that should be
mentioned. These use what I call step maximality. For this, we don't
need to use nonnegative continuations, and can work with Q^k instead
of Q^k|>=0.

DEFINITION 4. Let x in Q^k. The N ceiling of x is the least element of
N that is at least as large as all coordinates of x. We write NC(x).

DEFINITiON 5. S is a step maximal continuation of E containedin Q^k if
and only if for all x in Q^k\S there exists y in S, NC(y) <= NC(x),
such that xy is not order equivalent to any zw, z,w in E. S is a
weakly step maximal continuation of E containedin Q^k if and only if
every x in (S#\S)^k x {(0,1,...,k)} is order equivalent to some y in
S**^k x {(0,1,...,k)}. Here S** = {x in S#: there exists y in S, NC(y)
<= NC(x) such that xy is not order equivalent to any zw, z,w in E}.

PROPOSITION 4. Every finite subset of Q^k|<0 has a step maximal
continuation with S[0,...,n]|<0 = S[1,...,n+1]|<0.

PROPOSITION 5. Every finite subset of Q^k|<0 has a finite weakly step
maximal continuation with S[0,...,n]|<0 = S[1,...,n+1]|<0.

THEOREM 6. Proposition 4 is provably equivalent to Con(SRP) over
WKL_0. Proposition 5 is provably equivalent to Con(SRP) over EFA.

I'm now looking at the continuation of functions.

************************************************************
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 609th 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-599 can be found at the FOM posting
http://www.cs.nyu.edu/pipermail/fom/2015-August/018887.html

600: Removing Deep Pathology 1  8/15/15  10:37PM
601: Finite Emulation Theory 1/perfect?  8/22/15  1:17AM
602: Removing Deep Pathology 2  8/23/15  6:35PM
603: Removing Deep Pathology 3  8/25/15  10:24AM
604: Finite Emulation Theory 2  8/26/15  2:54PM
605: Integer and Real Functions  8/27/15  1:50PM
606: Simple Theory of Types  8/29/15  6:30PM
607: Hindman's Theorem  8/30/15  3:58PM
608: Integer and Real Functions 2  9/1/15  6:40AM

Harvey Friedman