FOM: 67:Nested Min Recursion/Large Cardinals

[Harvey Friedman]

This is the 67th in a series of 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
13:Min recursion/Provably recursive functions  3/20/98  4:45AM
14:New characterizations of the provable ordinals  4/8/98  2:09AM
14':Errata  4/8/98  9:48AM
15:Structural Independence results and provable ordinals  4/16/98
10:53PM
16:Logical Equations, etc.  4/17/98  1:25PM
16':Errata  4/28/98  10:28AM
17:Very Strong Borel statements  4/26/98  8:06PM
18:Binary Functions and Large Cardinals  4/30/98  12:03PM
19:Long Sequences  7/31/98  9:42AM
20:Proof Theoretic Degrees  8/2/98  9:37PM
21:Long Sequences/Update  10/13/98  3:18AM
22:Finite Trees/Impredicativity  10/20/98  10:13AM
23:Q-Systems and Proof Theoretic Ordinals  11/6/98  3:01AM
24:Predicatively Unfeasible Integers  11/10/98  10:44PM
25:Long Walks  11/16/98  7:05AM
26:Optimized functions/Large Cardinals  1/13/99  12:53PM
27:Finite Trees/Impredicativity:Sketches  1/13/99  12:54PM
28:Optimized Functions/Large Cardinals:more  1/27/99  4:37AM
28':Restatement  1/28/99  5:49AM
29:Large Cardinals/where are we? I  2/22/99  6:11AM
30:Large Cardinals/where are we? II  2/23/99  6:15AM
31:First Free Sets/Large Cardinals  2/27/99  1:43AM
32:Greedy Constructions/Large Cardinals  3/2/99  11:21PM
33:A Variant  3/4/99  1:52PM
34:Walks in N^k  3/7/99  1:43PM
35:Special AE Sentences  3/18/99  4:56AM
35':Restatement  3/21/99  2:20PM
36:Adjacent Ramsey Theory  3/23/99  1:00AM
37:Adjacent Ramsey Theory/more  5:45AM  3/25/99
38:Existential Properties of Numerical Functions  3/26/99  2:21PM
39:Large Cardinals/synthesis  4/7/99  11:43AM
40:Enormous Integers in Algebraic Geometry  5/17/99 11:07AM
41:Strong Philosophical Indiscernibles
42:Mythical Trees  5/25/99  5:11PM
43:More Enormous Integers/AlgGeom  5/25/99  6:00PM
44:Indiscernible Primes  5/27/99  12:53 PM
45:Result #1/Program A  7/14/99  11:07AM
46:Tamism  7/14/99  11:25AM
47:Subalgebras/Reverse Math  7/14/99  11:36AM
48:Continuous Embeddings/Reverse Mathematics  7/15/99  12:24PM
49:Ulm Theory/Reverse Mathematics  7/17/99  3:21PM
50:Enormous Integers/Number Theory  7/17/99  11:39PN
51:Enormous Integers/Plane Geometry  7/18/99  3:16PM
52:Cardinals and Cones  7/18/99  3:33PM
53:Free Sets/Reverse Math  7/19/99  2:11PM
54:Recursion Theory/Dynamics 7/22/99 9:28PM
55:Term Rewriting/Proof Theory 8/27/99 3:00PM
56:Consistency of Algebra/Geometry  8/27/99  3:01PM
57:Fixpoints/Summation/Large Cardinals  9/10/99  3:47AM
57':Restatement  9/11/99  7:06AM
58:Program A/Conjectures  9/12/99  1:03AM
59:Restricted summation:Pi-0-1 sentences  9/17/99  10:41AM
60:Program A/Results  9/17/99  1:32PM
61:Finitist proofs of conservation  9/29/99  11:52AM
62:Approximate fixed points revisited  10/11/99  1:35AM
63:Disjoint Covers/Large Cardinals  10/11/99  1:36AM
64:Finite Posets/Large Cardinals  10/11/99  1:37AM
65:Simplicity of Axioms/Conjectures  10/19/99  9:54AM
66:PA/an approach  10/21/99  8:02PM

In postings #13, 14, 14', we discussed unnested min recursion. Whereas
unnested min recursion is arguably simpler in some respects than nested min
recursion, the latter is more general and is arguably more natural. Also,
the strength of nested min recursion is easier to establish.

As far as the general mathematical logic community is concerned (not the
general mathematics community) nested min recursion is now my favorite
choice of context for discrete/finite independence results, as well as the
context for lifting such results to the higher large cardinals.

