Introduction

• $I\Delta_0$ (defined Parikh 1971) is the fragment of Peano Arithmetic (open axioms for $0$, $S$, $+$, `$\cdot$`, and induction) where the main axiom schema has been restricted to formulas all of whose quantifiers are bounded (the $\Delta_0$-formulas).
• It is closely associated with computational complexity as the $\Delta_0$-formulas express exactly sets in the linear time hierarchy, LINH, sets computed in linear time on an alternating TM with a fixed number of alternations. (Lipton 1978).
• We can expand the language of arithmetic with functions for $|x| := \lceil log_2(x +1) \rceil$; $x \monus y := x-y$ if $x-y > 0$, $0$ otherwise; and $MSP(x,i) := \lfloor x/2^i \rfloor$ without changing the sets definable by $\Delta_0$-formulas. Adding appropriate starting axioms gives a conservative extension of $I\Delta_0$. (Lipton 1978, Bennett 1962, Wrathall 1978).
• If we further expand the language with a faster growth function $x \# y := 2^{|x||y|}$, the bounded formulas can then precisely define the sets in the polynomial time hierarchy, and the resulting theory is Buss' theory $S_2$ (Buss 1985) which has been extensively studied both for what its fragments can prove about computational complexity and what they cannot.
• $S_2$ has natural subtheories $S^i_2$ that to some degree model reasoning about $P^{\Sigma^p_{i-1}}$ sets, sets computable in polynomial time with access to an oracle computing a $\Sigma^p_{i-1}$-set (Buss 1985).
• Today, I'd like to talk about how to come with with "natural" sub-theories of $I\Delta_0$ -- where the scare quotes mean I ought to define the word "natural".
• I also want to talk a little about what is known about $I\Delta_0$ and its sub-theories and why I think they are interesting.

Hierarchies of Bounded Formulas

• Because we are going to look at first-order theories within $I\Delta_0$ and $S_2$, we start by describing some hierarchies of bounded formulas:
  • $\Sigma^b_0$ (aka $\Pi^b_0$) are the bounded arithmetic formulas whose quantifiers are all of the form
    $(\forall x \leq |t|)$ or $(\exists x \leq |t|)$ (the sharply bounded formulas).
  • For $i>0$, $\Sigma^b_i$ (resp. $\Pi^b_i$) are the closure of the $\Pi^b_{i-1}$ (resp. $\Sigma^b_{i-1}$) formulas under conjunctions, disjunctions, $(\exists x \leq t)$ and $(\forall x \leq |t|)$ (for $\Pi^b_i$, $(\forall x \leq t)$ and $(\exists x \leq |t|)$).
  • The prenex variant of the $\Sigma^b_i$ formulas, the $\SIG{i}$-formulas, look like: $$(\exists x_1 \leq t_1) \cdots (Qx_i \leq t_i) (Qx_{i+1}\leq|t_{i+1}|)A$$ where $A$ is an open formula. So we have $i+1$ alternations, innermost being length-bounded.
  • A $\PI{i}$-formula is defined similarly but with the outer quantifier being universal.
  • For the above, we have assumed we have $x\#y$ in the language.
  • To emphasize whether we have $x\#y$, we'll add a subscript 1 to say we don't and a 2 to say we do, for example, $\Sigma^b_{i,1}$.
  • $E_i$ (resp. $U_i$) are defined analogously except where we start with $E_0=U_0$ being the quantifier free formulas. These hierarchies are usually defined in the language without $x\#y$.
  • Kent-Hodgson 1982 have shown for $i > 0$, $\Sigma^b_i$ (resp. $\Pi^b_i$) formulas define exactly the $\Sigma^p_i$ (resp. $\Pi^p_i$) sets, those sets computed by an alternating Turing Machine with $i$ alternations the outermost being nondeterministic (resp. co-nondeterministic).

Bounded Arithmetic Theories

