[FOM] 623: Optimal Function Theory 2

[Harvey Friedman]

THIS POSTING IS SELF CONTAINED

In Optimal Function Theory 1,
http://www.cs.nyu.edu/pipermail/fom/2015-September/019128.html we came
to a breakthrough idea (in this context where every visible increase
in communicable clarity sounds for a great deal), by moving from sets
to partial functions to finally everywhere defined functions, where
the notion of support of an everywhere defined function is crucially
used. This move allows a significantly simpler punch line, which now
becomes a rather simple equation. Here support means simply the places
at which the function is not 0.

This revelation-for-me, using everywhere defined functions and
supports, now leads me to roll back some evolving old formulations,
which were designed for an environment with sets or partial functions.
Now that we are using only everywhere defined functions and supports,
we will now roll some of these back.

1. EMULATIONS, CONTINUATIONS, OPTIMALITY IN Q

Fix a subset E of Q. f,g will always denote functions from E^k into E.
We work with functions f,g:E^k into E.

DEFINITION 1.1. Q,Z+,N are the set of all rationals, positive
integers, and nonnegative integers, respectively. We use
p,q,x,y,z,w,u,v for rationals, and a,b,c,d,e,k,n,m,r,s,t for positive
integers. Functions are treated as sets of ordered pairs. For S
containedin Q^k, S|<=p is the set of all elements of S all of whose
coordinates are <= p. We say that S is below p if and only if all
coordinates of all elements of S are < p.

DEFINITION 1.2. A k-inequality takes the form s <,<=,>,>=,=,not= t,
where s,t are either a variable v_1,...,v_k or a term F(w_1,...,w_k),
where the w's are among the v's. Here F is a letter representing an
undetermined function f:E^k into E. The support of f:E^k into E is {x
in E^k: f(x) not= 0}.

EXAMPLES. k = 3. v_2 not= v_2. v_3 > F(v_2,v_2,v_3). F(v_1,v_1,v_1) <=
F(v_2,v_3,v_3).

DEFINITION 1.3. We say that g emulates f if and only if every set of
k-inequalities that has a solution in g with all g evaluations
nonzero, has a solution in f with all f evaluations nonzero. We say
that g continues f if and only if g emulates f and g extends f on the
support of f.

DEFINITION 1.4. We say that g is an optimal emulation of f if and only
if g is an emulation of f where no emulation of f properly extends g
on the support of g. We say that g is an optimal continuation of f if
and only if g is a continuation of f where no emulation of f properly
extends g on the support of g.

There is some robustness here.

THEOREM 1.1. g is an optimal emulation of f if and only if g is an
emulation of f where no emulation of g properly extends g on the
support of g. g is an optimal continuation of f if and only if g is a
continuation of f where no continuation of g (emulation of f,
emulation of g) properly extends g on the support of g. Every optimal
continuation is an optimal emulation. Every step optimal continuation
is a step optimal emulation. Every step optimal emulation is an
optimal emulation. Every step optimal continuation is a step optimal
emulation.

We also consider a sharper form of optimality.

DEFINITION 1.5. We say that g is a step optimal emulation of f if and
only if each g|<=n is an optimal emulation of f |<=n. We say that g is
a step optimal continuation of f if and only if every g|<=n is an
optimal continuation of f|<=n.

2. IMPLICITlY Pi01 PROPOSITIONS

THEOREM 2.1. Every f:Q^k into Q has a step optimal continuation. it
follows that every f:Q^k into Q has a step optimal emulation, optimal
continuation, and optimal emulation.

THEOREM 2.2. Theorem 2.1 for optimal emulations and continuations is
provable in RCA_0. Theorem 2.1 for step optimal emulations and step
optimal continuations is provably equivalent to ACA_0 over RCA_0.

PROPOSITION 2.3. Every f:Q^k into Q (with finite support) has an
optimal emulation with min(1,g(1,...,k)) = min(1,g(2,...,k+1)).

PROPOSITION 2.4. Every f:Q^k into Q with finite support containedin
Q|<1, has an optimal continuation with min(1,g(1,...k)) =
min(1,g(2,...,k+1)).

PROPOSITION 2.5. Every f:Q^k into Q (with finite support) has a step
optimal emulation with min(1,g(1,...,k)) = min(1,g(2,...,k+1)).

PROPOSITION 2.6. Every f:Q^k into Q with finite support containedin
Q|<1, has a step optimal continuation with min(1,g(1,...k)) =
min(1,g(2,...,k+1)).

PROPOSITION 2.7. Every f:Q^k|<=k+1 into Q|<=k+1 (with finite support)
has an optimal emulation with min(1,g(1,...,k)) = min(1,g(2,...,k+1)).

PROPOSITION 2.8. Every f:Q^k|<=k+1 into Q^k|<=k+1 with finite support
containedin Q|<1, has an optimal continuation with min(1,g(1,...k)) =
min(1,g(2,...,k+1)).

Propositions 2.3 - 2.8 can be seen to be implicitly Pi01 via Goedel's
Completeness Theorem.

THEOREM 2.9. Propositions 2.5 - 2.8 are provably equivalent to
Con(SRP) over WKL_0. Propositions 2.3,2.4 are provable in WKL_0 +
Con(SRP). Here we use either form of Propositions 2.3, 2.5, 2.7.

