数理解析研究所講究録976 巻 1997 年 1-12

1

Bounded Arithmetic$\mathrm{v}\mathrm{s}$. Propositional Calculus

Noriko H. Arai (新井紀子)
Department of Computer Science, Hiroshima City University

151 Ozuka, Asaminami-ku, Hiroshima 731-31 Japan

Introduction1

In [11], Cook and Reckhow showed a close relation between the relative efficiency of propoproblem, though it is rather unrealistic to dream to show thesitional calculi andinequality
by showing that there is no super system for propositional logic.
However, recent researches have revealed that the study of lengths of proofs in propositional calculi may benefit substantially to solve other open problems in the computational. It was Cook’s result [9] which revealed the fact that certain
complexity such assystems of bounded arithmetic bridges the hierarchy of computational complexity and that ofpropositional calculus. In [9], he introduced an equational system $PV$ as a theory of polynomial time functions analogous to the theory of primitive recursive functions, $PRA$ . $PV$
contains a schema which allows function symbols to be introduced for every polynomial timecomputable function and an induction schema to be applied for open formulas in $PV$ . He
showed that any $PV$ -proof can be translated into polynomial-size $eF$ -proofs and that $PV$ isable to prove the formalized consistency of $eF:PV$ can prove that “A is a tautology” whenhas a polynomial-size $eF$-proof.
Buss introduced the system
as the formal foundation for polynomial-time computablefunctions [5]. It has a
set of function symbols, a set of axioms on the functions and thelength induction on -predicates, whereas $PV$ has an infinite set of function symbols and theinduction on open formulas. Buss showed that
corresponds with the polynomial
time hierarchy [20] in the sense that every -functions is -definable in , and the converse
holds true: every -definable function in
is in . Later, it was shown that the polynomial
time hierarchy provably collapses if and only if
does, or equivalently if and only ifisfinitely axiomatizable [17], [7]. In particular, the following relations hold:$\mathrm{P}=?\mathrm{N}\mathrm{P}$$\mathrm{P}\neq \mathrm{N}\mathrm{P}$$\mathrm{P}=?NC^{1}$$A$$S_{2}^{i}$$\mathfrak{H}\mathrm{n}\mathrm{i}\mathrm{t}\mathrm{e}$$\Sigma_{i}^{p}$$S_{2}=def \bigcup_{i=0}^{\infty}S_{2}i$$S_{2}^{i}$$S_{2}^{i}$$\Sigma_{i}^{b}$$\coprod_{i}^{p}$$\Sigma_{i}^{b}$$\coprod_{i}^{p}$$S_{2}$

1.

$S_{2}^{1}$

is a system which characterizes the functions in

2. Any3.

$S_{2}^{1}$$S_{2}$$S_{2}^{1}$$\mathrm{P}$as$\Sigma_{1}^{b}$-definable functions.

proof of bounded formula is translatable into polynomial-size $eF$ proofs [6], [3].

proves the consistency of $eF$ .

Here rises an interesting question: what systems of bounded arithmetic characterize thefunctions in the classes of computational complexity such as
and $NC^{1}$ , and to what
propositional calculi are they tranSlatable’. The answers are partly known: there does exist
a bounded arithmetic which characterize functions inand it is translatable into a wellknown propositional calculus, bounded depth Frege.
It was conceived that the class of problems solved by bounded depth circuits $(AC^{0})$ isclosely related to the class of tautologies having polynomial-size bounded depth Frege proofs.
At the same time, it had been strongly predicted that the class of problems (and functions)$AC^{0}$$AC^{0}$

2. Among them were theandrelated to “counting” would draw the line separatingthat the parity problem
Ajtai
1983,
showedprinciple.
In
pigeonhole
theandparity problem
gives the superpolynomial lowerbound for $AC^{0}[1]$ . Later the lowerbound was improved toexponential [22], [13].
There rose a totally different interest in the field of bounded arithmetic: what is the weakest
bounded arithmetic which proves the fact that there are infinitely many primes? The famous
Euclid’s proof for the existence of infinitely many primes uses the function !, though the next
prime of is bounded by polynomial of .
is defined as a bounded arithmetic with the language of Peano arithmetic
The system
proves theand the induction on the class of bounded formulas. Woods showed that[21].
In [18],principle
pigeonhole
theprovesitprimesifmanyinfinitelyof
existence
to a new relation symbol are translatable tothey showed that proofs in the relativised
the line, Ajtai showed that the pigeonhole
proofs.
Along
depth
Frege
boundedpolynomial-size
does notprinciples do not have polynomial-size bounded depth Frege proofs and that[2].
simultaneously
principle
prove the pigeonhole
There are a few attempts to find a suitable system of bounded arithmetic which characor ALOGTIME. In [4], Arai introduced a system called AID
terizes the functions inwhich is an analogue to , and in [8], Clote introduced ALV that of $PV$ . Accordingly,(ALOGTIME), AID (ALV) and Frege will enjoy the similar relations that $P,$ $S_{2}^{1}(PV)$ and $eF$
do [10].
The map of hierarchies of propositional calculi, bounded arithmetic and complexity classes,
shown in the literature, can be sketched as follows: for systems below the horizontal line,
lowerbounds are known.
$NC^{1}$$AC^{0}$$p$$p$$\mathrm{I}\triangle 0$$\mathrm{I}\triangle_{0}$$(\triangle 0-)$$R$$\mathrm{I}\triangle 0$$\mathrm{I}\triangle_{0}(R)$$NC^{1}$$NC^{1}$$S_{2}^{1}$extended E’regePV$\mathrm{P}$$\mathrm{F}\mathrm{r}\mathrm{e}\mathrm{g}\mathrm{e}+\mathrm{s}\mathrm{u}\mathrm{b}\mathrm{s}\mathrm{t}\mathrm{i}\mathrm{t}\mathrm{u}\mathrm{t}\mathrm{i}_{\mathrm{o}\mathrm{n}}$$S_{2}^{1}$$\mathrm{F}\mathrm{r}\mathrm{e}\mathrm{g}\mathrm{e}+\mathrm{r}\mathrm{e}\mathrm{n}\mathrm{a}\mathrm{m}\mathrm{i}\mathrm{n}\mathrm{g}$Frege,$\mathrm{L}\mathrm{K}$

