[FOM] Arithmetic with Limited Exponentiation

[Dmytro Taranovsky]

An important part in our quest to understand the structure of knowledge 
is to find natural weak systems that capture much of mathematics.  
Exponential Function Arithmetic (EFA) captures most arithmetic, but can 
we go further by limiting exponentiation?

Formally, we can define weaker systems, but conceptually we encounter an 
obstacle:
For every k, IDelta_0 (arithmetic with only bounded quantifier 
induction) proves that there is a cut I such that
* I is closed under '+' and '*' (and contains 0 and 1)
* for every i in I, 2_k^i exists (a_b^c is a^a^...^a^c (b exponentials))

Thus, even in a very weak system (interpretable in Robinson arithmetic 
Q), we can in a sense iterate exponentiation any fixed finite number of 
times.  However, we do not want for (for example) 2^2^...^2 (16 2s) to 
have a short existence proof.  The issue is that meaningfulness of 
quantifiers over natural numbers implies a certain ability to do an 
unbounded search over natural numbers. Meaningfulness of quantifiers 
implies that N (the set of natural numbers) has certain attributes of a 
completed totality.  The combinatorial strength of this principle is the 
partial ability to do exponentiation.

However, ordinary mathematics uses quantifiers in a limited way, and in 
particular uses only a very small number of unbounded quantifier 
alternations. By restricting quantifiers, we may restrict exponentiation 
while still capturing much mathematical practice. Specifically, for a 
fixed small k, restrict sentences to those reducible to a boolean 
combinations of
Qx_1 Qx_2 ... Qx_k phi(x_1,x_2,...,x_k)
where each Q is a quantifier and phi is a bounded quantifier formula.  
For quantifier counting, a quantifier may be over (fixed-length) tuples 
of variables.  Also note that in derivation systems that use open 
formulas, a k-1 quantifier formula may correspond to a k quantifier 
sentence.
I think that the consistency of IDelta_0 restricted this way is provable 
in EFA, but I do not have a proof.  For many statements, k=1 suffices -- 
most number theory theorems have natural Pi^0_1 strengthenings.  
However, it is annoying to always modify statements this way, and k=2 
allows one to speak of (for example) an algorithm having linear time 
without specifying a proportionality constant. For second order 
theories, basic axioms on real numbers appear to need at least k=3 
(which we will use below), and k=4 allows general Pi^1_2 statements (and 
k=5 -- Pi^1_3).

We can arrange (through additional axioms if necessary) that provability 
in the original theory agrees with the theory restricted to k quantifier 
sentences.  The original theory may have an iterated exponential 
speed-up of proofs, but that speed-up should only be likely for 
sentences that (perhaps indirectly) involve very large numbers.
An alternative is to allow arbitrary formulas but limit the cut rule to 
restricted formulas, thus treating unrestricted formulas as having 
limited epistemic validity.  This should get systems that -- provably in 
EFA + iterated exponentiation -- are equivalent to (for example) 
IDelta_0, yet with consistency provable in EFA.  However, absence of 
modus ponens is problematic, and allowing the cut rule for arbitrary 
sentences (but not open formulas) would allow length n existence proof 
of about 2_{log*(n)}^n.

Let us define the exponential index of a theory as
maximum k such that existence of 2_k^n has a proof of length n^O(1).

Challenge:  Find natural theories with small exponential indices that 
capture much of mathematics.
If S is a natural theory of exponential index k, then I conjecture that 
provably in a weak base theory, S has no inconsistency proof P (coded by 
a natural number) such that 2_{k+2}^P exists.
Besides exponential index, theories vary by the amount of induction, and 
one can intuitively associate a computational complexity class with a 
theory based on exponential index and the complexity corresponding to 
permitted induction.


I will now discuss one weak theory and its variations.  Even for finite 
programs, it is often useful to talk of input-time-output relation 
without noting implementation, and the natural language for this is to 
use infinite sets.  Also, restricted exponentiation prevents equivalence 
of binary and unary numbers, so for maximum usability we want three types:
1. ordinary or unary numbers -- as in physical sizes; closed under '+' 
and '*'. One extension is to require closure under quasipolynomial 
functions, specifically n-->floor(n^(log n)) (n>0).
2. words or binary numbers -- as in data that a program can manipulate.
3. sets or predicates on words.

Axiomatization:
* Basic axioms.
* Induction (PIND): Every nonempty set has a word of minimum length.
* Bounded quantifier comprehension:
forall P thereis Q forall w (Q(w) <==> phi(P,w)) where phi is a bounded 
quantifier formula (P may be a tuple of variables; w is a word).

Its exponential index is (at least) 5: Define I_0 = {x: 2^2^2^x exists 
as a binary number}, I_1 = {x: I_0 is closed under y->y+2^x}, and I_2 = 
{x: I_1 is closed under y->y+2^x}. Membership in I_2 is Pi^0_3 and hence 
meaningful for constants, allowing us to prove say I_2(100). The 
exponential index rises to 9 if unary numbers are closed under 
quasipolynomial functions, and the system is extended to make sets with 
bounded word length count as numbers and behave accordingly, and we 
allow sentences with five blocks of unbounded quantifiers.  (5 and 9 are 
lower bounds; I do not have a proof of optimality.)

One extension is to allow recursive comprehension, but I do not know 
whether that will preserve finite exponential index.  Even Weak Konig's 
Lemma can be added, but then we would lose optional interpretability of 
predicates as equivalence classes of programs.

Bounded quantifier formulas correspond to the polynomial hierarchy PH 
(or relativized PH if the formula has a free set variable). There are 
natural comprehension schemes that (assuming basic comprehension) 
correspond to different complexity classes:
* counting hierarchy: Q(w) = |{v<w: phi(P,v)}| (with Q encoded by a set)
* PSPACE: Q(w) = phi(P, {v: Q(v) and w-len(w) < v < w})
* EXPTIME: Q(w) = phi(P, {v<w: Q(v)})
* exponential hierarchy:  Treat quantifiers over sets containing only 
words of restricted length as bounded.
* In the other direction (corresponding to S^1_2), one can restrict 
comprehension to polynomial time P, but allow induction for NP formulas.

Capturing the counting hierarchy is useful to define acceptance 
probability of a polynomial time randomized (or even quantum) 
computation.  Acceptance probability (after rescaling to get an integer) 
is complete for #P, which is conjectured to be outside PH; however 
approximations are in PH.  For quantum computation, even approximations 
are not known to be in PH.

There is a hierarchy of systems based on how many times exponentiation 
can be effectively applied (and on other restrictions on comprehension 
and induction).  A good project would be to catalog some of these 
systems of arithmetic and analysis, show that their consistency is 
provable in EFA, and see how much mathematics can be done in them.

Sincerely,
Dmytro Taranovsky