OnprovablydisjointNP-pairs BRICS

BRICSRS-94-36A.A.Razborov:OnprovablydisjointNP-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 c 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

Alexander A. Razborov Steklov Mathematical Institute

Vavilova 42, 117966, GSP{1, Moscow, RUSSIA November 11, 1994

Abstract

In this paper we study the pairs (^UV) 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 sucient 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(^S2) +^Sb2;PIND 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 (UV ), 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.

1

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 *)^ff s^jf ²U^g

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 sucientlystrong pseudo-random generators exist then theseU 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²)+^Sb2;PIND of Bounded Arithmetic can prove that U^\V = for some

NP

-pair (UV ) 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 forprovingthe factU^\V =. Namely, for a variety of systemsT of Bounded Arithmetic, we consider the class of

NP

-pairs for which this fact is provable inT.

We exhibit a natural

NP

-pair which is completein this class under the many-one reduction.

Roughly speaking, the rst component in this pair consists of all satisable CNF, and the second component consists of those unsatisable CNF which allow a short refutation in the propositional proof system associated withT. 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 2

separation exists, we have the independence of

NP

⁶

P

=poly from the theory T modulo the hardness assumption. For the theory^S(S²)+^Sb2;PIND 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 quantiers. 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 familiaritywith 1], and use the now-standard notation for denoting various hierarchies and fragments of Bounded Arithmetic from that book. L¹ is the rst order language which consists of the constant 0, function symbols S+ ^b12x^cjx^j, and of the predicate symbol . L² is obtained from L¹ by augmenting it with the smash symbol

# which has the intended meaning x#y = 2^jxjjyj. Lk() (k = 12) is the rst-order language obtained from Lk by appending to the latter two new unary predicate symbols (a)(a), and ^Lk is the second-order language based on Lk. To simplify the notation, we will sometimes be using several predicate symbols (second-order variables in the case of

Lk) like¹²::: or ¹²:::: 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 Lk() or in ^Lk

(k = 12). All they contain the set BASICk of simple open axioms describing basic properties of symbols fromLk. On the top of it, second-order theories also always include the comprehension axiom scheme ^10b;CA. The dierence between theories is specied by the amount of induction allowed.

Behind the standard hierarchy bibi of bounded formulae we also need its split version

S_bi^S_bi in the languageL²() 11]. ^Sb0 =^Sb0is the set ofallbounded formulae which contain either only occurrences of or only occurrences of . The inductive denition of

S_bi^+1S_bi⁺¹ is the same as for _bi⁺¹bi⁺¹. 3

The hierarchy EiUi (see e.g. 17]) was dened as the ordinary hierarchy of bounded formulae in the language of Peano Arithmetic (where we do not have the notion of a sharply bounded quantier at all). A bounded formula isDi in a theoryT if it is provably equivalent to anEi- andUi-formula inT. We extend this hierarchy to the language L¹() simply by counting sharply bounded quantiers exactly as ordinary quantiers. The split versions ^SEi^SUi^SDi of this hierarchy in the language L¹() are dened analogously to ^S_bi^S_bi.

The following table summarizes the denitions of the theories of Bounded Arithmetic considered in this paper¹:

Theory Underlying language Induction scheme

S²ⁱ() L²() _bi()^;PIND

SS²ⁱ L²() ^Sbi^;PIND

IEi() L¹() Ei()^;IND

SIEi L¹() ^SEi^;IND

T²ⁱ() L²() _bi()^;IND

ST²ⁱ L²() ^S_bi^;IND

I⁰() L¹() ⁰()^;IND

S²() L²() ^b()^;PIND

U^{11 L1 11b;}PIND

U^{21 L2 11b;}PIND

V^{11 L1 11b;}IND

V^{21 L2 11b;}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 i1, ^SS²ⁱ⁺¹ is ^8S_bi⁺¹-conservative over ^ST²ⁱ.

1we have introduced the natural notation ^SS2iST2i for the theories ^S(^S2) +^{Sbi ;PIND S}(^S2) +

S^bi;INDfrom 11] and^SIEi for the split versions of the theories ^IEi(). Also, ^{b *)Si0bi}.

4

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.

Dierent proof systems are usually specied by the syntactic requirements placed on the sequents allowed in the proof:

For a xed constant w > 0, we denote by Rw the system of bounded resolutions. All sequents in the proof must have the form `<sup>1</sup>:::`p ^;! `p<sup>+1</sup>:::`q, where `is 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, resolutionsis the same system as Rw, only without any restrictions on the length of the sequents.

Fd is the depth-d Frege system: all formulae appearing in the proof must either have

the form _r

1

_

i¹⁼¹ r²^⁽i¹⁾

i²⁼¹ :::^{rd(i1:::i_^d;1)}

i^d=1 `i¹:::i^d (1)

(d-formulae) or

r¹

^

i¹⁼¹ r²_⁽i¹⁾

i²⁼¹ :::^{rd(i1:::i_^d;1)}

i^d=1 `i¹:::i^d (2)

(d-formulae), where `i¹:::i^d are literals. The inference rules are modied for un- bounded fan-in, e.g. (^{^}:right) looks like

;^;!Ai (i²I)

;^;!Vi²IAi : Note thatF⁰ =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 ex- tension axioms of the form p A, where p is a new propositional variable (called extension atom) which did not appear earlier in the proof.

5

For an unsatisable CNF = ^Vi²I^Wj²Jⁱ`ij and a proof system P we denote by sP() the minimal possible number of logical symbols in a P-derivation of the empty sequent from the sequents<sup>;!f</sup>`ij^jj ²Ji^g (i²I).

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

For many theories of Bounded ArithmeticT there exists a propositional proof system PT

closely associated with T in the following sense:

a)

T proves the soundness of PT,

b)

every proof in T of a formula A with appropriately low logical complexity can be eciently transformed into a short PT-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 Tr(a) be the predicate asserting that the truth assignment makes the Boolean formula encoded by the string (0):::(a^;1) true (truth denition).

Proposition 2.2 (7]).

Tr(a) ^{has a 11b}-denition in U¹¹ about which U^{11 proves the} usual Tarski's conditions.

LetTrd(a) be the variant of Tr(a) in which (0):::(a^;1) encodes a Boolean formula from d d. The following is straightforward:

Lemma 2.3.

For any xed d 0, Trd(a) has a ^SDd⁺¹-denition in ^SIE⁰ about which ^SIE⁰ proves the usual Tarski's conditions.

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

SIE^{0 `8}x < a(¹(x)¹(x))(Trd(a¹)Trd(a¹)): (3) Let the ^10b-formula RefP(a⁰a¹⁰¹) assert that the string ⁰(0):::⁰(a^{0 ;}1) en- codes an inference of lengtha⁰ in the propositional proof systemP of the empty sequent from the clauses of the CNF encoded by¹(0):::¹(a^1;1). The following two propositions are slight modications 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 PV and S²¹ 1, Chapter 6] and RSUV -isomorphism 14, 15, 9]):

6

Proposition 2.4.

U^{11 `}RefF(a⁰a¹⁰¹)^:Tr²(a¹¹).

Proposition 2.5.

V^{11 `}RefEF(a⁰a¹⁰¹)^:Tr²(a¹¹).

Paris and Wilkie 8] showed that I⁰()^`RefF^d(a⁰a¹⁰¹)^:Tr²(a¹¹) for any xed d0. We will need the following renement of their result:

Lemma 2.6.

For any xed d0, ^SIEd⁺²()^`RefF^d(a⁰a¹⁰¹)^:Tr²(a¹¹).

Proof.

AssumingTr²(a¹¹), we prove by induction onc that in ANY one of the rst c sequents of the inference encoded by ⁰there EXISTS either a formula in the antecedent such that^:Trd(a¹) or a formula in the succedent such that Trd(a¹). By Lemma 2.3, the formula expressing this fact is in^SUd⁺², and^SUd^+2;IND is available in^SIEd⁺².

Let us now x propositional variables p¹p²:::pn:::q¹q²:::

Denition 2.7 (see e.g. 7]).

For every A(~a) ^{2 10b}, where all free variables are displayed, and a tuple of integers~n we dene the propositional formula^hA(~a)ⁱ~nby induction on the complexity of A:

a)

ifA does not contain occurrences of and , and A(~n) is true false] on integers then

hA(~a)ⁱ~n *) 1 0, respectively]"

b)

if A(~a) = (t(~a)) (t(~a))] then ^hA(~a)ⁱ~n *) pt⁽~n⁾ qt⁽~n⁾, respectively]"

c)

^h:A(~a)ⁱ~n *)^:hA(~a)ⁱ~n"

d)

^hA(~a)B(~a)ⁱ~n*)^hA(~a)ⁱ~n^hB(~a)ⁱ~n for^{2f^_g}"

e)

^h(⁹xt(~a))A(~ax)ⁱ~n *)^Wmt⁽~n^)hA(~ab)ⁱ~nm"

f)

^h(⁸xt(~a))A(~ax)ⁱ~n *)^Vmt⁽~n^)hA(~ab)ⁱ~nm.

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^{21 `} A(~a), where A(~a) is a ^10b-formula with all free variables displayed. Then there exists a quasipolynomial time² algorithm which for any tuple of integers ~n given in the unary form 1^~n produces an F-proof of the propositional formula ^hA(~a)ⁱ~n.

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

