BRICS RS-94-36 A. A. Razborov: On provably disjoint NP-pairs

BRICS

Basic Research in Computer Science

On provably disjoint NP-pairs

Alexander A. Razborov

BRICS Report Series RS-94-36 ISSN 0909-0878 November 1994 Copyright \begin{matrix}c \\ ◯ \end{matrix} 1994, BRICS, Department of Computer Science

University of Aarhus. All rights reserved.

Reproduction of all or part of this work is permitted for educational or research use on condition that this copyright notice is included in any copy.

See back inner page for a list of recent publications in the BRICS Report Series. Copies may be obtained by contacting:

BRICS Department of Computer Science University of Aarhus Ny Munkegade, building 540 DK - 8000 Aarhus C Denmark

Telephone: +45 8942 3360
Telefax: +45 8942 3255
Internet: BRICS@daimi.aau.dk

On provably disjoint NP-pairs

Alexander A. Razborov^{∗} Steklov Mathematical Institute Vavilova 42, 117966, GSP–1, Moscow, RUSSIA

November 11, 1994

Abstract

In this paper we study the pairs (U, V) of disjoint NP-sets representable in a theory T of Bounded Arithmetic in the sense that T proves U ∩ V = ∅. For a large variety of theories T we exhibit a natural disjoint NP-pair which is complete for the class of disjoint NP-pairs representable in T. This allows us to clarify the approach to showing independence of central open questions in Boolean complexity from theories of Bounded Arithmetic initiated in [11]. Namely, in order to prove the independence result from a theory T, it is sufficient to separate the corresponding complete NP-pair by a (quasi)poly-time computable set. We remark that such a separation is obvious for the theory S(S_{2}) + SΣ_{2}^{b} − P IND considered in [11], and this gives an alternative proof of the main result from that paper.

1. Introduction

In this paper we study the class of pairs (U, V), where U and V are disjoint NP-sets. There are at least two good reasons to be interested in this issue.

Firstly, the question of existence of such a pair not separable by a set in P is closely connected to the existence of public-key cryptosystems [5].

∗Part of this work was done while the author was visiting BRICS, Basic Research in Computer Science, Centre of the Danish National Research Foundation. Supported by the grant # 93-011-16015 of the Russian Foundation for Fundamental Research, and by an AMS-FSU grant.

The second motivation comes from the attempts to understand on the formal level the machinery existing in non-uniform Boolean complexity for proving lower bounds [10, 12, 11]. Of the main importance for this approach is the following observation.

Let U consist of truth-tables of all “simple” Boolean functions, and let

V ⇀ ↽ {f ⊕ s | f ∈ U } ,

where s is a supposedly complex function in the same number of variables as f. Then proving that s is indeed complex is equivalent to showing that U ∩ V = ∅.

Based upon the notion of a natural proof [12], it was implicitly shown in [11] that if sufficiently strong pseudo-random generators exist then these U and V can not be separated by a quasipolynomial time computable set. It was (also implicitly) shown there that if some particular system S(S_{2}) + SΣ_{2}^{b} − P IND of Bounded Arithmetic can prove that U ∩ V = ∅ for some NP-pair (U, V) then this pair can not be separated by a quasipolynomial time computable set. Putting things together, we obtain the independence result modulo the hardness assumption.

The question if there exist disjoint NP-pairs which can not be separated by a set in P is open. Moreover, it was shown in [6] that there exists an oracle relative to which P ≠ NP, and still such pairs do not exist. Thus, the assumption of the existence of P-inseparable disjoint NP-pairs seems to be stronger than merely P ≠ NP. It should be noted, however, that this assumption is implied by both P ≠ UP (see e.g. [13, Theorem 9]) and, for obvious reasons, by P ≠ NP ∩ co − NP.

It is known [5, Theorem 6] that every disjoint NP-pair is many-one reducible to another disjoint NP-pair in which both components are NP-complete. However, it is open whether there exists an NP-pair which is complete in the class of all disjoint NP-pairs under a natural reduction. The reason lies in the highly non-constructive nature of the condition U ∩ V = ∅: e.g. we apparently can not enumerate pairs of nondeterministic poly-time machines producing all disjoint NP-pairs.

In this paper we try to build the hierarchy of disjoint NP-pairs based upon the strength of logical tools needed for proving the fact U ∩V = ∅. Namely, for a variety of systems T of Bounded Arithmetic, we consider the class of NP-pairs for which this fact is provable in T. We exhibit a natural NP-pair which is complete in this class under the many-one reduction. Roughly speaking, the first component in this pair consists of all satisfiable CNF, and the second component consists of those unsatisfiable CNF which allow a short refutation in the propositional proof system associated with T. This reduces the approach suggested in [11] to the very concrete algorithmic question: for which theories T the associated complete NP-pair can be separated by a quasipolynomial time computable set? Whenever such a separation exists, we have the independence of NP ⊈ P/poly from the theory T modulo the hardness assumption. For the theory S(S_{2}) + SΣ_{2}^{b} − P IND the separating set is fairly obvious, and this gives us an alternative, and, perhaps, more natural (not to be confused with the concept from [12]!) proof of the main result from [11].

The paper is organized as follows. In Section 2 we recall necessary facts from Bounded Arithmetic and propositional calculus. In Section 3 we formulate the main concept of an NP-pair representable in a theory T and formulate our main result. In Section 4 we demonstrate one nice feature of the split versions introduced in [11]: we show that they allow some sort of elimination of sharply bounded quantifiers. The next section 5 contains the proof of our main theorem. In Section 6 we show how to reduce the approach to proving independence results in Bounded Arithmetic to purely complexity questions. The paper is concluded by a brief discussion of their status in Section 7.

2. Background from Logic

2.1. Systems of Bounded Arithmetic

We assume the familiarity with [1], and use the now-standard notation for denoting various hierarchies and fragments of Bounded Arithmetic from that book. L_{1} is the first order language which consists of the constant 0, function symbols S, +, ·, ⌊\frac{1}{2}x⌋, |x|, and of the predicate symbol ≤. L_{2} is obtained from L_{1} by augmenting it with the smash symbol # which has the intended meaning x#y = 2^{|x|·|y|}. L_{k}(α, β) (k = 1, 2) is the first-order language obtained from L_{k} by appending to the latter two new unary predicate symbols α(a), β(a), and L_{k} is the second-order language based on L_{k}. To simplify the notation, we will sometimes be using several predicate symbols (second-order variables in the case of L_{k}) like α_{1}, α_{2}, … or β_{1}, β_{2}, …: they can always be combined into a single α or β using an easy encoding.

The theories we are interested in will be either in the language L_{k}(α, β) or in L_{k} (k = 1, 2). All they contain the set BASIC_{k} of simple open axioms describing basic properties of symbols from L_{k}. On the top of it, second-order theories also always include the comprehension axiom scheme Σ_{0}^{1,b} − CA. The difference between theories is specified by the amount of induction allowed.

Behind the standard hierarchy Σ_{i}^{b}, Π_{i}^{b} of bounded formulae we also need its split version SΣ_{i}^{b}, SΠ_{i}^{b} in the language L_{2}(α, β) [11]. SΣ_{0}^{b} = SΠ_{0}^{b} is the set of all bounded formulae which contain either only occurrences of α or only occurrences of β. The inductive definition of SΣ_{i+1}^{b}, SΠ_{i+1}^{b} is the same as for Σ_{i+1}^{b}, Π_{i+1}^{b}.

The hierarchy E_{i}, U_{i} (see e.g. [17]) was defined as the ordinary hierarchy of bounded formulae in the language of Peano Arithmetic (where we do not have the notion of a sharply bounded quantifier at all). A bounded formula is D_{i} in a theory T if it is provably equivalent to an E_{i}- and U_{i}-formula in T. We extend this hierarchy to the language L_{1}(α, β) simply by counting sharply bounded quantifiers exactly as ordinary quantifiers. The split versions SE_{i}, SU_{i}, SD_{i} of this hierarchy in the language L_{1}(α, β) are defined analogously to SΣ_{i}^{b}, SΠ_{i}^{b}.

The following table summarizes the definitions of the theories of Bounded Arithmetic considered in this paper^{1}:

Theory Underlying language Induction scheme
S_{2}^{i}(α, β)  L_{2}(α, β)  Σ_{i}^{b}(α, β) − P IND
SS_{2}^{i}  L_{2}(α, β)  SΣ_{i}^{b} − P IND
IE_{i}(α, β)  L_{1}(α, β)  E_{i}(α, β) − IND
SIE_{i}  L_{1}(α, β)  SE_{i} − IND
T_{2}^{i}(α, β)  L_{2}(α, β)  Σ_{i}^{b}(α, β) − IND
ST_{2}^{i}  L_{2}(α, β)  SΣ_{i}^{b} − IND
IΔ_{0}(α, β)  L_{1}(α, β)  Δ_{0}(α, β) − IND
S_{2}(α, β)  L_{2}(α, β)  Σ^{b}(α, β) − P IND
U_{1}^{1}  L_{1}  Σ_{1}^{1,b} − P IND
U_{2}^{1}  L_{2}  Σ_{1}^{1,b} − P IND
V_{1}^{1}  L_{1}  Σ_{1}^{1,b} − IND
V_{2}^{1}  L_{2}  Σ_{1}^{1,b} − IND

Table 1: Summary of fragments of Bounded Arithmetic

We will need the following easy generalization of [2, Theorem 5] to our setting (see [11]):

Proposition 2.1. For i ≥ 1, SS_{2}^{i+1} is ∀SΣ_{i+1}^{b}-conservative over ST_{2}^{i}.

1we have introduced the natural notation SS_{2}^{i}, ST_{2}^{i} for the theories S(S_{2}) + SΣ_{i}^{b} − P IND, S(S_{2}) + SΣ_{i}^{b} − IND from [11] and SIE_{i} for the split versions of the theories IE_{i}(α, β). Also, Σ^{b} ⇀ ↽ ⋃_{i≥0} Σ_{i}^{b}.

