FOM: 13:Min recursion/Provably recursive functions

[Harvey Friedman]

This is the 13th in a series of positive self contained postings to fom
covering a wide range of topics in f.o.m. Previous ones are:

1:Foundational Completeness   11/3/97, 10:13AM, 10:26AM.
2:Axioms  11/6/97.
3:Simplicity  11/14/97 10:10AM.
4:Simplicity  11/14/97  4:25PM
5:Constructions  11/15/97  5:24PM
6:Undefinability/Nonstandard Models   11/16/97  12:04AM
7.Undefinability/Nonstandard Models   11/17/97  12:31AM
8.Schemes 11/17/97    12:30AM
9:Nonstandard Arithmetic 11/18/97  11:53AM
10:Pathology   12/8/97   12:37AM
11:F.O.M. & Math Logic  12/14/97 5:47AM
12:Finite trees/large cardinals  3/11/98  11:36AM

A complete archiving of fom, message by message, is available at
http://www.math.psu.edu/simpson/fom/index.html
Also, my series of positive postings (only) is archived at
http://www.math.ohio-state.edu/foundations/manuscripts.html

This is a copy of an e-mail of mine dated 2:59PM 4/23/97 (predates the fom)
in which I make a number of claims concerning natural characterizations of
the provably recursive functions and ordinals of set theory. Natural here
has a more liberal interpretation than "natural discrete/finite
independence results." Here recursions are allowed such as Kleene's
primitive recursion or Godel's primitive recursion in finite types.


4/23/97
Dear Colleagues,

A longstanding primary goal of proof theory - arguably the primary goal -
has been the "natural" characterization of the provably recursive functions
and ordinals of standard formal systems, starting with the classical case
of Peano Arithmetic, solved by Gentzen (and also by Godel with his
Dialectica interpretation). The most common approach has been through
ordinal notation systems, and less commonly, functional interpretations.

The ordinal notation systems used for this purpose have been getting
steadily more complicated - perhaps too complicated to be fully
satisfactory. Also functional interpretations have their own serious
complications, particularly in terms of their relation to standard
mathematical constructions; consider Spector's Bar Recursion for second
order arithemetic.

The approach here goes all the way through ZFC with certain large cardinal
axioms, and promises to work for all large cardinal axioms proposed; i.e.,
for the various elementary embedding axioms. We anticipate very manageable
increases in complexity as one goes through the higher large cardinal
axioms.

Our approach is closer in spirit to the functional interpretations as
opposed to the ordinal notation approach. We expect, however, to give later
versions that are somewhat closer in spirit to the ordinal notation
approaches as well; but we don't know, as of yet, how to subsume the known
work via ordinal notations into this work.

This approach is, however, much simpler than the functional
interpretations - even Godel's Dialectica interpretation for Peano
Arithmetic. Everything takes place at the lowest possible type, so there
are no functionals of higher type. The basic idea is to exploit partial
solutions to recursion equations with the min operator (min recursion).
Concentrating on the total solutions gets one absolutely nowhere.

This work is closely related to my work on "finite independence results."
There we concentrated on avoiding recursion schemes and the like at all
costs, even though the schemes used here are totally natural for logicians
and theoretical computer scientists. The current "finite independence
results" are formulated in the context of operators on finite functions;
one studies Ramsey properties of their fixed points.

There are a number of additional delicate technical constructions involved
here that are not present in the work on "finite independence results" and
vice versa. And much could go wrong.

There are a lot of details to be checked, and there will have to be
probably another 100 plus page paper on this, with lots of constructions
involving non omega models of set theory of new kinds. So treat this as a
very tentative report.

As will become clear, this is a place where proof theory, set theory,
model theory, and recursion theory all meet in a serious way.

The probability that this is going to work as I outline is sufficiently
high for me to tell you about it. I am mainly interested in feedback at
this point, particularly from proof theorists.