• $BASIC_1$ is a fixed set of open formula axioms for the symbols $0$, $S$, $+$, $\cdot$, $|x| :=$ length of $x$, $\monus$, $\MSP{x}{i}$, $\leq$.
• $BASIC_2$ adds a fixed set of open axioms for $x\#y$.
• Because we have $\MSP{x}{i}$ and $\monus$ in the language, it is possible to define as a term $\beta_{a}(i, w)$, the function which projects out the $i$th block of $a$ bits out of $w$.
• We can also define pairing and the function $\BIT(j, w)$ as a terms.
• We add to BASIC, $L^mIND_{A}$ induction axioms of the form: $$A(0) \wedge \forall x<|t|_m[A(x) \IMP A(S(x))] \IMP A(|t|_m)$$ Here $t$ is a term made of compositions of variables and our function symbols and where we are using the definition $|x|_0=x$, $|x|_m=| |x|_{m-1}|$.
• $T^i_k$, where $k=1,2$, is the theory $\BASIC_k$$+$$\Sigma^b_{i,k}$-$\IND$, where $IND$ = $L^0IND$.
  $S^i_k$ is the theory $\BASIC_k$$+$$\Sigma^b_{i,k}$-$\LIND$.
  $IE_i$ is the theory $\BASIC_1$$+$$E_i$-$\IND$.
  $I\Delta_0 := \cup_i IE_i = \cup_i S^i_1$, $S_k := \cup_i S^i_k$.

Bounded Arithmetic Definability

• Let $\Psi$ be a class of formulas, we say a theory $T$ can $\Psi$-define a function $f$ if there is a $\Psi$-formula $A_f$ such that
  $\qquad T \proves \forall x \exists! y A_f(x, y)$ and
  $\qquad \nat\models \forall x A_f(x, f(x)).$
• A formula $A(\vec{x})$ is a $\Delta^b_{i}$ (resp. $\hat\Delta^b_{i}$) predicate of $T$ if
  $\qquad T \proves A(\vec{x}) \IFF A_\Sigma(\vec{x})$ and
  $\qquad T \proves A(\vec{x}) \IFF A_\Pi(\vec{x})$
  where $A_\Sigma(\vec{x})$ is $\Sigma^b_{i+1}$ (resp. $\hat\Sigma^b_{i}$) and $A_\Pi(\vec{x})$ is $\Pi^b_{i+1}$ (resp. $\hat\Pi^b_{i}$) .
• (Buss 1987, Jerabek 2006) For $i\geq 0$, $S^{i+1}_2$ is $\forall\Sigma^b_{i+1}$-conservative over $T^i_2$.
• (Buss 1985,1987, Krajicek 1993) For $i\geq 0$, the $\Delta^b_{i+1}$-predicates are $T^i_2$ and $S^{i+1}_2$ are precisely the $P^{\Sigma^p_i}$ sets, the $\Delta^b_{i+1}$-predicates of $S^i_2$ are the $L^{\Sigma^p_i}$ sets. Here $L$ is Logspace.
• For $\Sigma^b_{i+1}$-definable (multi)functions one gets $FP^{\Sigma^p_i}$ for $T^i_2$ and $S^{i+1}_2$, and $FP^{\Sigma^p_i}(wit, log)$ for $S^i_2$.
• On the other hand, for the $\Delta^b_{i+1}$-predicates/$\Sigma^b_{i+1}$-definable functions of $S^i_1$, $T^i_1$, or $IE_i$, no nice characterizations are known. One criteria we would like for "natural" sub-theories of $I\Delta_0$ are correspondences to studied complexity classes.

Closure Properties