2.2. Propositional proof systems

In this paper we will be exclusively working with sequential (= natural deduction) proof systems. The cut rule will be always present.

Different proof systems are usually specified by the syntactic requirements placed on the sequents allowed in the proof:

• For a fixed constant w > 0, we denote by R_{w} the system of bounded resolutions. All sequents in the proof must have the form ℓ_{1}, …, ℓ_{p} ⟶ ℓ_{p+1}, …, ℓ_{q}, where ℓ_{i}s are literals (that is, either propositional variables or their negations) and, moreover, q ≤ w. Applying cosmetic (¬:right) rule, we can always move all literals to the succedent, after which the cut rule turns into the familiar resolution rule.

• R, resolutions is the same system as R_{w}, only without any restrictions on the length of the sequents.

• F_{d} is the depth-d Frege system: all formulae appearing in the proof must either have the form

⋁_{i_{1}=1}^{r_{1}} ⋀_{i_{2}=1}^{r_{2}(i_{1})} … ⋁ ⋀_{i_{d}=1}^{r_{d}(i_{1},...,i_{d−1})} ℓ_{i_{1}...i_{d}}  (1)

(Σ_{d}-formulae) or

⋀_{i_{1}=1}^{r_{1}} ⋁_{i_{2}=1}^{r_{2}(i_{1})} … ⋁ ⋀_{i_{d}=1}^{r_{d}(i_{1},...,i_{d−1})} ℓ_{i_{1}...i_{d}}  (2)

(Π_{d}-formulae), where ℓ_{i_{1}...i_{d}} are literals. The inference rules are modified for unbounded fan-in, e.g. (∧:right) looks like

\frac{Γ ⟶ A_{i}, Δ (i ∈ I)}{Γ ⟶ ⋀_{i∈I} A_{i}, Δ}.

Note that F_{0} = R.

• F is the ordinary Frege system. At this point it is no longer important that we work in the sequential calculus, but we prefer to stick to this for the sake of uniformity.

• EF is the extended Frege proof system [18, 4]. It additionally allows us to use extension axioms of the form p ≡ A, where p is a new propositional variable (called extension atom) which did not appear earlier in the proof.

For an unsatisfiable CNF ϕ = ⋀_{i∈I} ⋁_{j∈J_{i}} ℓ_{ij} and a proof system P we denote by s_{P} (ϕ) the minimal possible number of logical symbols in a P -derivation of the empty sequent from the sequents ⟶ {ℓ_{ij} | j ∈ J_{i} } (i ∈ I).

2.3. Correspondence between theories of Bounded Arithmetic and propositional proof systems

For many theories of Bounded Arithmetic T there exists a propositional proof system P_{T} closely associated with T in the following sense:

a) T proves the soundness of P_{T},

b) every proof in T of a formula A with appropriately low logical complexity can be efficiently transformed into a short P_{T} -proof of the propositional variant of A.

In this section we recall those details of this correspondence which will be important in the sequel.

Let T r(a, α, β) be the predicate asserting that the truth assignment α makes the Boolean formula encoded by the string β(0) … β(a − 1) true (truth definition).

Proposition 2.2 ([7]). T r(a, α, β) has a Δ_{1}^{1,b}-definition in U_{1}^{1} about which U_{1}^{1} proves the usual Tarski’s conditions.

Let T r_{d}(a, α, β) be the variant of T r(a, α, β) in which β(0) … β(a−1) encodes a Boolean formula from Σ_{d} ∪ Π_{d}. The following is straightforward:

Lemma 2.3. For any fixed d ≥ 0, T r_{d}(a, α, β) has a SD_{d+1}-definition in SIE_{0} about which SIE_{0} proves the usual Tarski’s conditions.

Note for the record that this truth definition can also be assumed to satisfy the natural property

SIE_{0} ⊢ ∀x < a(α_{1}(x) ≡ β_{1}(x)) ⊃ (T r_{d}(a, α, α_{1}) ≡ T r_{d}(a, α, β_{1})).  (3)

Let the Σ_{0}^{1,b}-formula Ref_{P} (a_{0}, a_{1}, β_{0}, β_{1}) assert that the string β_{0}(0) … β_{0}(a_{0} − 1) encodes an inference of length ≤ a_{0} in the propositional proof system P of the empty sequent from the clauses of the CNF encoded by β_{1}(0) … β_{1}(a_{1}−1). The following two propositions are slight modifications of [7, Theorem 2.4] and [7, Theorem 2.5] respectively (the latter also follows from earlier results of Cook [3] via the correspondence between P V and S_{2}^{1} [1, Chapter 6] and RSUV -isomorphism [14, 15, 9]):

Proposition 2.4. U_{1}^{1} ⊢ Ref_{F} (a_{0}, a_{1}, β_{0}, β_{1}) ⊃ ¬T r_{2}(a_{1}, α, β_{1}).

Proposition 2.5. V_{1}^{1} ⊢ Ref_{EF} (a_{0}, a_{1}, β_{0}, β_{1}) ⊃ ¬T r_{2}(a_{1}, α, β_{1}).

Paris and Wilkie [8] showed that IΔ_{0}(α, β) ⊢ Ref_{F_{d}}(a_{0}, a_{1}, β_{0}, β_{1}) ⊃ ¬T r_{2}(a_{1}, α, β_{1}) for any fixed d ≥ 0. We will need the following refinement of their result:

Lemma 2.6. For any fixed d ≥ 0, SIE_{d+2}(α, β) ⊢ Ref_{F_{d}}(a_{0}, a_{1}, β_{0}, β_{1}) ⊃ ¬T r_{2}(a_{1}, α, β_{1}).

Proof. Assuming T r_{2}(a_{1}, α, β_{1}), we prove by induction on c that in ANY one of the first c sequents of the inference encoded by β_{0} there EXISTS either a formula ϕ in the antecedent such that ¬T r_{d}(a_{1}, α, ϕ) or a formula ϕ in the succedent such that T r_{d}(a_{1}, α, ϕ). By Lemma 2.3, the formula expressing this fact is in SU_{d+2}, and SU_{d+2}−IND is available in SIE_{d+2}.

Let us now fix propositional variables p_{1}, p_{2}, …, p_{n}, …, q_{1}, q_{2}, …

Definition 2.7 (see e.g. [7]). For every A(a⃗, α, β) ∈ Σ_{0}^{1,b}, where all free variables are displayed, and a tuple of integers n⃗ we define the propositional formula ⟨A(a⃗)⟩n⃗ by induction on the complexity of A:

a) if A does not contain occurrences of α and β, and A(n⃗) is true [false] on integers then ⟨A(a⃗)⟩n⃗ ⇀ ↽ 1 [0, respectively];

b) if A(a⃗) = α(t(a⃗)) [β(t(a⃗))] then ⟨A(a⃗)⟩n⃗ ⇀ ↽ p_{t(n⃗)} [q_{t(n⃗)}, respectively];

c) ⟨¬A(a⃗)⟩n⃗ ⇀ ↽ ¬⟨A(a⃗)⟩n⃗;

d) ⟨A(a⃗) ∗ B(a⃗)⟩n⃗ ⇀ ↽ ⟨A(a⃗)⟩n⃗ ∗ ⟨B(a⃗)⟩n⃗ for ∗ ∈ {∧, ∨, ⊃};

e) ⟨(∃x ≤ t(a⃗))A(a⃗, x)⟩n⃗ ⇀ ↽ ⋁_{m≤t(n⃗)}⟨A(a⃗, b)⟩_{n⃗,m};

f) ⟨(∀x ≤ t(a⃗))A(a⃗, x)⟩n⃗ ⇀ ↽ ⋀_{m≤t(n⃗)}⟨A(a⃗, b)⟩_{n⃗,m}.

The following two propositions slightly modify and strengthen [7, Theorems 3.2,3.1] (the latter also follows from [3]):

Proposition 2.8. Let U_{2}^{1} ⊢ A(a⃗, α, β), where A(a⃗, α, β) is a Σ_{0}^{1,b}-formula with all free variables displayed. Then there exists a quasipolynomial time^{2} algorithm which for any tuple of integers n⃗ given in the unary form 1n⃗ produces an F -proof of the propositional formula ⟨A(a⃗)⟩n⃗.

2that is with running time 2^{(log n)^{O(1)}}. The corresponding class of functions/predicates computable in quasipolynomial time will be denoted by QP.

Proposition 2.9. Let V_{1}^{1} ⊢ A(a⃗, α, β), where A(a⃗, α, β) is in Σ_{0}^{1,b}. Then there exists a polynomial time algorithm which for any 1n⃗ produces an EF -proof of ⟨A(a⃗)⟩n⃗.

The same remains true after replacing “V_{1}^{1}” by “V_{2}^{1}”, and “polynomial time” by “quasipolynomial time”.

A similar result about the provability in IΔ_{0}(α, β) was established in [8]. It, however, requires more serious adjustment to our purposes, so we defer this until Section 5.

3. Representations of disjoint NP-pairs in systems of Bounded Arithmetic

Definition 3.1. Let U and V be two disjoint sets in NP, and T be either a first-order theory in the language L_{k}(α, β) or a second-order theory in the language L_{k} (k = 1, 2). The pair (U, V) is representable in T if there exist Σ_{0}^{1,b}-formulae A(a, α), B(a, β), C(a, b, α), D(a, b, β) with all free variables displayed such that:

a) for every w = (w_{0}, w_{1}, …, w_{N−1}) ∈ {0, 1}^{N}, if w ∈ U then

N ⊧ ∃α (A(N, α) ∧ ∀i < N(C(N, i, α) ≡ w_{i} = 1)) ,

and if w ∈ V then

