[FOM] Arithmetic with Limited Exponentiation II

[Dmytro Taranovsky]

Part of foundations of mathematics is finding weak systems that capture 
much of mathematics -- and are convenient to work with.  A natural 
notion of weak is interpretable in IDelta_0, which is arithmetic with 
bounded quantifier induction.  Going below IDelta_0 under 
interpretability requires restricting first order logic (assuming that 
every number has a successor and addition and multiplication have a few 
basic properties), and conversely if first order logic is restricted to 
boolean combinations of Pi^0_k sentences, IDelta_0 does not have length 
n proof of existence of 2^2^...^n (k+5 2s).

Here, I will present and analyze a natural hierarchy of theories 
interpretable in IDelta_0.  It is surprising how much can be 
interpreted, including (new result) Weak Konig's Lemma.

Familiarity with my "Arithmetic with Limited Exponentiation" posting 
(Nov 21, 2015) is not required.  A good background can be found in 
"Interpretability in Robinson's Q" in the Bulletin of Symbolic Logic.


== The Theory and its Extensions ==

The theory will have 4 types:
* unary numbers, as in physical sizes; this type is used for convenience 
and intuitive appeal; n is unary iff 2^n exists as binary
* binary numbers, as in digital data; below, by numbers we will mean 
binary numbers
* functions: map numbers into numbers
* operators: map functions into functions.

Notes:
* Many Pi^0_2 number theory theorems will need to weakened as: For every 
unary number there is a binary number such that the bounded-quantifier 
relation holds.
* One can add additional types of numbers, such as small numbers (say n 
is small iff 2^n exists as unary), and additional types of operators, 
such as hyperoperators (mapping operators into operators).
* Because pairing will be codable, arity of functions and operators does 
not matter.
* Equality is primitive only for numbers. f=g means A.n f(n)=g(n), so 
f=g is not a bounded quantifier formula.
* The language is very expressive.  For example, under the 
set-theoretical interpretation, the Continuum Hypothesis is equivalent to
E.F A.f,g E.n F(n,f)=g or F(n,g)=f  (n is a natural number and f and g 
are functions)

Define mu(x<n:phi(x)) as the least number x<n such that phi(x) holds, 
and 0 if there is no such number.  E. and A. stand for existential and 
universal quantifier respectively.

Axioms:
1. Basic arithmetical axioms.  Include constants 0 and 1, and functions 
'+', '*', and x->x^len(x) (len is bit length; len(x) = floor(lg x)+1, 
except that len(0)=0).
2. Induction for bounded quantifier formulas.  Equivalently, A.f (A.n 
f(n)=f(n+1) ==> A.n f(n)=f(0)).
3. Bounded collection:  A.m E.n f(m,n)=1 ==> A.m E.n A.m'<m E.n'<n 
f(m',n')=1
4. Extensionality: F(f)(m) != F(g)(m) ==> E.n f(n) != g(n)
5. Bounded quantifier comprehension:
     a. functions: E.f f(x) = mu(y<T(x):phi(x,y))   (T is a term; T and 
phi do not use f)
     b. operators: E.F A.f F(f)(x) = mu(y<T(x):phi(x,y,f))   (T is a 
term; T and phi do not use F)
    where phi is a bounded quantifier formula
    - each numeric quantifier is in the form A.z<S or E.z<S where S is a 
term that does not use z.
    - each function quantifier is in the form 5a (i.e. one can use 
bounded minimization to define new functions).
    - each operator quantifier is in the form 5b.

Notes:
* Per convention, the axioms are open formulas that are assumed to be 
universally quantified.
* Bounded quantifier formulas appear very expressive:  They can use 
functions and operators, and have quantifiers of the form E.n<f(m) (and 
E.n<F(f)(m) and so on), and even use mu to get new functions as input to 
operators.
* To get a theory that corresponds to polynomial time computation, treat 
quantification over binary numbers as unbounded, limit comprehension to 
polynomial time comprehension, and change induction to induction over 
unary numbers on (relativized) NP predicates.
* Bounded collection (even for polynomial time relations) is not 
provable in PRA, even if extended with all true Pi^0_2 statements, but 
it is very useful for dealing with arbitrary recursive functions.
* If we used predicates instead of functions, and coded functions by 
predicates, then recursive comprehension would be necessary for basic 
things such as existence of {n: f(n)=0}.  By using functions directly, 
we avoid the need to include unlimited recursive comprehension to get a 
meaningful theory of functions.