This posting concerns only results at the levels of Mahlo and suble
cardinals. Subsequent postings will involve cardinals that are incompatible
with the axiom of constructibility such as measurable cardinals and beyond.

NESTED MIN RECURSION/MAHLO CARDINALS

1. Preliminaries.

Let N be the set of all nonnegative integers.

For each k >= 1, we will use the k-ary elementary terms. These are the
terms with IF THEN ELSE, the usual < on N, constants from N, variables
x_1,x_2,... ranging over N, and the k-ary function symbol F.

It is obvious how to evaluate the k-ary elementary terms if elements of N
are assigned to the variables, and a function from N^k into N is assigned
to F.

We need to consider the evaluation of k-ary elementary terms where F:N^k
into N is a partial function. We choose the most natural mode of
evaluation, where in the course of evaluating the term, we come across F at
a k-tuple that does not lie in the domain of F, then the k-ary elementary
term is undefined.

For the sake of completeness, we give the inductive definition as follows.
We let Val(t) be the value of t, which lies in N union {infinity}. Here
infinity indicates undefinedness.

Val(x_i) is the value assigned to x_i.

If (Val(t_1),...,Val(t_k)) in dom(F) then Val(F(t_1,...,t_k)) =
F(Val(t_1,...,t_k)). Otherwise, Val(F(t_1,...,t_k)) = infinity.

If Val(s) < Val(t) < infinity then Val(IF s < t THEN r ELSE u) = Val(r).

If Val(t) <= Val(s) < infinity then Val(IF s < t THEN r ELSE u) = Val(u).

If Val(s) or Val(t) = infinity then Val(IF s < t THEN r ELSE u) = infinity.

A formal nested min recursion NMR is an equation of the form

F(x_1,...,x_k) = min t

where x_1,...,x_k are the first k variables, and t is a k-ary elementary
term term.

Intuitively, this equation means that F(x_1,...,x_k) is the least value of
t. If t mentions variables other than x_1,...,x_k, then generally there
will be many values of t to consider when taking the min.

The arity of NMR is k.

We now must discuss what we mean by a standard solution to NMR. This is a
function F:N^k into N such that the equation holds in the following sense.
Let x_1,...,x_k in N. Then F(x_1,...,x_k) is the least value of t, where
all variables in t other than x_1,...,x_k are allowed to range over N, and
where every occurrence of F in t is interpreted as the function
F/x_1,...,x_k:N^k into N, where

F/x_1,...,x_k(y_1,...,y_k) = F(y_1,...,y_k) if (y_1,...,y_k) <lex
(x_1,...,x_k); 0 otherwise.

Here <lex is the lexicographic ordering on N^k.

THEOREM 1.1. There is a unique standard solution to NMR.

The absolutely crucial key point in min recursion is the consideration of
solutions to NMR whose domain may not be all of N^k.

A solution to the NMR

F(x_1,...,x_k) = min t

is a partial function F:N^k into N such that the equation holds in the
following sense. Let (x_1,...,x_k) in dom(F). Then F(x_1,...,x_k) is the
least value of t, where all variables in t other than x_1,...,x_k are
allowed to range over N, and where every occurrence of F in t is
interpreted as the function F/x_1,...,x_k:dom(F) into N, where

F/x_1,...,x_k(y_1,...,y_k) = F(y_1,...,y_k) if (y_1,...,y_k) <lex
(x_1,...,x_k); 0 otherwise.

Note that for many values of the variables in t other than x_1,...,x_k, the
term t may be undefined, making no contribution to the min.

If the min is empty, then F(x_1,...,x_k) is considered undefined. Thus if F
is a solution to NMR then all associated min's are nonempty.

A large solution to NMR is a solution whose domain contains E^k for some
infinite E containedin N.

2. Large solutions to nested min recursions on omega.

PROPOSITION 2.1. Every nested min recursion has a large solution which is
not surjective.

PROPOSITION 2.2. The intersection of all large solutions to any given
nested min recursion is finite.

PROPOSITION 2.3. The intersection of all domains of large solutions to any
given nested min recursion is finite. The intersection of all ranges of
large solutions to any given nested min recursion is finite.

Let MAH = ZFC + {there exists an n-Mahlo cardinal}_n.

THEOREM 2.4. All parts of Propositions 2.1 - 2.3 are equivalent to the
1-consistency of MAH over RCA_0.