N ⊧ ∃β (B(N, β) ∧ ∀i < N(D(N, i, β) ≡ w_{i} = 1)) ;

b)

T ⊢ (A(a, α) ∧ B(a, β)) ⊃ ∃x < a(C(a, x, α) ≢ D(a, x, β)).

Informally, condition a) says that A and B specify some Ũ ⊇ U and Ṽ ⊇ V as projections of P-sets if k = 1 and QP-sets if k = 2. b) means that Ũ ∩ Ṽ = ∅ is provable in T.

We exploit the ordinary notion of ≤_{m}^{p}-reducibility in the context of promise problems. Namely, (U, V) ≤_{m}^{p} (U′, V′) means that there is a polynomially time computable function f : {0, 1}^{∗} ⟶ {0, 1}^{∗} such that f(U) ⊆ U′ and f(V) ⊆ V′. The variant ≤_{m}^{qp} of this reducibility is defined in the same way with the difference that we only require f to be in QP.

Theorem 3.2. a) Let T be one of the theories

SS_{2}^{i}, IE_{i}, ST_{2}^{i} (i ≥ 1), IΔ_{0}(α, β), S_{2}(α, β), U_{1}^{1}, U_{2}^{1}, V_{1}^{1}, V_{2}^{1}.

Then the class of NP-pairs representable in T is closed under ≤_{m}^{p}-reducibility.

b) If, moreover, T ∈ {SS_{2}^{i}, ST_{2}^{i}, S_{2}(α, β), U_{2}^{1}, V_{2}^{1}} then this class is closed under ≤_{m}^{qp}- reducibility.

Proof. a). Assume that (U, V) is representable in T via bounded formulae A(a, α), B(a, β), C(a, b, α), D(a, b, β), and let (U′, V′) ≤_{m}^{p} (U, V) via a polynomial time computable function f. Then for a suitable polynomial p(a) we have Σ_{0}^{1,b}-formulae P rot(a, γ_{0}, γ_{1}), Output(a, b, γ_{0}, γ_{1}) and Δ_{0}-definable in IΔ_{0}(γ_{0}, γ_{1}) function symbol Length(a, γ_{0}, γ_{1}) expressing the following:

• P rot(a, γ_{0}, γ_{1}) – “γ_{1}(0) … γ_{1}(p(a) − 1) is (the encoding of) the protocol of the polytime computation of f on the input string γ_{0}(0) … γ_{0}(a − 1)”;

• Length(a, γ_{0}, γ_{1}) is the length of the output of γ_{1} if P rot(a, γ_{0}, γ_{1}) and 0 otherwise;

• Output(a, b, γ_{0}, γ_{1}) – “P rot(a, γ_{0}, γ_{1}), b < Length(a, γ_{0}, γ_{1}) and the bth bit of γ_{1}’s output is equal to 1”.

We now set:

A′(a, α_{0}, α_{1}, α_{2}) ⇀ ↽ P rot(a, α_{0}, α_{1}) ∧ A(Length(a, α_{0}, α_{1}), α_{2})
∧ ∀x < Length(a, α_{0}, α_{1})(C(a, x, α_{2}) ≡ Output(a, x, α_{0}, α_{1}))
B′(a, β_{0}, β_{1}, β_{2}) ⇀ ↽ P rot(a, β_{0}, β_{1}) ∧ B(Length(a, β_{0}, β_{1}), β_{2})
∧ ∀x < Length(a, β_{0}, β_{1})(D(a, x, β_{2}) ≡ Output(a, x, β_{0}, β_{1}))
C′(a, b, α_{0}, α_{1}, α_{2}) ⇀ ↽ α_{0}(b)
D′(a, b, β_{0}, β_{1}, β_{2}) ⇀ ↽ β_{0}(b).

We claim that A′, B′, C′, D′ provide a representation of (U′, V′) in the theory T. Condition a) from Definition 3.1 is straightforward. In order to see b), suppose, arguing informally in T, that ∀x < a(α_{0}(x) ≡ β_{0}(x)),

A′(a, α_{0}, α_{1}, α_{2}) and B′(a, β_{0}, β_{1}, β_{2}). Applying SU_{1} − IND on c ≤ p(a) (which is available in T) to the formula ∀x < c(α_{1}(x) ≡ β_{1}(x)), we find ∀x < p(a)(α_{1}(x) ≡ β_{1}(x)). Thus,

T  P_{T} reducibility
SIE_{i} (i ≥ 2) F_{i−2} ≤_{m}^{p}
ST_{2}^{i}, SS_{2}^{i+1} (i ≥ 2) F_{i−2}  ≤_{m}^{qp}
U_{2}^{1}  F  ≤_{m}^{qp}
V_{1}^{1}  EF  ≤_{m}^{p}
V_{2}^{1}  EF  ≤_{m}^{qp}

Table 2: (SAT^{∗}, REF (P_{T})) is complete in the class corresponding to T

Length(a, α_{0}, α_{1}) = Length(a, β_{0}, β_{1}) and ∀x < Length(a, α_{0}, α_{1})(Output(a, x, α_{0}, α_{1}) ≡ Output(a, x, β_{0}, β_{1})). From the definition of A′, B′ we conclude

∀x < Length(a, α_{0}, α_{1})(C(a, x, α_{2}) ≡ Output(a, x, β_{2})),

and this contradicts condition b) for the original pair (U, V) (after substituting a := Length(a, α_{0}, α_{1}), α := α_{2}, β := β_{2}).

Part b) is proved in exactly the same way.

Let now SAT^{∗} ⇀ ↽ {⟨ϕ, 1^{t}⟩ | ϕ is a satisfiable CNF}. For a propositional proof system P, let REF (P) ⇀ ↽ {⟨ϕ, 1^{t}⟩ | ϕ is an unsatisfiable CNF and s_{P} (ϕ) ≤ t}. Obviously, SAT^{∗}, REF (P) ∈ NP and SAT^{∗} ∩ REF (P) = ∅. The following theorem is the main result of this paper.

Theorem 3.3. Let T be one of the theories in the left column of Table 2, and P_{T} be the corresponding proof system in the middle column. Then (SAT^{∗}, REF (P_{T})) is complete in the class of disjoint NP-pairs representable in T with respect to the reducibility given in the right column.

The proof of this theorem will be given in two subsequent sections.

We conclude this section with the following corollary asserting a certain symmetry of pairs (SAT^{∗}, REF (P)):

Corollary 3.4. (REF (F_{d}), SAT^{∗}) ≤_{m}^{p} (SAT^{∗}, REF (F_{d})) (d ≥ 0), (REF (F), SAT^{∗}) ≤_{m}^{qp} (SAT^{∗}, REF (F)), and (REF (EF), SAT^{∗}) ≤_{m}^{p} (SAT^{∗}, REF (EF)).

Proof. Immediately follows from Theorem 3.3 since the notion of a pair representable in a theory T is symmetric with respect to the two components U, V.

4. Elimination of sharply bounded quantifiers in split versions

