FOM: 38:Existential Properties of Numerical Functions

[Harvey Friedman]

This is the 38th 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

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

FAVORITE SELF CONTAINED POSTINGS: 21, 25, 27, 31, 32, 34, 35', 37, 38.

EXISTENTIAL PROPERTIES OF NUMERICAL FUNCTIONS
by
Harvey M. Friedman
March 26, 1999

Here we view ordinary Ramsey theory as the theory of existential properties
of numerical functions with finite range. Under this point of view, exotic
Ramsey theory is the theory of existential properties of numerical
functions with arbitrary range. Exotic Ramsey theory is connected with
epsilon_0, Peano Arithmetic, and fast growing functions
(<epsilon_0-recursive functions).

1. Ordinary Ramsey theory and existential properties.
2. Exotic Ramsey theory and existential properties.
3. Powers of 2.

1. ORDINARY RAMSEY THEORY AND EXISTENTIAL PROPERTIES

We consider all statements of the form

1) (for all F:Z+^k into [1,r])(there exists distinct x_1,...,x_n in Z+)(s_1
= t_1 & ... & s_m = t_m),

where k,r are positive integers and each s_i,t_i is an expression of the
form F(y_1,...,y_k), where the y's are among the variables x_1,...,x_n.

EXAMPLE: (for all F:Z+^2 into [1,5])(there exists distinct
x_1,x_2,x_3)(F(x_1,x_2) = F(x_1,x_3) & F(x_1,x_2) = F(x_2,x_3)). This is
true, and is an easy consequence of Ramsey's theorem for pairs with five
colors and a homogeneous set of size 3.

THEOREM 1.1. (dichotomy). Any sentence of form 1) is either true or has a
counterexample which is definable by IF THEN ELSE, <, and constants. The
problem of determining whether a sentence of form 1) is true is in
nondeterministic exponential time.

In fact, we consider the following larger class of sentences:

2) (for all F_1,...,F_p:Z+^k into [1,r])(there exists x_1,...,x_n in Z+)(phi),

where p,k,r in Z+, and phi is a quantifier free formula involving
F_1,...,F_p,x_1,...,x_n,<,=, and constants. I.e., phi involves
F_1,...,F_p,x_1,...,x_n,<,=, constants, and the connectives: and, or, not,
if then.

THEOREM 1.2. (dichotomy). Any sentence of form 2) is either true or has a
counterexample which is definable by IF THEN ELSE,<, and constants. The
problem of determining whether a sentence of form 1) is true is
nondeterministic exponential time complete.

It is obvious by compactness that any true sentence phi of type 1) or 2) is
strongly true in the sense that there is a positive integer #(phi) such
that phi remains true if we replace

x_1,...,x_n in Z+

by

1 <= x_1,...,x_n <= #(phi).

Henceforth, we let #(phi) be the least such integer. If phi is false, we
take #(phi) = infinity.

THEOREM 1.3. The problem of determining whether #(phi) = #(psi) holds for
sentences phi,psi of form 2) is complete for iterated exponential time. The
same is true for determining #(phi) < #(psi).

2. EXOTIC RAMSEY THEORY AND EXISTENTIAL PROPERTIES

As a starting point, we consider 1) with range Z+:

3) (for all F:Z+^k into Z+)(there exists distinct x_1,...,x_n in Z+)(s_1 =
t_1 & ... & s_m = t_m),

where k in Z+ and each s_i,t_i is an expression of the form F(y_1,...,y_k),
where the y's are among the variables x_1,...,x_n. It is easy to see that
these sentences have essentially no content:

THEOREM 2.1. A sentence in form 3) is true if and only if for all 1 <= i <=
m, s_i is identical to t_i.

However, consider this:

4) (for all F:Z+^k into Z+)(there exists x_1 < ... < x_n from Z+)(s_1 <=
t_1 & ... & s_m <= t_m),

where k in Z+ and each s_i,t_i is an expression of the form F(y_1,...,y_k),
where the y's are among the variables x_1,...,x_n.

THEOREM 2.2. (dichotomy). Any sentence of form 4) is either true or has a
counterexample which is definable by IF THEN ELSE,-,<, and constants. This
"dichotomy for 4)" is provably equivalent to "epsilon_0 is well ordered"
within RCA_0. There is a log/lin decision procedure for determining whether
any sentence of form 4) is true.

We also consider the following larger class of sentences, analogously to 2):

5) (for all F_1,...,F_p:Z+^k into Z+)(there exists x_1,...,x_n in Z+)(phi),