Here SRP = ZFC + {there exists a cardinal with the k-stationary Ramsey
property}_k.

At this time, we don't know much about the status of Propositions 2.3, 2.4.

There is another related punch line that should be mentioned. We can replace

min(1,g(1,...,k)) = min(1,g(2,...,k+1))

with

g(1,...,k,p) = g(2,...,k+1,p), p < 1.

We obtain the same results with this modified punch line.

There is a natural additional parameter associated with emulations
(and continuations). This is the number of variables allowed in the
sets of inequalities. We chose not to introduce this parameter here
because it doesn't affect the results much and we don't want any
unnecessary complications in the statements. We also consider some
less concrete forms of Propositions 2.3 - 2.8, but not in this posting
- in a later posting.

3. EMULATIONS AND OPTIMALITY IN {0,...,n!}

Here we only consider f,g:{0,...,n!}^2 into {0,...,n!}^2.

DEFINITION 3.1. A binary k-inequality takes the form s
<,<=,>,>=,=,not= t, where s,t are either a variable v_1,...,v_k or a
term F(x,y), where x,y are among the v's. Here F is a letter
representing an undetermined function f:{0,...,n!}^2 into {0,...,n!}.
f:{0,...,n!}^2 into {0,...,n!}. The support of f is {w in
{0,...,n!}^2: f(w) not= 0}.

DEFINITION 3.2. g is a k-emulation of f if and only if every set of
binary k-inequalities that has a solution in g with all g evaluations
nonzero, has a solution in f with all f evaluations nonzero.

DEFINITION 3.3. We say that g is a factorial optimal k-emulation of f
if and only if g is an emulation of f with no k-emulation of f
properly extending g on the support of g, by a triple from the <= k
sums of <=k length g products of factorials. We say that g is an
optimal continuation of f if and only if g is a continuation of f
where no emulation of f properly extends g on the support of g.

DEFINITION 3.4. We say that g is a factorial step optimal k-emulation
of f if and only if each g|<=i! is a step optimal k-emulation of
f|<=i!.

THEOREM 3.1. Every f:{0,...,n!}^2 into {0,...,n!} has a factorial
optimal k-emulation. Every ff;{0,...,n!}^2 into {0,...,n!} has a
factorial step optimal k-emulation.

PROPOSITION 3.2. Every f:{0,...,n!}^2 into {0,...,n!} has a factorial
optimal k-emulation without the value (8k)!!-1.

PROPOSITION 3.3. Every f;{0,...,n!}^2 into {0,...,n!} has a factorial
step optimal k-emulation without the value (8k)!!-1.

Note that Propositions 3.2, 3.3 are explicitly Pi01.

THEOREM 3.4. Propositions 3.2, 3.3  are provably equivalent to
Con(SMAH) over ACA.

Here SMAH is ZFC + {there exists a strongly k-Mahlo cardinals}_k.

4. TEMPLATES

The punch line in Propositions 2.3 - 2.8

min(1,g(1,...,k)) = min(1,g(2,...,k+1)).

is an equation involving min, k-ary g, and rational constants. There
is no nesting of g. This suggests the following Templates.

TEMPLATE 3.1. Let alpha be a finite set of unnested equations
involving min, max, k-ary function g, and constants from Q.  Every
f:Q^k into Q (with finite support) has a step optimal emulation g
satisfying alpha.

TEMPLATE 3.2. Let alpha be a finite set of unnested equations
involving min, max, k-ary function g, and constants from Q.  Every
f:Q^k|<=k+1 into Q|<=k+1 (with finite support) has an optimal
emulation g satisfying alpha.

There are also entirely analogous Templates 3,3, 3.4 for continuations
rather than emulations.

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

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

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

I don't anticipate much difficulties in establishing this conjecture
given the simplicity of the punch line.

In section 2, we discussed the modified punch line G(1,...,k,p) <=
G(2,...,k+1,p), p < 1. This provides material at various levels of
ambitiousness for more Templates.

Most ambitious of all, directly along these lines, is the obvious
Template that uses any quantifier free sentence in G, <, rational
constants, and universally quantified parameters over Q (or Q|<=k+1),
allowing nesting of G's. We conjecture that every instance of this
Template is provable in WKL_0 + Con(SRP) or refutable in RCA_0.

**********************************************************
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 623rd 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
611: Function Emulation/Continuation Theory 2  9/8/15  12:58AM
612: Binary Operation Emulation and Continuation 1  9/7/15  4:35PM
613: Optimal Function Theory 1  9/13/15  11:30AM
614: Adventures in Formalization 1  9/14/15  1:43PM
615: Adventures in Formalization 2  9/14/15  1:44PM
616: Adventures in Formalization 3  9/14/15  1:45PM
617: Removing Connectives 1  9/115/15  7:47AM
618: Adventures in Formalization 4  9/15/15  3:07PM
619: Nonstandardism 1  9/17/15  9:57AM
620: Nonstandardism 2  9/18/15  2:12AM
621: Adventures in Formalization  5  9/18/15  12:54PM
622: Adventures in Formalization 6  9/29/15  3:33AM

Harvey Friedman