Let us consider the analogue E_{i}^{#}, U_{i}^{#} of the hierarchy E_{i}, U_{i} in the language L_{2}, and its split versions SE_{i}^{#}, SU_{i}^{#} in the language L_{2}(α, β). Thus, SE_{i}^{#}, SU_{i}^{#} differ from SE_{i}, SU_{i} only in the underlying language, whereas the syntactic inductive definitions for both hierarchies are the same. The theories IE_{i}^{#}, SIE_{i}^{#} have the obvious meaning. In this section we prove the following:

Theorem 4.1. SIE_{i}^{#} = ST_{2}^{i} for all i ≥ 0.

Proof. Since SE_{i}^{#} ⊆ SΣ_{i}^{b}, it suffices to show that SIE_{i}^{#} ⊢ SΣ_{i}^{b} − IND. This will be immediately implied by the following

Claim 4.2. Let 0 ≤ j ≤ i. Then every SΣ_{j}^{b}-formula is equivalent in SIE_{i}^{#} to a SE_{j}^{#}- formula.

Proof of Claim 4.2. W.l.o.g. we may assume that A ∈ SΣ_{j}^{b} contains only connectives {¬, ∧, ∨} and, moreover, that negations appear on atomic subformulae only. Now we apply induction on ⟨j, |A|⟩.

Base j = 0 is obvious since SΣ_{0}^{b} = SE_{0}^{#}.

Inductive step. Let j > 0 and A ∈ SΣ_{j}^{b}. If A ∈ SΠ_{j−1}^{b}, we convert (¬A) into the equivalent form Ā ∈ SΣ_{j−1}^{b} obeying the above restrictions, and apply to Ā the inductive assumption with j := j − 1. If A = B ∗ C or A = (∃x ≤ t)B(x), the inductive step is obvious (SE_{j}^{#} is closed under these operations).

The only nontrivial case is A = (∀x ≤ |t|)B(x). By the inductive assumption, B(a) is equivalent in SIE_{i}^{#} to a SE_{j}^{#}-formula, and we can further assume that this formula is in the prenex normal form. That is to say,

SIE_{i}^{#} ⊢ A ≡ ∀x ≤ |t|∃y_{1} ≤ s_{1} … ∃y_{ℓ} ≤ s_{ℓ}∀z^{(2)} ≤ r^{(2)} … Qz^{(j)} ≤ r^{(j)}C(x, y⃗, z^{(2)}, …, z^{(j)}),

where C is a Boolean combination of SE_{0}^{#}-formulae. The crucial point is that since SIE_{i}^{#} contains S_{2}^{1}, it can also define all Σ_{1}^{b}-definable in S_{2}^{1} function symbols. Moreover, usage of this symbols does not increase the logical complexity of formulae in terms of the hierarchy SE_{i}^{#} (remember that SE_{0}^{#} consists of all bounded formula either not containing α or not containing β).

We claim that the formula^{3}

D(a, b⃗) ⇀ ↽ ∀x ≤ |a|∀z^{(2)} ≤ r^{(2)} … Qz^{(j)} ≤ r^{(j)}C(x, (b_{1})_{x+1}, …, (b_{ℓ})_{x+1}, z^{(2)}, …, z^{(j)})

is equivalent to a formula in SE_{j}^{#}. This is obvious if j ≥ 2 (in fact, D is even in SU_{j−1}^{#}). If j = 1, we can represent C(a, b⃗) in the equivalent form

C(a, b⃗) ≡ ⋀_{i=1}^{m} (C′_{i}(a, b⃗, α) ∨ C′′_{i}(a, b⃗, β)) ,

and we are left to show that ∀x ≤ |a| (C′_{i}(a, b⃗, α) ∨ C′′_{i}(a, b⃗, β)) is equivalent to a SE_{1}^{#}- formula. The required formula is simply

∃y′ ≤ 4a∃y′′ ≤ 4a(∀x ≤ |a|(C′_{i}(x, b⃗, α) ≡ Bit(x, y′))

∧ ∀x ≤ |a|(C′′_{i}(x, b⃗, β) ≡ Bit(x, y′′)) ∧ ∀x ≤ |a|(Bit(x, y′) = 1 ∨ Bit(x, y′′) = 1)).

Now, when we know that D(a, b⃗) is provably equivalent to a SE_{j}^{#}-formula, we can apply SE_{j}^{#} − P IND on a to the formula (∃y_{1} ≤ SqBd(a, s_{1})) … (∃y_{ℓ} ≤ SqBd(a, s_{ℓ}))D(a, y⃗) to see that SIE_{i}^{#} ⊢ A ≡ (∃y_{1} ≤ SqBd(t, s_{1})) … (∃y_{ℓ} ≤ SqBd(t, s_{ℓ}))D(t, y⃗).

This completes the proof of Claim 4.2.

As we noted above, Theorem 4.1 follows.

Remark 4.3. It is worth noting that the similar question T_{2}^{i} =^{?} IE_{i}^{#} is open.

5. Proof of Theorem 3.3

We start by showing that (SAT^{∗}, REF (P_{T})) is representable in T (this part is easier). It is sufficient to consider the cases (T, P_{T}) = (SIE_{i}, F_{i−2}), (U_{2}^{1}, F) or (V_{1}^{1}, EF) (in fact, for the second case we will be able to show that (SAT^{∗}, REF (F)) is representable already in U_{1}^{1}). This is actually almost explicitly contained in Propositions 2.4, 2.5 and Lemma 2.6.

Formally, we construct the representation A(a, α_{0}, α), B(a, β_{0}, β), C(a, b, α), D(a, b, β) of (SAT^{∗}, REF (P_{T})) in T as follows:

3to avoid collision with another usage of β, we denote the xth member of a sequence b by (b)_{x} rather than by β(x, b)

• A(a, α_{0}, α) asserts that the string α(0) … α(a − 1) encodes a pair of the form ⟨ϕ, 1^{t}⟩, where ϕ is a CNF such that T r_{2}(|ϕ|, α_{0}, ϕ);

• B(a, β_{0}, β) asserts that the string β(0) … β(a − 1) encodes ⟨ϕ, 1^{t}⟩, where ϕ is a CNF such that Ref_{P_{T}} (t, |ϕ|, β_{0}, ϕ);

• C(a, b, α) ⇀ ↽ α(b);

• D(a, b, β) ⇀ ↽ β(b).

Then condition a) of Definition 3.1 is straightforward. Condition b) is also easy to see: arguing informally in T, if we have ∀x < a(α(x) ≡ β(x)), where α(0) … α(a − 1) encodes a pair ⟨ϕ_{α}, 1^{t_{α}}⟩, and β(0) … β(a − 1) encodes a pair ⟨ϕ_{β}, 1^{t_{β}}⟩, then |ϕ_{α}| = |ϕ_{β}| and ∀x < |ϕ_{α}|(ϕ_{α}(x) ≡ ϕ_{β}(x)). This, along with T r_{2}(|ϕ_{α}|, α_{0}, ϕ_{α}), implies by (3) T r_{2}(|ϕ_{β}|, α_{0}, ϕ_{β}), and now we only have to apply Lemma 2.6, Proposition 2.4 or Proposition 2.5 (depending on T) with a_{0} := t, a_{1} := |ϕ_{β}|, β_{1} := ϕ_{β}.

Now we prove the second part of Theorem 3.3. Namely, assume that (U, V) is representable in T, where T is one of the theories in the left column of Table 2. We want to show that (U, V) is reducible to (SAT^{∗}, REF (P_{T})).

For this we need to modify Definition 2.7. Firstly we enlarge our alphabet of propositional variables. Now it will consist of all variables of the form p_{A(a⃗,α),n⃗}, q_{B(a⃗,β),n⃗}, all free variables in A, B ∈ Σ_{0}^{1,b} being displayed, and we identify original p_{n}, q_{n} with p_{α(a),n}, q_{α(a),n}. Note that this time we have two different alphabets corresponding to the languages L_{1}, L_{2}; it will be always clear from the context which one is used. Also we assume for simplicity that A and B contain the connectives from {¬, ∧, ∨} only.

We define the modification {A(a⃗)}n⃗ of ⟨A(a⃗)⟩n⃗ by extending item b) in Definition 2.7 to

b)^{∗} if A(a⃗, α) [B(a⃗, β)] contains occurrences of α [β] but does not contain occurrences of β [α] then {A(a⃗, α)}n⃗ ⇀ ↽ p_{A(a⃗,α),n⃗} [{B(a⃗, β)}n⃗ ⇀ ↽ q_{B(a⃗,β),n⃗}, respectively].

In accordance with this, items c)-f) are restricted to the case when the formula on the left-hand side contains occurrences of both α and β.

Denote be Def_{α} the following set of propositional sequents, where A, B run over all Σ^{b}(α)-formulae, and t runs over all first-order terms^{4}:

p_{A(t⃗(a⃗)),n⃗} ⟷ p_{A(a⃗),t⃗(n⃗)};
p_{¬A(a⃗),n⃗} ⟷ p̄_{A(a⃗),n⃗};

4we will use the notation Γ ⟷ Δ for denoting the pair of sequents Γ ⟶ Δ and Δ ⟶ Γ

p_{A(a⃗)∧B(a⃗),n⃗} ⟶ p_{A(a⃗),n⃗};
p_{A(a⃗)∧B(a⃗),n⃗} ⟶ p_{B(a⃗),n⃗};
p_{A(a⃗),n⃗}, p_{B(a⃗),n⃗} ⟶ p_{A(a⃗)∧B(a⃗),n⃗};
p_{A(a⃗)∨B(a⃗),n⃗} ⟶ p_{A(a⃗),n⃗}, p_{B(a⃗),n⃗};
p_{A(a⃗),n⃗} ⟶ p_{A(a⃗)∨B(a⃗),n⃗};
p_{B(a⃗),n⃗} ⟶ p_{A(a⃗)∨B(a⃗),n⃗};
p_{(∃x≤a)A(x,b⃗),n,m⃗} ⟶ p_{A(a,b⃗),0,m⃗}, …, p_{A(a,b⃗),n,m⃗};  (4)
p_{A(a,b⃗),n,m⃗} ⟶ p_{(∃x≤a)A(x,b⃗),n′,m⃗} (n ≤ n′);
p_{(∀x≤a)A(x,b⃗),n′,m⃗} ⟶ p_{A(a,b⃗),n,m⃗} (n ≤ n′);
p_{A(a,b⃗),0,m⃗}, …, p_{A(a,b⃗),n,m⃗} ⟶ p_{(∀x≤a)A(x,b⃗),n,m⃗}.  (5)

Def_{β} is defined in the same way.

We also consider the variant Σ′_{d}, Π′_{d} of the hierarchy Σ_{d}, Π_{d} of Boolean formulae (see Section 2.2) by allowing ℓ_{i_{1}...i_{d}} in (1), (2) to have the form p ∗ q, where ∗ ∈ {∧, ∨}, and p, q are propositional variables from the corresponding alphabets. Let F′_{d} be the variant of the proof system F_{d} in which we allow the formulae from Σ′_{d} ∪ Π′_{d} in the proofs.

Lemma 5.1. Let T be one of the theories in the left column of Table 2. Assume that

T ⊢ ∃x⃗ ≤ t⃗(a⃗)(A(a⃗, x⃗, α) ∧ B(a⃗, x⃗, β)),

where A, B ∈ Σ_{0}^{1,b} with all free variables displayed, and t⃗(a⃗) are arbitrary terms of the underlying language. Then there exists a polynomial or quasipolynomial, depending on the entry in the right column, algorithm which for every tuple of integers n⃗ written in unary produces a proof of the empty sequent in the system F′_{i−2}, F or EF determined by the middle column from the set of axioms

Def_{α}, Def_{β}, {⟶ p̄_{A(a⃗,b⃗,α),n⃗,m⃗}, q̄_{B(a⃗,b⃗,β),n⃗,m⃗} | m⃗ ≤ t⃗(n⃗)} .  (6)

Proof. We start with the case of second-order theories (lines 3-5) as it rather easily follows from known results. Namely, we can construct in polynomial or quasipolynomial (depending on the underlying language) time F -proofs

Def_{α} ⊢ ⟨A(a⃗, b⃗, α)⟩_{n⃗,m⃗} ≡ p_{A(a⃗,b⃗,α),n⃗,m⃗}

and

Def_{β} ⊢ ⟨B(a⃗, b⃗, β)⟩_{n⃗,m⃗} ≡ q_{B(a⃗,b⃗,β),n⃗,m⃗}.

Using these, we construct F -proofs of the formulae ⟨¬(A(a⃗, b⃗, α)∧B(a⃗, b⃗, β))⟩_{n⃗,m⃗} (m⃗ ≤ t⃗(n⃗)) from the axioms (6). Then we construct, using Propositions 2.8, 2.9, an F -proof or EF - proof, depending on the theory T, of the formula ⟨∃x⃗ ≤ t⃗(a⃗)(A(a⃗, x⃗, α) ∧ B(a⃗, x⃗, β))⟩n⃗, and apply a sequence of cuts to derive the empty sequent.

Assume now that T is a first-order theory from the first two lines of Table 2. If T comes from the second line, then we can, using Proposition 2.1 and Theorem 4.1, replace it by SIE_{i}^{#}. Now, the theories SIE_{i} and SIE_{i}^{#} differ only in the underlying language, and the rest of the proof is absolutely identically for them. So, we consider only the case of SIE_{i}.

Every SE_{j}-formula (j ≥ 1) is equivalent to a formula in the prenex normal form and it is easily seen to be further equivalent in SIE_{0} to a formula of the form

\begin{matrix}∃x^{(1)} ≤ t⃗^{(1)}(a⃗)∀x^{(2)} ≤ t⃗^{(2)}(a⃗) … Qx^{(j)}(a⃗) ≤ t⃗^{(j)}(a⃗) \\ (C(a⃗, x^{(1)}, …, x^{(j)}, α) ∗ D(a⃗, x^{(1)}, …, x^{(j)}, β)) , \end{matrix}  \} (7)

where ∗ ∈ {∧, ∨}. Denote by SE′_{j} the class of formulae having the form (7), and let SU′_{j} be the dual class. For C ∈ SE′_{j} [C ∈ SU′_{j}] we denote by C̄ the dual formula in C ∈ SU′_{j} [C ∈ SE′_{j}, respectively] logically equivalent to (¬C). Note that for C(a⃗) ∈ SU′_{i−2} and every tuple n⃗, the propositional formula {C(a⃗)}n⃗ is in Π′_{i−2}.

For C(a⃗) ∈ SE′_{i−1}\SU′_{i−2}; C(a⃗) = (∃x⃗ ≤ t⃗(a⃗))D(a⃗, x⃗), where D(a⃗, b⃗) is in SU′_{i−2}, denote by Γ_{C(a⃗),n⃗} the cedent consisting of the formulae {D(a⃗, b⃗)}_{n⃗,m⃗} (m⃗ ≤ t⃗(n⃗)). If C(a⃗) ∈ SU′_{i−2}, we let Γ_{C(a⃗),n⃗} consist of the single formula {C(a⃗)}n⃗.

For C(a⃗) ∈ SU′_{i} \ SE′_{i−1}; C(a⃗) = (∀x⃗ ≤ t⃗(a⃗))D(a⃗, x⃗), where D(a⃗, b⃗) is in SE′_{i−1}, denote by G_{C(a⃗),n⃗} the collection of sequents {⟶ Γ_{D(a⃗,b⃗),n⃗,m⃗} | m⃗ ≤ t⃗(n⃗)}. In the case C(a⃗) ∈ SE′_{i−1}, we let G_{C(a⃗),n⃗} consist of the single sequent ⟶ Γ_{C(a⃗),n⃗}.

The following two statements are proven by an easy induction on the logical complexity of C: Statement 5.2. For every C(a⃗, b⃗) ∈ SU′_{i−2} and terms t⃗(a⃗) there is a polynomial time algorithm which for any tuple of integers n⃗ (written in unary) produces an F′_{i−2}-proof of {C(a⃗, b⃗)}_{n⃗,t⃗(n⃗)} ⟷ {C(a⃗, t⃗(a⃗))}n⃗ from Def_{α}, Def_{β}.

Statement 5.3. Let C(a⃗) ∈ SE′_{i−1}.

a) There exists a polynomial time algorithm which for any 1n⃗ and any formula L ∈ Γ_{C(a⃗),n⃗} produces an F′_{i−2}-proof

Def_{α}, Def_{β}, G_{C̄(a⃗),n⃗} ⊢ L ⟶ .

b) There exists a polynomial time algorithm which for any 1n⃗ and any sequent (⟶ Γ) ∈ G_{C̄(a⃗),n⃗} produces an F′_{i−2}-proof

Def_{α}, Def_{β} ⊢⟶ Γ_{C(a⃗),n⃗}, Γ.

We are going to prove the following generalization of Lemma 5.1:

Statement 5.4. Suppose that

\begin{matrix}SIE_{i} & ⊢ & A_{1}(a⃗), …, A_{k}(a⃗), B_{1}(a⃗), …, B_{ℓ}(a⃗) \\ & & ⟶ A_{k+1}(a⃗), …, A_{r}(a⃗), B_{ℓ+1}(a⃗), …, B_{s}(a⃗), \end{matrix}  \} (8)

where A_{1}, …, A_{k}, B_{ℓ+1}, …, B_{s} ∈ SU′_{i}; B_{1}, …, B_{ℓ}, A_{k+1}, …, A_{r} ∈ SE′_{i}, and all free variables are explicitly displayed. Then there exists a polynomial time algorithm which for any tuple of integers n⃗ written in unary and any cedents Γ_{1}, …, Γ_{s}, where (⟶ Γ_{ν}) ∈

\{ \begin{matrix}G_{B̄_{ν}(a⃗),n⃗} if 1 ≤ ν ≤ ℓ \\ G_{B_{ν}(a⃗),n⃗} if ℓ + 1 ≤ ν ≤ s, \end{matrix} produces an F′_{i−2}-proof

Def_{α}, Def_{β}, G_{A_{1}(a⃗),n⃗}, …, G_{A_{k}(a⃗),n⃗}, G_{Ā_{k+1}(a⃗),n⃗}, …, G_{Ā_{r}(a⃗),n⃗} ⊢⟶ Γ_{1}, …, Γ_{s}.  (9)

Proof of Statement 5.4. As we noticed above, every SE_{i}-formula is equivalent in SIE_{0} to an SE′_{i}-formula. Thus we can assume that SE_{i} − IND in the proof (8) is applied only to SE′_{i}-formulae. By the Cut Elimination Theorem (see e.g. [1, Theorem 4.3]) we can also assume that all formulae appearing in this proof belong to SE′_{i} ∪ SU′_{i}. Let P be this reduced proof.

Now we apply induction on the number of inferences in P. As usual, the argument splits into many cases depending on the final inference (the case when P consists of a single axiom is completely trivial). Most of these cases are straightforward, so we consider explicitly only a few of them. We can assume w.l.o.g. that the final sequent of P has the form A_{1}(a⃗), …, A_{r}(a⃗) ⟶ B_{1}(a⃗), …, B_{s}(a⃗), where A_{1}, …, A_{r}, B_{1}, …, B_{s} ∈ SU′_{i}. Suppose that we are given integers n⃗ and (⟶ Γ_{ν}) ∈ G_{B_{ν}(a⃗),n⃗} (1 ≤ ν ≤ s), and we have to construct efficiently an F′_{i−2}-proof (9).

(∨:left). Assume that the final inference of P has the form

\frac{A′(a⃗), A_{2}(a⃗), …, A_{r}(a⃗) ⟶ B_{1}(a⃗), …, B_{s}(a⃗) A′′(a⃗), …, A_{r}(a⃗) ⟶ B_{1}(a⃗), …, B_{s}(a⃗)}{A′(a⃗) ∨ A′′(a⃗), A_{2}(a⃗), …, A_{r}(a⃗) ⟶ B_{1}(a⃗), …, B_{s}(a⃗)}.

Due to the syntactic structure of SU′_{i}-formulae, (A′(a⃗)∨A′′(a⃗)) ∈ SU′_{0}. Hence, by induction hypothesis we have F′_{i−2}-proofs of the sequent ⟶ Γ_{1}, …, Γ_{s} from both

Def_{α}, Def_{β}, {A′(a⃗)}n⃗ , G_{2}, …, G_{r}

and

Def_{α}, Def_{β}, {A′′(a⃗)}n⃗ , G_{2}, …, G_{r}.

We modify the first proof by adding {A′(a⃗)}n⃗ to antecedents of all its sequents. This will result in an F′_{i−2}-proof of {A′(a⃗)}n⃗ ⟶ Γ_{1}, …, Γ_{s} from axioms Def_{α}, Def_{β}, G_{2}, …, G_{r}. A similar procedure applied to the second proof gives us a proof of {A′′(a⃗)}n⃗ ⟶ Γ_{1}, …, Γ_{s} from the same axioms. The sequent ⟶ {A′(a⃗)}n⃗ , {A′′(a⃗)}n⃗, however, has an obvious proof from Def_{α}, Def_{β}, {A′(a⃗) ∨ A′′(a⃗)}n⃗. Applying twice the cut rule, we will find the desired proof Def_{α}, Def_{β}, {A′(a⃗) ∨ A′′(a⃗)}n⃗ , G_{2}, …, G_{r} ⊢⟶ Γ_{1}, …, Γ_{s}. It is easy to see that the whole construction is polynomial time computable.

(∀ ≤:left). Assume that the final inference of P has the form

\frac{A(a⃗, t(a⃗)), A_{2}(a⃗), …, A_{r}(a⃗) ⟶ B_{1}(a⃗), …, B_{s}(a⃗)}{t(a⃗) ≤ s(a⃗), (∀x ≤ s(a⃗))A(a⃗, x), A_{2}(a⃗), …, A_{r}(a⃗) ⟶ B_{1}(a⃗), …, B_{s}(a⃗)}.

If t(n⃗) ≤ s(n⃗) is false, everything is obvious. Otherwise, it is easy to see that every sequent in G_{A(a⃗,b),n⃗,t(n⃗)} has a short proof from Def_{α}, Def_{β}, G_{(∀x≤s(a⃗))A(a⃗,x),n⃗}, and, by Statement 5.2, the same is true for every sequent in G_{A(a⃗,t(a⃗)),n⃗}. Hence we can apply the inductive assumption.

(∀ ≤:right). Assume that the final inference of P is

\frac{b ≤ t(a⃗), A_{1}(a⃗), …, A_{r}(a⃗) ⟶ B_{1}(a⃗), …, B_{s−1}(a⃗), B(a⃗, b)}{A_{1}(a⃗), …, A_{r}(a⃗) ⟶ B_{1}(a⃗), …, B_{s−1}(a⃗), (∀x ≤ t(a⃗))B(a⃗, x)}.

If (∀x ≤ t(a⃗))B(a⃗, x) ∈ SE′_{i−1} then it is actually in SU′_{i−2}. By inductive assumption, we have efficient F′_{i−2}-proofs Def_{α}, Def_{β}, G_{1}, …, G_{r} ⊢⟶ Γ_{1}, …, Γ_{s−1}, {B(a⃗, b)}_{n⃗,m} for all m ≤ t(n⃗). Applying (5) followed by a sequence of cuts in the case B(a⃗, b) ∈ SU′_{0}, and (∧:right) otherwise, we find an efficient proof of ⟶ Γ_{1}, …, Γ_{s−1}, {(∀x ≤ t(a⃗))B(a⃗, x)}n⃗ from the same axioms.

If (∀x ≤ t(a⃗))B(a⃗, x) ∉ SE′_{i−1} then (⟶ Γ_{s}) ∈ G_{B(a⃗,b),n⃗,m} for some m ≤ t(n⃗), and we simply use the proof of ⟶ Γ_{1}, …, Γ_{s−1}, Γ_{s} available by inductive assumption.

(∃ ≤:left). The final inference has the form

\frac{b ≤ t(a⃗), A(a⃗, b), A_{2}(a⃗), …, A_{r}(a⃗) ⟶ B_{1}(a⃗), …, B_{s}(a⃗)}{(∃x ≤ t(a⃗))A(a⃗, x), A_{2}(a⃗), …, A_{r}(a⃗) ⟶ B_{1}(a⃗), …, B_{s}(a⃗)}.

(∃x ≤ t(a⃗))A(a⃗, x) should necessarily belong to SE′_{i−1}, hence G_{(∃x≤t(a⃗))A(a⃗,x),n⃗} and G_{A(a⃗,b),n⃗,m} consist of single sequents with empty antecedents. Denote by Δ and Δ_{m}, respectively, their succedents.

By inductive assumption, for any m ≤ t(n⃗) we have an F′_{i−2}-proof Def_{α}, Def_{β}, (⟶ Δ_{m}), G_{2}, …, G_{r} ⊢⟶ Γ_{1}, …, Γ_{s}. These proofs give raise to proofs

Def_{α}, Def_{β}, L, G_{2}, …, G_{r} ⊢ Γ_{1}, …, Γ_{s}

for every L ∈ ⋃_{m≤t(n⃗)} Δ_{m}. Also, ⟶ Δ_{0}, Δ_{1}, …, Δ_{t(n⃗)} has an efficient proof from Def_{α}, Def_{β}, (⟶ Δ). Now we argue as in the case (∨:left).

(SE′_{i} − IND). The last inference has the form

\frac{A_{1}(a⃗), …, A_{r}(a⃗), A(a⃗, b) ⟶ A(a⃗, b + 1), B_{1}(a⃗), …, B_{s}(a⃗)}{A_{1}(a⃗), …, A_{r}(a⃗), A(a⃗, 0) ⟶ A(a⃗, t(a⃗)), B_{1}(a⃗), …, B_{s}(a⃗)},

where A(a⃗, b) is in SE′_{i}. Replacing A(a⃗, b) by Ā(a⃗, t(a⃗)− . b) if necessary, we may assume that A is instead in SU′_{i} and, moreover, one of the following is true:

a) A(a⃗, 0) is on the list A_{1}, …, A_{k}, B_{ℓ+1}, …, B_{s}, and A(a⃗, t(a⃗)) is on the list B_{1}, …, B_{ℓ}, A_{k+1}, …, A_{r} in (8);

b) A(a⃗, 0), A(a⃗, t(a⃗)) are on the same list, and A ∈ SE′_{i−1}.

Let us first analyze case a).

Denote by D_{m} the set of sequents G_{A(a⃗,b),n⃗,m}. Then we know from the inductive assumption that for every m < t(n⃗) and every (⟶ Δ_{m+1}) ∈ D_{m+1}, the sequent ⟶ Δ_{m+1}, Γ_{1}, …, Γ_{s} has an efficient F′_{i−2}-proof from the axioms Def_{α}, Def_{β}, G_{1}, …, G_{r}, D_{m}. Appending to the succedents of all sequents in this proof Γ_{1}, …, Γ_{s}, we will construct F′_{i−2}-proofs

Def_{α}, Def_{β}, G_{1}, …, G_{r}, {⟶ Δ_{m}, Γ_{1}, …, Γ_{s} | (⟶ Δ_{m}) ∈ D_{m} } ⊢⟶ Δ_{m+1}, Γ_{1}, …, Γ_{s}.

Now we combine these proofs together and get a polynomially time constructible proof

Def_{α}, Def_{β}, G_{1}, …, G_{r}, {⟶ Δ_{0}, Γ_{1}, …, Γ_{s} | (⟶ Δ_{0}) ∈ D_{0})} ⊢⟶ Δ_{t(n⃗)}, Γ_{1}, …, Γ_{s}

for every (⟶ Δ_{t(n⃗)}) ∈ D_{t(n⃗)}. This completes the analysis of the induction rule in the case when A(a⃗, 0) is on the list A_{1}, …, A_{k}, B_{ℓ+1}, …, B_{s} in (8), and A(a⃗, t(a⃗)) is on the list B_{1}, …, B_{ℓ}, A_{k+1}, …, A_{r}.

In the remaining case b), A is in SE′_{i−1}. This implies that D_{m} consists of a single sequent (⟶ Δ_{m}), and we have already constructed above a proof

Def_{α}, Def_{β}, G_{1}, …, G_{r}, (⟶ Δ_{0}) ⊢⟶ Δ_{t(n⃗)}, Γ_{1}, …, Γ_{s}.  (10)

Let D̄_{m} ⇀ ↽ G_{Ā(a⃗,b),n⃗,m}. Then, depending on which one of the two lists in (8) contains the formulae A(a⃗, 0), A(a⃗, t(a⃗)), we have to construct efficiently either a proof

Def_{α}, Def_{β}, G_{1}, …, G_{r}, (⟶ Δ_{0}), D̄_{t(n⃗)} ⊢⟶ Γ_{1}, …, Γ_{s}

or proofs

Def_{α}, Def_{β}, G_{1}, …, G_{r} ⊢⟶ Δ̄_{0}, Δ_{t(n⃗)}, Γ_{1}, …, Γ_{s}

for all (⟶ Δ̄_{0}) ∈ D̄_{0}. These modifications of (10) are easily obtained using Statement 5.3.

This completes the proof of Statement 5.4.

In order to get Lemma 5.1 for the remaining case T = ISE_{i}, we only have to apply Statement 5.4 with k := r := 1, s := 0, A_{1}(a⃗) ⇀ ↽ ∀x⃗ ≤ t⃗(a⃗)(A(a⃗, x⃗, α) ∨ B(a⃗, x⃗, β)) (for i > 2 notice that axioms (6) imply {A_{1}(a⃗)}n⃗ via one application of (∧:right)). Thus, the proof of Lemma 5.1 is also completed.

Now we are ready to finish the proof of Theorem 3.3. Recall that we have an NP-pair (U, V) representable in T, and let A(a, α), B(a, β), C(a, b, α), D(a, b, β) be the corresponding formulae from Definition 3.1. Then

T ⊢ ∃x ≤ a + 1∃y ≤ 1((x < a ∧ y = 0 ∧ C(a, x, α) ∧ ¬D(a, x, β))
∨ (x < a ∧ y = 1 ∧ ¬C(a, x, α) ∧ D(a, x, β))
∨ (x = a ∧ ¬A(a, α)) ∨ (x = a + 1 ∧ ¬B(a, β))).

We apply to this proof Lemma 5.1 and find, within (quasi)polynomial in N time a propositional proof P_{N}

Def_{α}, Def_{β}, p_{A(a),N}, q_{B(a),N}, (⟶ p̄_{C(a,b),N,i}, q_{D(a,b),N,i}) (i < N),
(⟶ p_{C(a,b),N,i}, q̄_{D(a,b),N,i}) (i < N) ⊢⟶

in the corresponding system F′_{i−2}, F or EF. Let t(N) be the size of P_{N}, and let Def′_{α,N} be the CNF which is obtained by taking sequents in Def_{α} actually used as axioms in P_{N}, and moving their antecedents to the right-hand side with the (¬:right) rule.

Now we are ready to describe the reduction from (U, V) to (SAT^{∗}, REF (P_{T})). Namely, this reduction takes a binary string w = (w_{0}w_{1} … w_{N−1}) of length N to ⟨ϕ(w), 1^{t(N)}⟩, where ϕ(w) is the CNF obtained from Def′_{α,N} by applying to it the restriction ρ_{w} assigning p_{A(a),N} to 1 and assigning all p_{C(a,b),N,i} to w_{i} (i < N).

Assume that w ∈ U. Then, by Definition 3.1 a), there exists α ⊆ N such that N ⊧ A(N, α) and for every i < N, N ⊧ C(N, i, α) ≡ w_{i} = 1. The total assignment of ps which sends every p_{E(a⃗,α),n⃗} to 1 if N ⊧ E(n⃗, α) and to 0 otherwise, satisfies Def′_{α,N} and extends ρ_{w}. Thus, ϕ(w) ∈ SAT.

