[FOM] 610: Function Continuation Theory 1

[Harvey Friedman]

THIS POSTING IS SELF CONTAINED

We now move from sets to functions.This has some unexpected benefits.
The punch line for the implicitly Pi01 statements is now a conditional
shift identity. For the explicitly Pi01 statements, we are now able to
use a weakened form of maximality, rather than bring in additional
considerations. This is a major advantage. In addition, continuation
of functions has a crude analogy with a famous topic in mathematics
called "analytic continuation". Of course, this may stay merely a
crude analogy.

1. FUNCTIONS IN Q^k

DEFINITION 1.1. Q,Z,N,Z+ is the set of all rationals, integers,
nonnegative integers, and positive integers, respectively.
n,m,r,s,t,i,j denote positive integers unless otherwise indicated.

DEFINITION 1.2. Let E containedin Q^k, x,y in Q^k, p in Q. E|>p,
E|>=p, E|<p, E|<=p consists of the elements of E whose coordinates are
all >p, >=p, <p, <=p, respectively. x is y above (below) p if and only
if we have no distinct x_i,y_i > p (< p). If x,y are undefined
expressions, then x is y above (below) p automatically. f is a
function in X if and only if f is a partial function from X into X.
Functions are treated as sets of ordered pairs.

DEFINITION 1.3. Let f be a function in Q^k and X containedin Q^k. A
continuation of f in X is a function g in X such that
i. f containedin g.
ii. For any x,y in g there exists z,w in f such that xy and zw are
order equivalent.
A maximal continuation of f in X is a continuation of f in X which is
not a proper subset of any continuation of f in X.

PROPOSITION 1.1. Every finite function in Q^k|>k has a maximal
continuation in Q^k|>=0, where g(0,...,k-1) is g(1,...,k) above k.

We now use step maximality on Q^k.

DEFINITION 1.4. Let f be a function in Q^k. A step maximal
continuation of f in Q^k is a function g in Q^k where each g|<=n is a
maximal continuation of f in Q^k|<=n.

PROPOSITION 1.2. Every finite function in Q^k|<0 has a step maximal
continuation in Q^k, where g(0,...,k-1) is g(1,...,k)  below 0.

THEOREM 1.3. Propositions 1.1, 1.2 are provably equivalent to Con(SRP)
over WKL_0.

2. FINITE FUNCTIONS

DEFINITION 2.1. g is a factorial maximal continuation of f in
{1,...,n}^k if and only if g is a continuation of f in {1,...,n}^k
with no continuation f union (g union {x})|<=max(x) of f in
{1,...,n}^k, where x notin g is a k tuple of factorials and
coordinates of values of f at factorials. S containedin Q^k omits p in
Q if and only if p is not a coordinate of any element of S.

PROPOSITION 2.1. For n > k, every function in {1,...,k}^k has a
factorial maximal continuation in {1,...,n!}^k that omits (8k)!!-1.

THEOREM 2.2. Proposition 1 is provably equivalent to Con(SMAH) over ACA.

************************************************************
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 610th 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
609. Finite Continuation Theory 17

Harvey Friedman