AID
ALV

, NK

$\Downarrow\#$bounded depth Frege$\Downarrow$$\Downarrow$$\Downarrow$.. .

ALOGTIME$\Downarrow\#$$\Downarrow \mathrm{t}^{l}$...

$\mathrm{I}\triangle_{0}(f)$...

$AC^{0}$In this paper, we give a technique to translate bounded -proofs into polynomial-size $eF$
proofs, which is called the linewise translation. When a bounded normal form -proof isgiven, the proof can be viewed as a pile of computations with the free variables in the end
sequent as its input. Since it is a bounded proof, every non-parameter variable in the proof
must be eliminated as a bound variable bounded by a term . Hence, the range of does notexceed . We can inductively compute the bound of in terms of parameter variables. Then,
we are ready to compute the polynomial space bound for the computation associated witheach line of the proof. Now, it is ready to be translated into polynomial-size $eF$ proofs almost
automatically.
$S_{2}^{1}$$S_{2}^{1}$

$a$

$t$

$t$

$a$

$a$

3

Translation ofFrege proofs

2

proofs to polynomial-size extended$\mathrm{S}_{2}^{1}$

Now we present our translation algorithm fromdefinitions [6].

Definition 1 Let be a term ofby:$t$$S_{2}^{1}$$S_{2}^{1}$

into $eF$ . We first follow Buss’ original. The bounding polynomial$q_{t}(n)$of is defined inductively$t$

1. $q_{0}(n)=1$
2. $q_{a}(n)=n$ for any variable$a$

3. $q_{s(t)}(n)=qt(n)+1$
4. $q_{t+u}(n)=q_{t}(n)+q_{u}(n)$5. $q_{t\cdot u}(n)=q_{t}(n)+q_{u}(n)$6. $q_{t\# u}(n)=qt(n)\cdot q_{u}(n)+1$7.

$q_{|t|}(n)=q \lfloor\frac{1}{2}\iota\rfloor(n)=q\iota(n)$Proposition 1 If
numbers of length1.

$|t(_{\vec{X}})|\leq qt(n)$2. $q_{t}(n)\geq n$ if

is a term and, then the following holds;$t(a_{1}, \ldots , a_{k})$$\leq n$$\ldots$,$x_{k}$

are variables ranging over natural,$var(t)\neq\emptyset$

Definition 2 Let
tively defined by:$x_{1},$$A$.

be a bounded formula of$S_{2}^{1}$. The bounding polynomial$q_{A}$of$A$

is induc-

1. $q_{t=u}=qt\leq u=qt+q_{u}$2. $q_{A\wedge B}=q_{AB}\vee=q_{A}\supset B=q_{A}+qB$

3. $q_{\neg A}=qA$
4.

$q_{(\exists x\leq t}$) $A(n)=q_{(x\leq}\forall\iota)A(n)=q_{\iota}(n)+qA(n+qt(n))$

Proposition 2 The bounded formula.
length$A(x_{1}, \ldots , x_{k})$where$|x_{i}|\leq n$, only refers to numbers of$\leq q_{A}(n)$Proposition 3 [5] Let be a bounded formula inprovesthen there is a boundedin A. Suppose that
free, free variable normal form.
$A$

be the list offree variables
pr.oof of such that it is free-cut$S_{2}^{i}(i\geq 1)$$S_{2}^{i}$$A_{f}$$S_{2}^{i}$and$\vec{a}$$A$proofs into free variable normal proofs increases the size of proofs
Note that translating
only linearly. On the contrary, producing free-cut free proofs requires superexponential function in general. However, it makes only the difference of constant when we focus on only one
proof. Without loss of generality, we only consider free-cut free, free variable normal form
proofs.
proofsNow we are going to define a bounding term $tm(b;P)$ for a free variable in an
in .
so that ranges over natural numbers bounded by$S_{2}^{i}$$S_{2}^{i}$$S_{2}^{i}$$b$$\overline{tm(b\cdot,P)}$$b$

be a bounded, free-cut free and free variable normal form proof in .
be a variable occurring in . The bounding term $tm(b;P)$ of is inductively defined by:

Definition 3 Let
Let

$b$

$S_{2}^{1}$

$P$

$P$

$S_{2}^{1}$

$P$

$b$

4
1. $tm(b;P)=b$ if is a parameter variable.
$b$

2. Otherwise, let denote the unique elimination inference of inable , of which elimination inference appears below , assume
defined. Note that is one of
$I$

$b$

$I$

$\Sigma_{1}^{b}$. For every free vari-that.tm $(a;P)$ is already

$I$

$a$

$P$

-PIND
$\frac{\Gamma,A(\lfloor\frac{1}{2}b\rfloor)arrow A(b),\triangle}{\Gamma,A(0)arrow A(u),\triangle}$($\forall\leq$: right)$\frac{b\leq u,\Gammaarrow\triangle,C(b)}{\Gammaarrow\triangle,(\forall x\leq u)c(_{X)}}$or($\exists\leq$: le $ft$ )$\frac{b\leq u,A(b),\mathrm{r}arrow\triangle}{(\exists x\leq u)A(_{X),\mathrm{r}arrow\triangle}}$where $u=u(\vec{a})$ . Since occur free ininferences appear below .
$\vec{a}$$u$.

, either they are parameter variables or their$I$$\mathrm{d}\mathrm{i}\mathrm{n}\dot{1}\mathrm{n}\mathrm{a}\mathrm{t}\mathrm{i}_{\mathrm{o}\mathrm{n}}$Define $tm(b;P)=u(\vec{a}/tm(a;\prec P))$ .
For a technical reason, we extend the language ofby introducing a new set of free$b^{k}(k=0,1,2,\ldots)$variables,.
. it means a free variable ranging over of length lessthan or equal to . The elimination inference of must be one of -PIND, (: right)or (: left) as shown above. Furthermore, must be greater or equal to the length of$u(\vec{a}/tm(\vec{a},P))$ so thatis large enough for to be replaced by the term .
$S_{2}^{1}$$\mathrm{I}\mathrm{n}\mathrm{t}\mathrm{u}\mathrm{i}\mathrm{t}\mathrm{i}\mathrm{v}\mathrm{e}\mathrm{l}\mathrm{y}_{J}$$k$$b^{k}$$(\forall\leq)$$\Sigma_{1}^{b}$$k$$(\exists\leq)$$k$$b^{k}$$u$Lemma 1 Suppose that is a free-cut free, free variable normal form
proof of a bounded. When we replace every free variable by $b^{k}(k=q_{tm(bP};)(n))f$ we again obtain aformulawell-formed proof in the extended language.
$P$$S_{2}^{1}$$A(a)arrow$$b$$S_{2}^{1}$(Proof.) Obvious from the definition of $tm(b;P)$ .
Lemma 2 Let be a bounded, free-cut free and free variable normal form proof in , andbe a variable occurring in P. Suppose that the lengths of parameter variables are bounded. Then, ranges over of length $\leq q_{tm(b;P)}(n)$ in .
$P$

$S_{2}^{1}$

$b$

$b.y$

$P$

$b$

$n$

Definition 4 Let be a bounded, free-cut free and free variable normal form proof inandbe a formula in . The bounding polynomialof in , is defined by where$A^{*}=A(b/t\vec{m}(barrow;P))$ .
$P$$A(b)arrow$$S_{2}^{1}$

$P$

$A$

$q_{(A;P)}$$P$$q_{A^{*}}$

We take a polynomial function $p(n)$ as the bounding polynomial of so that it dominates
all the-polynomials of formulas in .
For example, we can define the bounding polynomial of as follows: suppose that each
is in the form
. Then,$P$$P$$\mathrm{b}_{0}\mathrm{u}\mathrm{n}\mathrm{d}\mathrm{i}\mathrm{n}\mathrm{g}$$p$$q_{(A;^{p})}$$P$$d_{A}^{k}\cdot x^{k}+\cdots+d_{A}^{1}\cdot x+d_{A}^{0}$$p(x)=C_{m}\cdot x^{m}+\cdots+c_{1}\cdot X+c0$

is defined by$c_{i}= \max${$d_{A}^{i}|A$is a formula in

$P$

}.

5
Lemma 3 Let be a bounded, free-cut free and free variable normal form proof inof whichparameter variables areandbe a subproof of P. Let and be the bounding
polynomials ofand , respectively. Suppose that $|a_{i}|\leq n$ for all $1\leq i\leq k_{f}$ and that$|b|\leq q_{tm(b;P)}(n)$for every non-parameter variable in the end-sequent of Q. Then,$P$$S_{2}^{1}$$a_{1},$$P$$Q$$\ldots,$ $a_{k)}$