Assume that w ∈ V, and take β ⊆ N so that N ⊧ B(N, β) and for every i < N, N ⊧ D(N, i, β) ≡ w_{i} = 1. Hit the proof P_{N} with the restriction which extends ρ_{w} by additionally sending every q_{E(a⃗,β),n⃗} to 1 if N ⊧ E(n⃗, β) and to 0 otherwise. This restriction assigns the same values to p_{C(a,b),N,i} and q_{C(a,b),N,i}, hence it forces to 1 all axioms of P except for, possibly, those in Def′_{α,N}. Thus we get a proof of the empty sequent from the clauses of ϕ(w), and its size is at most t(N). For the first-order case we additionally note that every F′_{i−2}-proof becomes an F_{i−2}-proof if we assign truth values to all q-variables. Hence ⟨ϕ(w), 1^{t(N)}⟩ ∈ REF (P_{T}).

This completes the proof of Theorem 3.3.

6. Application to independence results

The purpose of this section is to recast one approach to proving independence results in Bounded Arithmetic in purely complexity terms.

Let us fix an integer-valued superpolynomially-growing function t(n) computable in time 2^{O(n)}. Denote by SIMP LE_{t} the language consisting of truth-tables of those Boolean functions f_{n} which have circuit size at most t(n), where n is the number of variables of f_{n}. Obviously, SIMP LE_{t} ∈ NP. It turns out that the computational hardness of this language to a certain extent captures the hardness of proving lower bounds on the circuit size of explicit functions.