We can define three natural maps from nested min recursions into finite
sets as follows. #1(NMR) is the intersection of all large solutions to NMR.
#2(NMR) is the intersection of all domains of large solutions to NMR.
#3(NMR) is the intersection of all ranges of large solutions to NMR.

THEOREM 2.5. The functions #i, 1 <= i <= 3, are each bounded by a provably
recursive function of MAH + 1-Con(MAH) but not by any provably recursive
function of MAH.

We can characterize the provably recursive functions of MAH as follows.
Write n*k for the k-tuple whose coordinates are all k.

Let NMR be of arity k. For n in N, define NMR[n] to be the unique f(n*k)
such that f is a solution to NMR whose domain contains (E union [0,n])^k
for some infinite E containedin N, if there is such a unique integer;
undefined otherwise. Note that NMR[n] defines a partial function from N
into N which may or may not be total.

THEOREM 2.6. The provably recursive functions of MAH are exactly the total
functions NMR[n].

3. The proof theoretic ordinal of MAH.

Let T be a system containing RCA_0. The proof theoretic ordinal of T
(written ord(T)) is the sup of all ordinals alpha such that there exists a
partial recursive index e for which

i) phi_e is a well ordering of omega of order type alpha;
ii) T proves that phi_e is a well ordering of omega.

If every Pi-1-1 sentence provable in T is true, then ord(T) is a recursive
ordinal. This hypothesis is called Pi-1-1 reflection on T.

Let NMR_1 and NMR_2 be nested min recursions of arity k. We write NMR_1 >*
NMR_2 if and only if for all f,g, if f,g are, respectively, large
nonsurjective solutions to NMR_1,NMR_2 with the same domain, then f(1*k) >
g(1*k).

There are some alternative definitions of >* that may be more natural from
some points of view. Here are a few:

i) f > g at every tuple all of whose coordinates are nonzero;
ii) for all n >= 1, f(n*k) > g(n*k);
iii) for all sufficiently large n, f(n*k) > g(n*k).

The results will be the same.

It appears that >* is not transitive and is complete Pi-1-1. Nevertheless,
we can work with it to designate a large proof theoretic ordinal.

Let MAH' = ZFC + for all n there exists an n-Mahlo cardinal.

THEOREM 3.1. The following are provable in MAH'. There is no infinite
forward chain in >*.

If R is any relation with no infinite forward chains then we can assign
ordinals to elements of the field of R as follows. The ordinal assigned to
x in fld(R) is the least ordinal greater than all ordinals assigned to y
such that x R y. We define ord(R) to be the least ordinal not assigned to
any element of fld(R).

THEOREM 3.2. ord(MAH) < ord(>*) < ord(MAH').

To hit ord(MAH) on the button, we define the subrelations >*k, k >= 1, on
the nested min recursions of arity k.

THEOREM 3.3. ord(MAH) is the union over k of ord(>*k).

Where are the elementary recursive well orderings that proof theorists are
used to?

THEOREM 3.4. Assume Pi-1-1 reflection holds for MAH. There is a restriction
of >* to an elementary recursive set which is an elementary recursive well
ordering
of type ord(MAH). There are restrictions of the >*k to elementary recursive
sets which are elementary recursive well orderings of types approaching
ord(MAH).

One might want to pull these elementary recursive well orderings out
naturally. This is hopeful.

4. Concrete infinite solutions.

Assuming 1-Con(MAH), it can be shown that there are continuumly many large
solutions to any nested min recursion. Here we consider relatively concrete
large  solutions. This leads to arithmetic sentences that are independent
of MAH without considering combinatorial properties of finite solutions.

We can look at

i) arithemtical solutions. I.e., the graph of the function is an
arithmetical set.
ii) partial recursive solutions.
iii) recursive solutions. I.e., the function is partial recursive and the
domain is a recursive set.
iv) elementary recursive solutions. I.e., the extension of the function
with 0 off of its domain is an elementary recursive function.
v) polynomial time solutions. I.e., the extension of the function with 0
off of its domain is a polynomial time computable function using base 2
representations of integers.

PROPOSITION 4.1. Every nested min recursion has a large arithmetical
solution. In fact, it has a polynomial time computable solution defined at
every tuple of powers of 2.

PROPOSITION 4.2. The intersection of all large arithmetical solutions to
any given nested min recursion is finite. The intersection of all domains
of polynomial time computable solutions defined at every tuple of powers of
2 to any given nested min recursion is finite.

