Total Search Problems in Bounded Arithmetic and Improved Witnessing

Abstract

We define a new class of total search problems as a subclass of Megiddo and Papadimitriou’s class of total ${\mathsf {NP}}$ search problems, in which solutions are verifiable in ${\mathsf {AC}}^0$. We denote this class $\forall \exists {\mathsf {AC}}^0$. We show that all total ${\mathsf {NP}}$ search problems are equivalent, w.r.t. ${\mathsf {AC}}^0$-many-one reductions, to search problems in $\forall \exists {\mathsf {AC}}^0$. Furthermore, we show that $\forall \exists {\mathsf {AC}}^0$ contains well-known problems such as the Stable Marriage and the Maximal Independent Set problems. We introduce the class of Inflationary Iteration problems in $\forall \exists {\mathsf {AC}}^0$, and show that it characterizes the provably total ${\mathsf {NP}}$ search problems of the bounded arithmetic theory corresponding to polynomial-time. Cook and Nguyen introduced a generic way of defining a bounded arithmetic theory ${\mathsf {VC}}$ for complexity classes ${\mathsf {C}}$ which can be obtained using a complete problem. For such C we will define a new class ${\mathsf {KPT[C]}}$ of $\forall \exists {\mathsf {AC}}^0$ search problems based on Student-Teacher games in which the student has computing power limited to ${\mathsf {AC}}^0$. We prove that ${\mathsf {KPT[C]}}$ characterizes the provably total ${\mathsf {NP}}$ search problems of the bounded arithmetic theory corresponding to ${\mathsf {C}}$. All our characterizations are obtained via “new-style” witnessing theorems, where reductions are provable in a theory corresponding to AC $^0$.

Appendix A: Proof of Theorem 15

In what follows, when we say that a theory $\mathcal {T}$ proves a sequent

$$\begin{aligned} \varphi _1, \ldots , \varphi _k\longrightarrow \psi _1, \ldots \psi _l, \end{aligned}$$

we mean that $\mathcal {T}$ proves

$$\begin{aligned} \bigwedge _{i = 1}^{k} \varphi _i \supset \bigvee _{j = 1}^l \psi _j. \end{aligned}$$

Buss [5] originally proved his witnessing theorem for ${\mathsf {V}}^1$ via a witnessing lemma. Here, we do the same; that is to say, we use a new-style witnessing lemma in order to prove Theorem 15.

Lemma 17

(New-style Witnessing Lemma for ${\mathsf {V}}^1$ ). Suppose that the theory ${\mathsf {V}}^1$ proves a sequent $\varGamma (A)\longrightarrow \varDelta (A)$ of the form

$$\begin{aligned} \ldots , \exists X_i \phi '_i(X_i), \ldots , \varLambda \longrightarrow \varPi , \ldots , \exists Y_j \psi '_j(Y_j), \ldots \end{aligned}$$

(10)

where $\phi '_i, \psi '_j, \varLambda$ and $\varPi$ are $\varSigma ^B_0$-formulae. Then there is an ${\mathsf {IITER}}$ problem $Q_F$ with graph $\psi _F$ and ${\mathsf {F}}{\mathsf {AC}}^0$-functions $\varvec{G}$ such that $\overline{{\mathsf {V}}}^0$ proves the sequent $\varGamma '\longrightarrow \varDelta '$, which is

$$\begin{aligned} \ldots , \phi '_i(\beta _i), \ldots , \varLambda , \psi _F(A, \varvec{\beta }, \gamma ) \longrightarrow \varPi , \ldots , \psi '_j(G_j(A, \varvec{\beta }, \gamma )), \ldots \end{aligned}$$

(11)

We will use a version of the sequent calculus to prove this lemma. Given a sequent calculus proof $\pi$ of (10) we try to show the conclusion of Lemma 17 by structural induction on the depth of a sequent S in $\pi$. If we use directly a sequent calculus for ${\mathsf {V}}^1$, we have the issue that the $\varSigma ^B_1$-${\mathsf {COMP}}$ axiom is in general not equivalent to a $\varSigma ^B_1$-formula. As a result, the proof $\pi$ may contain formulae that are not $\varSigma ^1_1$. To circumvent this obstacle, we need to work with a slightly different theory $\widetilde{{\mathsf {{V}}}}^1$ equivalent to ${\mathsf {V}}^1$. For that, first consider the following definition:

Definition 18