Extensions:
6. Add (or assert existence of) SUM operator: SUM(f)(n) = sum(f(n): 0<=i<n).
7. More generally, treat quantification over P(n) (using functions) or 
P(P(n)) (using operators) as bounded, or otherwise allow a high 
computational complexity class in defining functions and operators. 
(Here, P stands for power set, and n is a number. A boolean function f 
codes an element of P(n) iff A.m>=n f(m)=0, and a boolean F codes an 
element of P(P(n)) iff F(f) depends on f only through {m<n:f(m)=0}.)
8. Allow quasipolynomial time functions: x->x^len(x)^len(len(x)).

For a fixed k (but not simultaneously for all k in N), we can even allow
Omega_k:  For all x, x^len(x)^...^len^k(x) exists, where len^k is k-fold 
iteration of len.
Function Omega_k:  x->x^len(x)^...^len^k(x) exists as a function.

The language and the theory can be extended with hyperoperators (and any 
fixed finite number of types) defined analogously to operators, and 
satisfying extensionality and bounded quantifier comprehension, and with 
one extension treating quantifiers over P(P(P(n))) as bounded.

Further Extensions:
9. Recursive Comprehension:  A.x E.y phi(x,y) ==> E.f A.x phi(x,f(x)) 
(bounded quantifier phi).
10. Weak Konig's Lemma (WKL):  Every infinite depth binary tree (coded 
by a boolean function) has an infinite path.

Note: Axioms 9 and 10 are extremely useful for mathematical analysis, 
but 9 breaks the relation between functions and bounded time 
computability, and 10 breaks the relation between functions and 
computability.  Also, I have not worked out recursive comprehension for 
operators, including the right definition, theory strength, and its 
relation with higher types, extensionality, and WKL.

Formula Expressiveness
A Pi_k sentence is a sentence of the type QX_1 QX_2 ... QX_k phi, where 
each Q is a quantifier (A. or E.), the first Q being A. (or E. for 
Sigma_k), each X_i is a tuple of variables, and phi is a bounded 
quantifier formula.
Under the set-theoretical interpretation, Pi_{k+1} formulas correspond 
to Pi^2_k formulas.  A Sigma^2_1 formula can be coded as E.F A.g phi 
where phi is bounded quantifier.  Conversely, (assuming comprehension) a 
Sigma_1 formula can be witnessed by an operator which is zero on all but 
a finite set of functions. Sigma_1 statements are essentially Sigma^0_1, 
and all true Sigma_1 statements are provable from the axioms 1-5 (even 
if phi may quantify over P(n) and P(P(n))).


== Real Numbers and Analysis ==

Reverse mathematics up to RCA_0 illuminated much of the structure of 
mathematical analysis.  Going further, and doing analysis without full 
recursive comprehension will illuminate which constructions use bounded 
versus unbounded time.  Studying weak theories also shows the complexity 
of certain constructions, such as the equivalence between (a) being able 
to do integration, (b) having SUM operator (axiom 6), and (c) having 
oracles for relativized PP problems.

Because of absence of exponentiation, there are two natural notions of 
real numbers, both of which satisfy real field axioms.  For every unary 
number t, ordinary real numbers are defined with 2^-t error, and 
approximate real numbers are defined with 1/t error.  They can can 
defined as follows.
* Ordinary real numbers:  Let (n,f) code n+sum(f(2^i)/2^i: i>0) where n 
is an integer and each f(2^i) is in {0,1,2}.
* Approximate real numbers:  Same as above, but n is a unary integer and 
use f(2^2^i) in place of f(2^i).
A function R->R may depend only the value of the real number, as opposed 
to an intensional function that may depend on the code.

Without recursive comprehension (and to a lesser extent, without WKL), 
classically equivalent notions become nonequivalent. Nevertheless, there 
is a notion of a continuous function on R^n that captures what we need 
(for axioms 1-5):
f is continuous iff there is a function g(x,r,delta) --> epsilon, such 
that |y-x|<r and |y-z|<epsilon ==> |f(y)-f(z)|<delta and for delta>0, 
epsilon>0.
In other words, f is uniformly continuous in every ball, and there is a 
function witnessing this.  This works because every closed bounded 
subset of R^n is compact; the base theory appears too weak to properly 
handle arbitrary separable metric spaces.

With this definition, every continuous function R^n->R^n can be coded by 
a numeric function (with the code also coding g), as opposed to an 
operator.  Using axioms 1-6, we can show that integration exists as an 
operator, and is linear and satisfies most of its basic properties; 
axiom 6 is not needed for approximate reals.

We can also do reverse mathematics.