MIN RECURSION AND THE PROVABLY RECURSIVE FUNCTIONS AND ORDINALS OF SET
THEORY I

April 23, 1997

We say that a subset R of N^r is basic if and only if it is definable by a
quantifier free formula over the structure (N,<) with parameters allowed.

A min recursion of type (k,p,q) is a formal equation of the form

F(x) = min{y <= x: (therexists z)(therexists w_1,...,w_q < x)
(R(x,y,z,w_1,...,w_q,F(w_1),...,F(w_q)))},

where R is any basic subset of N^k+k+p+qk+qk.

It is often convenient to identify this min recursion with the relation R.

We shall see that the study of solutions in the integers to such discrete
functional equations is intimately tied up with large cardinals. It turns
out that basic structural facts about solutions in the integers cannot be
established without using large cardinals.

We now wish to interpret the above discrete functional equation. We need
to use the following conventions:

        i) < indicates the usual lexicographic ordering on N^k;
        ii) min refers to the usual lexicographic ordering on N^k;
        iii) if the min is over the empty set then the value is the zero
vector in N^k;
        iv) x,y,w_1,...,w_q each range over N^k;
        v) z ranges over N^p.

First observe that there is exactly one F:N^k into N^k such that the
equation holds for all x in N^k. This is proved by induction on the
lexicographic ordering. We call this the standard solution to R.

Let A be a subset of N^k. Observe that there is still exactly one f:A into
N^k obeying the equation for all x in A, subject to the five conventions.
Here we could take the w_i to range over A and have the same effect.

We define the solutions to the min recursion R to be the functions f:A
into A obeying the equation for all x in A, subject to the five
conventions.

Note that we are requiring that the range be contained in the domain in
order to be a genuine solution. In general, it will not be the case that
for every A contained in N^k, there is a solution f:A into A.

If f:A into A is a solution to the min recursion R, then f is the standard
solution if and only if A = N^k. Every solution other than the standard
solution is called a nonstandard solution.

Fix k >= 1, A contained in N^k, and f:A into A.

We say that A is large if and only if A contains an infinite Cartesian
power. We say that f is large if and only if A is large.

We say that f:A into A is of order n if and only if n is the least integer
>= 1 such that the n-th iterate of f is identical to the (n+1)-st iterate
of f. We say that f is of finite order if and only if for some n >= 1, f is
of order n.

We say that f:A into A is (elementary) recursive if and only if there is
an (elementary) algorithm such that for all x in N^k,

        i) if x is in A then the algorithm returns f(x);
        ii) if x is not in A then the algorithm returns "undefined".

The following result demonstrates the relationship with large cardinals.
Let MAH be the following system of set theory: ZFC + {there exists a
k-Mahlo cardinal}_k.

THEOREM 1. The following are provably equivalent in RCA_0.
        i) every min recursion has a large nonstandard solution;
        ii) every min recursion has a large solution which is not onto;
        iii) every min recursion has a large solution of finite order;
        iv) every min recursion has a large (elementary) recursive solution;
        v) every min recursion has a nonstandard (elementary) recursive
solution of finite order whose domain contains the appropriate Cartesian
power of the powers of 2;
        vi) MAH is 1-consistent.

Note that iv) and v) are purely arithmetic assertions, and so constitute
arithmetic sentences that are independent of ZFC. The equivalence of
iv),v), and vi) is provable in EFA (elementary function arithmetic).

We now want to use standard solutions to min recursions in order to
characterize the provably recursive functions of MAH. We cannot do this
directly; the standard solutions to min recursions are recursive in the
levels of the hyperarithmetic hierarchy below the ordinal omega^omega, and
this is best possible. I.e., for each ordinal alpha < omega^omega, there is
a min recursion whose standard solution is complete in the alpha-th Turing
jump.

We have discovered a stability condition on min recursions which
guarantees that the standard solution is a provably recursive function of
MAH. In fact, the provably recursive functions of MAH are characterized as
the standard solutions of min recursions which are suitably stable. Here
are the details.