(Cook and Nguyen [8]). Let $\psi (X)$ be an $\mathcal {L}^2_A$-formula. Then $\psi$ is a single- $\varSigma ^1_1$ -formula if $\psi$ is of the form $\exists Y \varphi (X, Y)$, where $\varphi$ is a $\varSigma ^B_0$-formula. If $\psi$ is of the form $(\exists Y \le t) \varphi (X, Y)$, where $\varphi$ is a $\varSigma ^B_0$-formula and t is an $\mathcal {L}^2_A$-term not involving Y, then $\psi$ is a single- $\varSigma ^B_1$ -formula.

Definition 19

(Cook and Nguyen [8]). The theory ${\tilde{V}}^1$ is axiomatized by the axioms of ${\mathsf {V}}^0$ plus the single-$\varSigma ^B_1$-${\mathsf {IND}}$ axiom scheme.

Below, we merely state that $\widetilde{{\mathsf {{V}}}}^1 = {\mathsf {V}}^1$ without proof. A full proof of it can be found in [8, Theorem VI.4.8].

Theorem 20

(Cook and Nguyen [8]). The theories ${\tilde{V}}^1$ and ${\mathsf {V}}^1$ are the same.

The sequent calculus ${\mathsf {LK}}$-${\tilde{V}}^1$ for ${\tilde{V}}^1$ is essentially the sequent calculus ${\mathsf {LK}}$-${\mathsf {V}}^0$ for ${\mathsf {V}}^0$ (c.f. [8]) augmented with the single- $\varSigma ^B_1$-${\mathsf {IND}}$ rule, which is

where $\chi \in \varSigma ^{\mathrm {B}}_1$, and b is an eigenvariable and cannot appear in the lower sequent.

The sequent calculus ${\mathsf {LK}}$-${\tilde{V}}^1$ satisfies the following property, whose proof can be found in [8]:

Theorem 21

(Cook and Nguyen [8]). Suppose that $\widetilde{{\mathsf {{V}}}}^1$ proves a sequent $\varGamma \longrightarrow \varDelta$ consisting only of single-$\varSigma ^1_1$-formulae. Then there is an ${\mathsf {LK}}$-$\widetilde{{\mathsf {{V}}}}^1$ proof $\pi$ of $\varGamma \longrightarrow \varDelta$ such that every formula in $\pi$ is a single-$\varSigma ^1_1$-formula.

We are now ready to prove Lemma 17. The proof technique we use to prove Lemma 17 is similar to the one used for Theorem VI.4.1 in [8, p. 154] (which is a witnessing theorem for ${\mathsf {V}}^1$), which adopts the same proof technique as Buss (cf. [5, Theorem 5]).

Proof

(of the New-style Witnessing Lemma for ${\mathsf {V}}^1$ , Lemma 17 ). Since $\widetilde{{\mathsf {{V}}}}^1$ and ${\mathsf {V}}^1$ are the same, it follows that $\widetilde{{\mathsf {{V}}}}^1$ proves (10). By Theorem 21, let $\pi$ be an ${\mathsf {LK}}$-$\widetilde{{\mathsf {{V}}}}^1$ proof of (10) such that every formula in $\pi$ is a single-$\varSigma ^1_1$-formula. We show that $\overline{{\mathsf {V}}}^0$ proves the conclusion of Lemma 17 by induction on the depth of a sequent S in $\pi$. The inductive proof splits into cases, depending on whether S is an initial sequent or generated by the use of an inference rule. The most crucial case is the case of the single-$\varSigma ^B_1$-${\mathsf {IND}}$ rule.

Suppose that S is obtained by the application of the single-$\varSigma ^B_1$-${\mathsf {IND}}$ rule. Then S is the bottom sequent of

where (omitting the parameters $A$) $\psi (b)$ is of the form $(\exists X \le r(b)) \psi _0(b, X)$ and

$$\begin{aligned} \varPi = \varPi ', \exists Y_1 \psi '_1(Y_1),\ldots , \exists Y_l \psi '_l(Y_l). \end{aligned}$$