Theorem (axioms 1-5):  Intermediate value theorem is equivalent to 
recursive comprehension for predicates.
Proof Sketch:  If the function has no rational zeros, use the 
constructive version (below) and wait until the interval becomes short 
enough before returning it.  Conversely, given a recursive function f, 
we can find a polynomial time function on reals with one zero, and that 
zero will code f.
Note:  In the base system, the complexity of a function is decoupled 
from its growth rate, so finding complex predicates does not prove 
existence of fast growing functions.

Problem:  Find other natural equivalents to recursive comprehension.

A constructive weakening of intermediate value theorem is provable in 
the base system:  If f is continuous, and f(0)<0 and f(1)>0, then there 
is g such that g(n) returns (a_n,b_n), where |f(x)|<1/n for all x in the 
interval (a_n,b_n) and a_j < a_k < b_k < a_j for j<k.  We can also show 
that every continuous function on [0,1] has a supremum.  However, having 
a maximum value, along with many other statements in analysis, is 
equivalent to Weak Konig's Lemma.  Some of these equivalences have been 
worked out in a theory called BTFA and its extensions.


== Interpretability in IDelta_0 ==

Despite its expressiveness and apparent power, the theory (axioms 1-10) 
is interpretable in IDelta_0.  Furthermore, under our interpretation in 
IDelta_0, there is a definable cut K and a formula phi coding the 
satisfaction relation for bounded quantifier formulas whose length is in 
K.  I plan to include more details in an upcoming paper, but here I will 
present the main construction.

In IDelta_0 (and even in extended Robinson arithmetic Q^+), we have a 
rich collection of definable cuts:
* Given a definable cut I, there is a definable cut J that such that for 
n all in J, 2^n is in I
* Unless I satisfies Sigma_2 induction (and Sigma_k induction), there is 
a definable cut J < I.
These cuts are obtained through alternation of unbounded quantifiers and 
illustrate that the real strength of IDelta_0 is through meaningfulness 
of unbounded quantification.  Also, if Sigma_2 induction holds, then we 
can use it code a model of WKL_0, so we will assume that it fails on the 
cuts we will consider.

In its general form, the theory can be parameterized by
k_1 -- numbers satisfy Omega_{k_1}
k_2 -- the number of higher types (i.e. k_2 = 2 if we use just functions 
and operators)
k_3 -- number of exponentials sufficient for computation of bounded 
quantification (with axiom 7 and its analogues k_3 = k_2+1, and without 
it k_3 = 1).
k_4 -- (not used in the proof) for restricted quantification theories, 
maximum k such that Pi_k sentences are allowed.

Let 2_a^b = 2^2^...^b (a 2s).

The construction will use three cuts: K<=J<I
I -- satisfies Omega_1
J -- satisfies Omega_{k_1}, and with 2_{k_3}^n in I for some n not in J.
K -- closed under '+','*', and such that for every total recursive 
function f on I
      - I is closed under f^{2_{k_2}^n} for all n in K
      - if f is total on J, J is also closed under f^{2_{k_2}^n} for all 
n in K

Interpretation:
* Numbers are elements of J.
* Functions are polynomial time functions on I whose runtime is 
(len(x)+len(M))^c, with (M,c) included in the code, and
   - M is in I
   - there is n in K such that c < 2_{k_2+1}^n
   - the function is total on J.
* Operators (and hyperoperators, etc.) and bounded quantifier formulas 
are coded by a sequence of bounded-quantifier definitions whose total 
length (number of bits) is in K, and that may refer to numbers and 
functions.

Notes:
* WKL can be shown as follows.  Given a (coded) predicate P on J, we can 
use the polynomial time computability to compute P up to some point 
beyond J, and then choose a path through the binary tree corresponding to P.
* A length n bounded quantifier formula can apply a function up to about 
2_{k_2}^n number of times.  For example, set F_0(f) = f*f, F_{n+1} = 
F_n*F_n ('*' is composition), so F_n(f) = f^{2^2^n}.  This speed up 
characterizes the inherent strength of a basic ability to use higher types.
* Conversely, for an operator F with bounded-quantifier definition 
length n, there is a function g such that F(f)(m) uses f only for 
arguments less than h^{2_{k_2}^n}(m) where h(x) = max(y<=x:f(y)+g(y)).  
Similar results also hold for higher types, and extensionality follows.

Using cut elimination, the interpretability implies that for every 
finite k_1,k_2,k_3,k_4 if we restrict first order logic to boolean 
combinations of Pi_{k_4} sentences, there is k such that every proof of 
existence of 2_k^n has length >n.

Sincerely,
Dmytro Taranovsky
http://web.mit.edu/dmytro/www/main.htm