7

Proposition 2.9.

Let V^{11 `} A(~a), where A(~a) is in ^10b. Then there exists a polynomial time algorithm which for any 1^~n produces an EF-proof of ^hA(~a)ⁱ~n.

The same remains true after replacing \V¹¹" by \V²¹", and \polynomial time" by

\quasipolynomial time".

A similar result about the provability in I⁰() 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

Denition 3.1.

Let U and V be two disjoint sets in

NP

, and T be either a rst-order theory in the language Lk() or a second-order theory in the language ^Lk (k = 12).

The pair (UV ) is representable inT if there exist ^10b-formulae

A(a)B(a)C(ab)D(ab) with all free variables displayed such that:

a)

for everyw = (w⁰w¹:::wN^;1)^2f01^gN, if w²U then

N

^j=⁹ (A(N )^{^8}i < N(C(Ni )wi = 1)) and ifw²V then

N

^j=⁹(B(N)^{^8}i < N(D(Ni)wi = 1))"

b)

T ^`(A(a)^{^}B(a))⁹x < a(C(ax)⁶D(ax)):

Informally, condition a) says that A and B specify some U^e U and V^e V as pro- jections of

P

-sets if k = 1 and

QP

-sets if k = 2. b) means that U^{e \}V =^e is provable in T. We exploit the ordinary notion of _pm-reducibility in the context of promise problems.

Namely, (UV )_pm (U⁰V⁰) means that there is a polynomially time computable function f : ^f01^{g ;! f}01^g such that f(U) U⁰ and f(V ) V⁰. The variant ^qp_m of this reducibility is dened in the same way with the dierence that we only requiref to be in

QP

.

8

Theorem 3.2. a)

Let T be one of the theories

SS^2iIEi^ST²ⁱ (i1)I⁰()S²()U¹¹U²¹V¹¹V²¹:

Then the class of

NP

-pairs representable in T is closed under _pm-reducibility.

b)

If, moreover, T ^{2 fS}S^2iST²ⁱS²()U²¹V^21g then this class is closed under ^qp_m- reducibility.

Proof.

a). Assume that (UV ) is representable in T via bounded formulae

A(a)B(a)C(ab)D(ab), and let (U⁰V⁰) _pm (UV ) via a polynomial time computable functionf. Then for a suitable polynomial p(a) we have ^10b-formulae

Prot(a⁰¹)Output(ab⁰¹) and ⁰-denable in I⁰(⁰¹) function symbol Length(a⁰¹) expressing the following:

Prot(a⁰¹) { \¹(0):::¹(p(a)^;1) is (the encoding of) the protocol of the poly- time computation off on the input string ⁰(0):::⁰(a^;1)""

Length(a⁰¹) is the length of the output of ¹ if Prot(a⁰¹) and 0 otherwise"

Output(ab⁰¹) { \Prot(a⁰¹), b < Length(a⁰¹) and the bth bit of ¹'s output is equal to 1".

We now set:

A⁰(a⁰¹²) *) Prot(a⁰¹)^{^}A(Length(a⁰¹)²)

^ 8x < Length(a⁰¹)(C(ax²)Output(ax⁰¹)) B⁰(a⁰¹²) *) Prot(a⁰¹)^{^}B(Length(a⁰¹)²)

^ 8x < Length(a⁰¹)(D(ax²)Output(ax⁰¹)) C⁰(ab⁰¹²) *) ⁰(b)

D⁰(ab⁰¹²) *) ⁰(b):

We claim that A⁰B⁰C⁰D⁰ provide a representation of (U⁰V⁰) in the theoryT.

Condition a) from Denition 3.1 is straightforward.