where p,k_1,...,k_p,r_1,...,r_p,n in Z+, and phi is a quantifier free
formula involving only F_1,...,F_p,x_1,...,x_n,<,=, and constants. But the
following is well known:

THEOREM 2.3. The set of true sentences of the form 5) is recursively
undecidable, even if < does not appear.

In order to obtain decidability, we need to put a natural restriction on
the atomic subformulas of phi:

6) (for all F_1,...,F_p:Z+^k into Z+)(there exists x_1,...,x_n in Z+)(phi),

where p,k,n in Z+, and phi is a quantifier free formula all of whose atomic
subformulas are of the form x_i < x_j, or F_i(y_1,...,y_k) <
F_j(z_1,...,z_k), where the y's and z's are among the variables
x_1,...,x_n.

Note that this condition on phi amounts to nothing more or lee than
treating the domain and range of the functions as separate sorts (whose
elements cannot be compared).

THEOREM 2.4. (dichotomy). Any sentence of form 6) is either true or has a
counterexample which is definable by IF THEN ELSE,-,<, and constants. This
"dichotomy for 6)" is provably equivalent to "epsilon_0 is well ordered"
within RCA_0.  The problem of determining whether a sentence of form 6) is
true is  nondeterministic exponential time complete.

We now wish to develop the theory of #(phi) as in section 1. In section 1,
the spaces of functions considered are all compact, and so #(phi) exists if
and only if phi is true. Here the relevant spaces of functions are not
compact; in fact, there are simple examples of true phi in class 6) for
which #(phi) does not exist.

Thus we say that a function F:Z+^k into Z+ is limited if and only if for
all x in Z+^k, F(x) <= max(x). Note that this set of functions is compact.

7) (for all limited F:Z+^k into Z+)(there exists x_1 < ... < x_n from
Z+)(s_1 <= t_1 & ... & s_m <= t_m),

where k in Z+ and each s_i,t_i is an expression of the form F(y_1,...,y_k),
where the y's are among the variables x_1,...,x_n.

8) (for all limited F_1,...,F_p:Z+^k into Z+)(there exists x_1,...,x_n in
Z+)(phi),

where p,k,n in Z+, and phi is a quantifier free formula all of whose atomic
subformulas are of the form x_i < x_j, or F_i(y_1,...,y_k) <
F_j(z_1,...,z_k), where the y's and z's are among the variables
x_1,...,x_n.

It is clear by compactness that for any phi of form 7) or 8), #(phi) is
finite if and only if phi is true.

THEOREM 2.5. The following are provably equivalent in RCA_0:
i) dichotomy for 7);
ii) dichotomy for 8);
iii) PA is 1-consistent.
In addition, the problem of determining whether a sentence in 8) is true is
nondeterministic exponential time complete.

THEOREM 2.6. #(phi) for phi in 7) or for phi in 8) are not <epsilon_0
recursive but are epsilon_0 recursive. In fact, they strictly dominate
every <epsilon_0 recursive function at infinitely many arguments whose
value is finite.

THEOREM 2.7. The problem of determining whether #(phi) = #(psi) for
sentences phi,psi of form 8) is complete for level epsilon_0 time. The same
is true for determining #(phi) < #(psi).

3. POWERS OF 2

There is another way of avoiding the undecidability of 5). Let P be the
powers of 2; i.e., {2^n:n in Z+}. We can use any reasonable sufficiently
thin subset of Z+, but we stick to P to simplify the discussion.

9) (for all F_1,...,F_p:Z+^k into Z+)(there exists x_1,...,x_n in P)(phi),

where p,k,n in Z+, and phi is a quantifier free formula involving
x_1,...,x_n,F_1,...,F_p.

So in 9), we don't treat the domain and range as separate sorts.

10) (for all limited F_1,...,F_p:Z+^k into Z+)(there exists x_1,...,x_n in
P)(phi),

where p,k,n in Z+, and phi is a quantifier free formula involving
x_1,...,x_n,F_1,...,F_p.

THEOREM 3.1. In RCA_0, dichotomy for 9) is provably equivalent to
"epsilon_0 is well ordered" and dichotomy for 10) is provably equivalent to
the 1-consistency of PA. The problem of determining whether a sentence in
9) or 10) is true is nondeterministic exponential time complete.

THEOREM 3.2. The problem of determining whether #(phi) = #(psi) for
sentences phi,psi of form 10) is complete for level epsilon_0 time. The
same is true for determining #(phi) < #(psi).