Here $\varPi ', \psi '_1, \ldots , \psi '_l$ is a sequence of $\varSigma ^B_0$-formulae. Let $\eta (b, \beta )$ denote the formula $|\beta | \le r(b) \wedge \psi _0(b, \beta )$. By the induction hypothesis, let $Q_{F_1}$ be an ${\mathsf {IITER}}$ problem specified by $F_1$ and $t_1$, with graph $\psi _{F_1}$, and $G^1_1, \ldots , G^1_l$ and $G^1_{l + 1}$ be the witnessing functions for the formulae in $\varPi , \psi (b + 1)$ such that $\overline{{\mathsf {V}}}^0$ proves the following (omitting the parameters $A$, $\varvec{\lambda }$, where $\varvec{\lambda }$ are witnesses for the formulae in $\varLambda$):

$$\begin{aligned} \eta (b,\beta ), \varLambda ', \psi _{F_1}(b,\beta , \gamma ) \longrightarrow \varPi ''(G^1_j(b, \beta , \gamma )), \eta (b + 1,G^1_{l + 1}(b, \beta , \gamma )) \end{aligned}$$

(12)

where $\varLambda '$ is the result of witnessing $\varSigma ^1_1$-formulae in $\varLambda$ and leaving the rest unchanged and $\varPi ''(G^1_j(b,\beta , \gamma )) = \varPi ', \psi '_1(G^1_1(b,\beta ,\gamma )), \ldots , \psi '_l(G^1_l(b,\beta ,\gamma ))$. Our goal is to construct an ${\mathsf {IITER}}$ problem $Q_F$ (with graph $\psi _F$) and ${\mathsf {F}}{\mathsf {AC}}^0$-functions $G_1, \ldots , G_l$ and $G_{l + 1}$ such that $\overline{{\mathsf {V}}}^0$ proves the following:

$$\begin{aligned} \eta (0, \beta _0), \varLambda ', \psi _F(\beta _0, \gamma ) \longrightarrow \varPi ''(G_j(\beta _0, \gamma )), \eta (t, G_{l +1}(\beta _0, \gamma )). \end{aligned}$$

(13)

The intuitive idea behind the definition of $Q_F$ is that, assuming that $\eta (0,\beta _0)$ is true, we will repeatedly use $Q_{F_1}$ and $G^1_{l + 1}$ in order to generate witnesses $\beta _1, \ldots , \beta _n$ for $\psi (1), \ldots , \psi (n)$, respectively, for $n \le t$. If $n < t$, then $Q_{F_1}$ failed to generate a witness to $\psi (n + 1)$. Therefore, assuming that the hypothesis for (13) is true and using (12), we obtain our desired goal.

In what follows, the string concatenation function $X *_z Y$ is an ${\mathsf {F}}{\mathsf {AC}}^0$ string function that concatenates the first z bits of X with Y and can be recursively extended in the natural way. Omitting the subscripts to $*$, we write $Y_0 *\ldots *y *\ldots *Y_k$ for $Y_0 *\ldots *Y *\ldots *Y_k$, where Y is the string representing the unary notation of the number value y.

We assume that the search variable for $Q_F$ is of the form

$$\begin{aligned} \gamma = \langle A, \beta _0, \varvec{\lambda }\rangle *_s S_0 *_{2s} S_1 *_{3s} \ldots *_{(m + 1)s} S_m, \end{aligned}$$

where s (s is obtained from t and the bounding term r, in the induction-formula $\psi$, and the bounding term $t_1$ for $Q_{F_1}$) is a suitable $\mathcal {L}^2_A$-term that bounds $|\langle A, \beta _0, \varvec{\lambda }\rangle |, |S_0|, \ldots , |S_m|$; the symbol $S_i$ denotes $i *\beta _i *\gamma _i *1$ and $m \le t$. Note here that, even though we omitted the subscripts to $*$ in $S_i$, they are somehow implicit. Let us now define the transition function F for $Q_F$. In the following, we again omit the parameters $A, \varvec{\lambda }$ for F. As usual, we will drop the subscripts to $*$ in $F(\beta _0,\gamma )$. If $\gamma =\emptyset$, then

$$\begin{aligned} F(\beta _0, \gamma ) = \langle A, \beta _0, \varvec{\lambda }\rangle *0 *\beta _0 *\emptyset *1. \end{aligned}$$

(14)

Assume now that $\gamma \not = \emptyset$ and suppose that $m < t$ and $\eta (m, \beta _m)$ is true. Then there are two cases to consider. First, if $|\gamma _m| \le t_1 \wedge \gamma _m < F_1(m, \beta _m, \gamma _m) \wedge \lnot \psi _{F_1}(m, \beta _m, \gamma _m)$ is true, then