• The $\Sigma^b_{i+1}$-definable (multi)functions of $T^i_2$, $S^i_2$ and the $\Delta_0$-definable function of $I\Delta_0$ enjoy nice closure properties: they are closed under composition, and some kind of recursion. So this is another property we'd like for "natural" sub-theories of $I\Delta_0$.
• For example, let $t, r$ be terms and $g$ and $h$ be $\Sigma^b_{i+1}$-definable in $T^i_2$ and $S^{i+1}_2$ then the function $f$ defined by the following bounded primitive recursion (BPR) is also $\Sigma^b_{i+1}$-definable:
  \( \EQN{ F(0,\vec{x}) &=&g(\vec{x})\\ F(n+1,\vec{x})&=&min(h(n,\vec{x},F(n,\vec{x})),r(n,\vec{x}))\\ f(n,\vec{x}) &=& F(|t(n,\vec{x})|,\vec{x}) }\)
  (follows from Buss 1987, given in this form Pollett 1997).
• For $I\Delta_0$, using Bennett 1962 one can show if $f$, $g$, $h_0$, $h_1$ can be $\Delta_0$-defined then so is $f$ defined by: \( \EQN{ f(0, \vec{x}) &= &g(\vec{x})\\ f(2n, \vec{x}) &=& h_0(n,\vec{x}, f(n,\vec{x}))\\ f(2n+1, \vec{x}) &=& h_1(n,\vec{x}, f(n,\vec{x})) }\)
  provided $|f(n, \vec{x})| < O(\sqrt{|n| + \sum_i|x_i|)}).$
• The above recursion scheme for $f$, $g$, $h_0$, $h_1$ where $f(n,\vec{x}) < |k(n,\vec{x})|$, we'll call $B_2RN$.
• Clote 1988 shows that the logspace computable functions can be defined as the closure of our language with $x\#y$, under composition, $B_2RN$, and another recursion scheme $CRN$.

What complexity classes live in $\Delta_0$?

• The figure to the right is a subset of a diagram in Volume A of the Handbook of TCS.
• $\mbox{SC} := \cup_k \mbox{SC}^k := \mbox{DTISP}(poly, log^k)$. (DTISP = deteministic time space)
• NL = nondeterministic logspace, NL=co-NL (Immerman-Szelepcsenyi 1987).
• $\mbox{NC}^1$ are languages recognized by uniform poly-size, log-depth fan-in 2 AND, OR, NOT circuit families.
• LOGCFL := logspace reducible to a context-free language, LOGDFCL := logspace reducible to a deterministic context-free language.
• Jones 1969 was the first to show the context-free languages are in $\Delta_0$.
• Sudborough 1975 shows NL is contained in LOGCFL.
• The SC containment and logspace closures follow from the next theorem...

Nepomnjascij's Theorem (1970)

Arithmetics for LINH subclasses

• We now briefly mention some arithmetics related to the complexity classes a couple slides back.
• Each of these theories is either a first-order theory in the language with $x\#y$, or is a second-order theory where we have number and string sorts, none are first-order theories in a language without $x\#y$.
• Many of these papers also show a "bounded reverse mathematics" results. I.e., computational complexity results which are provable in the theory.
• For $NC^1$, Clote Takeuti 1995 give first-order theories $TNC^0$, $TLS$, whose esb-definable functions are respectively $NC^1$, and $L$. Pollett 2002 gives simplified versions of both these theories whose $\hat\Sigma^b_1$-definable functions are $NC^1$ and $L$.
• Arai 2000 gives first-order whose $\Sigma^b_0$-definable functions are $NC^1$, and Pitt 2000 gives an equational theory with $NC^1$ definable functions. These papers show their theories prove the correctness of the Boolean Sentence Value Problem, as well as facts about Frege proof systems.
• Cook Morioka 2005, Cook Nguyen 2005, and Cook Nguyen's book 2010, give second order theories, $VNC^1$, $VL$, $VNL$ whose $\Delta^B_1$ -predicates are respectively, $NC^1$, $L$, and $NL$. They also show these theories can prove properties of associated complete problems for these complexity classes. For example, PATH, st-CONN, and KROM formulas (CNF formulas where each clause has two literals).
• Kuroda 2012 gives second-order theories $VLCFL$ and $VLDCFL$ whose $\Sigma^B_1$-definable functions are LOGCFL and LOGDCFL respectively. She shows $VLCFL$ can prove the pumping lemma for context-free languages.
• As far as I am aware no one has published a paper with an arithmetic for SC.