In order to see b), suppose, arguing informally in T, that ⁸x < a(⁰(x) ⁰(x)), A⁰(a⁰¹²) andB⁰(a⁰¹²). Applying^SU^1;IND on cp(a) (which is available in T) to the formula ⁸x < c(¹(x) ¹(x)), we nd ⁸x < p(a)(¹(x) ¹(x)). Thus,

9

T PT reducibility

SIEi (i2) Fi^;2 pm

ST^2iSS²ⁱ⁺¹ (i2) Fi^;2 qpm

U²¹ F ^qpm

V¹¹ EF pm

V²¹ EF ^qpm

Table 2: (SATREF(PT)) is complete in the class corresponding toT

Length(a⁰¹) = Length(a⁰¹) and ⁸x < Length(a⁰¹)(Output(ax⁰¹) Output(ax⁰¹)). From the denition of A⁰B⁰ we conclude

8x < Length(a⁰¹)(C(ax²)Output(ax²))

and this contradicts condition b) for the original pair (UV ) (after substituting a :=

Length(a⁰¹) := ² := ²).

Part b) is proved in exactly the same way.

Let now SAT *) ^fh1^tij is a satisable CNF^g. For a propositional proof sys- tem P, let REF(P) *) ^fh1^tij is an unsatisable CNF and sP()t^g. Obviously, SATREF(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 PT be the corresponding proof system in the middle column. Then (SATREF(PT)) 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 (SATREF(P)):

Corollary 3.4.

(REF(Fd)SAT)pm (SATREF(Fd)) (d0), (REF(F)SAT)^qpm

(SATREF(F))^{, and} (REF(EF)SAT)_pm (SATREF(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 UV .

10

4. Elimination of sharply bounded quantiers in split versions

Let us consider the analogueEi^#Ui^# of the hierarchyEiUiin the language L², and its split versions ^SEi^#SUi^# in the language L²(). Thus, ^SEi^#SUi^# dier from^SEi^SUi only in the underlying language, whereas the syntactic inductive denitions for both hierarchies are the same. The theoriesIEi^#SIEi^# have the obvious meaning. In this section we prove the following:

Theorem 4.1.

^SIE_i^# =^ST²ⁱ for all i0.

Proof.

Since ^SEi^{# S}bi, it suces to show that ^SIEi^{# ` S}bi ^;IND. This will be immediately implied by the following

Claim 4.2.

^Let 0 j i. Then every ^S_bj-formula is equivalent in ^SIEi^# to a ^SEj^#- formula.

Proof of Claim 4.2.

W.l.o.g. we may assume that A ^{2 S}_bj contains only connectives

f:^{^_g}and, moreover, that negations appear on atomic subformulae only. Now we apply induction on ^hj^jA^ji.

Base

j = 0 is obvious since^Sb0 =^SE^0#.

Inductive step.

Let j > 0 and A ^{2 S}bj. If A ^{2 S}bj^;1, we convert (^:A) into the equivalent form %A ^{2 S}bj^;1 obeying the above restrictions, and apply to %A the inductive assumption with j := j ^;1. If A = B C or A = (⁹x t)B(x), the inductive step is obvious (^SEj^# is closed under these operations).

The only nontrivial case is A = (⁸x^jt^j)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,

SIEi<sup># `</sup>A <sup>8</sup>x<sup>j</sup>t<sup>j9</sup>y<sup>1</sup>s<sup>1</sup>:::<sup>9</sup>y` s`⁸~z⁽²⁾~r⁽²⁾:::Q~z^(j)~r^(j)C(x~y~z⁽²⁾:::~z^(j)) whereC is a Boolean combination of ^SE^0#-formulae. The crucial point is that since^SIEi^#

contains S²¹, it can also dene all ^b1-denable inS²¹ 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).

11

We claim that the formula³

D(a~b) *)⁸x^ja^j8~z⁽²⁾~r⁽²⁾:::Q~z^(j)~r^(j)C(x(b¹)x⁺¹:::(b`)x⁺¹~z⁽²⁾:::~z^(j)) is equivalent to a formula in ^SEj^#. This is obvious if j 2 (in fact, D is even in ^SUj^#;1).

If j = 1, we can represent C(a~b) in the equivalent form C(a~b) ^{^m}

i⁼¹

Ci⁰(a~b)^_Ci⁰⁰(a~b)

and we are left to show that ⁸x ^ja^jCi⁰(a~b)^_Ci⁰⁰(a~b) is equivalent to a ^SE^1#- formula. The required formula is simply

9y⁰4a⁹y⁰⁰4a⁸x^ja^j(Ci⁰(x~b) Bit(xy⁰))

^ 8x^ja^j(Ci⁰⁰(x~b)Bit(xy⁰⁰))^{^8}x^ja^j(Bit(xy⁰) = 1^_Bit(xy⁰⁰) = 1): Now, when we know thatD(a~b) is provably equivalent to a^SEj^#-formula, we can apply

SEj^{# ;}PIND on a to the formula (⁹y¹ SqBd(as¹)):::(⁹y` SqBd(as`))D(a~y) to see that ^SIEi<sup># `</sup>A(<sup>9</sup>y<sup>1</sup> SqBd(ts<sup>1</sup>)):::(<sup>9</sup>y` SqBd(ts`))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 questionT²ⁱ =^? IEi^# is open.

5. Proof of Theorem 3.3

We start by showing that (SATREF(PT)) is representable in T (this part is easier). It is sucient to consider the cases (TPT) = (^SIEiFi^;2)(U²¹F) or (V¹¹EF) (in fact, for the second case we will be able to show that (SATREF(F)) is representable already in U¹¹). This is actually almost explicitly contained in Propositions 2.4, 2.5 and Lemma 2.6.

Formally, we construct the representation A(a⁰)B(a⁰)C(ab)D(ab) of (SATREF(PT)) 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(^xb)

12

A(a⁰) asserts that the string (0):::(a^;1) encodes a pair of the form^h1^ti, where is a CNF such that Tr²(^jj0)"

B(a⁰) asserts that the string (0):::(a^;1) encodes ^h1^ti, where is a CNF such that RefP^T(t^jj0)"

C(ab) *) (b)"

D(ab) *) (b).

Then condition a) of Denition 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 ^h1^ti, and (0):::(a^;1) encodes a pair ^h1^ti, then ^jj= ^jj and ⁸x <

j^j((x) (x)). This, along with Tr²(^jj0), implies by (3) Tr²(^jj0), and now we only have to apply Lemma 2.6, Proposition 2.4 or Proposition 2.5 (depending on T) with a⁰ :=ta¹ :=^jj1 :=.

Now we prove the second part of Theorem 3.3. Namely, assume that (UV ) is repre- sentable in T, where T is one of the theories in the left column of Table 2. We want to show that (UV ) is reducible to (SATREF(PT)).

For this we need to modify Denition 2.7. Firstly we enlarge our alphabet of proposi- tional variables. Now it will consist of all variables of the form pA⁽~a⁾~nqB⁽~a⁾~n, all free variables in AB^210b being displayed, and we identify original pnqn with p⁽a⁾nq⁽a⁾n. Note that this time we have two dierent alphabets corresponding to the languages L¹L²"

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 ^{f:^_g} only.

We dene the modication ^fA(~a)^g_~n of ^hA(~a)ⁱ~n by extending item b) in Denition 2.7 to b) if A(~a) B(~a)] contains occurrences of ] but does not contain occurrences of ]^{then f}A(~a)^g~n *) pA⁽~a⁾~n ^fB(~a)^g~n*) qB⁽~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 AB run over all ^b()-formulae, and t runs over all rst-order terms⁴:

pA⁽~t⁽~a⁾⁾~n ^!pA⁽~a⁾~t⁽~n⁾"

p^:A⁽~a⁾~n ^!p%A⁽~a⁾~n"

4we will use the notation ;^! for denoting the pair of sequents ;^;! and ^;!;

13

pA⁽~a^{)^}B⁽~a⁾~n ^;!pA⁽~a⁾~n"

pA⁽~a^{)^}B⁽~a⁾~n ^;!pB⁽~a⁾~n"

pA⁽~a⁾~npB⁽~a⁾~n ^;!pA⁽~a^{)^}B⁽~a⁾~n"

pA⁽~a^)_B⁽~a⁾~n ^;!pA⁽~a⁾~npB⁽~a⁾~n"

pA⁽~a⁾~n ^;!pA⁽~a^)_B⁽~a⁾~n"

pB⁽~a⁾~n ^;!pA⁽~a^)_B⁽~a⁾~n"

p⁽⁹_xa⁾_A⁽_x~b⁾_n~m ^;!p_A⁽_a~b⁾⁰_~m:::p_A⁽_a~b⁾_n~m" (4) p_A⁽_a~b⁾_n~m ^;!p⁽⁹_xa⁾_A⁽_x~b⁾_n⁰_~m (n n⁰)"