$$\begin{aligned} F(\beta _0, \gamma ) = \langle A, \beta _0, \varvec{\lambda }\rangle *S_0 *\ldots *S_{m - 1} *m *\beta _m *F_1(m, \beta _m, \gamma _m) *1. \end{aligned}$$

(15)

Second, if $|\gamma _m| \le t_1 \wedge \gamma _m < F_1(m, \beta _m, \gamma _m) \wedge \psi _{F_1}(m, \beta _m, \gamma _m)$, then

$$\begin{aligned} F(\beta _0,\gamma ) = \langle A, \beta _0, \varvec{\lambda }\rangle *S_0 *\ldots *S_m *(m + 1) *G^1_{l + 1}(m, \beta _m, \gamma _m) *\emptyset *1. \end{aligned}$$

(16)

In all other cases, $F(\beta _0, \gamma ) = \gamma$. Let $t_{Q_F}$ be $(t + 2)\cdot s$ and $Q_F$ be specified by F and $t_{Q_F}$. Finally, we define the ${\mathsf {F}}{\mathsf {AC}}^0$-functions $G_i$, for $i = 1,\ldots , l + 1$, as follows:

$$\begin{aligned} G_j(\beta _0, \gamma ) = {\left\{ \begin{array}{ll} \beta _0 &{} \quad \text {if } t = 0 \\ G^1_j(m, \beta _m, \gamma _m) &{} \quad \text {otherwise,} \end{array}\right. } \end{aligned}$$

The fact that $\overline{{\mathsf {V}}}^0$ proves (13) follows from (13)’s assumptions, from the following claim, the induction hypothesis and the definition of $G_j$ above. As a side remark, note that if $t = 0$, then $\overline{{\mathsf {V}}}^0$ proves (13) trivially.

Claim

We reason in $\overline{{\mathsf {V}}}^0$. Suppose that $t \not = 0$, $\eta (0, \beta _0)$ is true and $\gamma = \langle A, \beta _0, \varvec{\lambda }\rangle *S_0 *\ldots *S_m$ is a solution to $Q_F(\beta _0)$, where $S_i$ is again of the form $i *\beta _i *\gamma _i *1$. Then $\eta (m, \beta _m)$ is true; $\gamma _m$ is a solution to $Q_{F_1}(m,\beta _m)$; and either $\lnot \eta (m + 1, G^1_{l + 1}(m, \beta _m, \gamma _m))$ or $\eta (t, G_{l + 1}(\beta _0, \gamma ))$ is true.

Proof of Claim. Since $\gamma$ is a solution to $Q_F(\beta _0)$, then we have two possibilities: either $\gamma = \emptyset$ and $F(\beta _0, \gamma ) = \gamma$, or

$$\begin{aligned} |\gamma | \le t_{Q_F} \wedge \gamma < F(\beta _0, \gamma ) \wedge [|F(\beta _0, \gamma )| > t_{Q_F} \vee F(\beta _0, F(\beta _0, \gamma )) = F(\beta _0, \gamma )]. \end{aligned}$$

Note that, by the definition of F, $\emptyset$ cannot be a solution to $Q_F(\beta _0)$ and $|F(\beta _0,\gamma )| \le t_{Q_F}$. Therefore, we have that

$$\begin{aligned} \gamma \not = \emptyset \wedge \gamma < F(\beta _0, \gamma ) = F(\beta _0, F(\beta _0, \gamma )). \end{aligned}$$

(17)

The only way for (17) to hold is if (16) is true. This implies that $\eta (m, \beta _m)$ holds and $\psi _{F_1}(m, \beta _m, \gamma _m)$ is true; that is to say, $\gamma _m$ is a solution $Q_{F_1}(m, \beta _m)$. Hence, we are left with proving the following:

$$\begin{aligned} \lnot \eta (m + 1, G^1_{l + 1}(m, \beta _m, \gamma _m)) \vee \eta (t, G_{l + 1}(\beta _0,\gamma )). \end{aligned}$$

If $m + 1 = t$, then we are done. So, assume that $m + 1 < t$. For the sake of contradiction, assume that $\eta (m + 1, G^1_{l + 1}(m, \beta _m, \gamma _m))$ holds. This means that $F(\beta _0,\gamma ) < F(\beta _0, F(\beta _0,\gamma ))$, which is a contradiction. Thus, we are done with the proof of the claim.    $\square$

This finishes the proof of Lemma 17.