For example, in [12] Razborov and Rudich introduced the notion of a natural proof justified by a careful analysis of existing proofs for restricted models. This notion can be reformulated in terms of purely structural properties of SIMP LE_{t}: a natural proof (against the class P/poly) consists of a set L ∈ P such that L ∩ SIMP LE_{t} = ∅ for some superpolynomial function t(n), and L is “dense” in the sense that P[f_{n} ∈ L] ≥ 2^{−O(n)}, where f_{n} is the random function in n variables. The main result from [12] says that if there exists a pseudo-random number generator with hardness 2^{n^{Ω(1)}} then there exists no L with these properties even in P/poly (and it was observed in [11] that this further extends to sets L computable by quasipolynomial size circuits).

Let s = {s_{n} | n ∈ ω } be any sequence of Boolean functions from the class E (= DT IME(2^{O(n)})). We define SIMP LE_{t}^{⊕s} as the language

{f_{n} ⊕ s_{n} | n ∈ ω, f_{n} ∈ SIMP LE_{t} } .

Note that SIMP LE_{t}^{⊕s} is in NP.

If SIMP LE_{t} ∩ SIMP LE_{t}^{⊕s} = ∅ then, in particular, s_{n} ∉ SIMP LE_{t} for all n. On the other hand, if SIMP LE_{t} ∩ SIMP LE_{t}^{⊕s} ≠ ∅, and f_{n} belongs to the intersection, then we can combine the two size-t(n) circuits for f_{n} and f_{n} ⊕s_{n} with a single P ARIT Y gate at the top to get a size-O(t(n)) circuit for s_{n}. This means that, roughly speaking, the function s is hard if and only if SIMP LE_{t} ∩ SIMP LE_{t}^{⊕s} = ∅.

