On Parallel Hierarchies and R_{k}^{i}

Stephen Bloch ^{∗}

September 23, 1996

Abstract

This paper defines natural hierarchies of function and relation classes, constructed from parallel complexity classes in a manner analogous to the polynomial-time hierarchy. A number of structural results about these classes are proven: relationships between them and the levels of PH; relationships between these classes and definability in the bounded arithmetic theories R_{k}^{i}; and several results relating conservation among theories of bounded arithmetic to the collapse of complexity classes.

1 Introduction

Rohit Parikh, in [Par71], studied weak theories of arithmetic that have induction only for bounded, or Δ_{0}, formulæ. These theories became known as theories of bounded arithmetic, and were further developed in [Bus86a]. In that paper, Sam Buss restricted induction not only to bounded formulæ, but to bounded formulæ of fixed complexity Σ_{i}^{b}. Furthermore, Buss distinguished between an exponential-length and a polynomial-length form of induction, defining thereby two related hierarchies of logical theories T_{2}^{i} and S_{2}^{i}, and proved basic relationships among them such as that S_{2}^{i} ⊆ T_{2}^{i} ⊆ S_{2}^{i+1} for i ≥ 1. Most importantly, Buss showed that the proof strength of S_{2}^{i} corresponded exactly to accepted notions of computational complexity: the functions at level i of the polynomial time hierarchy are precisely those with a Σ_{i}^{b} graph, provably total and single-valued in S_{2}^{i}.

Expanding on this work, various researchers [All91, Clo89, CT92] introduced a third hierarchy of theories R_{2}^{i} based on log-length induction, and demonstrated that R_{2}^{1} analogously characterized the functions computable in the parallel class N C. But no natural description was known of the computational content of R_{2}^{i} proofs for i > 1, in part because many natural arguments about log-length induction seem to require quasipolynomial, rather than polynomial, growth rates (although see [Blo92, Blo95b] for an exception). Attention therefore turned to the theories R_{3}^{i}, in which terms have quasipolynomial growth. Buss, Krajíček, and Takeuti [BKT93] described the problems for which R_{3}^{i} can prove the existence of solutions, relying on a somewhat complex notion of multi-valued functions computed with a limited number of queries to a witnessing oracle.

∗Math/Computer Science Dept, Adelphi University. This work was supported by Judy Goldsmith’s NSERC operating grant OGP0121527 while the author was at the University of Manitoba; further work was done variously at the University of Kentucky, Adelphi University, and the DIMACS research center at Rutgers University.

A preliminary version [Blo95a] of the present paper claimed to characterize the functions provably total and single-valued in R_{2}^{i}, R_{3}^{i}, R_{4}^{i}, etc. by natural oracle-based parallel complexity classes □_{i,k}^{c} (defined below; for example, □_{1,2}^{c} = ALOGT IME)^{1}, without the complications of multi-valued functions, witnessing oracles, or artificial bounds on the number of oracle queries. S. Buss pointed out a subtle flaw: one of the proofs implicitly relied on the following.

Conjecture 1.1 (S. Buss) If R_{k}^{i} ⊢ (∀x⃗)(∃y)A(x⃗, y), with A ∈ Σ_{i,k}^{b}, then there is a Σ_{i,k}^{b} formula B such that R_{k}^{i} ⊢ (∀x⃗)(∃!y)B(x⃗, y) and R_{k}^{i} ⊢ B(x⃗, y) ⊃ A(x⃗, y).

The corresponding statement for theories S_{2}^{i} was shown in [Bus86a], using the polynomialtime self-reducibility of SAT (i.e. given a yes/no oracle for SAT, one can find a satisfying assignment in polynomial time). Since SAT is not known to be self-reducible in □_{1,k}^{c}, this technique doesn’t carry over easily, and neither [BKT93] nor the author have been able to prove the conjecture for R_{k}^{i}. As a result, it is conceivable that some of the ∀∃Σ_{i}^{b} consequences of R_{k}^{i} correspond to multi-valued functions that R_{k}^{i} cannot prove are extensions of □_{i,k}^{c} functions.

For another view of the problem, consider the “existential instantiation” inference in a natural deduction system (or its analogues in other styles of proof systems), which given the hypothesis ∃xφ(x), introduces a new constant symbol a about which nothing is known except φ(a), and reasons with a henceforth. The computational analogue is, given a list of numbers of which at least one has a desired property, to choose an arbitrary number from the list with the desired property. Although polynomial time can do this in many circumstances, it is not clear that □_{1,k}^{c} can.

However, we show that □_{i,k}^{c} comprises, if not all of the Σ_{i,k}^{b} consequences of R_{k}^{i}, at least a “large” subset of them: indeed, if we restrict our attention to single-valued functions, □_{i,k}^{c} does comprise exactly the Σ_{i,k}^{b} consequences of R_{k}^{i}. This suffices to prove other results relating conservativity among theories of bounded arithmetic to collapses of complexity classes.

For example, [BKT93] asked whether the known ∀∃Σ_{i+1}^{b} conservativity between S_{3}^{i} and R_{3}^{i+1} also holds between S_{2}^{i} and R_{2}^{i+1}; we give circumstantial evidence that it does not, as such conservativity would imply a collapse of complexity classes (see Theorem 6.11).

With the aid of an ingenious interactive computational model, [KPT91] showed that if S_{2}^{i+1} ≡ T_{2}^{i}, then Σ_{i+1}^{p} ⊆ Δ_{i+1}^{p}/poly and therefore the polynomial hierarchy collapses to at most Σ_{i+2}^{p} = Π_{i+2}^{p}. [Bus94] simplified the proof and strengthened the result: under the same hypotheses, Σ_{i+1}^{p} ⊆ Δ_{i+1}^{p}/poly, and therefore the polynomial hierarchy collapses, provably in T_{2}^{i}. The present paper shows (see Theorem 7.4) that any equivalence of the form R_{k}^{i+1} ≡ S_{k}^{i}, with i ≥ 1, k ≥ 3, would imply a similar collapse of complexity classes, e.g. (for k = 3) the collapse of the quasipolynomial hierarchy, provably in S_{k}^{i}.

Section 2 defines the hierarchies of logical theories, the models of parallel computation, and the hierarchies of parallel complexity classes used in this paper. Section 3 proves a variety of basic relationships among these complexity classes. Section 4 shows that R_{k}^{i} can define a number of useful functions (e.g. sequence coding) and prove a number of useful properties of them. Section 5 shows a direct link between the complexity classes of the present paper and those defined in [BKT93, Kra93]. Section 6 proves that the computational class □_{i,k}^{c} is contained in the Σ_{i}^{b} consequences of R_{k}^{i}. Section 7 gives results analogous to those of [KPT91, Bus94] relating the collapse of theories of bounded arithmetic to the collapse of complexity classes. We conclude by discussing some of the remaining results we would most like to prove about these theories.

1The □_{i,k}^{c} characterizations depend both on the function-theoretic characterization of [Blo94] and on circuits with oracle gates, as in [Wil85, Wil87].

2 Definitions

2.1 Universe(s) of Discourse

Most of the existing literature on theories of bounded arithmetic treats the theories as operating over a universe of natural numbers. However, many aspects of parallel computation are easier to formulate in terms of bit-strings. Dyadic notation provides a convenient bijection between the two. To avoid confusion, we shall think of parallel computation as operating on strings in the language { t, f}^{∗}; when interpreting such a string as a natural number, we read t as the dyadic digit 2 and f as the dyadic digit 1.

2.2 Languages, Notation, and Growth Rates

We work with several first-order languages of arithmetic, similar to those used in [Bus86a] and [BKT93], with whose notation I assume the reader is familiar. First we define a collection of term and relation symbols.

Definition 2.1 The language L_{1} consists of

• the variable symbols a, b, c, d, w, x, y, z, possibly subscripted with an integer

• the constant symbols 0 and 1, with their usual interpretations

• the binary infix relation symbols = and ≤ with their usual interpretations

• the binary infix function symbols +, −^{.}, and · with their usual interpretations (where

x −^{.} y = max(0, x − y))

• the unary “outfix” function symbol || interpreted to mean λx.⌊log_{2}(x + 1)⌋, the number of digits in x’s dyadic representation, and

• the binary prefix function symbol Msp interpreted to mean λx. ⌊\frac{x+1}{2^{y}}⌋−^{.}1 ( i.e. the result of deleting the rightmost y digits from x’s dyadic representation).

and any term constructed from these by composition and λ-abstraction.

Definition 2.2 For k > 1, the language L_{k} is the language L_{1} augmented with the binary infix function symbols #_{2}, #_{3}, #_{4}, … #_{k}, pronounced “smash two”, “smash three”, and so on. “Smash two” is often simply called “smash”.

The intended interpretations of these symbols are as follows: x#_{2}y = 2^{|x|·|y|} − 1, x#_{3}y = 2^{|x|#_{2}|y|}−1, …, x#_{k}y = 2^{|x|#_{k−1}|y|}−1. These smash functions are discussed in [Cob65, Hoo83, Nel86, Bus86a, All91], all of which use unimportantly different definitions (e.g., using binary, rather than dyadic, lengths, or omitting the “−1”).

We shall frequently refer to “the length of an L_{k}-term”, or |L_{k}| for short. For example, if we say “f(x) ∈ |L_{1}|” or “f(x) is bounded by the length of an L_{1} term”, we mean that f is at most a linear function in the length of x. Similarly, |L_{2}| means a polynomial, or 2^{O(log)}, in the lengths of the free variables; |L_{3}| is quasipolynomial, or 2^{2^{O(log log)}}, in the lengths of the free variables, and so on. We shall likewise refer to “the log of the length of an L_{k}-term”, abbreviating it ||L_{k}|| (the slight abuse of notation, equating log with length, doesn’t affect the results).

One can define a number of other useful functions and relations as abbreviations for terms and formulæ over this basic syntax:

x < y ⇔ x + 1 ≤ y
x ≥ y ⇔ y ≤ x
x > y ⇔ y < x
2 = 1 + 1
PwrTwo(x) ⇔ |2 · x −^{.} 2| + 1 = |2 · x −^{.} 1|
x^{2} = x · x
2^{|x|} = (x#_{2}1) + 1
Lsp(x, y) = x −^{.} 2^{min(y,|x|)} · Msp(x, y)
Substr(x, y, z) = Lsp(Msp(x, y), z)
Bit(i, x) = Substr(x, i, 1)
⌊\frac{x}{2}⌋ = Msp(x + 1, 1)
Parity(x) = Lsp(x, 1)
Conc(x, y) = x · 2^{|y|} + y
Shl(x, y) = Lsp(Conc(x, y), |x|)
Fh(x) = Msp (x, ⌊\frac{|x|}{2}⌋)
Bh(x) = Lsp (x, ⌊\frac{|x|}{2}⌋)

Note that the Conc, Msp, and Lsp functions act as inverses: Msp(Conc(x, y), |y|) = x, Lsp(Conc(x, y), |y|) = y, and (for (|y| ≤ |x|) Conc(Msp(x, y), Lsp(x, y)) = x. (Allen, in [All91], defined these functions differently, operating on binary rather than dyadic numbers, with the odd result that the “back half” of a 40-digit number could be anywhere from 0 to 20 digits long, depending on leading zeroes; in our setting it will always be exactly 20 digits.)

2.3 Syntactic Complexity

We next define an hierarchy of syntactic formula classes, analogous to the classes Σ_{i}, Π_{i}, Δ_{i} familiar to recursion theorists. The following definitions differ from those in [Bus86a] mainly in the presence of a second subscript k; since Buss was only concerned with a language analogous to L_{2}, his results apply to our classes with k = 2.

Definition 2.3 A bounded quantifier with bound of the form |t(x)|, i.e. one whose outermost function symbol is | ⋯|, is said to be sharply bounded.

Definition 2.4 The classes Σ_{i,k}^{b} and Π_{i,k}^{b} are the smallest sets of formulæ satisfying the following inductive definition (where t is a term in language L_{k}).

• Σ_{0,k}^{b} = Π_{0,k}^{b} is the set of formulæ in language L_{k} in which all quantifiers are sharply bounded.

• Π_{i,k}^{b} ⊆ Σ_{i+1,k}^{b}.

• Σ_{i,k}^{b} ⊆ Π_{i+1,k}^{b}.

• If A ∈ Σ_{i+1,k}^{b}, then the formula (∃x ≤ t)A is also in Σ_{i+1,k}^{b}.

• If A ∈ Π_{i+1,k}^{b}, then the formula (∀x ≤ t)A is also in Π_{i+1,k}^{b}.

• If A, B ∈ Σ_{i,k}^{b} (respectively Π_{i,k}^{b}), then so are A ∧ B and A ∨ B.

• If A ∈ Σ_{i,k}^{b} and B ∈ Π_{i,k}^{b} (respectively vice versa), then (A ⊃ B) ∈ Π_{i,k}^{b} (respectively Σ_{i,k}^{b}).

• If A ∈ Σ_{i,k}^{b} (respectively Π_{i,k}^{b}), then so are both (∀x ≤ |t|)A and (∃x ≤ |t|)A.

When the language L_{k} is clear from context, particularly when k = 2, we omit the subscript k.

2.4 Classical Theories of Bounded Arithmetic

The theory T_{k}^{i} is axiomatized by a fixed, finite set of quantifier-free axioms and the inference rule Σ_{i,k}^{b} − IND, which we write in Gentzen sequent-calculus form:

\begin{matrix}Γ(b⃗), A(a, b⃗) & ⟶ & A(a + 1, b⃗), Δ(b⃗) \\ Γ(b⃗), A(0, b⃗) & ⟶ & A(t(b⃗), b⃗), Δ(b⃗) \end{matrix}

where A ∈ Σ_{i,k}^{b} and t ∈ L_{k}.

The theory S_{k}^{i} is axiomatized similarly, but with one of two (provably equivalent; see [Bus86a, All91]) induction inferences in place of IND.

Σ_{i,k}^{b} − P IND (“prefix induction”):

\begin{matrix}Γ(b⃗), A (⌊\frac{a}{2}⌋, b⃗) & ⟶ & A(a, b⃗), Δ(b⃗) \\ Γ(b⃗), A(0, b⃗) & ⟶ & A(t(b⃗), b⃗), Δ(b⃗) \end{matrix}

Σ_{i,k}^{b} − LIND (“length induction”):

\begin{matrix}Γ(b⃗), A(a, b⃗) & ⟶ & A(a + 1, b⃗), Δ(b⃗) \\ Γ(b⃗), A(0, b⃗) & ⟶ & A(|t(b⃗)|, b⃗), Δ(b⃗) \end{matrix}

The theory R_{k}^{i} is axiomatized similarly, with one of four induction schemes, called DCI, P P IND, LP IND, and LLIND. They are shown to be equivalent in [All91, CT92] (in a sufficiently expressive language, such as L_{k} for k ≥ 2).

The DCI induction scheme introduced in [All91] uses functions Fh and Bh that return the “front half” and “back half” respectively of a number’s binary representation. We use, instead, the more well-behaved Fh and Bh functions defined in section 2.2. As a side effect, we must use more base cases: in addition to 0 and 1, we need 2 in order for DCI to be valid.

Σ_{i,k}^{b} − DCI (“divide and conquer induction”):

Γ(b⃗), A(Bh(a), b⃗), A(Fh(a), b⃗) ⟶ A(a, b⃗), Δ(b⃗) ; Γ(b⃗), A(0, b⃗), A(1, b⃗), A(2, b⃗) ⟶ A(t(b⃗), b⃗), Δ(b⃗)

Σ_{i,k}^{b} − P P IND:

\begin{matrix}Γ(b⃗), A(Fh(a), b⃗) & ⟶ & A(a, b⃗), Δ(b⃗) \\ Γ(b⃗), A(1, b⃗), A(2, b⃗) & ⟶ & A(t(b⃗), b⃗), Δ(b⃗) \end{matrix}

Σ_{i,k}^{b} − LP IND:

\begin{matrix}Γ(b⃗), A (⌊\frac{a}{2}⌋, b⃗) & ⟶ & A(a, b⃗), Δ(b⃗) \\ Γ(b⃗), A(0, b⃗) & ⟶ & A(|t(b⃗)|, b⃗), Δ(b⃗) \end{matrix}

Σ_{i,k}^{b} − LLIND:

\begin{matrix}Γ(b⃗), A(a, b⃗) & ⟶ & A(a + 1, b⃗), Δ(b⃗) \\ Γ(b⃗), A(0, b⃗) & ⟶ & A(||t(b⃗)||, b⃗), Δ(b⃗) \end{matrix}

The reader seeking more detail and discussion of these theories and induction schemes is referred to [Bus86a, All91, CT92, Blo92].

2.5 Axiomatizing Bounded Arithmetic

The theory R_{2}^{1} seems to require a few more base functions than S_{2}^{1}. Where [CU93] used the language \{0, Sx, |x|, ⌊\frac{x}{2}⌋, x + y, x · y, x#y\} for their theory IS_{2}^{1}, [All91] generalizes the ⌊\frac{x}{2}⌋ function to Msp(x, y), and adds the functions x−^{.}y, Bit(i, x), and Lsp(x, i) in defining a theory similar to R_{2}^{1}. We shall do the same, except that we defined Bit and Lsp by abbreviation (see section 2.2).

The defining axioms for all these symbols follow. Fourteen, labelled “(CU)”, are (straightforward adaptations of) corresponding axioms in [CU93]. Several others, labelled (A), appear (modulo obvious adaptations) in [All91]. I use different defining axioms for Msp and # from those in [All91].

• 0 ≤ x (CU)

• x ≤ 1 ⊃ x = 0 ∨ x = 1 (A)

• x ≤ y ⊃ (x = y ∨ x + 1 ≤ y) (CU)

• (x ≤ y ∧ y ≤ z) ⊃ x ≤ z (CU)

• (x ≤ y ∧ y ≤ x) ⊃ x = y (CU)

• x ≤ y ∨ y ≤ x (CU)

• |0| = 0 (CU)

• |(2 · x) + 1| = |x| + 1 (CU)

• |(2 · x) + 2| = |x| + 1 (CU)

• x ≤ y ⊃ |x| ≤ |y| (CU)

• x + 0 = x (CU)

• x + y = y + x (A)

• (x + y) + z = x + (y + z) (CU)

• x + y ≤ x + z ↔ y ≤ z (CU)

• x ≤ y ⊃ x −^{.} y = 0 (A)

• y ≤ x ⊃ (x −^{.} y) + y = x (A)

• x · 1 = x (CU)

• x · (y + z) = (x · y) + (x · z) (CU)

• Msp(x, 0) = x (A)

• |x| ≤ i ⊃ Msp(x, i) = 0 (A)

• (Msp(x, i) = 2 · Msp(x, i + 1) + 1) ∨ (Msp(x, i) = 2 · Msp(x, i + 1) + 2) (A)

• Msp(2 · x + 1, i + 1) = Msp(x, i)

• Msp(2 · x + 2, i + 1) = Msp(2 · x + 1, i + 1)

The present paper defines the smash functions slightly differently than does [CU93], as mentioned in section 2.2, so the axioms for #_{2}, …, #_{k} become simply

• |x#_{2}y| = |x| · |y|

• |(x#_{2}y) −^{.} 1| = |x#_{2}y| −^{.} 1

• ⋮

• |x#_{k}y| = |x|#_{k−1}|y|

• |(x#_{k}y) −^{.} 1| = |x#_{k}y| −^{.} 1

In addition, the theory R_{k}^{i} has the inference rules of LKB (see [Bus86a]) and DCI on all formulæ in Σ_{i,k}^{b}.

2.6 Circuits and Uniformity

Our complexity classes are defined in terms of uniform families of multiple-output circuits, which furthermore may contain “oracle gates”. (In addition, for technical reasons, we introduce “output gates” which compute the identity function of their single input.) Wilson [Wil85, Wil87] introduced a similar notion of oracle gates, and I follow his convention that an oracle gate’s “size” and “depth” are its fanin and the log of its fanin respectively. (This convention is crucial to some of the proofs in the k = 2 case; it makes no difference for k ≥ 3.)

Most of the circuit families in this paper are described by genus:

Definition 2.5 An oracle circuit family of genus k is a circuit family with at most |L_{k}| output gates, depth at most ||L_{k}||, and fanin at most 2 except for its oracle gates. All oracle gates in a given circuit family with input x⃗ have fanin exactly |t(x⃗)|, where t ∈ L_{k} is a nontrivial term in the following sense.

Definition 2.6 A term t(x⃗) is nontrivial if it is bounded below by the maximum of its free variables.

Actually, we only need that |t(x⃗)| = Ω(|x⃗|), i.e., t is bounded below by a polynomial in which all its free variables x⃗ appear with positive degree and positive coefficient. But for our purposes, this more inclusive definition does not seem worth its added complexity.

Most results in this paper are stated “for k ≥ 2” or “for k ≥ 3”. Some would hold even for k = 1, but genus 1 circuit families are so ill-behaved (e.g., not closed under composition) that we shall usually ignore the k = 1 case.

Lemma 2.7 For k ≥ 2, an oracle circuit family of genus k has size (i.e., number of gates) at most |L_{k}|.

Proof: Recall that by convention, an oracle gate has the same “size” as a tree of boundedfanin gates of the same “depth”. So for purposes of size, we may assume there are no oracle gates. Thus the size of any single-output circuit is |L_{k}|. There may be as many as |L_{k}| output gates in a circuit. But since |L_{k}| is closed under multiplication for k ≥ 2, the total size remains |L_{k}|.

All circuit families in this paper are assumed to be uniform in the U_{E^{∗}} sense of [Ruz81]. However, we must slightly extend Ruzzo’s definition of the extended connection language to handle multiple-output circuits and oracle gates. The following definition is formulated using strings of 0’s and 1’s interpreted in binary; however, this notation can be easily interconverted with dyadic by using +, −^{.}, and 2^{|x|}.

Definition 2.8 The descendant of a gate γ along path p ∈ {0, 1}^{∗} is defined by the following algorithm:

let “the current gate” be γ

while |p| > 0,

let r be the fanin of the current gate (either 0, 1, 2, or |t|)

(if r = 0, the descendant is undefined)

let c be the binary number represented by the leftmost max (1, ⌈log(r)⌉) bits of p (if |p| < ⌈log(r)⌉, the descendant is undefined) remove the leftmost ⌈log(r)⌉ bits of p update the current gate to be the c-th leftmost child of the current gate return the current gate

Definition 2.9 Each gate in an oracle circuit has a type, encoded as a binary number, as follows:

• The type of an input gate is an ordered pair: a constant-length indication that it is an input gate, and a binary number indicating which bit of input it is.

• The type of an output gate is an ordered pair: a constant-length indication that it is an output gate, and a binary number indicating which bit of output it is. (An output gate is assumed to have fanin exactly 1, and to compute the identity function.)

• The type of a bounded-fanin internal gate is an ordered pair: a constant-length indication that it is a bounded internal gate, and a constant-length indication of what Boolean function it computes.

• The type of an oracle gate for a relation ρ is a constant-length indication that it is a ρ-oracle gate.

Definition 2.10 The extended connection language of an oracle circuit family is the set of 4-tuples ⟨n, γ, p, τ⟩ such that n is the binary representation of the number of inputs to the circuit, γ is a binary number identifying a gate in the circuit, p ∈ {0, 1}^{∗}, and either |p| = 0 and τ is the type of gate γ, or |p| ≥ 1 and τ is a binary number identifying the descendant of γ along path p.

Definition 2.11 (Ruzzo) A family of circuits of depth T (n) and size Z(n) is U_{E^{∗}}-uniform if its extended connection language is recognizable by an alternating Turing machine (with random access to a read-only input tape) in time O(T (n)) and space O(log(Z(n))).

Lemma 2.12 An oracle-free circuit family of genus k ≥ 2 is U_{E^{∗}}-uniform iff its extended connection language is in AT IME(||L_{k}||).

Proof: Straightforward; note that k ≥ 2 is necessary in order for the depth bounds ||L_{k}|| to be closed under constant factors.

The class of such circuit families is “self-uniform” in that they are exactly as powerful as the ATM’s that define their uniformity (see Theorems 3 and 4 of [Ruz81]). Henceforth whenever we speak of “uniform” circuit families, we mean this sense of uniformity.

2.7 Complexity Classes

The polynomial-time hierarchy contains relation classes Σ_{i}^{p}, Π_{i}^{p}, and Δ_{i}^{p}, and function classes □_{i}^{p} (see, e.g., [Bus86a]). Buss mentions in passing that analogous definitions and theorems hold if the language is expanded to L_{k}, for k ≥ 2. We therefore generalize the notation:

Definition 2.13 The complexity classes Σ_{i,k}^{p}, Π_{i,k}^{p}, Δ_{i,k}^{p}, and □_{i,k}^{p}, for k ≥ 1, are defined as follows:

• Σ_{0,k}^{p} = Π_{0,k}^{p} = Δ_{0,k}^{p} = DTIME(|L_{k}|).

• For i ≥ 0, Σ_{i+1,k}^{p} is the closure of Π_{i,k}^{p} under L_{k}-bounded existential quantification.

• For i ≥ 0, Π_{i+1,k}^{p} is the closure of Σ_{i,k}^{p} under L_{k}-bounded universal quantification.

• For i ≥ 0, Δ_{i+1,k}^{p} = DTIME(|L_{k}|)^{Σ_{i,k}^{p}} = DTIME(|L_{k}|)^{Π_{i,k}^{p}}.

• □_{0,k}^{p} = FDTIME(|L_{k}|), i.e., the functions computable in DTIME(|L_{k}|).

• For i ≥ 0, □_{i+1,k}^{p} = FDTIME(|L_{k}|)^{Σ_{i,k}^{p}} = FDTIME(|L_{k}|)^{Π_{i,k}^{p}}.

For example, Δ_{1,2}^{p} is P, Σ_{1,2}^{p} is N P, and □_{2,3}^{p} is the class of functions computable in quasipolynomial time with oracles for nondeterministic quasipolynomial time. We also define analogous classes based on parallel complexity:

Definition 2.14 The complexity classes Σ_{i,k}^{c}, Π_{i,k}^{c}, Δ_{i,k}^{c}, and □_{i,k}^{c}, for k ≥ 1, are defined as follows:

• Σ_{0,k}^{c} = Π_{0,k}^{c} = Δ_{0,k}^{c} = the class of relations decidable by a uniform family of singleoutput circuits of genus k, containing no oracle gates.

• For i ≥ 0, Σ_{i+1,k}^{c} is the closure of Π_{i,k}^{c} under L_{k}-bounded existential quantification

• For i ≥ 0, Π_{i+1,k}^{c} is the closure of Σ_{i,k}^{c} under L_{k}-bounded universal quantification.

• For i ≥ 0, Δ_{i+1,k}^{c} is the class of relations decidable by a uniform family of single-output circuits of genus k, containing oracle gates for some Σ_{i,k}^{c} or Π_{i,k}^{c} relation.

• □_{0,k}^{c} is the class of functions computable by a uniform family of |L_{k}|-output circuits of genus k, with no oracle gates.

• For i ≥ 0, □_{i+1,k}^{c} is the class of functions computable by a uniform family of |L_{k}|-output circuits of genus k, containing oracle gates for some Σ_{i,k}^{c} or Π_{i,k}^{c} relation.

Henceforth families with the uniformity, size, depth, and gate restrictions above will be called Σ_{i,k}^{c}, Π_{i,k}^{c}, and Δ_{i,k}^{c} circuit families respectively.

At the k = 2 level, it is not clear whether the “most natural” parallel complexity class is N C^{1} or N C. For example, Corollary 5.8 below characterizes □_{i,k}^{c} (which for k = 2 is based on N C^{1}). But although Theorem 6.1 also holds for □_{i,k}^{c}, it can be strengthened in the k = 2 case to apply to classes based on N C. We now define these classes precisely.

Definition 2.15 (Allen) FN C is the class of functions computable by U_{E^{∗}}-uniform^{2} circuit families with polylog depth, polynomial size, and polynomially many outputs.

Definition 2.16 For any class X of relations on {0, 1}^{∗},

• FN C^{X} is the class of functions computable by U_{E^{∗}}-uniform, polylog depth, polynomial size, oracle circuit families with oracle gates of fanin |t| (where t ∈ L_{2} is nontrivial) for an X relation.

• N C^{X} is the class of relations whose characteristic functions are 0/1-valued FN C^{X} functions.

As usual, an oracle gate’s “depth” and “size” are considered to be ||t|| and |t| respectively. Note that since t is nontrivial, these are θ(||L_{k}||) and θ(|L_{k}|) respectively.

Normally we shall study classes of the form N C^{Σ_{i−1,2}^{c}} and FN C^{Σ_{i−1,2}^{c}}, by analogy to Δ_{i,k}^{c} and □_{i,k}^{c}.

2.8 Alternating Turing machines

We can also define an alternating Turing machine model to correspond to arbitrary levels in the Δ^{c} hierarchies.

Definition 2.17 An oracle alternating Turing machine of genus k is an alternating ||L_{k}||- time Turing machine whose states are partitioned into universal, existential, exclusive-or, and oracle states. The universal, existential, and exclusive-or states each have exactly two next states. The behavior of all oracle states in a given machine depends on a nontrivial global bound t ∈ L_{k}.

When the machine enters an oracle state for relation ρ, it guesses a binary number 0 ≤ j < |t(x)|, writes it and a delimiter at the end of a special oracle tape, and goes on to a next state deterministically. Let D_{j} denote the accept/reject decision of this next state given the number j; then the oracle state accepts iff the relation ρ holds of the |t|-bit string D_{|t|−1}D_{|t|−2} ⋯D_{2}D_{1}D_{0}. An oracle state is counted as taking ||t|| time steps.

2Allen actually defined FN C circuit families to be logspace uniform, but as he points out, it makes no difference at this level;see [Ruz81].

(Recall that [CKS81] defined ATM’s with NOT states, then proved that they could be eliminated. This proof appears not to work in the presence of oracle states, unless the oracles come from a class closed under complement. We use two-input exclusive-or states instead, as they can be “programmed” to compute either a NOT or an identity function by making one of their successor configurations unconditionally accept or reject.)

For example, if ρ were a |t|-way AND, a ρ-oracle state would be equivalent to universally guessing ||t|| bits, which could have equally well been done without an oracle in the same time. Similar reasoning holds for any ρ ∈ Δ_{0,k}^{c}, giving us

Lemma 2.18 For k ≥ 2, a relation is computable by an oracle ATM of genus k with a Δ_{0,k}^{c} oracle iff it is computable by an ATM of genus k with no oracles at all.

A more interesting situation arises when ρ is, say, a Σ_{1,k}^{c} relation; then there is no obvious way to simulate the oracle in less than |L_{k}| parallel time, exponentially too long. The following lemma may be seen as a generalization of Ruzzo’s theorems 3 and 4.

Lemma 2.19 For k ≥ 2, a relation is computable by an ATM of genus k with an oracle in Σ_{i−1,k}^{c} iff the relation is in Δ_{i,k}^{c}.

Proof: Let ρ be Δ_{i,k}^{c}, using gates for Σ_{i−1,k}^{c} oracle σ. We construct an ATM to compute ρ as follows. At all times, maintain on an extra tape the path from the root to the gate currently being simulated. Guess (in constant time) whether the gate is AND, OR, NOT, output, input, or oracle. Depending on the answer, then guess the remaining bits of its type. In any case, you now know the complete type of the gate; confirm this type in parallel with the U_{E^{∗}} uniformity algorithm. If AND or OR, simulate it by making the appropriate guess and appending a bit to the path. If NOT, simulate it with an exclusive-or state one of whose successors accepts unconditionally. If a σ oracle gate, simulate it with a σ oracle state, appending the number guessed to the path. If input, simulate it by accessing the input tape. If output, return an accept/reject decision.

Note that guessing the type of a gate takes constant time except for input and output gates, of which any given path contains at most one each. Thus the total time to simulate a path of length ||L_{k}|| is at most O(||L_{k}||), which is still ||L_{k}|| for k ≥ 2.

Conversely, let ρ be computable by an ATM of genus k with a Σ_{i−1,k}^{c} oracle σ. By standard techniques, assume all access to the input tape is at leaves. Furthermore, assume the ATM never overwrites the numbers it gets from oracle states; if it wishes to overwrite them, it has plenty of time to copy them onto writable work tapes first. As in [Ruz81], we construct a circuit with a gate labelled (t, a) for each time step t within the ||L_{k}|| time bounds and each configuration a within the ||L_{k}|| space bounds, and connect them in the obvious way. A σ-oracle state of the ATM, of course, becomes a σ-oracle gate in the circuit; at any subsequent time that the ATM reads from an oracle tape, the subcircuit reached by taking branch j through the oracle gate acts as though the ATM had read a j from the oracle tape. Note that this circuit family is still U_{E^{∗}}-uniform: given an input length and an instance of the extended connection language, the uniformity condition need only check whether all gates in the instance are labelled with suitable times and configurations, and whether the path in the instance respects the allowable fan-in of gates, and then follow paths by simulating ATM actions.

In particular, Δ_{0,k}^{c} is equal to ATIME(||L_{k}||) for all k ≥ 2. For example, Δ_{0,2}^{c} is known in the literature as ALOGTIME or uniform N C^{1}, and Δ_{0,3}^{c} is the class of problems solvable in uniform polylog depth, or alternating polylog time, or deterministic polylog space (for other relevant characterizations of these classes, see [Blo94]).

3 Basic Relationships among the Classes

In this section we prove “the easy theorems” about the classes defined in section 2.7, showing they constitute a well-behaved complexity hierarchy, before proceeding to more profound results.

Lemma 3.1 For k ≥ 2, Δ_{0,k}^{c} ⊆ Δ_{0,k}^{p}.

Proof: A Δ_{0,k}^{c} circuit family has size |L_{k}|, so a deterministic |L_{k}|-time program can construct the appropriate circuit and evaluate it.

Lemma 3.2 For k ≥ 2, Σ_{1,k}^{c} = Σ_{1,k}^{p}.

Proof: The ⊆ direction follows immediately from Lemma 3.1.

For the ⊇ direction, consider an arbitrary Σ_{1,k}^{p} machine, i.e., a nondeterministic |L_{k}|- time machine. Its computation can be simulated in Σ_{1,k}^{c} by guessing a string representing a complete computation of the machine, then checking that the first configuration contains the right input and initial conditions, the last configuration is accepting, and (in parallel for all j) that the j + 1-th configuration follows correctly from the j-th. The string is of length |L_{k}|^{2}, which for k ≥ 2 is |L_{k}|. The parallel check requires a |L_{k}|-way conjunction, which can be done easily by a Δ_{0,k}^{c} circuit family. Checking that a configuration follows correctly from the previous one requires checking that their tape contents are identical except for the square under the head in the earlier configuration; this again is a |L_{k}|-way conjunction, and easily within Δ_{0,k}^{c}.

This is not an earthshaking result; similar statements date at least to [Fag74]. But in our notation, it implies immediately the following theorem:

Theorem 3.3 For i ≥ 1, k ≥ 2, Σ_{i,k}^{c} = Σ_{i,k}^{p} and Π_{i,k}^{c} = Π_{i,k}^{p}.

In light of this theorem, we can dispense with proving basic properties of the Σ_{i,k}^{c} and Π_{i,k}^{c} classes: either we already know them, or we are unlikely to be able to prove them with present techniques. Indeed, we can dispense with the notations Σ_{i,k}^{c} and Π_{i,k}^{c} altogether. But we still don’t know much about the Δ_{i,k}^{c} and □_{i,k}^{c} classes. So we’ll prove a number of useful results about these classes and the relationships among them. The most trivial ones I state without proof:

Fact 3.4

• The Δ_{i,k}^{c} relations are the relations with characteristic functions in □_{i,k}^{c}.

• For i ≥ 0, k ≥ 1, Δ_{i,k}^{c} is closed under negation, finite disjunction and conjunction, and definition by Δ_{i,k}^{c} cases (and similarly with N C^{X} in place of Δ_{i,k}^{c}).

• For all i′ ≥ i ≥ 0 and k′ ≥ k ≥ 1, we have Δ_{i,k}^{c} ⊆ Δ_{i′,k′}^{c} and □_{i,k}^{c} ⊆ □_{i′,k′}^{c}.

• Σ_{i,k}^{c} ∪ Π_{i,k}^{c} ⊆ Δ_{i+1,k}^{c}.

Lemma 3.5 For i ≥ 0 and k ≥ 2, □_{i,k}^{c} and FN C^{X} are closed under composition.

Proof: Suppose functions f(y) and g(x) are in □_{i,k}^{c}. A multiple-output oracle circuit for f can be converted into one for f ∘ g by replacing the input gates for bits of y with the outputs of a multiple-output circuit for g. The resulting circuit is still □_{i,k}^{c}, because circuit depth is closed under addition for k ≥ 2.

The proof for FN C^{X} is similar.

Corollary 3.6 For i ≥ 0 and k ≥ 2, Δ_{i,k}^{c} is closed under substitution by □_{i,k}^{c} functions (similarly, N C^{X} is closed under FN C^{X} substitution).

Lemma 3.7 For k ≥ 2, Δ_{0,k}^{c} = Δ_{1,k}^{c}. (Similarly, N C = N C^{N C}.)

Proof: Let ρ ∈ Δ_{1,k}^{c}. Then ρ has a uniform circuit family of genus k containing oracle gates for some Σ_{0,k}^{c} (i.e., Δ_{0,k}^{c}) relation σ. To compute ρ in Δ_{0,k}^{c}, simply replace each oracle gate for σ with an entire circuit for σ (depth ||L_{k}||). If k = 2, then a σ-oracle gate is counted as having depth θ(log(|x|)) and the total depth of a ρ-circuit is O(log(|x|)), so each path can have had only constantly many σ-oracle gates. Replacing them with ||L_{k}||-depth σ-circuits adds only O(||L_{k}||) to the total depth, so the result has depth ||L_{k}||. On the other hand, if k ≥ 3, then replacing each σ-oracle gate with a ||L_{k}||-depth circuit at most multiplies the depth by ||L_{k}||, which is still within ||L_{k}|| for k ≥ 3. The uniformity of the new circuit family follows easily from the uniformity of the ρ family and the σ family.

The proof for N C is similar, relying on the convention that an oracle gate with fanin |t| is counted as having size |t|.

Lemma 3.8 For any i > 0, k ≥ 2, the function f(x⃗) is in □_{i,k}^{c} iff its bit-graph, the relation λj, x⃗.Bit(j, f(x⃗)), is in Δ_{i,k}^{c}.

Similarly, a function is in FN C^{X} iff its bit-graph is in N C^{X}.

Proof: (⇒): A circuit to do this consists of a |L_{k}|-bit multiplexer (which can be done in depth ||L_{k}||) composed with a circuit for f.

(⇐): Simply use |f(x⃗)| circuits in parallel, each computing a different bit of f.

Lemma 3.9 For i ≥ 0 and k ≥ 2, if ρ(x⃗) is equivalent to (∃y ≤ |s(x⃗)|)σ(x⃗, y) or to (∀y ≤ |s(x⃗)|)σ(x⃗, y), where σ ∈ Δ_{i,k}^{c} and s ∈ L_{k}, (respectively σ ∈ N C^{X}, with s ∈ L_{2}), then ρ is itself in Δ_{i,k}^{c} (respectively N C^{X}).

That is, Δ_{i,k}^{c} and N C^{X} are is closed under sharply-bounded quantifiers.

Proof: An AND or OR of fanin |L_{k}| can be evaluated by a bounded-fanin circuit of depth ||L_{k}||, i.e., at the cost of an additional ||L_{k}|| depth, allowable for k ≥ 2.

Lemma 3.10 For i ≥ 0, k ≥ 2, Δ_{i,k}^{c} ⊆ Δ_{i,k}^{p}. (Similarly, N C^{Σ_{i−1,2}^{p}} ⊆ Δ_{i,2}^{p}.)

Proof: The proof is similar to that of Lemma 3.1. A Δ_{i,k}^{p} program has time to construct a description of the Δ_{i,k}^{c} circuit (complete with oracle gates) and evaluate it, invoking a Σ_{i−1,k}^{p} oracle when necessary.

Corollary 3.11 For i ≥ 0, k ≥ 2, Δ_{i,k}^{c} ⊆ Σ_{i,k}^{p} ∩ Π_{i,k}^{p}.

(Similarly, N C^{Σ_{i−1,2}^{p}} ⊆ Σ_{i,2}^{p} ∩ Π_{i,2}^{p}.)

Corollary 3.12 For i ≥ 0, k ≥ 2, the classes Σ_{i,k}^{p} and Π_{i,k}^{p} are closed under definition by cases, as long as the decision is in either Δ_{i,k}^{c} or N C^{Σ_{i−1,2}^{p}}.

Lemma 3.13 For i ≥ 1, k ≥ 2, □_{i,k}^{c} ⊆ □_{i,k}^{p} and FN C^{Σ_{i−1,2}^{p}} ⊆ □_{i,2}^{p}.

Proof: Similar to that of Lemma 3.10. A □_{i,k}^{p} program has time to construct, for each of |L_{k}| output bits j, a complete description of the Δ_{i,k}^{c} circuit that computes the j-th output bit. The □_{i,k}^{p} program can then evaluate each of these circuits and concatenate the answers. All of this works because |L_{k}| is closed under multiplication for k ≥ 2.

Corollary 3.14 For i ≥ 0, k ≥ 2, the classes Σ_{i,k}^{p} and Π_{i,k}^{p} are closed under substitution by □_{i,k}^{c} (and FN C^{Σ_{i−1,2}^{p}}) functions.

Theorem 3.15 For i ≥ 1, k ≥ 2 we have Δ_{i,k}^{c} ⊆ Δ_{i,k}^{p} ⊆ Δ_{i+1,k}^{c} and □_{i,k}^{c} ⊆ □_{i,k}^{p} ⊆ □_{i+1,k}^{c}.

Proof: The inclusions Δ_{i,k}^{c} ⊆ Δ_{i,k}^{p} and □_{i,k}^{c} ⊆ □_{i,k}^{p} are Lemmas 3.10 and 3.13.

The inclusion Δ_{i,k}^{p} ⊆ Δ_{i+1,k}^{c} is immediate because Δ_{i,k}^{p} ⊆ Σ_{i,k}^{p}, for which Δ_{i+1,k}^{c} has an oracle.

For the inclusion □_{i,k}^{p} ⊆ □_{i+1,k}^{c}, observe that bit extraction is in □_{0,2}^{p}, so any desired bit of the □_{i,k}^{p} function can be found in Δ_{i+1,k}^{c}. It then remains only for □_{i+1,k}^{c} to compute each of these bits in parallel; the uniformity condition can easily specify which bit of the □_{i,k}^{p} function to extract.

4 Bootstrapping R_{k}^{i}

Every paper introducing a new theory of bounded arithmetic contains a “bootstrapping” section showing that the theory in question has nice closure properties, can encode sequences efficiently, etc. The present paper is no exception. Fortunately, much of the bootstrapping of R_{k}^{i} has already been done in [All91].

4.1 DCI, PPIND, LPIND, and LLIND

Theorem 4.1 (Folklore, Allen, Takeuti) In the presence of the quantifier-free axioms of R_{2}^{1}, the following are equivalent:

• Σ_{i}^{b}-DCI

• Σ_{i}^{b}-PPIND

• Σ_{i}^{b}-LPIND

• Σ_{i}^{b}-LLIND

Proof: DCI trivially simulates PPIND, since their conclusions are the same and PPIND has stronger hypotheses.

PPIND can simulate LPIND on the Σ_{i}^{b} formula A(x) as follows. Let B(x) = A(|x| −^{.} 1). Then clearly A(0) ⊃ B(0) ∧ B(1) ∧ B(2), taking care of the base cases of PPIND on B. For the induction step, observe that

B(Fh(x)) ⇒ A(|Fh(x)| −^{.} 1) ⇒ A (⌈\frac{|x|}{2}⌉ −^{.} 1) ⇒ A (⌊\frac{|x| −^{.} 1}{2}⌋) ⇒ A(|x| −^{.} 1) ⇒ B(x).

Thus we can do PPIND on B(x) up to B(2t + 1), which implies A(|t|) as desired.

LPIND can simulate LLIND in much the same way, letting B(x) = A(1 + |x −^{.} 1|) (i.e. B(x) is A of the binary length of x) and using LPIND on B(x) up to B(|2t + 1|).

To simulate DCI with LLIND, we shall interpret a bit string as a balanced binary tree of suitably aligned substrings, and prove by induction on the height of the tree that all vertices of the tree have a certain property. It is a straightforward exercise to define a term Block(x, w, i) which yields the i-th leftmost vertex of x in the w-th level from the bottom. One can then define, given a Σ_{i}^{b} formula A(x, y⃗), another Σ_{i}^{b} formula B(x, w, y⃗) stating that for all blocks b at level w of the tree interpretation of x, A(b, y⃗) holds. LLIND on the variable w in B(x, w, y⃗) then yields the desired result. For further details, see [Blo92], pp. 95–96.

4.2 Adding Symbols by Definition

Definition 4.2 (S. Buss) The function f(x⃗) is Σ_{i}^{b}-defined in theory T if there is a Σ_{i}^{b} formula A_{f}(x⃗, y) (in the language of T) such that T ⊢ (∀x⃗)(∃!y)A_{f}(x⃗, y) and N ⊧ f(n⃗) = m ↔ A_{f}(n⃗, m).

In particular, if f is Σ_{1}^{b}-defined in theory T, then let T^{f} denote the theory T augmented with the function symbol f (which may appear anywhere, including induction formulæ) and the defining axiom f(x⃗) = y ↔ A_{f}(x⃗, y). S. Buss [Bus86a] pointed out that every Σ_{i}^{b} (respectively Π_{i}^{b}) formula in T^{f} is T^{f}-provably equivalent to a Σ_{i}^{b} (resp. Π_{i}^{b}) formula not involving f. Thus if all of T ’s general axiom schemas are applicable to, say, “all Σ_{i}^{b} formulæ”, then f can be added to the language without changing the applicability of those schemas, and thus T^{f} is a conservative extension of T.

Definition 4.3 (Buss) A formula ϕ is Δ_{i}^{b} with respect to theory T if there are a Σ_{i}^{b} formula ϕ^{+} and a Π_{i}^{b} formula ϕ^{−}, both T -provably equivalent to ϕ.

Buss showed that if R is Δ_{1}^{b}-defined in theory T, then every formula of T^{R} is provably equivalent to a T formula of the same level of syntactic complexity, and so if all of T ’s general axiom schemas are applicable to “all Σ_{i}^{b} formulæ”, then T^{R} is a conservative extension of T.

4.3 Multi-variable induction

The various induction schemes of section 2.4 all apply to only one variable. It is often convenient (especially when Σ_{1}^{b}-defining a function of several arguments) to induct on two or more variables at once. [CU93] shows that IS_{2}^{1} can prove the validity of multi-variable PIND, by interleaving the bits of several variables into one. We shall do much the same in R_{2}^{1}, although we must change the method of interleaving to work for DCI. For simplicity, we define multi-variable induction only up to terms whose length is a power of two; this will suffice for our purposes, and ensures that repeatedly applying Bh and Fh to said term produces a full, balanced binary tree.

First we Σ_{1}^{b}-define a function Ins_{1} in R_{2}^{1}. This function takes a number and produces a number of exactly twice the dyadic length, formed by inserting a 1 digit after each dyadic digit of the original number. It has the Σ_{1}^{b} graph

φ(x, y) ⇔ |y| = 2 · |x| ∧ (∀i < |x|)(Bit(2 · i, y) = Bit(i, x) ∧ Bit(2 · i −^{.} 1, y) = 1).

The existence of such a y can be proven in R_{2}^{1} by a straightforward DCI on x, and so the Ins_{1} function may be added conservatively to the language of R_{2}^{1}.

We can likewise Σ_{1}^{b}-define functions OddBits and EvenBits, which extract the odd- and even-numbered bits of their one argument respectively; details are left to the reader. We then define (by composition) RotRight(x) = Conc(1, Msp(x, 1)) and Interleave(x, y) = Ins_{1}(x) + RotRight(Ins_{1}(x)) −^{.} (x#3). One can prove, without induction, that

|x| = |y| ⊃ OddBits(Interleave(x, y)) = x,
|x| = |y| ⊃ EvenBits(Interleave(x, y)) = y,
|x| = |y| ⊃ Bh(Interleave(x, y)) = Interleave(Bh(x), Bh(y)), and
|x| = |y| ⊃ Fh(Interleave(x, y)) = Interleave(Fh(x), Fh(y)).

If we wish to induct on the variables x_{1} and x_{2} at once in the Σ_{i}^{b} formula A(x_{1}, x_{2}, y⃗), we can do so by defining B(x, y⃗) as the Σ_{i}^{b} formula

(PwrTwo(|x|) ∧ |x| ≠ 1) ⊃ A(OddBits(x), EvenBits(x), y⃗),

and inducting on B instead (up to any value whose length is an even power of two). The precise definition of 2-variable DCI, omitting the free variables b⃗ which may appear anywhere, is

Γ, A(Bh(a_{1}), Bh(a_{2})), A(Fh(a_{1}), Fh(a_{2})) ⟶ A(a_{1}, a_{2}), Δ ; Γ, A(0, 0), A({1, 2}×{1, 2}), |t_{1}| = |t_{2}|, PwrTwo(|t_{1}| ⟶ A(t_{1}, t_{2}), Δ

Note that, in order for two-variable DCI to be valid, all five base cases A(0, 0, b⃗), A(1, 1, b⃗), A(1, 2, b⃗), A(2, 1, b⃗), and A(2, 2, b⃗) must hold. The base case A(0, 0, b⃗) implies B(0, b⃗). The other two base cases of B induction, B(1, b⃗), and B(2, b⃗), are vacuous, and the remaining four A base cases are used to prove the length 2 cases of B(Bh(x), b⃗), B(Fh(x), b⃗) ⟶ B(x, b⃗).

Once we can induct on two variables at once, the process can be iterated to handle any fixed number of variables.

4.4 Rounding Lengths

We define a sequence of fast-growing (by bounded arithmetic standards) functions RoundUp_{j}(x) inductively as follows:

RoundUp_{−1}(x) = x
RoundUp_{j+1}(x) = 2(2^{RoundUp_{i}(|x|)} − 1)

If RoundUp_{j+1} is provably total in R_{k}^{1}, it is clear (in R_{k}^{i}) that |RoundUp_{j+1}(x)| = RoundUp_{i}(|x|), that RoundUp_{j+1}(x) ≥ x, and that for j ≥ 0, all the dyadic digits of RoundUp_{j}(x) are 2’s (which implies for j ≥ 1, all the digits of |RoundUp_{j}(x)| are 2’s; for j ≥ 2, all the digits of ||RoundUp_{j}(x)|| are 2’s; and so on.) Furthermore, RoundUp_{0}(x) is the largest value y such that |y| = |x|; RoundUp_{1}(x) is the largest value y such that ||y|| = ||x||; and so on.

The functions can be explicitly bounded as follows:

RoundUp_{−1}(x) ≤ x
|RoundUp_{0}(x)| ≤ |x|
RoundUp_{0}(x) ≤ 2x
|RoundUp_{1}(x)| ≤ 2|x|
RoundUp_{1}(x) ≤ (x + 1)^{2}
|RoundUp_{2}(x)| ≤ (|x| + 1)^{2}
RoundUp_{2}(x) ≤ (2x + 1)#_{2}(2x + 1)
|RoundUp_{3}(x)| ≤ (2|x| + 1)#_{2}(2|x| + 1)
RoundUp_{3}(x) ≤ (2(x + 1)^{2})#_{3}(2(x + 1)^{2})
⋮

Without writing a precise general formula, it should be clear that RoundUp_{k} is bounded by an L_{k} term, for all k ≥ 1. So we may at least hope to Σ_{1}^{b}-define RoundUp_{k} in IR_{k}^{1}.

The RoundUp_{−1} and RoundUp_{0} functions have closed-form definitions, but we also point out, to get us started, that

RoundUp_{0}(x) = y ⇔ |y| = |x| ∧ (∀i < |y|)(Bit(i, y) = 2).

Then the remaining functions have graphs RoundUp_{1}(x) = y ⇔ ||y|| = ||x||∧ (∀i < ||y||)(Bit(i, |y|) = 2∧ (∀i < |y|)(Bit(i, y) = 2); RoundUp_{2}(x) = y ⇔ |||y||| = |||x|||∧ (∀i < |||y|||)(Bit(i, ||y||) = 2)∧ (∀i < ||y||)(Bit(i, |y|) = 2)∧ (∀i < |y|)(Bit(i, y) = 2), and so on. Clearly, all these graphs are Σ_{0}^{b}.

For j ≤ k, R_{k}^{1} can Σ_{1}^{b}-define RoundUp_{j} by first Σ_{1}^{b}-defining RoundUp_{j−1} and then proving that RoundUp_{j−1}(|x|) is bounded by a suitable sharply-bounded term in L_{k}; then 2^{RoundUp_{j−1}(|x|)} exists and the rest is trivial. Details are left to the reader.

The principal application for these functions in the present paper is to construct suitable values for multi-variable induction. For example, if y = RoundUp_{1}(x), then y ≥ x and PwrTwo(|y|+2), so if we let z = 4y +3, we can conclude |z| = |y|+2 and hence PwrTwo(|z|).

4.5 Comprehension and Extensionality

Theorem 4.4 R_{2}^{1} ⊢ x ≠ y ↔ (∃i < max(|x|, |y|))(Bit(i, x) ≠ Bit(i, y)).

This makes it easy to prove the single-valuedness of functions defined bitwise.

Proof: The ← direction is trivial by equality axioms. For the → direction, we Σ_{1}^{b}-define a function BitDiff(x, y), which returns 0 for x = y, and for x ≠ y returns the largest i such that Bit(i −^{.} 1, x) ≠ Bit(i −^{.} 1, y).

The BitDiff function has an obvious graph: BitDiff(x, y) = i ⇔ (x = y ∧ i = 0)∨ (Bit(i −^{.} 1, x) ≠ Bit(i −^{.} 1, y) ∧ (∀i < j ≤ max(|x|, |y|))(Bit(j −^{.} 1, x) = Bit(j −^{.} 1, y)))). The function thus defined is patently single-valued, by trichotomy. To prove that it’s total, first observe that if |x| ≠ |y|, then i = max(|x|, |y|) satisfies the requirements (since Bit(i, min(x, y)) = 0 ≠ Bit(i, max(x, y))).

Otherwise, |x| = |y|. We’d like to reason by 2-variable DCI, which only applies to values whose length is a power of 2. Observe that if we let x′ = Conc(Msp(4·RoundUp_{1}(x)+6, |x|), x) and y′ = Conc(Msp(4 · RoundUp_{1}(y) + 6, |y|), y), i.e. x and y padded on the left with 2’s up to length a power of 2, then any correct value for BitDiff(x′, y′) is also a correct value for BitDiff(x, y).

If x′ = y′ = 0, x′ = y′ = 1, or x′ = y′ = 2, then BitDiff(x′, y′) = 0.

If x′ = 1, y′ = 2 or vice versa, then BitDiff(x′, y′) = 1.

For |x′| > 1, assume BitDiff(Fh(x′), Fh(y′)) = i_{1} and BitDiff(Bh(x′), Bh(y′)) = i_{2}. If i_{1} ≠ 0, then i = i_{1} + |Bh(x′)| works; otherwise Fh(x′) = Fh(y′), so their corresponding bits are equal by equality axioms, so i = i_{2} works.

For another example of 2-variable DCI, R_{2}^{1} can Σ_{1}^{b}-define the OR function, which returns the bitwise disjunction of its two arguments, treating the dyadic digits 1 and 2 as f and t respectively, and assuming its arguments are of the same, power-of-2, length. OR is proven total by a straightforward DCI in two variables, and single-valued by Theorem 4.4.

We can now Σ_{1}^{b}-define a function named CountDown, which takes an argument z such that PwrTwo(||z||) (a restriction for technical reasons) and returns the concatenation, in reverse lexicographic order, of all 2^{||z||} dyadic numbers of length ||z||. It has the Σ_{0}^{b} graph CountDown(z) = w ⇔ PwrTwo(||z||) ⊃ (|w| = 2^{||z||} · ||z|| ∧ (∀i < 2^{||z||})(Substr(w, i · ||z||, ||z||) = i + 2^{||z||} − 1)). To define it, we first define several auxiliary functions.

• f_{1}(z, s) = w ⇔ (¬PwrTwo(|s|) ∧ w = 0)∨ (PwrTwo(|s|) ∧ |w| = 2^{||z||} · |s| ∧ (∀i < 2^{||z||})(∀j < |s|)(Bit(i · |s| + j, w) = 2 ↔ j = ||z||)) can be proven total by DCI on z. Clearly f_{1}(0, s) = 0 and f_{1}(1, s) = f_{1}(2, s) = (s#_{2}1) + 1. For larger z, let w′ = f_{1}(Bh(z), s). Then w = Conc(Shl(w′, 1), Shl(w′, 1)) satisfies the definition. Single-valuedness, for |s| a power of 2, is proven by Theorem 4.4; for |s| not a power of 2 it is trivial.

• f_{2}(z, s) = w ⇔ (¬PwrTwo(|s|) ∧ w = 0)∨ (PwrTwo(|s|) ∧ |w| = 2^{||z||} · |s| ∧ (∀i < 2^{||z||})(Substr(w, i · |s|, |s|) = i + (s#_{2}1))) can likewise be proven total by DCI on z. It is clear that f_{2}(0, s) = 0 and f_{2}(1, s) = f_{2}(2, s) = (s#_{2}1). For larger z, let w_{1} = f_{1}(Bh(z), s) and w_{2} = f_{2}(Bh(z), s). Then w = Conc(OR(w_{1}, w_{2}), w_{2}) satisfies the requirements. Single-valuedness is shown as before.

Now CountDown(z) can be defined, for ||z|| a power of 2, simply as f_{2}(z, |z|#_{2}1). I leave it for the reader to see how this all works.

The following theorems are all straightforward generalizations of theorems in [All91]:

• Given a Δ_{i}^{b} predicate A(x, y⃗), R_{k}^{i} Σ_{i}^{b}-defines the function f_{A}(z, y⃗) whose |z| bits indicate the truth values of A(0), A(1), …, A(|z| − 1).

• R_{k}^{i} Σ_{1}^{b}-defines efficient functions for encoding and decoding sequences, predicates for testing sequence-hood, and bounds for the size of encoded sequences.

• Successive bounded existential (respectively universal) quantifiers can be collapsed into one, provably in R_{k}^{i}.

• R_{k}^{i} proves Δ_{i}^{b}-replacement, i.e. if s and t are any terms not involving x or y, then (∀y ≤ |s|)(∃x ≤ t)ϕ(a⃗, x, y) implies (∃w)(∀y ≤ |s|)(β(w, y) ≤ t ∧ ϕ(a⃗, β(w, y), y)), where β is a sequence decoding function.

5 The Buss-Krajíček-Takeuti characterization

In [BKT93] is a characterization of the Σ_{i,3}^{b}-definable functions of R_{3}^{i}. The computational model in that paper uses “witnessing oracles”, which answer an existential query either with “no” or by providing a satisfying value (of quasipolynomial length) for the outermost existential quantifier. Since there may be multiple possible witnesses to a given existential question, the functions defined by invoking these witnessing oracles may be multi-valued. Nevertheless, in certain cases this computational model is equivalent to the parallel model of the present paper.

The main result of this section, Theorem 5.4, is that the function class FP_{3}^{Σ_{i−1}^{p}}[wit, log^{O(1)}] of [BKT93], restricted to single-valued functions, is precisely □_{i,3}^{c}. The author originally proved this indirectly, using results of [BKT93] and a flawed version of Theorem 6.1, but then, on a suggestion of S. Buss, discovered the direct (and, incidentally, valid!) proof presented here.

5.1 Background

Definition 5.1 (Buss, Krajíček, Takeuti) A multi-valued function f is computable in FP_{3}^{Σ_{i−1}^{p}}[wit, log^{O(1)}] iff there is a Turing machine that runs in quasipolynomial time and makes at most polylog many queries to a fixed Σ_{i−1}^{p} witnessing oracle, such that for all x, M outputs one of the values of f(x).

The notation FP_{3}^{Σ_{i−1}^{p}}, without the stuff in brackets, is what I call □_{i,3}^{p}. Note that the oracle may (in my notation) be Σ_{i−1,k}^{p} for any k ≤ 3, without changing the class thus defined: the machine making the query can precompute the quantifier bounds and pass them to the oracle as extra parameters.

Definition 5.2 (Buss, Krajíček, Takeuti) A multi-valued function f is weakly Σ_{i}^{b}-defined by theory T iff for some Σ_{i}^{b} formula A,

• T ⊢ (∀x)(∃y)A(x, y), and

• if A(n, m) holds in the natural numbers, then m is a value of f(n).

The following theorem was stated in [BKT93] only for k = 3 (with “log^{O(1)}” in place of “||L_{k}||”), but their proof generalizes easily to larger k.

Theorem 5.3 (Buss, Krajíček, Takeuti) For i ≥ 2, k ≥ 3, for any multi-valued function f, the following are equivalent:

• f ∈ FP_{k}^{Σ_{i−1,k}^{p}}[wit, ||L_{k}||]

• f is weakly Σ_{i,k}^{b}-defined by theory R_{k}^{i}

• f is weakly Σ_{i,k}^{b}-defined by theory S_{k}^{i−1}

(Note that the second requirement in Defn. 5.2 does not say “if and only if”. Buss, Krajíček, and Takeuti also defined a class called “strong FP_{3}^{Σ_{i−1}^{p}}[wit, log^{O(1)}]” and a notion of “strong Σ_{i}^{b}-definability” using “if and only if”, and proved these equivalent as well, but the difference is only relevant for multi-valued functions and so we shall ignore it henceforth.)

5.2 FP_{k}^{Σ_{i−1,k}^{p}} coincides with □_{i,k}^{c}: the k ≥ 3 case

Theorem 5.4 For i ≥ 2 and k ≥ 3, the restriction of FP_{k}^{Σ_{i−1,k}^{p}}[wit, ||L_{k}||] to single-valued functions is □_{i,k}^{c}.

Proof: (⊇): Suppose F ∈ □_{i,k}^{c}. Then F is computable by a uniform □_{i,k}^{c} circuit family with Σ_{i−1,k}^{p} yes/no oracle ρ.

With at most a constant factor increase in depth, we can assume that the circuit family is levelled, all output gates are at level 0, each even level contains no oracle gates, and each odd level consists entirely of oracle gates. (The last restriction requires excluding constantvalued ρ.) Embed the resulting gates in a rectangular array, indexed by row and column (r, c), in such a manner that a gate’s position in the array easily determines its gate number and thence its type. (For example, give every gate at an even level exactly two children, one or both of which it may ignore, and give every gate at an odd level exactly |t| children. Gate (r, c) is descended from output gate ⌊\frac{c}{(2|t|)^{r/2}} ⌋ or ⌊\frac{c}{2(2|t|)^{(r−1)/2}} ⌋, as r is even or odd respectively, by a path formed by repeatedly modding out 2 and |t| alternately. If |t| is first rounded up to a power of 2, all this is computationally trivial — c’s binary form is the concatenation of the output gate number and the path.) Thus the resulting circuit family is still U_{E^{∗}} uniform.

The output of gate (r, c) can be described by a single Σ_{i−1,k}^{p} relation σ(n, r, c, b⃗) where n is the input size and b⃗ are the outputs of row r + 1. (The relation σ simply determines the type of gate (r, c) and simulates it; the most complex case is that of an oracle gate, which is Σ_{i−1,k}^{p}.) Define ϕ(n, r, b⃗, j) to be the formula

(∃|w| = width of row r)(|w|_{1} ≥ j) ∧ (∀c < |w|)(Bit(c, w) ⊃ σ(|x|, r, c, b⃗))),

where |w|_{1} represents the number of 1’s in w. The ϕ relation is Σ_{i−1,k}^{b} (note i ≥ 2), and monotone in j, so for any fixed x, we can find the maximum j satisfying ϕ by binary search in ||L_{k}|| time. For this maximum j, the only possible witness w is the string representing exactly the values of all the gates at level r (assuming b⃗ correctly represents the values of all the gates at level r + 1), because the clause (∀c < |w|)(Bit(c, w) ⊃ σ(|x|, r, c, b⃗)) ensures that all the gates whose bit in w is 1 are correctly computed, and if any gate whose bit in w is 0 were incorrectly computed, j wouldn’t be maximal.

Thus ||L_{k}|| ϕ-queries, the last one witnessing, suffice to determine the outputs of all gates at level r from the outputs of all gates at level r + 1. Iterating this over the ||L_{k}|| levels, starting with the input, allows us to compute the correct values of all the gates at the output level, and thus the value of the function F.

(⊆): Suppose f ∈ FP_{k}^{Σ_{i−1,k}^{p}}[wit, ||L_{k}||] and f happens to be single-valued. As shown in [BKT93], we can assume without loss of generality that the quasipolynomial-time machine only uses an ordinary yes/no oracle until its last query, at which point it demands a witness. Furthermore, we can assume without loss of generality that it doesn’t demand this witness until it has confirmed by yes/no query that there is one.

Let formula ψ(x, w) assert that there is a computation of the FP_{k} machine (up to the time that it demands a witness) in which

• the computation starts with x on the input,

• for all j, if the j-th most significant bit of w is 1, then the j-th oracle query in the computation answers “yes”,

• the behavior of the machine is consistent with the alleged tape contents and alleged oracle answers in the computation, and

• all the “yes” oracle answers (at most ||L_{k}||) in the computation are correct.

The formula ψ(x, w) is Σ_{i−1,k}^{b} (note i ≥ 2), consisting of a bounded existential quantifier around some sharply-bounded universal quantifiers around a Σ_{i−1,k}^{p} oracle. Furthermore, ψ is monotone in each bit of w. Since w has only ||L_{k}|| many bits, we can find the lexicographically maximum w satisfying ψ by deterministic binary search. Having found this w, for each output bit r in parallel we query the Σ_{i−1,k}^{p} oracle ψ′(x, w, r), which asserts that there is a computation in which

• the computation starts with x on the input,

• for all j, the j-th most significant bit of w is exactly the answer to the j-th oracle query in the computation,

• the behavior of the machine is consistent with its alleged tape contents and the alleged oracle answers,

• all the “yes” oracle answers in the computation are correct, and

• there exists a witness to the final query that leads the machine to output a value with bit r set.

By maximality of w, there is a unique and correct such computation until the final witnessing query. Since we assumed f was single-valued, all the output bits will be consistent, even if the circuits to compute different bits happen to find different witnesses to the final oracle query.

Technically, a □_{i,k}^{c} circuit family contains only one oracle, and we have used oracle gates for both ψ and ψ′. But as usual, both can be replaced by oracles for your favorite Σ_{i−1,k}^{p}- complete problem (under □_{1,k}^{c} reductions). Thus f ∈ □_{i,k}^{c}.

5.3 The k = 2 case

[Kra93] shows that the predicates in P^{Σ_{i−1}^{p}}[O(log)] (i.e., P with O(log) queries to a Σ_{i−1}^{p} oracle) are those Σ_{i}^{b}-definable in S_{2}^{i−1}. His technique actually uses FP^{Σ_{i−1}^{p}}[wit, O(log)], but the restriction to predicates rather than functions allows him to eliminate the witnessing and multivaluedness at the last moment. Thus in the notation of [BKT93], he essentially proved

Theorem 5.5 (Krajíček) For i ≥ 2, for any multi-valued function f, the following are equivalent:

• f ∈ FP^{Σ_{i−1,2}^{p}}[wit, O(log)]

• f is weakly Σ_{i,2}^{b}-defined by theory S_{2}^{i−1}

Interestingly enough, the proof of Theorem 5.4 can be adapted for k = 2:

Theorem 5.6 For i ≥ 2, the restriction of FP^{Σ_{i−1}^{p}}[wit, O(log)] to single-valued functions is □_{i,2}^{c}.

Proof: The proof of Theorem 5.4 relies on k ≥ 3 in several ways, but these can all be fixed.

(⊇): The previous proof takes ||L_{k}|| time to do a binary search for each of the ||L_{k}|| rows of the array. Since ||L_{2}|| is not closed under multiplication, we can no longer afford this. However, by our convention, for some term t ∈ L_{2}, each oracle gate has “depth” ||t|| = θ(log(n)) (recall that t is nontrivial). But a □_{i,2}^{c} circuit has depth O(log(n)), so there must be a constant bound d on the number of oracle gates along any one path. Arrange the array in d meta-layers, each containing one row of oracle gates and O(log) rows of ordinary gates. We define a Δ_{0,2}^{c} relation σ′(n, r, c, b⃗) that does the same thing as σ for rows containing only ordinary gates. We then define a Σ_{1,2}^{p} relation ϕ′(n, r, b⃗) by (∃|w| = width of row r)(∀c < |w|)(Bit(c, w) ↔ σ′(|x|, r, c, b⃗))). The algorithm is then as before, but for ordinary rows we simply make a witnessing query to ϕ′ rather than doing a binary search on ϕ.

(⊆): We can still assume that an FP^{Σ_{i−1}^{p}}[wit, O(log)] machine demands witnesses only on its final query, by a lemma in [Kra93]. The rest of the proof is unaltered.

Note that Theorems 5.4 and 5.6 are unlikely to be improved to i = 1: in the latter case, such a result would imply P = ALOGT IME.

5.4 Applications and extensions

Corollary 5.7 For i ≥ 2, k ≥ 2,

Δ_{i,k}^{c} = P_{k}^{Σ_{i−1}^{p}}[||L_{k}||].

In other words, DT IME(|L_{k}|) with ||L_{k}|| queries to a Σ_{i−1}^{p} oracle is equal to AT IME(||L_{k}||) with unlimited queries to the same oracle.

This provides a new proof of, and generalizes, a result of [BH91].

Corollary 5.8 For i ≥ 2, k ≥ 2, the single-valued functions weakly Σ_{i,k}^{b}-definable in S_{k}^{i−1} are precisely □_{i,k}^{c}.

We can in fact improve on Corollary 5.8 by eliminating the word “weakly”. The following direct proof shows that the □_{i,k}^{c} functions can actually be Σ_{i,k}^{b}-defined in the usual, singlevalued sense in S_{k}^{i−1}.

Lemma 5.9 For i ≥ 2, k ≥ 2, S_{k}^{i−1} can Σ_{i,k}^{b}-define all the □_{i,k}^{c} functions.

Proof: Let f ∈ □_{i,k}^{c}. Then f is computed by some U_{E^{∗}}-uniform circuit family of genus k circuits with a fixed Σ_{i−1,k}^{p} oracle X. The existence of a computation to construct and simulate this circuit, with correct oracle queries, is certainly Σ_{i,k}^{b}, but we must show that S_{k}^{i−1} can prove both existence and uniqueness of the result. I’ll describe the algorithm first, then formalize it in S_{k}^{i−1}. First, assume the circuits are treelike (which is OK for □_{i,k}^{c}) and levelled. We’ll scan from left to right across the leaf layer, at each step computing the values of all the gates in the whole circuit whose descendant leaves are among the ones we’ve visited. For each leaf, this requires adding on at most the unique path from that leaf to the root, which is length ||L_{k}||, and we can find the lexicographically maximum (and hence correct) string of this length.

More formally, let Anc(r, x) be the number of gates in the circuit for x, all of whose descendant leaves are numbered r or lower. Define InfoTuple(w, r, x) to be the Σ_{i−1}^{b} formula asserting that

• w is an r-tuple of bit strings of lengths Anc(1, x), Anc(2, x) − Anc(1, x),…,Anc(r, x) − Anc(r − 1, x) respectively, and

• for all j < |w_{r}|, if the j-th most significant bit of w_{r} is t, then the j-th ancestor gate of leaf r outputs t when given input as specified in w.

Thus InfoTuple asserts that w is a possible assignment of values to the ancestors of leaves 1, …, r, in which at least all the “yes” answers are correct for their presumed inputs.

Define GtrTuple(w, w′) to be a Δ_{0}^{b} formula asserting that for some r, r′,

• w and w′ are tuples of r and r′ elements respectively,

• r ≥ r′,

• (∀j < r′)(w_{j} ≥ w′_{j}), and

• (r > r′) ∨ (∃j < r′)(w_{j} > w′_{j}).

That is, each bit-string entry of w, treated as a dyadic number, is at least as great as the corresponding entry of w′, and either at least one entry of w is greater than the corresponding entry of w′ or w is longer than w′.

Now define InfoSeq(W, r, x) to be the Σ_{i−1}^{b} formula^{3} asserting that • W is a sequence of exactly r tuples,

3this may look Π_{i}^{b}, but in practice r ≤ |W | so the universal quantifiers can be made sharply bounded.

• (∀j < r)InfoTuple(W_{j}, j, x), and

• (∀j < r − 1)GtrTuple(W_{j+1}, W_{j}).

By LIND on (∃W, r)InfoSeq(W, r, x), S_{k}^{i} can prove there is a maximum-length W satisfying InfoSeq(W, r, x) with r bounded by the number of leaves in the circuit; note that each tuple has |L_{k}| entries, each entry is bounded in numeric value by |L_{k}|, and each tuple in such a sequence must have a distinct set of entries. Let w denote the last element of this maximum-length W. It must contain a bit-string for each leaf, or w (and therefore W) could be extended by adding on a string of zeroes for the next leaf. The first bit-string, w_{1}, must have the maximum possible value consistent with input x, or W could be extended by increasing w_{1}. Thus all the “no” answers in w_{1} must be correct. Similarly, w_{2} must have the maximum possible value consistent with x and w_{1}, and so on; after |L_{k}| steps we conclude that every gate value in w is correct. Extracting the value of the function is then straightforward.

Since every step in the above algorithm is clearly single-valued, and the loop implicit in the above paragraph has at most |L_{k}| iterations, S_{k}^{i−1} proves the uniqueness of this value.

Corollary 5.10 For i ≥ 2, k ≥ 2, the single-valued functions Σ_{i,k}^{b}-definable in S_{k}^{i−1} are precisely □_{i,k}^{c}.

Corollary 5.11 For i ≥ 2, k ≥ 2, if T_{k}^{i−1} is conservative over S_{k}^{i−1} with respect to ∀∃Σ_{i,k}^{b} sentences ( i.e. if S_{k}^{i−1} ≡ T_{k}^{i−1}), then □_{i,k}^{c} = □_{i,k}^{p}.

6 Links to Bounded Arithmetic

In [Blo95a], I stated that □_{i,k}^{c} comprised exactly the functions Σ_{i,k}^{b}-definable in R_{k}^{i}. I am no longer convinced that □_{i,k}^{c} realizes all R_{k}^{i} proofs. However, in this section we prove that □_{i,k}^{c} is at least contained in the set of functions thus definable.

Theorem 6.1 For i ≥ 1, k ≥ 3, any single-valued function f ∈ □_{i,k}^{c} is Σ_{i,k}^{b}-definable in R_{k}^{i}. For i ≥ 1, k = 2, any single-valued function f ∈ FN C^{Σ_{i−1,2}^{p}} is Σ_{i,2}^{b}-definable in R_{2}^{i}.

This is proven by methods similar to those in [Bus86a, All91]. First, □_{i,k}^{c} (respectively FN C^{Σ_{i−1,2}^{p}}) is equal to a certain recursively-defined function algebra. Second, the base functions of this algebra are Σ_{i}^{b}-definable in R_{k}^{i}, and the operators preserve such Σ_{i}^{b}-definability, so any function in the algebra is Σ_{i}^{b}-definable in R_{k}^{i}.

6.1 A function algebra

We define a hierarchy of function algebras {A_{i,k}}_{i≥0,k≥2} by applying two simple operations to a fixed collection of base functions on the universe { f, t}^{∗}, which we identify with the natural numbers as described in section 2.1.

Definition 6.2 The BASE functions are the following:

• the constant functions f, t, and λ, which return the single-bit strings f and t and the empty string ( i.e. the dyadic numbers 1, 2, and 0), respectively;

• LSP(x, y), the rightmost |y| bits of x, or simply x if |y| > |x|.

• MSP(x, y), all but the rightmost |y| bits of x, or the empty string ( i.e. 0) if |y| > |x|.

• BIT(i, x), the i-th rightmost bit of x (treating i as a dyadic number),

• COND(w, x, y, z) = \{ \begin{matrix}x & if w = λ \\ y & if LSP(w, 1) = f \\ z & if LSP(w, 1) = t \end{matrix}

• CONC(x, y), the concatenation of x and y,

• BH(x), the rightmost ⌊\frac{|x|}{2}⌋ bits of x,

• FH(x), the leftmost ⌈\frac{|x|}{2}⌉ bits of x,

• NOT(x), the bitwise complement ^{4} of x,

• OR(x, y), the bitwise disjunction of x and y (undefined if |x| ≠ |y|), • AND(x, y), the bitwise conjunction of x and y (undefined if |x| ≠ |y|),

4which can also be written numerically as 3 · (2^{|x|} −^{.} 1) −^{.} x. Obviously, the bitwise definition is clearer.

We shall not even attempt to give numerical definitions of OR, AND, INS f, or INS t!

• INS f(x), a string exactly twice as long as x such that for all i < |x|, we have BIT (2i, INS f(x)) = f and BIT (2i + 1, INS f(x)) = BIT(i, x),

• INS t(x), defined analogously with BIT (2i, INS t(x)) = t.

Note that the functions MSP and LSP behave somewhat differently from their namesakes in Section 2.2. MSP and LSP consider only the length of their second argument, rather than treating the argument itself as a dyadic number. As a result, all the BASE functions have length determined by the lengths of their arguments (which makes it easier to envision multi-output circuit families computing them).

Definition 6.3 A function f is defined by |L_{k}|-bounded divide-and-conquer recursion (or DCR) from functions g and h if there is a term t ∈ L_{k} such that

f(z, b, x⃗) = \{ \begin{matrix}g(z, x⃗) & if |z| ≤ |b|, \\ h(z, b, x⃗, f(FH(z), b, x⃗), f(BH(z), b, x⃗)) & otherwise, \end{matrix}

and |f(z, b, x⃗)| ≤ |t(z, b, x⃗)| for all z, b, x⃗.

Note that this form of recursion does not necessarily go all the way down to 0; instead, the extra parameter b tells it when to bottom out. This extra parameter appears necessary in order to do many useful things with DCR; see [Blo94].

We extend this notion of divide-and-conquer recursion in the obvious way to define constantly many functions by simultaneous recursion:

Definition 6.4 Functions f_{1}, …, f_{j} are defined by simultaneous |L_{k}|-bounded divide-and-conquer recursion from functions g_{1}, …, g_{j} and h_{1}, …, h_{j} if there is a term t ∈ L_{k} such that for all 1 ≤ i ≤ j,

f_{i}(z, b, x⃗) = \{ \begin{matrix}g_{i}(z, x⃗) & if |z| ≤ |b|, \\ h_{i}(z, b, x⃗, f⃗(FH(z), b, x⃗), f⃗(BH(z), b, x⃗)) & otherwise, \end{matrix}

and |f_{i}(z, b, x⃗)| ≤ |t(z, b, x⃗)| for all z, b, x⃗.

Don’t confuse this with the multi-variable induction defined in section 4.3. First, this is a recursion scheme for defining functions, rather than an induction scheme for proving theorems. Second, this recursion scheme still applies to only one variable at once; it is called “simultaneous” because it defines several functions in parallel, in terms of one another.

Definition 6.5 The function algebra A_{i,k} is the closure of BASE and the 1-bit characteristic functions of Σ_{i−1,k}^{c} relations^{5} under the operations of composition and simultaneous |L_{k}|- bounded DCR.

5where Σ_{−1,k}^{p} is by convention {}

For example, we define a function COUNTUP(z) ∈ A_{0,2} which produces the concatenation of all 2^{||z||} bit-strings of length ||z||, in lexicographic order. (This example not only shows some of DCR’s power, but proves useful later on.)

Let SHL(x, y) = LSP(CONC(x, y), x); this appends y to x, discarding high bits so the result still has length |x|.

Let FALSES(x) = AND(x, NOT(x)), a string of |x| f’s.

Let

LENGTH′(x) = \{ \begin{matrix}λ & if |x| = 0 \\ CONC(LENGTH′(BH(x))), 1) & otherwise; \end{matrix}
LENGTH(x) = MSP(LENGTH′(CONC(x, 1)), 1)

LENGTH(x) is a string of 1’s of the same length as the dyadic representation of |x|; equivalently, LENGTH(x) is ||x|| written in unary.

Let

MASK(z, b) = \{ \begin{matrix}λ & if |z| = 0 \\ SHL(FALSES(b), 2) & if |z| = 1 \\ CONC(SHL(MASK(BH(z), b), 1), SHL(MASK(BH(z), b), 1)) & if |z| > 1, \end{matrix}

AUX(z, b) = \{ \begin{matrix}λ & if |z| = 0 \\ FALSES(b) & if |z| = 1 \\ CONC(AUX(BH(z), b), OR(MASK(BH(z), b), AUX(BH(z), b))) & if |z| > 1, \end{matrix}

and finally COUNTUP(z) = AUX(z, LENGTH(z)). I leave seeing how this works as an exercise for the reader.

Lemma 6.6 For i ≥ 0 and k ≥ 3, □_{i,k}^{c} = A_{i,k}. For i ≥ 0 and k = 2, □_{i,k}^{c} ⊆ A_{i,k} ⊆ FN C^{Σ_{i−1,k}^{p}}.

Proof: (A_{i,k} ⊆ □_{i,k}^{c} or F NC^{Σ_{i−1,k}^{p}}): For i = 0, all the BASE functions are clearly in □_{0,k}^{c}. By Lemma 3.5, □_{0,k}^{c} is closed under composition, and it is not hard to see that it’s closed under |L_{k}|-bounded DCR too. (This requires k ≥ 3 so circuit depth is closed under multiplication. For the k = 2 case, since FN C is closed under polynomial-bounded DCR [All91], we can conclude A_{0,2} ⊆ FN C.)

For i > 0, recall that the characteristic functions of Σ_{i−1,k}^{p} relations are in □_{i,k}^{c} (and FN C^{Σ_{i−1,k}^{p}}) by definition. The proof that A_{i,k} ⊆ □_{i,k}^{c} (or for k = 2, A_{i,2} ⊆ FN C^{Σ_{i−1,2}^{p}}) is almost exactly as before.

(□_{i,k}^{c} ⊆ A_{i,k}): First, note that it suffices to get Δ_{i,k}^{c} ⊆ A_{i,k}. Suppose f ∈ □_{i,k}^{c}; then its bit-graph is in Δ_{i,k}^{c} (and hence, as we shall show, in A_{i,k}). To get the whole function value at once, we use COUNTUP(f(x⃗)) to build a list, in lexicographic order, of all the ||f(x⃗)||-bit strings. Interpreting these in binary would give a list of the numbers 0, 1, …, 2^{||f(x⃗)||}−1, which we could use as inputs to the bit-graph to get the individual bits, then concatenate them all together with a DCR on CONC. The technique is spelled out in more detail in [Blo94].

Unfortunately, we’ve defined BIT and bit-graphs to interpret the bit position as dyadic, and COUNTUP(f(x⃗)) interpreted as a list of dyadic numbers gives 2^{||f(x⃗)||}−1, …, 2^{||f(x⃗)||+1}−2. We get around this by using not the bit-graph of f itself, but rather the bit-graph of f̂(x⃗) = f(x⃗)) f^{2^{||f(x⃗)||}−1}, i.e., f with 2^{||f||} − 1 f’s appended at the end; this is no problem for the U_{E^{∗}} uniformity criterion, so f̂ is still □_{i,k}^{c} and the above reasoning goes through.

(Δ_{i,k}^{c} ⊆ A_{i,k}): For i = 0, suppose f(x⃗) ∈ Δ_{0,k}^{c} (which is simply ATIME(||L_{k}||)). At the cost of a constant factor in time, we can assume the ATM is strictly alternating between existential and universal states and that it accesses its input tape only at leaves. In [Blo94], the author showed how to simulate the computation of such an ATM within a function algebra similar to A_{0,k}. In brief: A_{0,k} can construct a binary tree data structure called PATHS, each of whose leaves contains an encoding of the path from the root to that leaf. This binary tree represents the computation tree of the ATM, so we define a function EVALTREE by constant-bounded DCR on the tree, bottoming out upon reaching a single leaf, to combine the accept/reject decisions of the various ATM configurations into one. When this recursion bottoms out, we apply another function EVALLEAF, defined by |L_{k}|-bounded simultaneous DCR to compute the state and the contents of all the work tapes in parallel, to the encoded path to determine the ATM configuration at the corresponding leaf of the computation tree and decide whether it accepts. Thus Δ_{0,k}^{c} ⊆ A_{0,k}.

The i > 0 case is a little more complex, and the k = 2 case of it must be treated separately. For k ≥ 3, recall from Lemmas 2.19 and 3.8 that every □_{i,k}^{c} function’s bit-graph is in ATIME(||L_{k}||) with oracle states for Σ_{i−1,k}^{p} relations. At the cost of a ||t|| factor in time, we assume the levels of the ATM rotate strictly among universal, existential, exclusive-or, and oracle states. Let t denote the bounding term for all the oracle states in the machine, rounded up so that |t| is a power of 2. We construct a PATHS tree of depth equal to the time bound of the ATM (counting oracles as taking ||t|| time, as usual), and apply a modified version of EVALTREE, which at its base (i.e. a single leaf) invokes the EVALLEAF function exactly as for i = 0.

As defined in [Blo94], EVALTREE returned a bit indicating whether a certain subtree of the ATM’s computation tree accepted or rejected. In this setting, it will ultimately do the same, but it may have intermediate values up to |t(x)| bits long. The following algorithm describes the recursive phase of EVALTREE:

let v_{1} and v_{2} be EVALTREE(FH(T), b, x) and EVALTREE(BH(T), b, x) respectively.

let r be the remainder of ||T || mod (||t|| + 3).

If 0 ≤ r < ||t|| − 1, return the concatenation of strings v_{1} and v_{2}.

If r = ||t|| − 1, v_{1} and v_{2} should be strings of length |t|/2 each; concatenate them and return ρ of the resulting string, where ρ is the oracle for this circuit.

If r = ||t||, v_{1} and v_{2} should be single bits; return their AND. If r = ||t|| + 1, v_{1} and v_{2} should be single bits; return their OR. If r = ||t|| + 2, v_{1} and v_{2} should be single bits; return their XOR.

Since |T | is cut in half at each iteration, ||T || indicates the depth of a tree, up to an additive constant. Of every ||t||+3 levels of the PATHS tree, ||t|| are used to accumulate the answers from the |t| children of a given oracle configuration, one computes XOR, one OR, and one AND. The final value of EVALTREE is 1 or 0, indicating whether the ATM accepts or rejects. The value of a multi-bit function can be pieced together just as in the i = 0 case.

The algorithm described above can be implemented in A_{i,k}: use divide and conquer recursion to construct the unary numbers ||T || and ||t||, then divide ||T || by ||t|| + 3 in unary by repeated subtraction (using the MSP function), which takes at most ||T || iterations and therefore can be done by DCR on T. With the remainder in unary, we can then distinguish the five cases with a few MSP and COND functions.

For k = 2, ||L_{k}|| isn’t closed under multiplication, so we can’t afford to make the ATM rotate strictly among layers of universal, existential, exclusive-or, and oracle states. Instead, as in Theorem 5.6, we bound the number of oracle queries along any computation path by a constant d and arrange the ATM (at the cost of a constant factor of time) into d meta-layers each containing one layer of oracle states and ||L_{k}|| layers of other states, which (at the cost of another constant factor of time) we force to rotate strictly among universal, existential, and exclusive-or layers. The EVALTREE function changes accordingly: we give it an additional argument M, in which we give it the precomputed unary number ||P AT HS||/d, i.e. the depth of each metalayer, and at each step of the divide and conquer recursion we do the following:

let v_{1} and v_{2} be EVALTREE(FH(T), b, x, M) and EVALTREE(BH(T), b, x, M) re-

spectively. let r_{1} be the remainder of ||T || mod M If 0 ≤ r_{1} < ||t|| − 1, return the concatenation of strings v_{1} and v_{2}. If r_{1} = ||t||−1, v_{1} and v_{2} should be strings of length |t|/2 each; concatenate them and return ρ of the resulting string, where ρ is the oracle for this circuit.

Otherwise, let r_{2} be the remainder of r_{1} − ||t|| mod 3.

If r_{2} = 0, v_{1} and v_{2} should be single bits; return their AND. If r_{2} = 1, v_{1} and v_{2} should be single bits; return their OR. If r_{2} = 2, v_{1} and v_{2} should be single bits; return their XOR.

Again, the numbers ||T ||, M, r_{1}, and r_{2} are all available in unary, so we can do arithmetic on them easily.

This concludes the proof of lemma 6.6.

Lemma 6.7 For i ≥ 1, A_{i,2} = FN C^{Σ_{i−1,2}^{p}}.

Proof: Lemma 6.6 has already given us the ⊆ direction. For the ⊇ direction, which resembles the proof of Theorem 1.3.3 of [All91], let f ∈ FN C^{Σ_{i−1,2}^{p}} be computed by a (wolog, levelled) circuit family of depth O(log^{j}(n)). We reason by induction on j.

If j = 1, then f ∈ □_{i,2}^{c}, and therefore f ∈ A_{i,2} by Lemma 6.6. If j > 1, think of an f circuit as divided into O(log(n)) meta-layers of depth at most log^{j−1}(n) each. Let g be a function which, given the values of all the inputs to a meta-layer and a number indicating which meta-layer it is, computes all the outputs from that meta-layer. This function can be computed in depth O(log^{j−1}(n)) with a Σ_{i−1}^{p} oracle, even allowing for constructing a copy of the relevant part of the f circuit, so by the inductive hypothesis g ∈ A_{i,2}. The desired function f can then be computed by iterating g O(log(n)) times, which we can do by DCR. Since the f circuit is only polynomial size, each value of f and g need only be polynomially many bits long, so the DCR is polynomially bounded.

6.2 Definability in R_{k}^{i}

The main result of this section is the following:

Theorem 6.8 For i ≥ 1, k ≥ 2, if f ∈ A_{i,k}, then f is Σ_{i,k}^{b}-definable in R_{k}^{i}.

Proof: If f is the characteristic function of a Σ_{i−1,k}^{c} relation, then it is clearly Σ_{i,k}^{b}- definable, without induction. If f is one of the functions f, t, λ, MSP, LSP, BIT, COND, CONC, BH, or FH, then its encoding is Σ_{0,2}^{b}-definable, without induction, in the language of R_{k}^{i}. The same holds of NOT, less obviously: the definition is λx.(3 · (x#1) −^{.} x).

The INS f function has the Σ_{0}^{b} graph

φ(x, y) ⇔ |y| = |x| + |x| ∧ (∀i < |x|)(Bit(i + i, y) = 1 ∧ Bit(i + i + 1, y) = Bit(i, x)).

It can be proven total by a straightforward DCI on the Σ_{1}^{b} formula (∃y ≤ (x + 1)^{3})φ(x, y), and proven single-valued by Theorem 4.4.

The definition of INS t is similar. The AND and OR functions likewise have obvious Σ_{0}^{b} graphs based on their bitwise definitions; they can be proven total by 2-variable DCI and single-valued by Theorem 4.4.

Thus all the BASE functions, and the characteristic functions of Σ_{i−1,k}^{b} relations, are Σ_{i,k}^{b}-definable in R_{k}^{i}. The class of functions Σ_{i,k}^{b}-definable in R_{k}^{i} is trivially closed under composition, so we need only to prove it closed under |L_{k}|-bounded DCR.

Lemma 6.9 For i ≥ 1, k ≥ 2, if g and h are Σ_{i,k}^{b}-definable in R_{k}^{i}, and f is defined by |L_{k}|-bounded DCR on g and h, then f is Σ_{i,k}^{b}-definable in R_{k}^{i}.

Proof: Suppose R_{k}^{i} Σ_{i}^{b}-defines g and h by the formulæ ϕ_{g}(z, x⃗, y) and ϕ_{h}(z, b, x⃗, u_{1}, u_{2}, y) respectively, and f is defined from g and h with a length bound of |s|. We define a formula ϕ_{f}(z, b, x⃗, y) that Σ_{i,k}^{b}-defines f in R_{k}^{i} by asserting the existence of an encoded binary tree T representing the computation. At vertex i of this binary tree we’ll store data of the form ⟨y_{i}, z_{i}⟩ (of length O(|s| + |z|)) to assert that F (z_{i}, b, x⃗) = y_{i}. The root block must be equal to ⟨y, z⟩, each block ⟨y_{i}, z_{i}⟩ with |z_{i}| > |b| must be appropriately related to its children by ϕ_{h}, and each block ⟨y_{i}, z_{i}⟩ with |z| ≤ |b| must satisfy ϕ_{g}(z_{i}, x⃗, y_{i}).

In order to ensure that R_{k}^{i} can prove the existence of such a T, we represent T in a somewhat inefficient, “inflated” way: to represent a tree of depth ||z|| with O(|s| + |z|) bits of information at each vertex, we use an encoded bit-string of 4^{||z||−1} blocks, each of length O(|s| + |z|). Each subtree is represented by a string whose first half contains the data for the subtree’s root, padded with garbage bits of unspecified value. The third quarter of the string represents the left subtree, and the fourth quarter the right subtree. This enables us to apply divide-and-conquer induction easily to the whole tree; for details of the techniques, see [Blo94]. Note that even in inflated form, the length of T is a polynomial in |z| and |s|, so this construction works for k ≥ 2.

Theorem 6.8 follows immediately.

6.3 Conservation, pro and con

[BKT93] showed the following:

Theorem 6.10 (Buss,Krajíček,Takeuti) For i ≥ 2, k ≥ 3, R_{k}^{i} is ∀∃Σ_{i,k}^{b}-conservative over S_{k}^{i−1}.

Lemma 6.7 and Theorem 6.8, together with Corollary 5.8, gives us some insight as to why it has been so difficult to strengthen Theorem 6.10 to k = 2:

Theorem 6.11 For i ≥ 2, if R_{2}^{i} is conservative over S_{2}^{i−1} with respect to ∀∃Σ_{i,2}^{b} sentences, then FN C^{Σ_{i−1,2}^{p}} = □_{i,2}^{c}.

Proof: Every F NC^{Σ_{i−1,2}^{p}} function is R_{2}^{i}-definable. If it were also S_{2}^{i−1}-definable, it would be in □_{i,2}^{c}.

Recall that in Corollary 5.7, we showed a collapse of P with O(log) queries (or, equivalently, logspace — see [BH91]) down to NC^{1}, relative to oracles in each level of the polynomial hierarchy. Recall also that Wilson [Wil87] showed N C = N C^{1} in the presence of a suitable recursive oracle. By the above theorem, both of these results could be strengthened to “N C = N C^{1} relative to any Σ_{i−1}^{p}-hard oracle” if S_{2}^{i−1} ≺_{Σ_{i,2}^{b}} R_{2}^{i}.

7 Links to Complexity Hierarchies

The authors of [KPS90, KPT91] defined a notion of interactive computation called a “studentteacher game”, a dialogue between an omniscient teacher and a computationally limited student assigned to find the optimal solution to some problem. Each time the student presents a suboptimal solution, the teacher replies with “no, that’s not optimal; see, here’s a better solution”, and the student may then use this better solution in constructing the next solution. (In fact, the student may simply parrot it back as the next solution. This algorithm is called the trivial student.) With the aid of theorem 6.1 and this computational model, we can prove several results analogous to those of [KPT91].

7.1 A KPT witnessing theorem for S_{k}^{i}

Theorem 7.1 For i ≥ 1, k ≥ 3, and ϕ ∈ ∃Π_{i,k}^{b}, if S_{k}^{i} ⊢ (∃y)(∀z)ϕ(a, y, z), then there are □_{i+1,k}^{c} functions f_{1}, … f_{r} such that

S_{k}^{i} ⊢ ϕ(a, f_{1}(a), b_{1}) ∨ ϕ(a, f_{2}(a, b_{1}), b_{2}) ∨ … ∨ ϕ(a, f_{r}(a, b_{1}, … b_{r−1}), b_{r}).

That is, there is a □_{i+1,k}^{c} student that finds a witness for (∃y)(∀z)ϕ(a, y, z) within some constant number r of rounds, provably in S_{k}^{i}.

Proof: The proof resembles that of Theorem A of [KPT91], with two main differences. First, the equational theory contains a function symbol for every definition in A_{i+1,k} rather than in a Cobham-style algebra for FP^{Σ_{i}^{p}}. Second, prefix induction is replaced by divideand-conquer induction, and successor induction by prefix induction, throughout.

Define an equational theory CV_{i+1,k} with a function symbol for each function definition in A_{i+1,k}. Among the functions thus defined is, for every open formula ψ(x) ∈ Σ_{i,k}^{b}, the function h_{ψ} defined by h_{ψ}(s) = LEFT(h′_{ψ}(COUNTUP(s), s, |s|), s), where

h′_{ψ}(T, s, b) = \{ \begin{matrix}0 & if |T | ≤ |b| ∧ ¬ψ(LEFT(T, s)) \\ T + 1 & if |T | ≤ |b| ∧ ψ(LEFT(T, s)) \\ max(h′_{ψ}(Fh(T), s, b), h′_{ψ}(Bh(T), s, b)) & otherwise \end{matrix}

and LEFT(n, s) denotes the leftmost n bits of s, or all of s if n > |s|. The intent is that if ψ(λ) holds, then h′_{ψ}(COUNTUP(s), s, |s|) returns one more than the maximal length of a prefix p of s such that ψ(p) holds. We shall normally invoke this function with ψ monotone, ψ(λ) true, and ψ(s) false, so h_{ψ}(s) returns the minimal prefix p of s such that ψ(s) does not hold. Note, to satisfy the definitions, that |h_{ψ}(T, s, b)| is bounded by |T + 1|, that LEFT ∈ □_{0,2}^{c} = A_{0,2}, and that ψ ∈ Σ_{i,k}^{b} ⊆ Δ_{i+1,k}^{c}, and so ψ’s characteristic function is in □_{i+1,k}^{c} = A_{i+1,k}.

The theory CV_{i+1,k} is axiomatized with some reasonable set of open axioms about BASE (see, e.g, [Blo92, Blo95b]) as well as the following “induction” axiom for every h_{ψ} of the above form:

ψ(0) ∧ ¬ψ(s) ∧ h_{ψ}(s) = c ⊃ ψ (⌊\frac{c}{2}⌋) ∧ ¬ψ(c).

Note that this axiom implies ψ-PIND, and so CV_{i+1,k} is an extension of S_{k}^{i}. Furthermore, it is a conservative extension, as shown by the following two lemmas:

Lemma 7.2 For i ≥ 1, k ≥ 3, ψ ∈ Σ_{i,k}^{b}, S_{k}^{i} Σ_{i+1,k}^{b}-defines h_{ψ}.

Proof: The function graph h′_{ψ}(T, s, b) = c can be defined by

(∃w)(w is a binary tree of depth ||s||, each node containing an ordered pair with

lengths bounded by |T | and |s| respectively, and the root of the tree is ⟨T, c⟩, and for each leaf ⟨u, v⟩,

u = \{ \begin{matrix}λ & if ¬ψ(LEFT(v, s) \\ LEFT(v + 1, s) & if ψ(LEFT(v, s), and \end{matrix}

for each non-leaf node ⟨u, v⟩ with children ⟨u_{l}, v_{l}⟩ and ⟨u_{r}, v_{r}⟩, v = CONC(v_{l}, v_{r}) and u = max(u_{l}, u_{r}).

The whole formula is Σ_{i+1,k}^{b}. R_{k}^{i+1} can prove the totality of the function by DCI on T, so by Theorem 6.10 S_{k}^{i} can also prove totality. The uniqueness of h_{ψ} is easy by proving the uniqueness of w.

Lemma 7.3 For i ≥ 1, k ≥ 2, and ψ ∈ Σ_{i,k}^{b}, the theory S_{k}^{i} proves the “induction” axiom for h_{ψ}.

Proof: Consider the Σ_{i+1,k}^{b} ∩ Π_{i+1,k}^{b} formula

if w is as in the above definition of the graph of h′_{ψ}(T, s, b),

and if ψ(0) but ¬ψ(s), then for all nodes ⟨u, v⟩ in w, u = 0 ⇔ ¬ψ(LEFT(LEFT(|b|, v), s), u = RIGHT(|b|, v) + 1 ⇔ ψ(LEFT(RIGHT(|b|, v), s), and 1 ≤ u ≤ RIGHT(|b|, v) ⇔ ψ (⌊\frac{u}{2}⌋) ∧ ¬ψ(u).

By DCI on T in the above formula, we can prove it for T = COUNTUP(s). The root of any such w will be ⟨T, c⟩ for some c. The assumption ψ(0) rules out the possibility c = 0, and the assumption ¬ψ(s) rules out the possibility c = RIGHT(|b|, T) + 1 (since RIGHT(|b|, T) ≥ |s|), so only the third case remains. By [Bus87], S_{k}^{i} proves LIND, a fortiori DCI, on Σ_{i+1}^{b} ∩ Π_{i+1}^{b} formulæ.

Thus CV_{i+1,k} is a conservative extension of S_{k}^{i}. Now suppose S_{k}^{i} ⊢ (∃x)(∀y)ϕ(a, x, y) where ϕ ∈ ∃Π_{i,k}^{b}. Then CV_{i+1,k} proves it too, and by the same Herbrand argument as in [KPT91], CV_{i+1,k} proves

ϕ(a, f_{1}(a), b_{1}) ∨ ϕ(a, f_{2}(a, b_{1}), b_{2}) ∨ … ∨ ϕ(a, f_{r}(a, b_{1}, … b_{r−1}), b_{r})

for some constantly many A_{i+1,k} functions f_{1}, …, f_{r}. By conservativity of CV_{i+1,k} over S_{k}^{i}, S_{k}^{i} defines the same functions f_{1}, …, f_{r}, which are all □_{i+1,k}^{c}, and proves the same statement about them. This concludes the proof of Theorem 7.1.

7.2 Collapsing Bounded Arithmetic

A previous version of this paper contained an adaptation of the argument of [KPT91] that T_{2}^{i} = S_{2}^{i+1} ⇒ Σ_{i+1}^{p} ⊆ Δ_{i+1}^{p}/poly. However, Buss [Bus94] gave a simpler proof of a stronger result, so I’ll adapt that technique instead. The main substantive difference between the following proof and Buss’s is the replacement of prefix induction with divide and conquer induction; however, the proof technique is interesting enough to warrant another exposition.

Theorem 7.4 For i ≥ 1, k ≥ 3, if S_{k}^{i} = R_{k}^{i+1}, then

• S_{k}^{i} proves that every Σ_{i+1}^{b} formula B(x) is equivalent to a formula of the form C(x, A(x)) where A is a (Σ_{i+2}^{b} ∩ Π_{i+2}^{b})-defined function of S_{k}^{i} depending only on |x|, and C ∈ Π_{i+1}^{b};

• S_{k}^{i} proves Σ_{i+1,k}^{p} ⊆ Δ_{i+1,k}^{p}/poly;

• S_{k}^{i} = S_{k}^{i+1};

• S_{k}^{i} = S_{k}, which is therefore finitely axiomatized; and

• for every bounded formula in L_{k}, S_{k}^{i} proves it equivalent to a Boolean combination of Σ_{i+2,k}^{b} formulæ.

The idea, as in other proofs [KPT91, Bus94] involving student-teacher games, is to play the omniscient teacher, giving away as little information as possible, and playing for long enough that the student must show some semblance of originality. Later, a non-omniscient teacher faced with a new problem can enlist the aid of this same demonstrably nontrivial student and solve the problem. But before we can apply this technique, we must define some preliminary notions.

Definition 7.5 (Buss) Π_{i}^{B} is the class of quantified Boolean formulæ in prenex form containing i blocks of like quantifiers, starting with a ∀.

T RU^{i}(ϕ, w) is a formula stating that ϕ encodes a Π_{i}^{B} formula and w encodes a satisfying assignment of its free variables.

SAT^{i}(ϕ) is the formula (∃w ≤ ϕ)T RU^{i}(ϕ, w).

Note that T RU^{i} and SAT^{i} are formulæ in the language of bounded arithmetic, while ϕ is a numeric encoding of a quantified Boolean formula (but we shall often identify it with that quantified Boolean formula, for convenience). Note also that we assume the encodings of ϕ and w are reasonably efficient, encodable and decodable in ALOGTIME, and that any assignment of the free variables in ϕ has an encoding numerically less than ϕ itself. We assume standard functions for encoding and decoding sequences, e.g. SeqLen(s) = the length of the sequence encoded by s.

It is well known that SAT^{i} is complete for Σ_{i+1,2}^{p}, and therefore for Σ_{i+1,2}^{b} formulæ, under polynomial-time, many-one reductions. The techniques of the proof are not computationally demanding, and can be formalized in T_{2}^{i}, S_{2}^{i}, or even (with care) R_{2}^{i}, and the reductions can be weakened to N C or even ALOGTIME. Indeed, for k ≥ 2, SAT^{i} is complete for Σ_{i+1,k}^{p} and Σ_{i+1,k}^{b} under □_{0,k}^{c} many-one reductions; the larger growth rates are needed only during the reduction. And by standard techniques, T RU^{i} is Δ_{i+1}^{b} with respect to R_{2}^{i}.

The problem we shall set our student is, given a sequence of n encoded formulæ ϕ_{1}, ϕ_{2}, …, ϕ_{n}, to find the longest initial sequence ϕ_{1}, ϕ_{2}, …, ϕ_{m} all of which are satisfiable, and produce witnesses w_{1}, w_{2}, …, w_{m} for them. (To avoid funny behavior at 0, we give the student a witness w_{1} for ϕ_{1} for free.) However, we’ll accept a witnessed initial sequence if it is within a factor of 2 in length of the longest one. That is, the student is to realize the principle:

(∗) (∀ϕ_{1}, …, ϕ_{n} ≤ 2^{|a|})(∃w_{1}, …, w_{m} ≤ ϕ⃗)MaxSoln(a, ϕ⃗, w⃗)

where MaxSoln(a, ϕ⃗, w⃗) is defined by

SeqLen(w⃗) ≤ SeqLen(ϕ⃗)∧ (∀j ≤ SeqLen(ϕ⃗))ϕ_{j} ≤ 2^{|a|}∧ (∀j ≤ SeqLen(w⃗))w_{j} ≤ ϕ_{j}∧ (∀j ≤ SeqLen(w))T RU^{i}(ϕ_{j}, w_{j})∧ (SeqLen(ϕ⃗) ≥ 2 · SeqLen(w) ⊃ ∃j ≤ 2 · SeqLen(w))¬SAT^{i}(ϕ_{j}).

Note that MaxSoln ∈ Π_{i+1}^{b}, so (*) is a ∀∃Π_{i+1}^{b} statement, and provable in R_{k}^{i+1} by maximizing p ≤ ||ϕ⃗|| in the Σ_{i+1}^{b} formula

(∃w⃗ ≤ ϕ⃗)(|SeqLen(w⃗)| = p ∧ (∀j ≤ SeqLen(w⃗))T RU^{i}(ϕ_{j}, w_{j})).

If, as we shall assume for the rest of this theorem, S_{k}^{i} = R_{k}^{i+1} and therefore S_{k}^{i} could also prove principle (*), then Theorem 7.1 would imply the existence of a □_{i,k}^{c} student who witnesses it in some constant number r of rounds. If in a given round, the student proposes a sequence of witnesses w_{1}, …, w_{m} which is not “nearly maximal”, the teacher is obliged to demonstrate that by providing witnesses for at least the first 2m formulæ. Thus S_{k}^{i} = R_{k}^{i+1} implies there are functions f_{1}, …, f_{r}, Σ_{i+1}^{b}-defined in S_{k}^{i}, such that, for any witnesses w⃗ for ϕ⃗,

MaxSoln(a, ϕ⃗, f_{1}(a, ϕ⃗, w_{1})) ∨
MaxSoln(a, ϕ⃗, f_{2}(a, ϕ⃗, w_{1}, …, w_{2m_{1}})) ∨
MaxSoln(a, ϕ⃗, f_{3}(a, ϕ⃗, w_{1}, …, w_{2m_{2}})) ∨
⋮
∨ MaxSoln(a, ϕ⃗, f_{r}(a, ϕ⃗, w_{1}, …, w_{2m_{r−1}}))

where m_{j} = SeqLen(f_{j}(a, ϕ⃗, w_{1}, …, w_{2m_{j−1}})).

Define an original witness to be any witness the student produces without first being given. The trivial student, the one who never produces an original witness, will yield m_{1} = 1, m_{2} = 2, m_{3} = 4, …, m_{r} = 2^{r−1}. So to coax an original witness from our student, it suffices to let n ≥ 2^{r} and make all the formulæ satisfiable. Define the formula FindsOrigBy(a, m, ⟨ϕ_{1}, …, ϕ_{s}⟩) to be (∀w⃗ ≤ ϕ⃗ ≤ 2^{|a|})((∀j ≤ SeqLen(ϕ⃗))T RU^{i}(ϕ_{j}, w_{j})) ⊃

(SeqLen(f_{1}(a, ϕ⃗, ⟨w_{1}⟩)) > 1 ∨
SeqLen(f_{2}(a, ϕ⃗, ⟨w_{1}, w_{2}⟩)) > 2 ∨
SeqLen(f_{3}(a, ϕ⃗, ⟨w_{1}, w_{2}, w_{3}, w_{4}⟩) > 4 ∨ …
∨ SeqLen(f_{m}(a, ϕ⃗, ⟨w_{1}, …, w_{2^{m−1}}⟩) > 2^{m−1}))

This states that, no matter what witnesses are provided for the formulæ ϕ⃗, the game will produce at least one original witness within the first m rounds, and therefore an original witness for one of the first 2^{m} formulæ. The assumption S_{k}^{i} = R_{k}^{i+1} implies

S_{k}^{i} ⊢ (∀ϕ_{1}, …, ϕ_{2^{r}} ≤ 2^{|a|}) ((⋀_{j=1}^{2^{r}} SAT^{i}(ϕ_{j})) ⊃ FindsOrigBy(a, r, ϕ⃗)).

It is conceivable (assuming FindsOrigBy(a, m, ϕ⃗)) that, although the game is guaranteed to give an original witness for one of the first 2^{m} formulæ, the student uses the later formulæ to find it; for example, suppose the last formula in the sequence encodes a polynomial-time algorithm for SAT! The truth value of FindsOrigBy(a, m, ϕ⃗) may therefore depend on all of ϕ⃗, even though only the first 2^{m} ϕ’s are actually treated as formulæ to be witnessed. We therefore distinguish between the parts of ϕ⃗ that might be witnessed and the parts serving only as “advice” to the computation, and write, e.g, FindsOrigBy(a, m, ⟨ϕ_{1}, …, ϕ_{2^{m}}⟩, A).

Now consider the formula PreAdvice(a, m, A) defined by

(∀ϕ_{1}, …, ϕ_{2^{m}} ≤ 2^{|a|}) ((⋀_{j=1}^{2^{m}} SAT^{i}(ϕ_{j})) ⊃ FindsOrigBy(a, m, ϕ⃗, A)).

This states that, for any sequence of 2^{m} satisfiable formulæ ϕ⃗, and any witnesses for those formulæ, the game with advice A will produce an original witness for one of ϕ⃗.

Recall that

S_{k}^{i} ⊢ (∀ϕ_{1}, …, ϕ_{2^{r}} ≤ 2^{|a|}) ((⋀_{j=1}^{2^{r}} SAT^{i}(ϕ_{j})) ⊃ FindsOrigBy(a, r, ϕ⃗)).

Rephrasing this in terms of advice, S_{k}^{i} ⊢ PreAdvice(a, r, ⟨⟩). Since r is a constant, S_{k}^{i} proves without induction that there is a minimum m ≤ r such that (∃A)PreAdvice(a, m, A). Let Advice(a, m, A) assert that m is such a minimum, and A is a corresponding advice string. Then S_{k}^{i} ⊢ (∃m, A)Advice(a, m, A). Finally, given a formula ψ ∈ Σ_{i}^{B} and “auxiliary” formulæ ϕ_{1}, …, ϕ_{2^{m−1}}, let TestSeq(ϕ⃗, ψ) be the sequence of length 2^{m} formed by concatenating ϕ⃗ with 2^{m−1} copies of ψ.

Now we are ready to prove the theorem. I claim that S_{k}^{i} proves

(Advice(a, m, A) ∧ ψ ≤ 2^{|a|}) ⊃

(SAT^{i}(ψ) ↔
(∀ϕ_{1}, …, ϕ_{2^{m−1}} ≤ 2^{|a|})(⋀_{j=1}^{2^{m−1}} SAT^{i}(ϕ_{j}) ⊃ FindsOrigBy(a, m, TestSeq(ϕ⃗, ψ), A).

Proof: Assume Advice(a, m, A) and ψ ≤ 2^{|a|}. If ψ is satisfiable, then for any satisfiable sequence ϕ_{1}, …, ϕ_{2^{m−1}}, TestSeq(ϕ⃗, ψ) is a sequence of 2^{m} satisfiable formulæ and so, by PreAdvice(a, m, A), an original witness will be found for it.

On the other hand, if ψ is not satisfiable, then any original witness for TestSeq(ϕ⃗, ψ) must actually witness one of the first 2^{m−1} formulæ ϕ⃗, using ψ only as extra advice. Thus FindsOrigBy(a, m, TestSeq(ϕ⃗, ψ), A) is equivalent to FindsOrigBy(a, m − 1, ϕ⃗, ⟨A, ψ⟩). However, by minimality of m, there is no advice A′ for which PreAdvice(a, m − 1, A′) holds. In particular, for the advice A′ = ⟨A, ψ⟩, there must exist a satisfiable sequence ϕ_{1}, …, ϕ_{2^{m−1}} such that FindsOrigBy(a, m − 1, ϕ⃗, A′) is false.

Thus in the presence of the “advice” A, which depends only on a, the Σ_{i+1}^{b}-complete formula SAT^{i}(ψ) is equivalent to the Π_{i+1}^{b} formula

(∀ϕ_{1}, …, ϕ_{2^{m−1}} ≤ 2^{|a|}) ( ⋀_{j=1}^{2^{m−1}} SAT^{i}(ϕ_{j}) ⊃ FindsOrigBy(a, m, TestSeq(ϕ⃗, ψ), A)).

This proves the first part of the theorem: if B(x) ∈ Σ_{i+1}^{b}, then by the completeness of SAT^{i}, there is a poly-time function f such that B(x) ↔ SAT^{i}(f(x)). We can think of the advice A as a (not necessarily single-valued) function of a ≈ 2^{|f(x)|}, Σ_{i+2}^{p} ∩ Π_{i+2}^{p}-defined in S_{k}^{i}, so we have B(x) ↔ C(f(x), A(f(x))) where C(ϕ⃗, A) is the above Π_{i+1}^{b} formula.

The second part follows immediately. In fact, since the reduction function f above can be made quasilinear [Sch78], we get Σ_{i+1,k}^{p} ⊆ Δ_{i+1,k}^{p}/quasilinear.

The third, fourth, and fifth parts follow much as in [Bus94].

8 Conclusions

We have completed analogies with several previous results on the theories S_{2}^{i} and T_{2}^{i}, filling the following gaps in our understanding of bounded arithmetic:

• a general collapse of P[log] down to N C^{1}, relative to all nontrivial levels of the polynomial hierarchy, and analogues for quasipolynomial, etc. hierarchies (see Corollary 5.7)

• new complexity-theoretic implications of S_{k}^{i} ≡ T_{k}^{i} (see Corollary 5.11)

• an elegant computational characterization of the single-valued Σ_{i}^{b}-consequences of S_{k}^{i−1} (see Corollary 5.8)

• complexity-theoretic implications of extending the known ∀∃Σ_{i}^{b}-conservativity between S_{k}^{i−1} and R_{k}^{i} down to k = 2 (see Theorem 6.11)

• complexity-theoretic implications of S_{k}^{i} ≡ R_{k}^{i+1} (see Theorem 7.4)

This paper arose from the desire for more elegant computational characterizations of the Σ_{i,k}^{b} consequences of R_{k}^{i} and S_{k}^{i−1}. The classes □_{i,k}^{c} are natural, and seem to comprise a “large” subset of those consequences, but only under the explicit assumption of singlevaluedness. Let Φ_{i,k} denote an (as yet undescribed) computational class that captures exactly those consequences, without restricting to single-valued functions. Several research directions present themselves:

• Augment the computational class □_{i,k}^{c} with a symmetry-breaking primitive which, given a list of numbers at least one of which has a desired property, chooses an arbitrary element with that property. The resulting class would certainly include Φ_{i,k}, but would the reverse inclusion hold, i.e. would the primitive preserve R_{k}^{i} definability? Such a symmetry-breaking primitive, if not carefully restricted, would allow arbitrary bounded minimization and hence expand beyond □_{i,k}^{c} to all of □_{i,k}^{p}. Assuming this can be avoided, is there another, more elegant way to describe the class?

• Find complete problems for the levels of the polynomial hierarchy that are “parallel self-reducible”, i.e. an FN C or □_{1,k}^{c} circuit family with a yes/no oracle for the problem can construct a witness for its outermost existential quantifier. In this case, Φ_{i,k} would simply be F NC^{Σ_{i−1,k}^{p}} or □_{i,k}^{c} respectively.

Either approach would imply Conjecture 1.1. Either approach would allow us to describe Φ_{i,k} computationally and show, directly from its computational definition, that it can Σ_{i}^{b}- realize R_{k}^{i} proofs, and thus that it captures all the Σ_{i}^{b} consequences of R_{k}^{i}. We could then continue the analogy from known results on S_{2}^{i} and T_{2}^{i} to say

• ∀∃Σ_{i}^{b}-conservativity between S_{k}^{i} and R_{k}^{i} would imply Φ_{i,k} = □_{i,k}^{p}.

• ∀∃Σ_{i}^{b}-conservativity (i.e. equivalence) between S_{k}^{i−1} and T_{k}^{i−1} would likewise imply Φ_{i,k} = □_{i,k}^{p}.

On the other hand, perhaps Conjecture 1.1 is simply not true, and Φ_{i,k} is fundamentally and irremediably a class of multi-valued functions. If we still have an interest in singlevalued functions, then, this would suggest that R_{k}^{i} is “too big”, and that perhaps it should be reformulated, e.g. without existential instantiation (or its sequent-calculus analogue).

All the results presented in this paper can also be proven for a suitably axiomatized intuitionistic theory IR_{k}^{i} — indeed, the axiomatization in Section 2.5 was chosen to be intuitionistically useful. If one of the above approaches were successful, it seems likely that, by techniques similar to [Bus86b, CU93, Har92], Φ_{i,k} would capture all the consequences of IR_{k}^{i}, regardless of their syntactic complexity.

Several other holes remain in the web of analogies. One is our inability so far to prove analogues of Theorems 7.1 and 7.4 for k = 2, precisely the case of the greatest computational interest. Another is whether R_{2}^{i+1} is indeed ∀∃Σ_{i+1}^{b}-conservative over S_{2}^{i}.

[Kra93] shows that the equivalence S_{2}^{i} ≡ T_{2}^{i}, like the equivalence S_{2}^{i+1} ≡ T_{2}^{i}, would have surprising complexity-theoretic implications: any problem solvable in P^{Σ_{i−1}^{p}} could be solved with only O(log) many queries to its oracle. (It is not known whether this would imply the collapse of the polynomial hierarchy.) The author has not yet found a natural complexity class corresponding to the Σ_{i+1}^{b}-definable functions of R_{k}^{i}. Such a class would provide stronger (and presumably still less plausible) implications of R_{k}^{i} ≡ S_{k}^{i}.

The larger questions not addressed in this paper remain stubbornly unsolved: are there any equivalences among the theories R_{k}^{i}, S_{k}^{i}, and T_{k}^{i}, is the theory T_{k} = S_{k} = R_{k} finitely axiomatizable for any k, and do the corresponding complexity classes collapse?

Acknowledgments

I would like to thank Sam Buss for introducing me to the subject, for suggesting possible strengthenings of my preliminary results, for pointing me to related work in the literature, and (somewhat ruefully) for pointing out the error in the previous version of the paper. Thanks also to Judy Goldsmith, who provided postdoc support in the early stages of the project.

References

[All91] William Allen. Arithmetizing uniform NC. Annals of Pure and Applied Logic, 53(1):1–50, 1991. See also Divide and Conquer as a Foundation of Arithmetic, Ph.D. thesis, University of Hawaii at Manoa, 1988.

[BH91] Samuel R. Buss and Louise Hay. On truth-table reducibility to SAT. Information and Computation, 91:86–102, 1991.

[BKT93] Samuel R. Buss, Jan Krajíček, and Gaisi Takeuti. Provably total functions in bounded arithmetic theories R_{3}^{i}, U_{2}^{i} and V_{2}^{i}. In P. Clote and J. Krajíček, editors, Arithmetic, Proof Theory and Computational Complexity, pages 116–161. Oxford University Press, 1993.

[Blo92] Stephen Bloch. Divide and Conquer in Parallel Complexity and Proof Theory. PhD thesis, University of California, San Diego, 1992.

[Blo94] Stephen Bloch. Function-algebraic characterizations of log and polylog parallel time. computational complexity, 4(2):175–205, 1994. See also Proceedings of the Seventh Annual Structure in Complexity Theory Conference, 193–206, 1992.

[Blo95a] Stephen Bloch. On parallel hierarchies and R_{k}^{i}. In Daniel Leivant, editor, Proceedings of Workshop on Logic and Computational Complexity, number 960 in Lecture Notes in Computer Science. Springer-Verlag, 1995.

[Blo95b] Stephen Bloch. Parameter-free induction in bounded arithmetic. In preparation for submission, 1995.

[Bus86a] Samuel R. Buss. Bounded Arithmetic. Number 3 in Studies in Proof Theory. Bibliopolis (Naples), 1986.

[Bus86b] Samuel R. Buss. The polynomial hierarchy and intuitionistic bounded arithmetic. In Structures Proceedings, number 223 in Lecture Notes in Computer Science, pages 77–103. Springer-Verlag, 1986.

[Bus87] Samuel R. Buss. Axiomatizations and conservation results for theories of bounded arithmetic. In Proceedings of a Workshop in Logic and Computation, AMS Contemporary Mathematics, May 1987.

[Bus94] Samuel R. Buss. Relating the bounded arithmetic and polynomial time hierarchies. Manuscript, 1994.

[CKS81] A. Chandra, D. Kozen, and L. Stockmeyer. Alternation. Journal of the ACM, 28(1):114–133, January 1981.

[Clo89] Peter Clote. A first order theory for the parallel complexity class NC. Technical Report BCCS-8901, Boston College, 1989.

[Cob65] A. Cobham. The intrinsic computational difficulty of functions. In Y. Bar-Hillel, editor, Logic, Methodology and Philosophy of Science II, pages 24–30. North-Holland, 1965.

[CT92] Peter Clote and Gaisi Takeuti. Bounded arithmetic for NC, ALogT IME, L and NL. Annals of Pure and Applied Logic, 56:73–117, 1992.

[CU93] Stephen A. Cook and Alasdair Urquhart. Functional interpretations of feasibly constructive arithmetic. Annals of Pure and Applied Logic, 63(2):103–200, September 1993.

[Fag74] Ronald Fagin. Generalized first-order spectra and polynomial-time recognizable sets. In Richard M. Karp, editor, Complexity of Computations, volume 7 of SIAM-AMS Proceedings, pages 43–73. 1974.

[Har92] Victor Harnik. Provably total functions of intuitionistic bounded arithmetic. Journal of Symbolic Logic, 57(2):466–477, June 1992.

[Hoo83] Jay Hook. A many-sorted approach to predicative mathematics. PhD thesis, Princeton University, 1983.

[KPS90] Jan Krajíček, Pavel Pudlák, and Jiři Sgall. Interactive computations of optimal solutions. In Mathematical Foundations of Computer Science, volume 452 of Lecture Notes in Computer Science, pages 48–60. Springer, 1990.

[KPT91] J. Krajíček, P. Pudlák, and G. Takeuti. Bounded arithmetic and the polynomial hierarchy. Annals of Pure and Applied Logic, 52:143–153, 1991.

[Kra93] Jan Krajíček. Fragments of bounded arithmetic and bounded query classes. Transactions of the AMS, 338(2):587–598, August 1993.

[Nel86] Edward Nelson. Predicative Arithmetic. Princeton University Press, 1986.

[Par71] Rohit J. Parikh. Existence and feasibility in arithmetic. Journal of Symbolic Logic, 36:494–508, 1971.

[Ruz81] W. Ruzzo. On uniform circuit complexity. Journal of Computer and System Sciences, 22:365–383, 1981.

[Sch78] C.P. Schnorr. Satisfiability is quasilinear complete in NQL. Journal of the ACM, 25:136–145, 1978.

[Wil85] Christopher B. Wilson. Relativized circuit complexity. Journal of Computer and System Sciences, 31:169–181, 1985.

[Wil87] Christopher B. Wilson. Relativized NC. Math. Systems Theory, 20:13–29, 1987.