$p$

$q$

$Q$

$b$

1.

$P$

only refers to the numbers of which length $is\leq p(n)$ .

2. $p(n)\geq q(n)$ for all .
$n$

It is known that there are fan-out 1 polynomial-size family of Boolean circuits for computing
the function symbols of the language of : for each function symbol in, there is apolynomial function
such that the circuit [takes one or two inputs of length
tocomputes the function , and the size of [is bounded by $p_{f}(n)$ . Since they are fan-out 1
Boolean circuits, they are readily translated into Boolean formulas.
It is also known that there are polynomial-size extended Frege proofs for the BASIC axiomsof . We pick a polynomial function to dominate these polynomials. If is a bounded
proof and is the bounding polynomial of $P$ , the number of bits necessary for computation
carried out throughout in is bounded by $p(n)$ , where is the length of inputs.
$f$$S_{2}^{1}$$S_{2}^{1}$$f\mathrm{I}n$$p_{f}$$f$$n$$f\mathrm{J}_{n}$$P$$S_{2}^{1}$$p_{b}$$S_{2}^{1}$

$p$

$P$

$n$

We define, for each term , a vector of $m$ propositional formulas [of the value of when its free variables are assigned values of length$t$$t\mathrm{J}_{m}^{n}$$t$

giving the first$\leq n$

$m$

bits

.

Definition 5
1. [$0\mathrm{J}_{m}^{n}$

is a sequence of$m$false formulas (for example

2. If
is a variable with $k\leq m,$ [propositional variables$a^{k}$$v_{k-1}^{a^{k}},$

3. If

$a$

$t+u\mathrm{I}nm$

5. [$+\mathrm{I}_{m}([S\mathrm{I}_{m}^{n}, [t\mathrm{J}_{m}^{n})$$t\mathrm{I}_{m}^{n}$and$s(t)\mathrm{I}^{n}m’[\mathrm{L}^{\frac{1}{2}}t\rfloor \mathrm{I}^{n}m’[|t|\mathrm{I}_{m}^{n},$[$\neg p$).

is a sequence of $m-k$ false formulas followed by. If is a variable with $k>m,$ [is $v_{m-1}^{a^{k}a^{k}},$$a^{k}$$a^{k}.\mathrm{J}_{m}^{n}$$\ldots,$

is a variable (without subscript), Then, [

4. [
is [
to the output of [A$a^{k}\mathrm{I}_{m}^{n}$$v_{0}^{a}k$$\ldots,$$p$$a\mathrm{J}_{m}^{n}$is$[a^{n}\mathrm{J}_{m}^{n}$$v_{0}$.

(the formulas corresponding to the circuit for addition applied$[u\mathrm{I}_{m}^{n}\cdot)$$t\# u\mathrm{I}^{n}m$and [$t\cdot u\mathrm{I}_{m}^{n}$are defined similarly.

Definition 6 A first order formula is in negation-implication normal form (NINF) if every
negation is applied to an atomic subformula and there is no implication. For a bounded formulain NINF and , we define the propositional formula [inductively as follows:
$A$

$m$

1. [

$t=u\mathrm{I}_{m}^{n}$is$A\mathrm{J}_{m}^{n}$$EQ_{m-1}(\ovalbox{\tt\small REJECT}^{t}\mathrm{I}^{n}m’[u\mathrm{J}_{m}^{n})$, where$EQ_{m-1}( \vec{p}, qarrow)=\bigwedge_{k=0}^{m}(p-1krightarrow q_{k})$2. [$t\leq u\mathrm{I}_{m}^{n}$is$LE_{m-1}([t\mathrm{I}_{m}^{n}, [u\mathrm{J}_{m}^{n})$, where$LE_{m-1}(\vec{p}, qarrow)=mk\overline{=}\mathrm{v}_{0}^{1}$

3. [$\neg A\mathrm{J}_{m}^{n}$

4. [A Ais

$B\mathrm{J}_{m}^{n}$$\neg[A\mathrm{I}_{m}^{n}$

is [

for

$A\mathrm{I}_{m}^{n}$A$A$

atomic.

$[B\mathrm{J}_{m}^{n}$.

($\neg p_{k}$A$q_{k}$

A$\bigwedge_{k>j\geq 0}(pjrightarrow q_{j})$

).

6
is

5. [

$AB\mathrm{I}_{m}^{n}$

6. [$(\exists x\leq t)A(x)\mathrm{I}_{m}^{n}$$[A\mathrm{J}_{m}^{n}[B\mathrm{J}_{m}^{n}$is [Avariable such that $k=q_{t}(n)$ .

7. [$b^{k}\leq t$

is [variable such that $k=q_{t}(n)$ .

$8$

.

9.

$(\forall x\leq t)A(x)\mathrm{I}_{m}^{n}$$\simeq\log[(\exists x\leq k.

|t|)A(x)\mathrm{J}_{m}^{n}$where is not of the form
is called a quantifier variable$A(b^{k})\mathrm{I}nm$

$b$

$t$

’

is not of the form
is called a quantifier variable.

$\neg b^{k}\leq t\vee A(bk)\mathrm{I}_{m^{\mathrm{W}\mathrm{h}\mathrm{e}\mathrm{r}}}^{n},\mathrm{e}t$

is

$b$

$\bigvee_{k=0}^{m}-1[\overline{k}\leq|t|$A$A(\overline{k})\mathrm{I}_{m}^{n}$, where

$|s|$

and

$b^{k}$

is a new free

$|s|$

and

$b^{k}$

is a new free

is a term with value$\overline{k}$$k$and length$[( \forall x\leq|t|)A(x)\mathrm{I}nm\mathrm{i}_{\mathrm{S}}\bigwedge_{k=0^{1}}^{m-}[\neg\overline{k}\leq|t|A(\overline{k})\mathrm{I}_{m}^{n}\cdot$

For a sequent $Aarrow B$ , we define [bySuppose that a given formula $B$ occurs positively (resp. negatively) in an
proof, .
(for an existential variable ) andWe assign quantifier variables(for anuniversal variable ) to $B$ so that we will assign different sequences of quantifier variables forto distinct positive (resp. negative) occurrences of $B$ in but all positive (resp. negative)
occurrences of $B$ use the same sequence of quantifier variables for .
$Aarrow B\mathrm{J}_{m}^{n}$$[A\mathrm{I}_{m}^{n}\supset \mathbb{I}^{B}\mathrm{I}_{m}^{n}\cdot$$P$$S_{2}^{1}$$\epsilon_{0’ 1}^{b}\epsilon^{b},$$\mu_{0}^{d},$$x$$\ldots$$\mu_{1}^{d},$$\ldots$

$y$

$P$

$x$

$y$

Proposition 4 For any bounded formula , the propositional formula [in $m,$ .
$A$$A\mathrm{J}_{m}^{n}$is polynomial-size$n$3Main theorem

For the time being, we extend the use of extension inference. A free variable introduced by, can occur in the end-formula (sequent).
an extension rule,
When occurs in the end-formula , we can transform it to a valid $eF$ -proof by substituting
every occurrence of by .
$p$

$prightarrow\phi$$\psi$$p$$p$$\phi$

Theorem 1 Suppose thatis a bounded formula infree-cut free, free variable normal form proof of and$A(a^{n})arrow$

and
. Let
be a
be the number of lines in .
) $.wherepb(n)q(forsomeonsn)iSthe_{C}bounding.polynomialtantc$ of P. The size of)$A$$S_{2}^{1}$$Then_{f}thereareeF-$$theproof_{\mathit{8}}areboundedbyc\cdot m\cdot q\{_{n}^{n}proofsof[A\mathrm{I}_{q}n$$S_{2}^{1}$$P$$S_{2}^{1}\vdash A(a^{n})arrow$

$P$

$m$

Replace every free variable occurring inby , where) $(n)$ . We still have$A_{k}arrow$a well-formed
proof. In [6], they intend to show that for each sequent
in and for any and $m>q(n)$ , there is a polynomial-size $eF$ -proof of [ A... A
by the induction of the number of proof lines of . Intuitively, stands
V. .. Vfor the length of inputs and $m$ for the number of bits necessary for the computation. They let
and $m$ vary as occasion demands in each induction step, however, it is not suggested how toassign numbers to or $m$ . It is quite vague why the whole translation procedure terminatedin polynomial-time; unsuitable assignment of or $m$ can increase the size of the resulting $eF$
proofs exponentially.
Our direct translation use a much simpler induction hypothesis: both and $m$ remainunchanged throughout in the proof. It helps clarifying the underlying situation.
$b$

$P$

$b^{k}$$k=q_{tm\mathrm{t}^{b;}}P$$S_{2}^{1}$$B_{1},$$B_{l}$$\ldots,$$A_{k}arrow B_{1}$$A_{1},$$P$$n$$\ldots,$$A_{1}$$P$$B_{l}\mathrm{J}_{m}^{n}$

$n$

$n$

$n$

$n$

$n$

(Proof of the main theorem.)Base case:
Logical axioms and equality axioms: Straightforward.

7
Basic axioms of.
by$S_{2}^{1}$: For each basic axiom, there are extended Frege proofs of. size bounded$p_{b}(n)$Induction step:
Case 1 ( -right) Suppose$\neg$$P$

ends with$\frac{\Gammaarrow\triangle,B}{\neg B,\Gammaarrow\triangle}$,is atomic. By the induction hypothesis, there is a polynomial-size $eF$ -proof ofwhere. Note that [[is [From this,.
.
we can easily infer$B$$\Gammaarrow\triangle B\mathrm{I}_{q(n)}^{n}$$\Gammaarrow\triangle B\mathrm{J}_{q(n)}^{n}$$\Gamma \mathrm{I}_{q(n)}^{n}\supset[\triangle \mathrm{I}_{q()}^{n}n\mathrm{v}[B\mathrm{I}_{q(n)}^{n}\cdot$$[\neg B\mathrm{J}_{q(n)}^{n}\wedge[\Gamma \mathrm{I}_{q(n)}^{n}\supset[\triangle \mathrm{I}_{q(n)}^{n}\ln eF$

Case 2( -left) Similar to case 1.
$\neg$

Case$3$( -right) Suppose $P$ ends with$\vee$.

$\frac{\Gammaarrow B,\triangle}{\Gammaarrow B\vee c,\triangle}$

By the induction hypothesis, there is a polynomial-size $eF$ -proof of [By$eF$
From this, we can easily infer inthat$\Gammaarrow B\vee\triangle \mathrm{I}_{q(n)}^{n}\cdot$.

$\mathrm{d}\mathrm{e}\mathrm{f}\mathrm{i}[\mathrm{r}\mathrm{J}_{q}^{n}(n)\supset[B\mathrm{I}_{q}^{n}(n)^{}\mathrm{n}\mathrm{i}\mathrm{t}\mathrm{i}_{0}\mathrm{n},\mathrm{t}\mathrm{h}\mathrm{i}\mathrm{S}\mathrm{i}\mathrm{S}[\Gamma[c\mathrm{I}_{q}^{n}(n)\supset[B\mathrm{I}^{n}q(n,)\mathrm{I}^{n}q(n)\mathrm{v}[\triangle \mathrm{J}_{q(}n\mathrm{i}\mathrm{C}\mathrm{h}\mathrm{i}\mathrm{s}in)\mathrm{W}\mathrm{v}_{\mathrm{h}}[\triangle \mathrm{I}_{q}^{n}(n\Gamma^{\cdot}arrow(B\vee C)\mathrm{v}\Delta \mathrm{I}_{q(n)}n$Case 4: ( -right) Similar to case 3.
$\wedge$

Case 5: (Structural rule) A structural rule is one of a weakening inference, an exchange
inference and a contraction. If it is either a weakening or exchange, it is easy.
(Contraction)$\frac{\Gammaarrow B,B,\triangle}{\Gammaarrow B,\triangle}$.

, whichBy induction hypothesis, there is a polynomial-size $eF$-proof of [$\ln
B$ , it isIf a (not sharply) bound variable occurs
is [replaced by different quantifier variables and in the first and second occurrences of [’, . For each , weand [respectively. Suppose that [by an extension rule:
introduce a new variable$\Gammaarrow BB\Delta \mathrm{I}_{q.(n)}^{n}$$x$$\Gamma \mathrm{I}_{q}^{n_{\mathrm{t}n)}}\supset[B\mathrm{J}_{q(n)}^{n}[B\mathrm{I}_{q(n)}^{n}[\triangle \mathrm{I}_{q(n)}^{n}\cdot$

$b$

$c$

$b\mathrm{J}_{m}^{n}=\mu_{m-1},$$\ldots,$$B\mathrm{I}_{q(\rangle}^{n}n$$c\mathrm{I}_{m}^{n}=\nu_{m-1},$$\mu_{0}$$\ldots$$\nu_{0}$$k$$\eta_{k}$$\eta_{k}rightarrow$

Then, prove [[($([B\mathrm{I}_{q}n_{\mathrm{t}n)}(\vec{\mu}))$A$\Gamma \mathrm{I}_{q(n)}^{n}\supset[B\mathrm{I}^{n}q(n)(\eta^{\sim})[\triangle \mathrm{I}_{q}^{n}(n)$$\Gamma \mathrm{I}_{q(n)}^{n}\supset[B\mathrm{I}^{n}q(n)(\vec{\eta})\mathrm{v}[\Delta \mathrm{I}_{q()}n$

$n$

is

Case 6: ( -right) Suppose$\wedge$$\mu_{k}$)from$[\Gammaarrow B\vee\Delta \mathrm{I}^{n}q(n)$$P$$\vee$($\neg([B\mathrm{I}_{q}n((n)\vec{\mu}))$A$\nu_{k}$).

$[\Gamma \mathrm{I}_{q(n)}^{n}\supset[B\mathrm{I}_{q(n}^{n})(\vec{\mu})[B\mathrm{I}_{q(n}^{n})(\vec{\nu})[\triangle \mathrm{I}_{q(n}^{n}\rangle$.

ends with$\frac{\Gammaarrow B,\triangle\Gammaarrow C,\Delta}{\Gammaarrow B\wedge C,\triangle}$

We separate this inference into two steps:$\frac{\Gammaarrow B,\triangle\Gammaarrow C,\Delta}{\frac{\Gamma,\Gammaarrow B\wedge C,\Delta,\Delta}{\Gammaarrow B\wedge C,\triangle}}$

.

.

8
and
By the induction hypothesis, there are polynomial-size $eF$-proofs of [ $\Gammaarrow B,$$eF$$\Gammaarrow
B\wedge
C,$$\Gammaarrow
C,$
The
.
in
easily[. From them, we can conclude[
rest is treated as in case 5.
$\Delta,$$\triangle,$$\Gamma,$$\Delta \mathrm{I}_{q}^{n}(n)$$\triangle \mathrm{I}_{q(n)}n$$\triangle \mathrm{I}_{q()}^{n}n$Case $7:$ ( -left) Similar to case 6.
$\vee$

Case $8:$ ($(\exists\leq)$-right)Case 8. : (sharply bounded) Suppose that$P$$\mathrm{a}$ends with.

$\frac{\Gammaarrow B(_{S}),\triangle}{S\leq|i|,\Gammaarrow(\exists x\leq|t|)B(X),\Delta}$.
By induction hypothesis, there is a polynomial-size proof ofbythe quantifier
definition. Let
isA.
and be bounding terms of
the free variables
variables occurrlng in $B(s)$ . Let$0\leq
m\leq
k$
$(n)$
,
there
.
For
each
does
not
of
exceedThen,.
thelengthDefine)are short $eF$ -proofs of$[\Gammaarrow B(s)\triangle \mathrm{I}_{q(n}^{n})$$\mathrm{V}_{m}^{q(n)-1}=0[\overline{m}\leq|t|$$|t|)B(x)\triangle \mathrm{I}_{q}^{n}(n.)$$B(\overline{m})\mathrm{J}_{q(n}n)$the.

$b\mathrm{d}\mathrm{e}\mathrm{n}\mathrm{o}\mathrm{t}\mathrm{e}arrow$$\ln t$$c\mathrm{b}arrow \mathrm{e}$$c\mathrm{i}arrow \mathrm{n}P$$\vec{u}$

$k$

$|t|$

$k=q_{|t|(}c^{arrow}/\vec{u}$$[s=\overline{m}\mathrm{J}_{q(n)}^{n}\supset([B(s)\mathrm{I}^{n}q(n)(b/mbarrowarrow)rightarrow[B(\overline{m})\mathrm{I}_{q(n}^{n}))$where$b_{m}arrow$are quantifier variables used in$[(\exists x\leq$,. Combining these, we get $eF$ -proofs of$B(\overline{m})$$[ \Gamma \mathrm{I}_{q(n)}^{n}\supset\bigwedge_{m=0}^{k}[\neg(\overline{m}\leq|t|)\vee B(\overline{m})\triangle \mathrm{I}q(n)n$.

for all $m\geq k$ . Hence, we have
There are simple $eF$-proofs offor $m\geq k$ . Now we are ready to conclude$(\neg(\overline{m}\leq|t|)\vee B(\overline{m})$$\neg(\overline{m}\leq|t|)$$\triangle)rightarrow\triangle$[ $s\leq|t|$ A$\Gamma \mathrm{I}_{q(n)}^{n}\supset q(n)-1\mathfrak{m}=0$[($\overline{m}\leq|t|$A$B(\overline{m})$)$\triangle \mathrm{I}_{q(n)}^{n}$.

Use contraction to get[ $s\leq|t|$ A

Case 8.

$\Gammaarrow(\exists x\leq|t|)B(x)\Delta \mathrm{I}_{q(n)}^{n}$(not sharply bounded) Suppose$\mathrm{b}$$P$.

ends with$\frac{\Gammaarrow B(_{S}),\triangle}{s\leq t,\Gammaarrow(\exists x\leq t)B(x),\triangle}$.

Let
By induction hypothesis, there is a polynomial-size $eF$ -proof of [. Then, the. Define
the free variables in and be bounding terms oflength of does not exceed in . Let be the quantifier variable used in the place of in$c\mathrm{b}arrow \mathrm{e}$$\Gammaarrow B(s)\triangle \mathrm{I}_{q(n)}^{n}\cdot$

$t$

$P$

$k$

$t$

$(\exists x\leq t)B(_{X})$$c\mathrm{i}arrow \mathrm{n}P$$\vec{u}$$k=q_{t(c^{arrow/\vec{u})}}(n)$

$b$

$x$

.
$\ldots,$$\mu_{0}$,$[b \mathrm{I}_{q(n)}^{n}--,\mu\frac{\perp,\ldots\perp}{q(n)-k},k-1,$

where 1 is an abbreviation for a false formula. Let
We form the desired $eF$ -proof as follows:

1. The definition ofextension.

$\mu_{i}rightarrow\phi_{i}^{s}$$\phi_{i}^{s}$be the formula giving thefor $0\leq..i\leq k-1$ and$\mu jrightarrow\perp$$i^{th}$-bit of .
$s$

for $k\leq j\leq q(n)-1$ by

9
2. Derive [ $s\leq t$ A

( $(s\leq t)$ A $B(s)$ )$\Gammaarrow$$\triangle \mathrm{I}_{q(n)}^{n}$

3. Derive [ $s\leq t$ A
( $(b\leq t)$ A $B(b)$ )according to the value of .
$\Gammaarrow$from$\triangle \mathrm{I}_{q(}^{n}n)$$[\Gammaarrow B(s)\triangle \mathrm{I}_{q(n)}^{n}\cdot$

by replacing some of$\phi_{i}^{s}$and$\perp$by$\mu_{i}$$i$Case 9: ($(\forall\leq)$-left) Similar to case 8.

Case 10: (-right)In case 10, is used as an eigenvariable in a bounded quantifier inference.
lemma 1 guarantees that is large enough to cover the range of the term .
$(\forall\leq)$$a^{k}$$(\forall x$$k$$\leq t)$. Note that$t$Case 10. : (Sharply bounded) Suppose$\mathrm{a}$$P$ends with the inference.

$\frac{a^{k}\leq|t|,\Gammaarrow B(a^{k}),\triangle}{\Gammaarrow(\forall X\leq|t|)B(X),\triangle}$. By the induction hypothesis, there is a polynomial-size $eF$-proof. From them easily obtained
For $m\leq q(n)-1$ , let
be the formula giving the -bit of the natural number . Use

where$k=q_{tm\mathrm{t}a^{k};P)}(n)$$[a^{k}\leq$$|t|\wedge\Gammaarrow B(a^{k})\vee\triangle \mathrm{I}_{q}^{n}(n)$$[\Gamma \mathrm{I}_{q(n)}^{n}\supset[a^{k}\leq|t|\supset B(a^{k})\mathrm{I}^{n}q(n)\vee[\triangle \mathrm{I}_{q(n)}^{n}\cdot$$i^{th}$$\phi_{i}^{\overline{m}}$extension rule to replace
Then, we obtain [A$v_{i}^{a^{k}}$$\overline{m}\leq|t|$by$\phi_{i}^{\overline{m}}$$m$

for every $0\leq i\leq k$ in [A
. Combining these, we get $eF$-proofs of$a^{k}\leq|t|$$\Gammaarrow B(a^{k})\triangle \mathrm{I}_{q(n)}^{n}$.

$\Gammaarrow B(\overline{m})\triangle \mathrm{I}_{q(n)}^{n}$.

$[ \Gamma \mathrm{J}_{q(n)}^{n}\supset\bigwedge_{0m=}^{q(n)-1}[\neg(\overline{m}\leq|t|)\vee B(\overline{m}))\vee\triangle \mathrm{J}q(n)n$Hence, we have$q(n)-1$$[ \Gamma \mathrm{I}_{q(n)}^{n}\supset\bigwedge_{m=0}[(\overline{m}\leq|t|arrow B(\overline{m}))\vee..\triangle \mathrm{I}_{q(n)}n$

Use the method in case 3 to contract multiple occurrences of$\mathrm{b}$(Nonsharply bounded) Suppose$P$and get.

$[\Gammaarrow(\forall x\leq|t|)B(X)\vee\triangle \mathrm{I}_{q(n)}n$Case 10.

$\triangle’ \mathrm{s}$.

ends with$\underline{a^{k}\leq t,\Gammaarrow B(a^{k}),\triangle}$$\Gammaarrow(\forall x\leq t)B(x),$,$\triangle$

where $k=q_{tm(a^{kp)}};(n)$ . By the induction hypothesis, there is a polynomial-size $eF$-proof of[A. From this easily obtained [. Sinceis free variable normal form, the eigenvariableappears only as indicated above. Infer$a^{k}\leq t$$P$$\Gammaarrow B(a^{k})\vee\triangle \mathrm{I}_{q}^{n}(n)$$\Gammaarrow\neg(a^{k}\leq t)\vee B(a^{k})\vee\triangle \mathrm{I}_{q}^{n}(n)$$a^{k}$$[\Gamma \mathrm{I}_{q(n)}^{n}\supset([\neg(a^{k}\leq t)\vee B(a^{k})\mathrm{I}q(n)\mathrm{v}n[\triangle \mathrm{I}_{q}^{n}(n))$

which is$[\Gammaarrow(\forall x\leq t)B(x)\triangle \mathrm{I}_{q()}^{n}n$

.

,

10
Case 11: ($(\exists\leq)$-left) Similar to case 10.

Case 12: (Cut) Suppose$P$

ends with.

$\frac{\Gammaarrow\triangle,BB,\Piarrow\Lambda}{\Gamma,\Piarrow\Lambda,\triangle}$

Note that $B$ must be . Without loss of generality, we can assume that $B=(\exists x\leq t)C(x)$ ,. Define. Let be the free variables in and be bounding terms ofis
where. Then, the length of does not exceed . By the induction hypothesis, there arein. Now suppose that [and [ $B$ A
polynomial-size proofs of [$B$
has quantifier variable
in [ A
has quantifier variable and [[, . Since
for the same bound variable . We can assume that [ $b\mathrm{I}_{q(n)}^{n}=-\perp,$$\Sigma_{1}^{b}$

$C$

$k$

$t$

$k=q_{t(c^{\sim}}/\vec{u})(n)$$b$$\Gammaarrow\triangle\vee B\mathrm{I}_{q(n)}n$$B\mathrm{J}_{q(}^{n}n)$$\Piarrow\Lambda \mathrm{I}_{q}^{n}(n)$$\Gammaarrow\triangle B\mathrm{I}_{q}^{n}(n)$$d$$c\mathrm{i}arrow \mathrm{n}P$$\vec{u}$$t$$carrow$$\Sigma_{0}^{b}$$\Piarrow\Lambda \mathrm{J}_{q(n)}^{n}$$B\mathrm{J}_{q(n)}^{n}$$x$$\ldots,$$\perp,$$\mu^{b}k-1’\ldots$$\mu_{0}^{b}$$q(n)-k$$d$

is introduced by extension as in case 11: there is an$(\exists\leq)$-left inference

$I$

in

$P$

such that$\frac{a\leq t,C(a),\mathrm{r}arrow\Delta}{(\exists x\leq t)c(_{X),\Delta}\Gammaarrow}I$

and that$a$is an eigenvariable of

$I$

and [

$v^{a}a0$ . Then, replace$v_{i}^{a}$by$a\mathrm{I}_{q(n}^{n})=\sim\perp,\ldots,1q(n)-k’ v_{k}-1’\ldots,$. Now we have the same translation of in its left and right occurrences, and we are ready.
to make a cut inference in $eF$ . We obtain a polynomial-size $eF$ -proof of [ A
Here, it is crucial that the cut-formula is .
$B$$\mu_{i}^{b}$$\Gamma$$\Piarrow\Lambda\Delta \mathrm{J}_{q(n)}^{n}$$\Sigma_{1}^{b}$Case 13: ($\Sigma_{1}^{b}$-PIND) Suppose$P$

ends with$\frac{B(\lfloor\frac{1}{2}b^{k}\rfloor),\Gammaarrow\Delta,B(b^{k})}{B(0),\Gammaarrow\triangle,B(t)}I$

where $k=q_{tm(b;P)}k$ . Let By lemma 1, the length of does not exceed . Suppose that
) Use extension rule to-bit of . (For $i\geq k$ , set$(i<k)$ is a formula giving thebyfor $0\leq j\leq k$ . Then, we obtainreplace$k$$t$$i^{th}$$v_{i}^{b^{k}}$$\phi_{i}^{t}$$\phi_{i}^{t}rightarrow\perp.$$t$$\phi_{i-\mathrm{j}}^{t}$[$B( \lfloor\frac{t}{2^{j+1}}\rfloor)$A$\Gammaarrow\Delta\vee B(\mathrm{L}^{\frac{t}{2^{j}}}\rfloor)\mathrm{I}_{q(n\rangle}^{n}$.

Combiming these together by cut inferences, and using the technique in case 12, we obtain[ $B(0)$ A$\Gammaarrow\Delta,$ $B(t)\mathrm{I}_{q}^{n}(n)$.

$\square$We can shrink the size of the end-sequent of $eF$ proofs by deleting the contents of unnecessary higher bits.
Lemma 4 Let$A$

be a bounded formula in$S_{2}^{1}$For every $m\geq q_{A}(n)$ , there is a simple proof of$[A\mathrm{I}_{q(n)}^{n}\supset[A\mathrm{I}_{m}^{n}$.

. Let be a
andis a bounded formula inCorollary 1 Suppose thatand $m$ be the number of lines in .
free-cut free, free variable normal form proof of$eF$
are bounded by $c\cdot m\cdot q(n)\cdot pb(n)$proofsthe-proofs of [Then, there are). The size of$A(a^{n})\sim$$S_{2}^{1}$$S_{2}^{1}$$A\mathrm{I}_{q}^{n_{A}}\langle n$for some constant .
$c$$A(\vec{a})$$S_{2}^{1}\vdash A(a^{n})arrow$

$P$

$P$

11

4Translation of other bounded arithmetic to propositional calculi
We can extend our technique to translate bounded proofs of other bounded arithmetic topolynomial size propositional proofs.
In the translation given in the previous section, the crutial reason why we needed $eF$ but
proofs was that we cannot literally translate non-sharply bounded
not Frege to translate
to polynomial-size propositional formulas. Unlike sharply bounded quantifiers
formulas inwhich are ready to be translated into polynomial-size conjunctions or disjunctions of proposi,tional formulas,non-sharply bounded quantifiers require a superpolynomial function,, we have to pick an into be expressed as conjunctions and disjunctions. To avoid
stance satisfying $s\leq t$ A $A(s)$ to express $(\exists x\leq t)A(x)$ , that requires us to introduce the use
proofs are translatable to polynomial-size Fregeof extension. That means every bounded
proofs. (By choozing appropriate language, it is translatable to polynomial-size bounded depth
Frege proofs.)
proofs are translatable to $eF$ proofs of size
It is also quite clear that every boundedis that-IND is decomposed to $n^{O(n)}\log$ -many. The reason why it reqires
but not polynomially-many cuts.
The same technique also can be used to extend the result in [15].
$S_{2}^{1}$$S_{2}^{1}$$n^{o()}\log n$$n^{O(n)}\mathrm{l}\mathrm{o}\mathrm{g}$$s$$S_{2}^{0}$$T_{2}^{1}$$n^{o()}\log n$$n^{O(n)}\mathrm{l}\mathrm{o}\mathrm{g}$Corollary 2 Let $i\geq 1$ and$A(a)arrow$$\Sigma_{1}^{b}$

be a bounded formula. Assume that$T_{2}^{i}\vdash A(\vec{a})$.

Then, there is a polynomial function such that if every parameter variables ofhas polynomial-size -proofs.
andlength$p$$\leq n_{f}$$||A||_{n}^{p}(n)$Corollary 3 Let $i\geq 1$ andhas the$A$

has the$G_{i}$$A(\vec{a})$be a bounded formula. Assume that
$S_{2}^{i}\vdash A(\vec{a})$.

Then, there is a polynomial function such that if every parameter variables of, and
has polynomial-size -proofs.
length$p$$\leq n$$A$$||A||_{n}^{p}(n)$$G_{i}^{*}$

References[1] M. Ajtai, “ -formulae on finite structures”, Annals of Pure and Applied Logic, Vol.24(1983) 1-48.
$\Sigma_{1}^{1}$[2] M. Ajtai, “The complexity of the pigeonhole principle”, 29th Annual Symposium on theFoundations of Computer Science (1988) 346-55.

[3] N. H. Arai, “Translation ofmitted.

$S_{2}^{1}$

proofs into polynomial-size extended Frege proofs”, sub-[4] T. Arai, “Frege system, ALOGTIME and bounded arithmetic”, manuscript (1991).
[5] S. R. Buss, Bounded Arithmetic, Bibliopolis, Napoli, 1986.
[6] S. R. Buss et al., Weak Formal Systems and Connections to Computational Complexity,

Student-written lecture notes for topics course at U.C.Berkley, January-May, 1988.

12[7] S. R. Buss, “Relating the bounded arithmetic and polynomial time hierarchies, Annals ofPure and Applied Logic, Vol.75 (1995) 67-77.
[8] P. Clote, “On polynomial size Frege proofs of certain combinatorial principles”, in Arithmetic, Proof Theory, and Computational Complexity, Clarendon Press, Oxford (1993)

162-84.

[9] S. A. Cook, “Feasibly constructive proofs and the propositional calculus”, Proc. 7th
A.C.M. Symposium on the Theory of Computation (1975) 83-97.
[10] S. A. Cook, “Relating the provable collaspe of P to $NC^{1}$ and the power of logical theories”,
preprint (1996).
[11] S. A. Cook and R. Reckhow, “On the lengths of proofs in the propositional calculus”,
Proc. 6th ACM Symposium on Theory of Computing (1974) 135-148.

[12] S. A. Cook and R. A. Reckhow, “The relative efficiency of propositional proof systems”,
J. Symbolic Logic, Vol.44 (1979) 36-50.

Computational Limitaions for Small-Depth Circuits, The MIT Press, Cambridge, London, 1986.

[13] J. T.

$\mathrm{H}^{\mathrm{O}}\mathrm{a}\mathrm{S}\mathrm{t}\mathrm{a}\mathrm{d}$[14] M. Kikuchi, “On Buss and Tur\’an’s extensions of Haken’s results”, preprint.
[15] J. Kraj\’i\v{c}ek and P. Pudl\’ak, “Quantified propositional calculus and fragments of boundedarithmetic”, Zeitschrift f. Mathematikal Logik u. Grundlagen d. Mathematik, Vol.36 (1990)

29-46.

[16] J. Kraj\’i\v{c}ek, Bounded Arithmetic, Propositional Logic, and Complexity Theory, Cambridge
University Press, Cambridge, 1995.
[17] J. Kraj\’i\v{c}ek, P. Pudl\’ak and G. Takeuti, “Bounded arithmetic and the polynomial hierarchy”, Annals of Pure and Applied Logic, Vol.52 (1991) 143-153.
[18] J. Paris and A. Wilkie, “Counting problems in bounded arithmetic”, in: Methods inMathematical Logic, Lecture Notes in Mathematics Vol.1130 (Springer, Berlin, 1985) 317-

340.
[19] J. B. Paris, A. J. Wilkie and A. R. Woods, “Provability of the pigeonhole principle and theexistence of infinitely many primes”, Journal of Symbolic Logic, Vol.53 (1988) 1235-44.
$_{\backslash -\backslash },.\cdot$[20] L. J. Stockmeyer, “The polynomial-time hierarchy”, Theoretical Computer Science, Vo1.3(1976) 1-22.
[21] A. Woods, “Some problems in logic and number theory and their connections”, Ph.D.
Thesis, Manchester University (1981).

[22] A. Yao, “Separating the polynomial-time hierarchy by oracles”, Proc. 26th Annual IEEE
Symposium on Foundation of Computer Science (1985) 1-10.