Let now T be one of the theories of Bounded Arithmetic considered in this paper. We additionally assume that the function t^{♯} given by t^{♯}(N) ⇀ ↽ t(|N|) and the predicate S^{♯}(N, a) ⇀ ↽ s_{|N|}(a) = 1 can be defined by bounded formulae of the underlying language. Let LB_{t,s}(N, γ) be a Σ_{0}^{1,b}-formula asserting that γ does not encode a circuit of size t(|N|) = t^{♯}(N) computing s_{|N|} (our LB_{t,s}(N, γ) corresponds to LB(t^{♯}, s^{♯}, γ) in the notation of [11]). Thus, ∀ϕLB_{t,s}(2^{n}− . 1, ϕ) exactly expresses the fact s_{n} ∉ SIMP LE_{t}. Let SLB_{t,s}(N, α, β) assert that α and β do not encode circuits of size t(|N|) each such that the P ARIT Y of their outputs is s_{|N|}. Thus, ∀ϕ∀ψSLB_{t,s}(2^{n}− . 1, ϕ, ψ) means that SIMP LE_{t} ∩ SIMP LE_{t}^{⊕s} = ∅. Since the argument from the above paragraph is easy to formalize, we can study the provability of SLB_{t,s}(N, α, β) instead of LB_{t,s}(N, γ) (and the split versions were designed in [11] exactly for this purpose). Given Theorem 3.3, we can now reduce the question about provability of SLB_{t,s}(N, α, β) in T to the purely complexity question

(SIMP LE_{t}, SIMP LE_{t}^{⊕s}) ≤_{m}^{?} (SAT^{∗}, REF (P_{T})),  (11)

where ≤_{m} is the appropriate reducibility.

The following easy result (implicit in [11, Proof of Theorem 6.1]) shows that this complexity question is at least not meaningless:

Proposition 6.1. If there exists a pseudo-random number generator with hardness 2^{n^{Ω(1)}} then for any t, s with the above properties the pair (SIMP LE_{t}, SIMP LE_{t}^{⊕s}) can not be separated by quasipolynomial size circuits.

Proof. Assume that E = {E_{n} ⊆ {0, 1}^{(2^{n})} | n ∈ ω } is such a separator: SIMP LE_{t} ⊆ E, E ∩ SIMP LE_{t}^{⊕s} = ∅. Then for any n either |E_{n}| ≥ \frac{1}{2} · 2^{2^{n}} or |E_{n}| ≤ \frac{1}{2} · 2^{2^{n}}. In the first case we let L_{n} ⇀ ↽ (E_{n} ⊕ s_{n}), and in the second case we let L_{n} ⇀ ↽ {0, 1}^{(2^{n})} \ E_{n}. Then L ⇀ ↽ ⋃_{n∈ω} L_{n} is computable by quasipolynomial size circuits since one extra bit of information telling us which of the two cases takes place can be hardwared into the circuit. Also, L ∩ SIMP LE_{t} = ∅ and P[f_{n} ∈ L] ≥ 1/2. As we noticed above, this contradicts the main result from [12].

For completeness we also include an unconditional form of this proposition based upon [12, Theorem 4.4]. Recall [12] that a non-decreasing integer-valued function t(n) is halfexponential if

t^{−1}(n^{C}) ≤ o(log t(n))

for every C > 0, where

t^{−1}(n) ⇀ ↽ max {x | t(x) ≤ n} .

It is easy to see that any half-exponential function has superpolynomial rate of growth. Let us call t(n) strongly half-exponential if it satisfies

t^{−1}(n^{C}) ≤ (log t(n))^{o(1)}

for every C > 0.

Theorem 6.2. Let t(n) be any half-exponential function, and s = {s_{n} | n ∈ ω } be such that for some sequence of primes {p_{n} | n ∈ ω } and some primitive roots g_{n} mod p_{n}, s_{n} is poly-time nonuniformly Turing reducible to computing discrete logarithm mod p_{n} base g_{n}. Then there is no E ∈ P such that SIMP LE_{t} ⊆ E and SIMP LE_{t}^{⊕s} ∩ E = ∅. Moreover, if t(n) is strongly half-exponential, then no such E exists even in QP.

Proof. Assuming the contrary, we, like in the previous proof, would have a natural proof L ∈ P/poly with the additional property s_{n} ∈ L for all n ∈ ω. It can not exist (without any unproven assumptions!) by [12, Theorem 4.4]. It is also easy to see that if t(n) is strongly half-exponential then [12, Theorem 4.4] extends to L computable by quasipolynomial size circuits.

Proposition 6.1 and Theorem 6.2 show that in order to prove the independence of SLB_{t,s}(N, α, β) from a theory T, it is sufficient to separate the pair (SAT^{∗}, REF (P_{T})) by a (quasi)polynomial time computable set. We conclude this section by showing another proof of the main result from [11] which goes exactly along these lines.

Lemma 6.3. If a pair (U, V) of disjoint NP-sets is representable in SIE_{1} [SS_{2}^{2}] then there exists a constant w > 0 such that (U, V) ≤_{m}^{p} (SAT^{∗}, REF (R_{w})) [(U, V) ≤_{m}^{qp} (SAT^{∗}, REF (R_{w})), respectively].

Proof. By modifying the proof of Lemma 5.1 for the case SIE_{2}. Namely, we replace the axioms (4),(5) by

p_{(∃x≤a)A(x,b⃗),0,m⃗} ⟶ p_{A(a,b⃗),0,m⃗}
p_{(∃x≤a)A(x,b⃗),n+1,m⃗} ⟶ p_{(∃x≤a)A(x,b⃗),n,m⃗}, p_{A(a,b⃗),n+1,m⃗}
p_{A(a,b⃗),0,m⃗} ⟶ p_{(∀x≤a)A(x,b⃗),0,m⃗}
p_{(∀x≤a)A(x,b⃗),n,m⃗}, p_{A(a,b⃗),n+1,m⃗} ⟶ p_{(∀x≤a)A(x,b⃗),n+1,m⃗}

so that all sequents in Def_{α}, Def_{β} have bounded length. The important point is that if we can deduce (n + 1) sequents Γ ⟶ p_{A(a,b⃗),0,m⃗}, Δ; …; Γ ⟶ p_{A(a,b⃗),n,m⃗}, Δ in R_{w} then we can deduce Γ ⟶ p_{(∀x≤a)A(x,b⃗),n,m⃗}, Δ in R_{w′} for some w′ depending only on w, and similarly for Γ, p_{(∃x≤a)A(x,b⃗),n,m⃗} ⟶ Δ. For C(a⃗) ∈ SE′_{0}, the cedent Γ_{C(a⃗),n⃗} in our case always consists of the single formula {C(a⃗)}n⃗.