PROPOSITION 4.3. The intersection of all ranges of large arithmetical
solutions to any given nested min recursion is finite. The intersection of
all ranges of polynomial time computable solutions defined at every tuple
of powers of 2 to any given nested min recursion is finite.

Let MAH = ZFC + {there exists an n-Mahlo cardinal}_n.

THEOREM 4.4. All parts of Propositions 4.1 - 4.3 are equivalent to the
1-consistency of MAH over RCA_0.

The remaining results in sections 2 and 3 can be modified in this way with
the same results.

5. Finite solutions.

For A containedin N and r in N, define S_r(A) to be the set of all length r
sums from A with repetitions allowed. A length 0 sum is 0.

First we start with an infinite form. We call this "local summation".

PROPOSITION 5.1. Every k-ary nested min recursion has a solution F such
that for some r in N,

F(x_1,...,x_k) in S_r({x_1,...,x_k,0,1})

holds for all x_1,...,x_k drawn from some infinite subset of N.

The cleanest finite form that we know is independent of ZFC is as follows.

PROPOSITION 5.2. Every k-ary nested min recursion has a finite solution F
such that for some r > k,

F(x_1,...,x_k) in S_r({x_1,...,x_k,0,1})

holds for all x_1,...,x_k drawn from some r^2r element subset of N.

The full finite form is as follows.

PROPOSITION 5.3. Every k-ary nested min recursion has a finite solution F
such that for some r > k,

F(x_1,...,x_k) in S_r({x_1,...,x_k,0,1})

holds for all x_1,...,x_k drawn from some E*(2r) element subset of N.

Here E*(2r) is an exponential stack of 2's of height 2r. No effort has been
made to tighten the crude number E*(2r).

If any function is used in place of E*(2r) then the Proposition will follow
from Proposition 5.3. In fact, the strongest finite form along these lines
of Proposition 5.1 is as follows.

PROPOSITION 5.4. For all k-ary nested min recursions NMR there exists r
such that the following holds. For every p there exists a finite solution F
of NMR such that

F(x_1,...,x_k) in S_r({x_1,...,x_k,0,1})

holds for all x_1,...,x_k drawn from some p element subset of N.

Note that Propositions 5.2 and 5.3 are in Pi-0-2 form, whereas Proposition
5.4 is in Pi-0-4 form. Let SUB = ZFC + {there exists an n-subtle
cardinal}_n.

THEOREM 5.5. Propositions 5.1, 5.3, 5.4 are provably equivalent to
1-Con(SUB) over RCA_0. EFA is sufficient for 5.3 and 5.4.

THEOREM 5.6. Proposition 5.2 is provable in ZFC + {there exists an almost
ineffable cardinal} and implies the 1-consistency of ZFC + {there exists a
subtle cardinal}, over EFA.

We can easily extract rates of growth from Propositions 5.3 associated with
SUB, and Proposition 5.2 associated with the theories of a subtle and
almost ineffable cardinal.

6. An alternative for Mahlo cardinals; arithmetical recursion.

PROPOSITION 6.1. Every k-ary nested min recursion has a solution F such that

F(x_1,...,x_k) not= x_1 - 1,...,x_k - 1

holds for all x_1,...,x_k drawn from some infinite subset of N.

THEOREM 6.2. Proposition 6.1 is provably equivalent to 1-Con(MAH) over RCA_0.

The most obvious finite form is much weaker.

PROPOSITION 6.3. For all r >= 1, every k-ary nested min recursion has a
finite solution F such that

F(x_1,...,x_k) not= x_1 - 1,...,x_k - 1

holds for all x_1,...,x_k drawn from some r element subset of N.

Let ATR(<omega^omega) be ACA_0 + {the Kleene H-set on omega^k exists}_k. We
could define this with parameters, but it would have the same arithmetical
theorems.

THEOREM 6.4. Proposition 6.3 is provably equivalent to the 1-consistency of
ATR(<omega^omega) over EFA.

7. Type theory.

The logarithmic index of n in N is the number of times the base 2 logarithm
function can be applied to n.

THEOREJM 7.1. Every k-ary nested min recursion has a finite solution which
is defined on all k-tuples drawn from a set whose cardinality has
logarithmic index lying outside the range.

Note that this is an explicitly Pi-0-2 statement.

THEOREM 7.2. Theorem 7.1 is provably equivalent to the 1-consistency of
type theory over EFA.

We can easily extract rates of growth from Proposition 7.1 associated with
type theory.