For t >= 1, we use [t] for {0,...,t-1}.

Let A be a subset of some Cartesian power of N. We say that A is t-large
if and only if there is an infinite E contained in N and t >= 1 such that
(E union [t])^k is contained in A. We say that f:A into A is t-large if and
only if A is t-large.

Let R be a min recursion and t >= 1. A t-large solution to R is a solution
to R whose domain is t-large.

We say that R is t-stable if and only if all t-large solutions to R agree
on [t]^k.

We say that R is stable if and only if R is t-stable for all t >= 1.

A provably recursive function of a formal system (in which arithemetic can
be suitably formalized) is a function f:N^s into N^t which is computable by
a Turing machine TM such that the sentence

TM defines a function from N^s into N^t

is provable in the system.

THEOREM 2. The provably recursive functions of MAH are exactly the
compositions of standard solutions to stable min recursions.

Here compositions include any definition by substitution, with constants
from N allowed.

It is possible to make this characterization somewhat more concrete as
follows.

We say that R is (elementary) recursively t-stable if and only if all
t-large recursive solutions to R agree on [t]^k.

We say that R is (elementary) recursively stable if and only if R is
(elementary) recursively t-stable for all t >= 1.

THEOREM 3. The provably recursive functions of MAH are exactly the
compositions of standard solutions to (elementary) recursively stable min
recursions.

We now give a simple characterization of the provably recursive ordinals
of MAH. The provably recursive ordinals of a suitable system T are the
order types of the recursive well orderings that have a correct recursive
presentation that is provably a well ordering within T.

It is more convenient in this case to give the characterization in terms
of a specific diagonal intersection. This diagonal intersection approach
can also be taken for the above characterization of the provably recursive
functions; we present this below. But for the provably recursive functions,
it seems most natural to bring in the concept of stability, and use the
standard solutions.

Let R be a min recursion and t >= 1. Let R*t be the binary relation S on
N^k given by x S y if and only if

for all nonstandard t-large solutions F of R, F(x) < F(y).

Finally, let R* be the union of all the R*t, t >= 1. We say that R* is the
core ordering of the min recursion R.

THEOREM 4. The following are provably equivalent in RCA_0.

        i) the core ordering of any min recursion is a well founded
transitive relation;
        ii) every pi-1-1 sentence provable in MAH is true.

THEOREM 5. The provably recursive ordinals of MAH are exactly the ordinals
of the core orderings of min recursions.

If we use only (elementary) recursive nonstandard t-large solutions in the
definition of the R*t, then we will get the same results.

We now present the diagonal intersection approach to the provably
recursive functions of MAH.

Let R be a min recursion of type (k,p,q) and let t >= 1. We define R't as
the intersection of all t-large solutions to R. We take R' to be the union
of the R't, t >= 1. R' is called the core function of the min recursion R.
Note that R' is a partial function.

THEOREM 6. The following are provably equivalent in RCA_0.
        i) for all min recursions R and t >= 1, R't is finite;
        ii) the core function of any min recursion is recursive;
        iii) MAH is 1-consistent.

THEOREM 7. The provably recursive functions of MAH are exactly the total
core functions of min recursions.

We can also use only (elementary) recursive t-large solutions in the
definition of R't and get the same results.

In a future installment, we will discuss finite forms of the above
results. We will mention one result, which gives an explicitly pi-0-2
independence result.

THEOREM 8. The following are provably equivalent in EFA.
        i) for all r,k,p,q >= 1, every min recursion of type (k,p,q) has a
solution f where {1,2,4,8,...,2^r}^k containedin dom(f) properlycontainedin
[0,2^r+1)^k;
        ii) MAH is 1-consistent.

We also plan to discuss how the power of the statements and constructions
can be weakened in order to capture subsystems of MAH ranging from
fragments of 2nd-order arithmetic through type theory through roughly ZFC,
etcetera.