With these observations in mind, it is easy to see that the procedure described in the proof of Statement 5.4 for i = 2, actually gives in the case i = 1 a resolution proof in which the length of all clauses is bounded by some absolute constant (depending on the original proof P in SIE_{1}). The only additional remark which should be made is that the “bad” rules (∃ ≤:left), (∃ ≤:right) now simply do not occur in the proof.

Lemma 6.4. For every fixed constant w > 0, SAT^{∗} and REF (R_{w}) can be separated by a poly-time computable set.

Proof. The separator is

{⟨ϕ, 1^{t}⟩ | there is no derivation of the empty sequent from ϕ in the system R_{w} } .

It is poly-time computable simply by producing the list of all sequents of length at most w which can be derived from ϕ.

Theorem 6.5. A disjoint NP-pair is representable in SIE_{1} [S_{2}^{2}] if and only if it can be separated by a polynomial [quasipolynomial, respectively] time computable set.

Proof. Immediate from Theorem 3.2, Lemma 6.3 and Lemma 6.4.

The first part of the following theorem is exactly [11, Theorem 6.4]:

Theorem 6.6. If there exists a pseudo-random number generator with hardness 2^{n^{Ω(1)}}, then for any t, s with the properties stated at the beginning of this section,

SS_{2}^{2} ⊬ SLB_{t,s}(N, α, β).

If, in addition, t is half-exponential [strongly half-exponential], and s is reduced to the discrete logarithm problem as described in the statement of Theorem 6.2, then SIE_{1} ⊬ SLB_{t,s}(N, α, β) [SS_{2}^{2} ⊬ SLB_{t,s}(N, α, β), respectively] without any unproven assumptions.

Proof. Immediate from Theorem 6.5, Proposition 6.1 and Theorem 6.2.

7. Discussion

This paper brings to attention the question for which propositional proof systems P the pair (SAT^{∗}, REF (P)) can be separated by a (quasi)polynomial time computable set. In this section we try to locate this question with respect to more familiar hypothesis.

Let us first point out that the affirmative answer implies the following alternative:

Theorem 7.1. Assume that for some proof system P, SAT^{∗} and REF (P) can be separated by a poly-time computable set. Then one of the following is true:

a) P = NP,

b) the proof system P is not optimal in the sense that the function

s_{P} (n) ⇀ ↽ max {s_{P} (ϕ) | ϕ is an unsatisfiable CNF of length ≤ n}

is not bounded by any polynomial.

Proof. Let SAT^{∗} ⊆ L; L ∩ REF (P) = ∅; L ∈ P, and assume that b) does not take place. Then s_{P} (n) ≤ p(n) for some polynomial p, and ϕ ∈ SAT ≡ ⟨ϕ, 1^{p(|ϕ|)}⟩ ∈ L. Thus, SAT ∈ P.

This theorem might be taken as an evidence that any attempts to prove the existence of the separator by known methods are doomed to fail. We should be, however, somewhat careful with this conclusion. For example, the proof of Lemma 6.4, whatever simple, still does not tell us which of the two alternatives a) and b) is true for the system R_{w}. Of course, we know that b) is true, and, moreover, R_{w} is not even complete – but this has to be proved separately. Thus, simply knowing that either a) or b) is true might be surprising approximately to the same extent as knowing that one of the two alternatives LOGSPACE ≠ P or P ≠ PSPACE is true.

But, of course, we can not hope to show by the existing methods that (SAT^{∗}, REF (P)) (as well as any other disjoint NP-pair) is not separable. So, if we are interested in evidence toward the negative solution, the best we can hope for is to reduce to (SAT^{∗}, REF (P)) another pair which is believed to be hard.

I do not know of any example of a reduction from a presumably hard NP-pair to (SAT^{∗}, REF (EF)), which is the same, due to our main result, as an example of such pair representable in V_{1}^{1}.

There is, however, a number of “plain” reductions from (U, V) to (SAT^{∗}, REF (EF)), where (U, V) is separable but this fact is highly non-trivial. The best example of this kind (in the sense that it is applicable to the weakest system P) is provided by [11, Example 1]. Namely, let CHR ⇀ ↽ {< G, s > | G is an s − colourable graph}, and CL^{2} ⇀ ↽ {< G, s > | G contains a clique of size s^{2} }. Then (CHR, CL^{2}) is representable in ST_{2}^{3} and, thus, (CHR, CL^{2}) ≤_{m}^{qp} (SAT^{∗}, REF (F_{1})). On the other hand, the known polytime computable separator for (CHR, CL^{2}) is based upon very deep combinatorial ideas [16].

I do not know of any evidence of this sort that (SAT^{∗}, REF (R)) is hard. This could be the next accessible question.

8. Acknowledgement

I am indebted to Jan Krajíc̆ek for his initial suggestion to look for a propositional counterpart of the machinery from [11]. My thanks are also due to Søren Riis and Alan Selman for several useful remarks.

References

[1] S. R. Buss. Bounded Arithmetic. Bibliopolis, Napoli, 1986.

[2] S. R. Buss. Axiomatizations and conservations results for fragments of Bounded Arithmetic. In Logic and Computation, Contemporary Mathematics 106, pages 57–84. American Math. Society, 1990.

[3] S. A. Cook. Feasibly constructive proofs and the propositional calculus. In Proceedings of the 7th Annual ACM Symposium on the Theory of Computing, pages 83–97, 1975.

[4] S. A. Cook and A. R. Reckhow. The relative efficiency of propositional proof systems. Journal of Symbolic Logic, 44(1):36–50, 1979.

[5] J. Grollmann and A. L. Selman. Complexity measures for public-key cryptosystems. SIAM Journal on Computing, 17(2):309–335, April 1988.

[6] S. Homer and A. L. Selman. Oracles for structural properties: The isomorphism problem and public-key cryptography. Journal on Computer and System Sciences, 44(2):287–301, April 1992.

[7] J. Krajíc̆ek. On Frege and extended Frege proof systems. Manuscript, 1993.

[8] J. Paris and A. Wilkie. Counting problems in bounded arithmetic. In Methods in Mathematical Logic, Lecture Notes in Mathematics 1130, pages 317–340. Springer-Verlag, 1985.

[9] A. Razborov. An equivalence between second order bounded domain bounded arithmetic and first order bounded arithmetic. In P. Clote and J. Krajíc̆ek, editors, Arithmetic, Proof Theory and Computational Complexity, pages 247–277. Oxford University Press, 1992.

[10] A. Razborov. Bounded Arithmetic and lower bounds in Boolean complexity. To appear in the volume Feasible Mathematics II, 1993.

[11] A. Razborov. Unprovability of lower bounds on circuit size in certain fragments of Bounded Arithmetic. To appear in Izvestiya of the RAN, 1994.

[12] A. Razborov and S. Rudich. Natural proofs. Preliminary version appeared in Proceedings of the 26th ACM Symposium on Theory of Computing, pp. 204-213, 1994.

[13] A. L. Selman. Complexity issues in cryptography. Proceedings of Symposia in Applied Mathematics, 38:92–107, 1989.

[14] G. Takeuti. S_{3}^{i} and ∘ V_{2}^{i}(BD). Archive for Math. Logic, 29:149–169, 1990.

[15] G. Takeuti. RSUV isomorphisms. In P. Clote and J. Krajíc̆ek, editors, Arithmetic, Proof Theory and Computational Complexity, pages 364–386. Oxford University Press, 1992.

[16] É. Tardos. The gap between monotone and nonmonotone circuit complexity is exponential. Combinatorica, 8:141–142, 1988.

[17] G. Wilmers. Bounded existential induction. The Journal of Symbolic Logic, 50(1):72– 90, March 1985.

[18] �� �� ��� ����. � ��������� ������ � ���������� ������������ �. In �� �� ��������, editor, ������������ �� ��������������� ���������� � ������� ��������� ������� II� ������� ������� ��������� ����� �� �, pages 234–259. �����, ���������, 1968. Engl. translation: G. C. Tseitin, On the complexity of derivations in propositional calculus, in: Studies in mathematics and mathematical logic, Part II, ed. A. O. Slissenko, pp. 115-125.

Recent Publications in the BRICS Report Series

RS-94-36 Alexander A. Razborov. On provably disjoint NP-pairs. November 1994. 27 pp.

RS-94-35 Gerth St�lting Brodal. Partially Persistent Data Structures of Bounded Degree with Constant Update Time. November 1994. 24 pp.

RS-94-34 Henrik Reif Andersen, Colin Stirling, and Glynn Winskel. A Compositional Proof System for the Modal μ-Calculus. October 1994. 18 pp. Appears in: Proceedings of LICS ’94, IEEE Computer Society Press.

RS-94-33 Vladimiro Sassone. Strong Concatenable Processes: An Approach to the Category of Petri Net Computations. October 1994. 40 pp.

RS-94-32 Alexander Aiken, Dexter Kozen, and Ed Wimmers. Decidability of Systems of Set Constraints with Negative Constraints. October 1994. 33 pp.

RS-94-31 Noam Nisan and Amnon Ta-Shma. Symmetric Logspace is Closed Under Complement. September 1994. 8 pp.

RS-94-30 Thore Husfeldt. Fully Dynamic Transitive Closure in Plane Dags with one Source and one Sink. September 1994. 26 pp.

RS-94-29 Ronald Cramer and Ivan Damg� ard. Secure Signature Schemes Based on Interactive Protocols. September 1994. 24 pp.

RS-94-28 Oded Goldreich. Probabilistic Proof Systems. September 1994. 19 pp.

RS-94-27 Torben Bra� uner. A Model of Intuitionistic Af�ne Logic from Stable Domain Theory (Revised and Expanded Version). September 1994. 19 pp. Full version of paper appearing in: ICALP ’94, LNCS 820, 1994.

RS-94-26 S�ren Riis. Count(q) versus the Pigeon-Hole Principle. August 1994. 3 pp.