p⁽⁸_xa⁾_A⁽_x~b⁾_n⁰_~m^;!p_A⁽_a~b⁾_n~m (n n⁰)"

p_A⁽_a~b⁾⁰_~m:::p_A⁽_a~b⁾_n~m^;!p⁽⁸_xa⁾_A⁽_x~b⁾_n~m: (5) Def is dened in the same way.

We also consider the variant ⁰_d⁰_d of the hierarchy dd of Boolean formulae (see Section 2.2) by allowing`i¹:::i^d in (1), (2) to have the formpq, where^{2f^_g}, andpq are propositional variables from the corresponding alphabets. Let Fd⁰ be the variant of the proof systemFd 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 ^`9~x~t(~a)(A(~a~x)^{^}B(~a~x))

where AB ^{2 10b} 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^0;2F or EF determined by the middle column from the set of axioms

DefDef^n;!p%_A⁽_~a~b⁾_~n~m %q_B⁽_~a~b⁾_~n~m~m~t(~n)^o: (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) timeF-proofs

Def ^{`h</sup>A(~a~b)<sup>i</sup>~n~m p<sub>A</sub><sup>(</sup><sub>~a~b</sub><sup>)</sup><sub>~n~m</sub> and Def <sup>`h}B(~a~b)ⁱ~n~m q_B⁽_~a~b⁾_~n~m:

14

Using these, we constructF-proofs of the formulae^h:(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 theoryT, of the formula^h9~x ~t(~a)(A(~a~x)^{^}B(~a~x))ⁱ~n, and apply a sequence of cuts to derive the empty sequent.

Assume now thatT is a rst-order theory from the rst 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

SIEi^#. Now, the theories^SIEi and ^SIEi^# dier only in the underlying language, and the rest of the proof is absolutely identically for them. So, we consider only the case of ^SIEi. Every ^SEj-formula (j 1) is equivalent to a formula in the prenex normal form and it is easily seen to be further equivalent in ^SIE⁰ to a formula of the form

9~x⁽¹⁾~t⁽¹⁾(~a)⁸~x⁽²⁾~t⁽²⁾(~a):::Q~x^(j)(~a)~t^(j)(~a)

C(~a~x⁽¹⁾:::~x^(j))D(~a~x⁽¹⁾:::~x^(j))

9

>

>

>

>

=

>

>

>

>

(7) where ^{2f^_g}. Denote by ^SE_j⁰ the class of formulae having the form (7), and let ^SU_j⁰ be the dual class. For C ^2SEj⁰ C ^{2 S}Uj⁰] we denote by %C the dual formula in C ^{2 S}Uj⁰

C ^{2 S}Ej⁰, respectively] logically equivalent to (^:C). Note that for C(~a) ^{2 S}Ui^0;2 and every tuple~n, the propositional formula^fC(~a)^g_~n is in ⁰_i^;2.

ForC(~a)^2SEi^0;1nSUi^0;2"C(~a) = (⁹~x~t(~a))D(~a~x), where D(~a~b) is in^SUi^0;2, denote by ;C⁽~a⁾~n the cedent consisting of the formulaeⁿD(~a~b)^o_~n~m (~m~t(~n)). If C(~a)^2SUi^0;2, we let ;C⁽~a⁾~n consist of the single formula^fC(~a)^g_~n.

For C(~a)^2SUi^0nSEi^0;1" C(~a) = (⁸~x~t(~a))D(~a~x), where D(~a~b) is in^SEi^0;1, denote by^GC⁽~a⁾~nthe collection of sequents^n;!;_D⁽_~a~b⁾_~n~m ~m~t(~n)^o. In the caseC(~a)^2SEi^0;1, we let^GC⁽~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) ^{2 S}Ui^0;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^0;2-proof of

nC(~a~b)^o_~n~t(~n^{) !}

nC(~a~t(~a))^o_~n ^from DefDef.

Statement 5.3.

Let C(~a)^2SEi^0;1.

a)

There exists a polynomial time algorithm which for any 1^~n and any formula L ²

;C⁽~a⁾~n produces an F_i^0;2-proof

DefDef^GC⁽~a⁾~n ^`L^;!: 15