The Theories TLS and TLS'

• To come up with a "natural" hierarchies within $I\Delta_0$, let's look at how a couple of these first-order theories are defined:
  • The $\Psi$-WSN (weak successive nomination rule) is the following rule: $$\frac{ b \leq |k(j,\vec{a})|\sequent \exists! x \leq |k|A(j,\vec{a},b,x) } {\sequent \exists w \leq \bd(|k|,t)\forall j < |t| A(j,\vec{a},\hat\beta_{|k^*|}(j,w), \hat\beta_{|k^*|}(Sj,w))}$$ where $A\in\Psi$ and $\bd(a,b) := 2(2a\#2b)$.
  • $\Psi$-REPL (quantifier replacement) is the following rule:
    \(\qquad \EQN{\lefteqn{(\forall x \leq |s|)(\exists y \leq t(x,a))A(x,y,a) \IFF}\\ && (\exists w \leq \bd(t^*(|s|,a), s))(\forall x \leq |s|) A(x,\dot\beta_{|t^*(|s|,a)|,t}(x,w))} \)
    where $A\in\Psi$ and $\dot\beta_{t,s}(x,w) := \min(\hat\beta_t(x,w), s)$. Here $\min(x,y) := x+y \monus \max(x,y)$.
  • $\Psi$-$COMP$ (comprehension axiom) is the following axiom $COMP_A$ for $ A \in \Psi$:
    $$\exists y \leq 2^{|s|}\forall i < |s|(\BIT(i,y)=1 \equiv A(i, \vec{a})).$$
  • $TLS$ is the theory consisting of $\BASIC_2$$+$$open_2$-$\LIND{}$$+$$\SIG{1}$-$WSN$$+$$\SIG{1}$-$REPL$.
  • $TLS^1_2$ is $\BASIC_2$$+$$open_2$-$\LIND{}$$+$$\SIG{1}$-$WSN$.

Observations

• If we imagine $b$ being the work tape contents of a logspace machine and $A$ computing the next step of such a machine, then the $w$ asserted by WSN could give a complete computation of the machine on some input.
• So the point of $\SIG{1,2}$-$REPL$, and $\hat\Delta^b_i$-$COMP$ in these in the axiomatizations is to allow one to output polynomially many bits, where the $i$th bit is computed by $(i, x) \in L$ for some logspace computable language $L$.
• If $TLS^1_2$ proves a formula to be $\hat\Delta^b_1$, it can use $\SIG{1}$-$WSN$ to prove $COMP_A$.
• Using this, $TLS^1_2$ can prove its $\Sigma^b_1$-definable functions are closed under $B_2RN$ and $CRN$. In turn, given these closures, a witnessing argument shows $TLS$ is $\forall\hat\Sigma^b_1$-conservative over $TLS^1_2$.
• Define $TLS^i_2$ to be $\BASIC_2$$+$$open_2$-$\LIND{}$$+$$\SIG{i}$-$WSN$. Then can show $TLS^{i+1}_2 \supseteq S^i_2$ using $open_2$-$\LIND{}$ and that $TLS^{i+1}_2$ proves $\hat\Delta^b_{i+1}$-$COMP$.
• As $S^i_2$ can proves its $\SIG{i+1}$-definable multifunction are closed under $B_2RN$, one can carry out a witnessing argument on $TLS^{i+1}_2$ proofs to show $TLS^{i+1}_2$ is $\forall\hat\Sigma^b_{i+1}$-conservative over $S^i_2$.

Modifying $WSN$ to work without $\#$

• The $WSN$ rule uses $\#$ in the expression $bd(|k|, t)$, but if we only want to simulate $|t|/||k||$ steps with each configuration using $||k||$ bits then we need a number of size at most $2\cdot 2^{(||k||+1)(|t|/{||k||}+1)} < t^m$ for some fixed $m$.
• Let $\Psi$$-$$WSN^-$ be the rule for formulas $A \in \Psi$: $$\frac{ b \leq |k(j,\vec{a})|\sequent \exists! x \leq |k|A(j,\vec{a},b,x) } {\sequent \exists w \leq t^m\forall j < MSP(|t|,|||k|||) A(j,\vec{a},\hat\beta_{|k^*|}(j,w), \hat\beta_{|k^*|}(Sj,w))}$$
• Notice if $A$ matches the quantifier shape that Nepomnjascij's Theorem gives for logspace, then the conclusion of $WSN^-$ does as well.

EuH and EquH

• Consider the following hierarchy of formulas:
  $\qquad(Eu)_0(\Psi) :=$ the $\Psi$ formulas.
  $\qquad(Eu)_{k+1}(\Psi) :=$ $(Eu)_{k}(\Psi)$ and formulas of the form $(\exists x < t)\phi$ and $(\forall x < MSP(|t|,|||s|||))\phi$ for $\phi\in (Eu)_{k}(\Psi)$.
  $\qquad EuH(\Psi) := \cup_k (Eu)_{k}(\Psi).$
• Let $(Eu)_k := (Eu)_{k}(open)$ and $EuH := EuH(open)$.
• Define $(Equ)_k(\Psi)$, $(Equ)_k$, $EquH(\Psi)$, and $EquH$ similarly except allow the bound on universal quantifiers to be of the form $2^{p(||x||)}$ for some polynomial $p$.
• If we have $\#$ in the language then replacement axioms can be used to show any $EuH$ formula is equivalent to a $\SIG{1}$-formula. If we add $x\#_3 y = 2^{|x|\#|y|}$ to the language then using replacement any $EquH$ formula is equivalent to a $\SIG{1,3}$-formula.
• $EuH$ and $EuH(\hat\Pi^b_{i-1})$ seem like reasonable analogs of $\SIG{1}$ and $\SIG{i}$ for the language without $\#$.
• Nepomnjascij's Theorem and the fact that we can project and manipulate bits from a string with terms in our language, and so can check whether a logspace/SC configuration follows from a previous one, shows that $EuH$ contains logspace and $EquH$ contains $SC$.

Fragments of $I\Delta_0$

• Define $TLS^i_1$ for $i > 0$ to be $\BASIC_1$$+$$open_1$-$\LIND{}$$+$$EuH(\hat\Pi^b_{i-1})$-$WSN$.
• Define $TSC^i_1$ for $i > 0$ to be $\BASIC_1$$+$$open_1$-$\LIND{}$$+$$EquH(\hat\Pi^b_{i-1})$-$WSN$.
• $TLS^i_1$ can prove its sharply bounded $EuH(\hat\Pi^b_{i-1})$-definable functions are closed under $B_2RN$.
• The sharply bounded $EuH(\hat\Pi^b_{i-1})$-definable functions of $TLS^i_1$ are the sharply bounded logspace computable functions with access to a $\hat\Sigma^b_{i-1,1}$ oracle. In the $i=1$, case we get just logspace.
• The predicates in $TLS^i_1$ which are provably equivalent to an $EuH(\hat\Pi^b_{i-1})$ formula and the negation of such a formula are the$L^{\hat\Sigma^b_{i-1,1}}$-predicates.
• Analogous results hold for $TSC^i_1$ but where we replace logspace with SC.

Conclusion

• We have surveyed arithmetic classes within the linear time hierarchy.
• I have hopefully shown via Nepomnjascij's Theorem and quantifier replacement why $EuH(\hat\Pi^b_{i-1})$ is the natural analog of $\SIG{i}$ in the language without $\#$.
• Given this, the definability, closure properties of $TLS^{i}_1$ seem to make for a reasonable decomposition of $I\Delta_0$.