[FOM] 611: Function Emulation/Continuation Theory 2

[Harvey Friedman]

THIS POSTING IS SELF CONTAINED

although we start with some comments on
http://www.cs.nyu.edu/pipermail/fom/2015-September/019027.html But the
formal text, sections 1,2,3, are self contained.

We make some expositional improvements on
http://www.cs.nyu.edu/pipermail/fom/2015-September/019027.html We also
put the implicitly Pi01 statement into a fundamental context of
infinitely many statements, and move toward giving a decision
procedure for this attractive family of statements. Such a decision
procedure can only be established using large cardinals.

We have found that Continuations are arguably more natural than
Emulations. Both the implicitly and explicitly Pi01 statements are
better when stated with Emulations rather than Continuations. In the
case of the implicitly Pi01 statements, the version with Emulations is
only slightly simpler, but Continuations are arguably more natural
than Emulations. So I am left with both the Emulation and Continuation
versions of the implicitly Pi01 statements.

However, for the explicitly Pi01 statements, the versions with
Emulations are significantly simpler. So I only present the
Continuation forms of the explicitly Pi01 statements.

Now for a major expositional upgrade in the implicitly Pi01 statement.
Here is the version with Continuations from
http://www.cs.nyu.edu/pipermail/fom/2015-September/019027.html

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.

Recall that functions in X are maps from X to X. So the functions
involved here take values in Q^k.

I wrote "is" instead of "=" for the following reason. g(0,...,k-1)
and/or g(1,...,k) might be undefined. And then I wrote "above" for
k-tuples.

I had another way of saying the same thing, and I rejected it in favor
of what I wrote above. I now have second thoughts.

Here is what I like best now:

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

I chose the former rather than the latter because I was trying to get
away without referring to the coordinate functions g_1,...,g_k, AND I
was trying to get as close as I can to an actual equation.

But I have now decided that this new form above is better. There is no
longer any problem with abusing notation surrounding undefined
expressions. The condition

g_i(1,...,k) > k

automatically implies that g_i(1,...,k) is defined. NOW there is a
subtle difference between the two. In the new version, it is possible
that g_i(1,...,k) might be undefined, yet g_i(0,...,k-1) be defined,
in which case the new punch line holds. So in the independence proof,
one has to take this into account, and I do.

I have reworked the definition of factorial maximality so that it is
much clearer. I present two forms: factorial maximal and strong
factorial maximal.

The third section exploits the very basic logical form of the punch
line in the implicitly Pi01 statement.

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. For
tuples x_1,...,x_r, x_1x_2...x_r is the concatenation of x_1,...,x_r.

DEFINITION 1.2. Let E containedin Q^k and p in Q.  E|>p,
E|>=p, E|<p, E|<=p consists of the elements of E whose coordinates are
all >max(x), >=max(x), <max(x), <=max(x), respectively. 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. If X = Q^k then for 1
<= i <= k, f_i(x) is the i-th coordinate of f(x).

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

DEFINITION 1.4. Let f be a function in Q^k and X containedin Q^k. A
continuation of f in X is an emulation of f in X which contains f. A
maximal continuation of f in X is a continuation of f in X which is a
proper subset of any continuation of f in X.

Note that in Definitions 1.3, 1.4, we can change the last 'f' to 'g'
without any effect.

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

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

We now use step maximality on Q^k.

DEFINITION 1.5. Let f be a function in Q^k. A step maximal
emulation of f in Q^k is a function g in Q^k where each g|<=n is a
maximal emulation of f in Q^k|<=n. 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.3. Every finite function in Q^k has a step maximal
emulation in Q^k, where each g_i(0,...,k-1) < 0 is g(1,...,k).

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

THEOREM 1.5. Propositions 1.1 - 1.4 are provably equivalent to Con(SRP)
over WKL_0.

These Propositions are implicitly Pi01 via Goedel's Completeness Theorem.

2. FINITE FUNCTIONS IN {1,...,n!}^k

DEFINITION 2.1. Let f be a function in {1,...,n!}^k. g is a factorial
maximal emulation of f in {1,...,n!}^k if and only if g is an
emulation of f in {1,...,n!}^k, where all emulations of g in
{1,...,n!}^k have the same 2k-tuples from the factorials and the
coordinates of values of g at the factorials.

DEFINITION 2.2. Let f be a function in {1,...,k}^k. g is a strong
factorial maximal emulation of f in {1,...,n!}^k if and only if g is
an emulation of f in {1,...,n!}^k, where all emulations of
g|<=m in {1,...,m}^k have the same 2k-tuples from the factorials and
the coordinates of values of g at the factorials.

PROPOSITION 2.1. Every function in {1,...,n!}^k has a
factorial maximal emulation in {1,...,n!}^k that omits (8k)!!-1.

PROPOSITION 2.2. Every function in {1,...,n!}^k has a
strong factorial maximal emulation in {1,...,n!}^k that omits (8k)!!-1.

These Propositions are obviously explicitly Pi01.

THEOREM 2.3. Propositions 2.1 and 2.2 are provably equivalent to
Con(SMAH) over ACA.

3. TEMPLATE

It is most convenient to focus on

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

Now here is the main point. The punch line

each g_i(1,...,k) > k is g_i(0,...,k-1)

represents a quantifier free formula in the language with k k-ary
partial function symbols g_1,...,g_k, and <.

When working with logic with only partial functions, we use what is
called free logic, where = means both sides are defined and equal.
More generally, atomic formulas using the given relation and function
and constant symbols and =, imply that all terms are defined. "Being
defined" is then represented as

expression = expression

although it is natural to introduce up arrow and down arrow on terms
to indicated undefinedness and definedness, respectively, as well as
the special binary connector "Kleene equals" meaning that either both
dies are undefined or both sides are defined and equal. .

So the clause in question is written

g_1(1,...,k) > k arrows g_1(1,...,k) = g_1(0,...,k-1) and
...
g_k(1,...,k) > k arrows g_k(1,...,k) = g_k(0,...,k-1).

Note that there are no nestings of the g's. Down the road we want to
allow such nesting.

Let us call these "unseated quantifier free".

TEMPLATE 3.1. Let phi be an unnested quantifier free sentence in <,=
and k-ary g_1,...,g_k, with constants from Q.  Every finite function
in Q^k has a maximal emulation in Q^k|>= satisfying phi.

Note that every instance of Template 3.1 is implicitly Pi01 via
Goedel's Completeness Theorem.

We already know that there are instances of Template 3.1 that are
provably equivalent to Con(SRP) over WKL_0.

CONJECTURE. Every instance of Template 3.1 is provable or refutable in
WKL_0 + Con(SRP).

I will first try to exploit the structure of the phi that we use, to
obtain significant partial results. The phi that we use consists of a
finite conjunction of very simple sentences. In fact, there is really
only one conjunct, where we simply go through i = 1,...,k.

************************************************************
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 611th 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  9/315  1:17PM
610: Function Continuation Theory 1  9/4/15  3:40PM

Harvey Friedman