Algebraic proof systems over formulas

Dima Grigoriev^{a} Edward A. Hirsch^{b,1}

aIRMAR, Université de Rennes, Campus de Beaulieu, 35042 Rennes, cedex

           France, http://www.maths.univ-rennes1.fr/∼dima.

bSteklov Institute of Mathematics at St.Petersburg, 27 Fontanka, 191023

        St.Petersburg, Russia, http://logic.pdmi.ras.ru/∼hirsch.

Abstract

We introduce two algebraic propositional proof systems F-N S and F-PC. The main difference of our systems from (customary) Nullstellensatz and Polynomial Calculus is that the polynomials are represented as arbitrary formulas (rather than sums of monomials). Short proofs of Tseitin’s tautologies in the constant-depth version of F-N S provide an exponential separation between this system and Polynomial Calculus.

We prove that F-N S (and hence F-PC) polynomially simulates Frege systems, and that the constant-depth version of F-PC over finite field polynomially simulates constant-depth Frege systems with modular counting. We also present a short constant-depth F-PC (in fact, F-N S) proof of the propositional pigeon-hole principle. Finally, we introduce several extensions of our systems and pose numerous open questions.

Key words: Algebraic propositional proof systems, Frege systems

Dedicated to Anatol Slissenko from whom we have learned a lot

1 Introduction

A (Cook–Reckhow) proof system [CR79] for a language L is a polynomial-time computable function mapping strings in some alphabet onto L. If there would be a proof system Π for a co-NP-hard language such that for every x ∈ L,

1 Supported by CRDF, NATO, and RAS Young Scientists Program (6th contestexpertise, 1999, grant No.1).

Preprint submitted to Elsevier Science 23 February 2004

the shortest proof π of x (i.e., the shortest string π such that Π(π) = x) had size polynomial in the size of x, then we would have NP = co-NP.

A proof system Π_{1} polynomially simulates a proof system Π_{2} iff there is a polynomial-time computable function f mapping every Π_{2} proof π to a Π_{1} proof of the same element of L, i.e., Π_{1}(f(π)) = Π_{2}(π).

A propositional proof system is a proof system for the co-NP-complete language TAUT of all Boolean tautologies. Since this language is in co-NP, any proof system for a co-NP-hard language L can be considered as a propositional proof system. However, note that one needs to fix a concrete reduction of TAUT to L before proving, e.g., that such a system does (not) polynomially simulate another propositional proof system.

Algebraic proof systems played a significant role in propositional proof complexity during the past decade. The two most popular systems are Nullstellensatz (N S) [BIK^{+}96] and Polynomial Calculus (PC) [CEI96]. These are proof systems for the co-NP-hard problem of unsolvability of a system of polynomial equations: We are given several polynomials over a field 𝔽 and asked whether these polynomials have no common roots in the algebraic closure of 𝔽. The polynomials are represented as sums of monomials cxy…z, where x, y, …, z are variables, and c is a constant (represented in binary).

To see that this problem is co-NP-hard, note that a Boolean formula Φ in CNF in n variables x_{1}, …, x_{n} can be easily translated into polynomials F_{1}, …, F_{k} such that the polynomials

F_{1}, …, F_{k}, x_{1}^{2} − x_{1}, …, x_{n}^{2} − x_{n}

have no common roots iff Φ is unsatisfiable. Namely, let x_{j_{1}}, …, x_{j_{m}} be the variables occuring in the i-th clause C_{i} of Φ. Then F_{i} = l_{1}…l_{m} where l_{t} = x_{j_{t}} if x_{j_{t}} occurs positively in C_{i} and l_{t} = (1 − x_{j_{t}}) otherwise.

In PC, one starts with a system of polynomial equations (i.e., with a set of polynomials treated as axioms) and derives new polynomials using two rules

\frac{P_{1}; P_{2}}{P_{1} + P_{2}}  and  \frac{P}{P · Q}.

I.e., one can take a sum^{2} of two already derived polynomials P_{1} and P_{2}, or multiply an already derived polynomial P by an arbitrary polynomial Q. The goal is to derive the polynomial 1, because this proves that Φ is unsatisfiable.

2 Usually, an arbitrary linear combination is allowed, but clearly it can be replaced by two multiplications and one addition.

In N S, a proof of {F_{1}, …, F_{m}} is a set of polynomials {G_{1}, …, G_{m}} such that ∑_{i} F_{i}G_{i} = 1. Any such proof can be translated into PC in a natural way. However, the translation in the opposite direction is not possible: there is a sequence of tautologies having polynomial-size PC proofs but no polynomialsize N S proofs [CEI96]. In fact, N S is equivalent to the tree-like version of PC [BIK^{+}97].

It is known that both PC and N S are sound and complete, but they are not polynomially bounded. Namely, one can prove a linear lower bound on the maximum degree of intermediate polynomials (this is done in [Raz98] for axiom polynomials of logarithmic degree, and in [BGIP01] for axiom polynomials of constant degree; see also [AR01]). Then by [IPS99, Theorem 6.2] one obtains an exponential lower bound on the total number of monomials in the proof.

Pitassi [Pit97] considered a variant of PC where polynomials are represented as formulas (i.e., terms) and not as sums of monomials. The resulting system is still sound and complete, however, it is not a Cook–Reckhow proof system because no polynomial-time deterministic procedure is known that could decide whether an inference rule is applied in a right way. (Note: if we take a sum of two polynomials P and Q in this system, we get not just the term (P + Q)—the system would be incomplete in this way—but we can get an arbitrary term representing the same polynomial).

In this paper, we augment this system by primitive rules that help to demonstrate that two terms represent the same polynomial: associativity, commutativity, distributivity, etc. (See Subsection 2.1). These rules basically mean that we work in a commutative ring; throughout this paper we call them the primitive rules. We also require the next formula to be derived using either the primitive rules or as a formal combination (P_{1} + P_{2}) (resp., (P · Q)) of two already derived polynomials P_{1} and P_{2} (resp., of an already derived polynomial P and an arbitrary polynomial Q). Therefore, we replace every “hard” step like

\frac{(x + y) · (x − y)}{x^{2} − y^{2}}

by a sequence of “primitive” (polynomial-time verifiable) steps like

\frac{\frac{\frac{(x + y) · (x − y)}{x · (x − y) + y · (x − y)}}{\frac{(x − y) · x + (x − y) · y}{x^{2} − yx + xy − y^{2}}}}{\frac{\frac{x^{2} − xy + xy − y^{2}}{x^{2} + (−1 + 1)xy − y^{2}}}{\frac{x^{2} + 0 − y^{2}}{x^{2} − y^{2}} .}}

Although it may be still hard to derive a different term representing an already derived polynomial, we can show that the power of the new calculus is sufficient to polynomially simulate Frege systems. Namely, every proof in a Frege system can be translated into a proof in our new system (which we call F-PC) with at most polynomial increase in size (see Section 3).

In Section 4 we show that the tree-like version of F-PC is polynomially equivalent to F-N S, an analog of N S in which G_{i}’s may be represented as arbitrary formulas and the equality ∑_{i} F_{i}G_{i} = 1 must be proved using the primitive rules only (this system is defined in Subsection 2.2). It is known that Frege systems do not lose their power even if restricted to tree-like proofs (see, e.g., [Kra95]). Since our polynomial simulation of Frege systems by F-PC converts tree-like proofs into tree-like ones, it follows that F-N S polynomially simulates Frege systems.

We then consider the constant-depth version of F-PC (i.e., the depth of every formula in the proof is bounded by a constant, see Subsection 2.3 for definitions, cf. [GR00] where lower bounds for depth-3 arithmetic formulas were established) and restrict our attention to finite fields. It turns out (see Section 5) that this system polynomially simulates constant-depth Frege systems with modular gates. We follow [Kra95] in the definition of the latter system. This system has already been considered in [BIK^{+}97] in connection to N S with a constant number of levels of extension axioms.

We introduce also two extensions of F-PC: one extension based on Positivstellensatz (see Subsection 2.4) and another one allowing to deduce a polynomial when some its power is deduced (see Subsection 2.5). We illustrate a possible application of this “radical rule” by employing the trick of Rabinowitsch [vdW31, Part 2, Chapter 11] to transform a derivation of 1 from a set {1 − zF, F_{1}, …, F_{m}} into a derivation of F from the set {F_{1}, …, F_{m}}.

In Section 6 we present a short F-PC proof (over ℚ) of the propositional pigeon-hole principle (PHP) as well as for the subset sum problem. There is nothing surprising in the existence of polynomial-size F-PC proofs of PHP, because PHP has polynomial-size Frege proofs [Bus87] and F-PC polynomially simulates Frege systems. However, Buss’ proof [Bus87] involves a complicated construction of addition circuits while our proof is very simple and intuitive (actually, we employ the ability of F-PC to count). Our proof also has depth bounded by a constant, while constant-depth Frege systems do not have polynomial-size proofs of PHP [KPW95,PBI93]. In fact, our proof can be conducted in constant-depth F-N S.

The results of Section 6, however, do not suffice to prove an exponential gap between the lengths of proofs in PC and F-PC as propositional proof systems (see the discussion in the end of Section 6). In Section 7 we demonstrate this gap for Tseitin’s tautologies. In fact, we demonstrate the gap between PC and constant-depth F-N S, the weakest system among the ones introduced in this paper.

After this paper has been published, we realized that, in the case of finite fields, a system similar to our system F-PC was briefly considered in [BIK^{+}97] (it was called equational logic there) and Theorem 8 was formulated.

2 The systems F-PC and F-N S and their extensions

In this section we introduce the two systems we study in this paper, and discuss several extensions of these systems.

2.1 F-PC

The objects of our system F-PC are algebraic formulas. Formally, algebraic formulas are the members of the smallest set satisfying the following conditions:

(1) Constants (denoted by 1, −1, 0, etc.) are formulas.

(2) Variables are formulas.

(3) If P and Q are formulas, then the terms (P +Q) and (P ·Q) are formulas.

Constants and variables range over ℚ or over any finite field ℤ_{p}. Sometimes when speaking about algebraic formulas we will refer to them as polynomials.

Similarly to PC, the two basic rules are

\frac{P_{1}; P_{2}}{(P_{1} + P_{2})}  and  \frac{P}{(P · Q)}.  (2.1)

Note that (P_{1} + P_{2}) and (P · Q) here are terms (i.e., formal combinations): no actual addition or multiplication is done. Since these rules are able to produce only larger formulas, to derive the formula 1 (which is our goal) we need also some (invertible) simplification rules (called the primitive rules throughout this paper) yielding associativity, commutativity, distributivity, etc. We allow to apply the primitive rules (but not (2.1)!) to any subterms of the derived formulas, for example, the first rule below can be applied as

\frac{(A + ((P + Q) + R))}{(A + (P + (Q + R)))}. Here is the list of these rules:

\frac{((P + Q) + R)}{(P + (Q + R))},  \frac{(P + (Q + R))}{((P + Q) + R)},  (2.2)

\frac{((P · Q) · R)}{(P · (Q · R))},  \frac{(P · (Q · R))}{((P · Q) · R)},  (2.3)

\frac{(P + Q)}{(Q + P)},  \frac{(P · Q)}{(Q · P)},  (2.4)

\frac{((P + Q) · R)}{((P · R) + (Q · R))},  \frac{((P · R) + (Q · R))}{((P + Q) · R)},  (2.5)

\frac{(P · 1)}{P},  \frac{P}{(P · 1)},  (2.6)

\frac{(P · 0)}{0},  \frac{0}{(P · 0)}.  (2.7)

We also allow to replace a subterm P containing only constants by its value c_{P} (for example, (−1 + 1) simplifies to 0) and vice versa:

\frac{P}{c_{P}} ,  \frac{c_{P}}{P} .  (2.8)

An F-PC proof of a set {F_{1}, …, F_{m}} of algebraic formulas is the derivation of the formula 1 from the axioms F_{1}, …, F_{m} using the rules (2.1)–(2.8).

Remark 1 We could write “an F-PC refutation”, but write “ proof” to emphasize that F-PC is a Cook–Reckhow proof system. To reach a compromise between English and mathematics, the best way is to say that what we consider is a proof of the fact that {F_{1}, …, F_{m}} have no common roots.

As we already mentioned, to consider F-PC as a propositional proof system, we have to fix a reduction of TAUT to the language of all sets of algebraic formulas having no common roots. We could make this reduction from the reduction of formulas in CNF to sets of polynomials described in Section 1. However, the following (still standard) reduction is more natural.

There is still one variable for every Boolean variable (informally, true corresponds to 0, and false corresponds to 1). Our set of algebraic formulas will contain the formula x^{2} −x for each variable x occurring in the input tautology Θ and one additional formula φ(¬Θ) (cf. several polynomials in the reduction described in Section 1). We define φ inductively: φ(¬Φ) = (1 − φ(Φ)), and φ(Φ ⊃ Ψ) = (1 − φ(Φ)) · φ(Ψ) for Boolean formulas Φ and Ψ (one can easily extend φ to other logical connectives). We will refer to the algebraic formulas from the image of φ as Boolean polynomials (we will later show that for any of them we can derive P^{2} − P). Sometimes we will also call Boolean any other polynomial P for which we can derive P^{2} − P.

Remark 2 Any “refutation proof” of a Boolean polynomial φ(Φ) (i.e., the derivation of 1 from φ(¬Φ)) can be transformed into a “proper proof” of φ(Φ) (i.e., the derivation of φ(Φ) from the axioms x_{i}^{2} − x_{i}) by multiplying every line in the derivation by 1−φ(Φ). Note that the axiom φ(¬Φ) transforms into φ(Φ)(1 − φ(Φ)).

In what follows, we use −P instead of −1·P, use other common mathematical notation, and omit straightforward calculations, for example,

\frac{\frac{\frac{−P + P}{−P + 1 · P}}{\frac{(−1 + 1) · P}{0 · P}}}{0} .

Note that in F-PC we can (and will in this paper):

(1) Derive something from zero polynomial, because zero polynomial is trivially derivable from any other polynomial.

(2) Omit some of the brackets and ignore the order of operands, because associativity and commutativity make it easy to derive similar formulas from each other.

(3) Treat a polynomial F − G as an equality F = G and substitute G for an occurrence of F in any formula R containing F. This can be performed by extracting the multiplier M = M(R) of this occurrence (define M((P_{0} + P_{1})) = M(P_{i}) and M((P_{0} · P_{1})) = P_{1−i} · M(P_{i}), where P_{i} is the part of the formula (P_{0} + P_{1}) or (P_{0} · P_{1}) containing this occurrence of F; M(P) = 0 if P does not contain this occurrence; M(F) = 1 where F refers to the occurrence we mean), adding (G − F) · M to R and repeated carrying G − F in brackets. In particular, we can substitute x for x^{2} for any variable x.

(4) Multiply equalities F_{1} = G_{1} and F_{2} = G_{2}: Multiply F_{1} − G_{1} by F_{2} and F_{2} − G_{2} by G_{1}; the sum of the obtained polynomials is F_{1}F_{2} − G_{1}G_{2}, i.e., the equality F_{1}F_{2} = G_{1}G_{2}.

(5) Verify in the following simple way that F is derivable from G: open (some of the) brackets in both F and G, make appropriate substitutions using already derived equalities, group similar summands and compare the results. Clearly, one should care about the size of the proof obtained by opening the brackets.

2.2 F-N S

An F-N S proof of a set {F_{1}, …, F_{m}} of algebraic formulas consists of two parts:

(1) A multiset {G_{1}, …, G_{m}} of algebraic formulas.

(2) An F-PC derivation of 1 from the algebraic formula

∑_{i=1}^{m} F_{i}G_{i}

without the use of the two main rules (2.1) (i.e., we use only the primitive rules).

2.3 Constant-depth F-PC and F-N S

When we refer to constant-depth version of either F-PC or F-N S, we mean that the (initial and intermediate) polynomials are represented as formulas (terms) of depth bounded by a constant while the multiplication and the addition have arbitrary arity (i.e., we omit unnecessary brackets). The primitive rules must be modified accordingly.

The slight discrepancy with a trivial definition is motivated by the analogy between constant-depth F-PC and constant-depth Frege systems. Depth-k F-PC and F-N S are Cook–Reckhow proof systems for the language of all insolvable systems of depth-(k − 1) algebraic formulas (we consider k ≥ 3 to capture, at least, sums of monomials and their formal products). We need to decrease here the depth by one to make the system complete (the primitive rules can turn every depth-(k − 1) formula into a sum of monomials using intermediate formulas of depth at most k).

Since constant-depth Boolean formulas are usually considered in the basis of ¬ and unbounded-arity ∨ (and sometimes ∧ which is a shorthand: ⋀_{i} x_{i} = ¬ ⋁_{i} ¬x_{i}), we slightly modify the translation φ of Boolean formulas into algebraic formulas:

φ ( ⋁_{i=1}^{m} Φ_{i}) = ∏_{i=1}^{m} φ(Φ_{i}).

To get a propositional proof system, we must combine this reduction with a transformation of unbounded-depth Boolean formulas into constant-depth ones. Since we consider this system only in connection to constant-depth Frege systems (with modular counting), we do not need to fix this transformation.

Note that, formally, our reduction to systems of depth-(k − 1) algebraic formulas works well only for k ≥ 7, because otherwise we are unable to translate even a formula in 3-CNF (in fact, we still get a complete proof system for a co-NP-hard problem, but the reduction must be further modified).

2.4 F-PC> and F-N S>

Similarly to Positivstellensatz and Positivstellensatz Calculus [GV01] we define new systems F-N S> and F-PC>. An F-N S> proof of a set {F_{1}, …, F_{m}} of algebraic formulas consists of two parts:

(1) Two multisets {G_{1}, …, G_{m}} and {H_{1}, …, H_{l}} of algebraic formulas.

(2) An F-PC derivation of 1 from the algebraic formula

∑_{i=1}^{m} F_{i}G_{i} − ∑_{i=1}^{l} H_{i}^{2}

without the use of the two main rules (2.1) (i.e., we use only the primitive rules).

Similarly, an F-PC> proof of {F_{1}, …, F_{m}} is an F-PC derivation of a certain

algebraic formula of the form 1 + ∑_{i=1}^{l} H_{i}^{2} from the formulae F_{1}, …, F_{m}.

Alternatively, one can build algebraic formulas based versions of LS^{n} calculi [GHP01] where one translates Boolean formulas into inequalities P ≥ 0 instead of polynomials P. (These calculi are generalizations of Lovász-Schrijver calculi [LS91,Lov94].) For example, a Boolean formula Φ can be translated into the inequality −φ(Φ) ≥ 0 for the same φ as in Subsection 2.1; of course, x^{2}−x ≥ 0 and x − x^{2} ≥ 0 for each variable x must be added. The primitive rules (2.2)– (2.8) still can be applied to any subterm of an inequality. The rules for working with inequalities can be, e.g.,

\frac{P_{1} ≥ 0; P_{2} ≥ 0}{(P_{1} + P_{2}) ≥ 0} and \frac{P_{1} ≥ 0; P_{2} ≥ 0}{(P_{1} · P_{2}) ≥ 0}.

One can also introduce an axiom scheme Q^{2} ≥ 0 allowing to introduce the square of any algebraic formula Q. (This particular set of rules and axioms corresponds to the system LS_{∗}^{n} [GHP01].) The goal is to derive the inequality −1 ≥ 0.

We mention also that another complete system for deducing polynomial inequalities was considered in [LMR96], the main difference of the latter system is allowing to introduce auxiliary variables.

2.5 F-PC√

The (radical) system F-PC√ is the system F-PC extended by the rule

\frac{P^{2}}{P} .

One can also define the system PC√ similarly, and the system F-N S√ by including the radical rule in the list of primitive rules. Note that this rule is in accordance with Nullstellensatz [vdW31] since P vanishes on the variety given by the equalities F_{1} = … = F_{m} = 0 if and only if a certain power P^{d} belongs to the ideal generated by F_{1}, …, F_{m}. Although this rule looks redundant because every Boolean (i.e., comprising polynomials x_{i}^{2} − x_{i} for 1 ≤ i ≤ n) ideal is radical, this rule apparently could accelerate proofs in some cases.

Consider, for example, the following issue. We have defined an F-PC (resp., F-N S, PC, etc.) proof of Φ as a derivation of 1 from the set S = {φ(¬Φ), x_{1}^{2} − x_{1}, …, x_{n}^{2} − x_{n}}. Frequently, such a derivation is called “refutation” instead of “proof”. There is another possibility to prove that Φ is a tautology: let us call a “proper proof” a derivation of φ(Φ) from {x_{1}^{2} − x_{1}, …, x_{n}^{2} − x_{n}}. Formally, “refutations” and “proper proofs” give different propositional proof systems. (Note that in customary PC and N S using “proper proofs” instead of “refutations” needs updating the translation of formulas into polynomials since we defined it only for CNFs; for many Boolean formulas Φ, this results in exponentially large polynomials).

Trivially, any proof in a “proper proof” system can be transformed (with a negligible increase in size) into a proof in a “refutation” system. Can we do it in the reverse direction? For Boolean polynomial F = φ(Φ), the answer is “yes” in both F-PC (see Remark 2) and PC (because F^{2} − F is an element of the ideal generated by x_{i}^{2} − x_{i}, i.e., ∑ H_{i}(x_{i}^{2} − x_{i})). However, for non-Boolean F this may not work. Although it is impossible to transform a “refutation” of (1 − F) into a “proper proof” of F, we now show how to transform a “refutation” of (1 − zF) (where z is a new variable) into a “proper proof” of F, using the radical rule. For this, we apply “the trick of Rabinowitsch” [vdW31, Part 2, Chapter 11].

A “proper proof” of F in N S√ is a “proper proof” of F in N S followed by several applications of the radical rule to ∑_{i} F_{i}G_{i}. Consider an N S√ “refutation” (this is the same as N S “refutation”) (1 − zF)G + ∑_{i} F_{i}G_{i} = 1. Formally substituting the rational function 1/F for the variable z (observe that G and G_{0} could contain z) in the latter equality and cleaning the denominator, we get F^{d} = ∑_{i} F_{i}G′_{i} since the first term in the N S√ -refutation in question vanishes after the performed substitution; moreover, d ≤ max_{i} deg(G_{i}), deg(G′_{j}) ≤ deg(F^{d}) + max_{i} deg(G_{i}) ≤ (deg(F) + 1) · max_{i} deg(G_{i}). Now applying several times the radical rule this provides an N S√ derivation of F from {F_{1}, …, F_{m}} of degree growing at most polynomially in the degree of a N S√ derivation of 1 from {1 − zF, F_{1}, …, F_{m}}

To get a “proper proof” of F in PC√ from a “refutation” of (1−zF) in PC√, we verify by induction along the proof that for each its line ∑ F_{i}G_{i}, one can derive a polynomial F^{d_{z}+1} ∑ F_{i}G_{i}|_{z=1/F} by few applications of the rules of PC√, where d_{z} is the maximum degree of z in the intermediate polynomials

of the “refutation” (including the polynomials Q used in the \frac{P}{P · Q} rule).

Suppose that ∑ F_{i}G_{i} is obtained as the sum of two already derived polynomials ∑ F_{i}G_{1i} and ∑ F_{i}G_{2i}. By induction one can derive F^{d_{z}+1} ∑ F_{i}G_{1i}|_{z=1/F} + F^{d_{z}+1} ∑ F_{i}G_{2i}|_{z=1/F}. Clearly, this gives F^{d_{z}+1} ∑ F_{i}G_{i}|_{z=1/F}. If ∑ F_{i}G_{i} is obtained as the product of an already derived polynomial ∑ F_{i}G_{i1} and a polynomial Q, by induction we can derive F^{2d_{z}+1} ∑ F_{i}G_{i} (we multiply by F^{d_{z}}Q|_{z=1/F} instead of Q). Multiplying by F ∑ F_{i}G_{i} and using the radical rule, one gets F^{d_{z}+1} ∑ F_{i}G_{i}. Finally, we get “a proper PC√ proof” of F^{d_{z}+1}. Then the multiplication by F^{c} (where c+d_{z}+1 is the nearest power of two) and the repeated application of the radical rule allows one to derive F itself.

The same arguments can be conducted for F-N S√. We leave the corresponding question for F-PC√ open. (Note that in the cases of F-N S and F-PC degree bounds do not suffice for obtaining bounds on the size of derivation.)

3 F-PC simulates Frege systems

In this section it does not matter whether we consider F-PC over ℚ or over ℤ_{p}: we use only the existence of the constants 0, 1 and −1.

Theorem 3 The system F-PC polynomially simulates Frege systems.

PROOF. We consider Hilbert’s system: The axioms are

(A1) Γ ⊃ (Δ ⊃ Γ), (A2) (¬Δ ⊃ ¬Γ) ⊃ ((¬Δ ⊃ Γ) ⊃ Δ), (A3) (Γ ⊃ (Δ ⊃ Λ)) ⊃ ((Γ ⊃ Δ) ⊃ (Γ ⊃ Λ)).

The only rule of the inference is modus ponens: Γ and Γ ⊃ Δ imply Δ.

The main part of the proof is the following lemma.

Lemma 4 For any Boolean formula Φ, the shortest F-PC proof of the polynomial (φ(Φ))^{2} − φ(Φ) has size polynomial in size of Φ.

PROOF. We prove it by induction on the construction of Φ. Let G = φ(Γ), D = φ(Δ), and suppose that G^{2} − G and D^{2} − D have derivations of sizes γ ≤ c|Γ|^{2} and δ ≤ c|Δ|^{2} respectively (the constant c will be clear from what follows). Note that using the primitive rules we can easily derive R = (1−G)^{2} −(1−G) from G^{2} − G. Hence, in the case Φ = ¬Γ the polynomial (φ(Φ))^{2} − φ(Φ) has a derivation of size at most c|Φ|^{2} (if c is large enough). We now consider the case Φ = (Γ ⊃ Δ). By multiplying D^{2} −D by (1−G)^{2}, we obtain P = (1−G)^{2}D^{2} − (1 − G)^{2}D. On the other hand, we can derive Q = (1 − G)^{2}D − (1 − G)D by multiplying R by D. Summing P and Q, we derive ((1 − G)D)^{2} − (1 − G)D which is (φ(Φ))^{2} − φ(Φ). The size of this proof (from G^{2} − G and D^{2} − D) is upper bounded by d|Φ| for some constant d, i.e., the size of the proof from axioms is at most d|Φ| + c|Γ|^{2} + c|Δ|^{2} = c(|Γ| + |Δ|)^{2} + d|Φ| − 2c|Γ||Δ|. Now, choose c ≥ 2d; then the size of our proof is at most c|Φ|^{2}. □

We now show that φ translates axioms into polynomials having F-PC derivations of size polynomial in |Γ|, |Δ| and |Λ|.

(A1) Let G = φ(Γ), D = φ(Δ). Since we can derive G^{2} − G, by commutativity and distributivity we have (1 − G)G. Then we multiply it by (1 − D) and by commutativity and associativity we obtain (1 − G)((1 − D)G) = φ(Γ ⊃ (Δ ⊃ Γ)).

(A2) Here, we need to derive (1−D(1−G))·((1−DG)D) up to simplifications. Opening the brackets gives (D − D^{2}) + (GD^{2} − D^{2}G) + (D^{3}G − G^{2}D^{3}); it now remains to derive this formula. The first two summands can be easily derived from D^{2} − D and from the axioms, respectively. The third summand is G^{2} − G multiplied by −D^{3}.

(A3) Here, we need to derive (1−(1−G)((1−D)L))·((1−(1−G)D)((1−G)L)), where L = φ(Λ). This formula is equal to

(G^{3}L^{2} − 3G^{2}L^{2} + 3GL^{2} − L^{2})(D^{2} − D)
+(G^{2}D − 2GD + G + D − 1)(L^{2} − L) − L^{2}(G^{2} − G)

(it can be verified by opening all brackets), which is a sum of G^{2} − G, D^{2} − D and L^{2} − L multiplied by appropriate polynomials.

It is clear that modus ponens can be proved using size linear in the sizes of the formulas Γ and Γ ⊃ Δ: having φ(Γ) = G and φ(Γ ⊃ Δ) = (1 − G)D, we can multiply G by D, add the result to (1 − G)D, and after simplifications we have D, i.e., φ(Δ). Therefore, we can indeed transform the proof of a Boolean formula Θ in Hilbert’s system into a derivation of φ(Θ) in F-PC from the polynomials x_{i}^{2} − x_{i} with only a polynomial increase in size (moreover, the only point where non-linear increase can occur is the translation of the axioms of Hilbert’s system). Summing φ(Θ) with the axiom φ(¬Θ), we get 1. □

Remark 5 Note that Frege systems polynomially simulate F-PC over ℤ_{2}. However, we do not know whether it holds over any other field.

4 F-N S is just tree-like F-PC

How much of the power of F-PC is taken away by replacing it with F-N S? Although we do not know whether F-N S can polynomially simulate F-PC, in this section we show that F-N S still can polynomially simulate Frege systems. Namely, we show that F-N S can polynomially simulate tree-like F-PC (“treelike” means that every derived polynomial is used only once; if we need it again, we must derive it once more), cf. [BIK^{+}97] which proves that N S polynomially simulates tree-like PC over ℤ_{p}. The claim now follows since treelike Frege systems have the same power as usual (DAG-like) ones (see, e.g., [Kra95]), and the proof of Theorem 3 translates tree-like Frege proofs into tree-like F-PC proofs.

Clearly, tree-like F-PC simulates F-N S, cf. the fact that tree-like PC simulates N S [BIK^{+}97]. Therefore, the following theorem establishes the equivalence between tree-like F-PC and F-N S.

Theorem 6 F-N S polynomially simulates tree-like F-PC.

PROOF. We first show that a tree-like F-PC proof can be transformed (with at most polynomial increase in size) into two derivations:

(1) A derivation π_{T} of some formula T from the axioms using no primitive rules.

(2) A derivation π_{T,1} of 1 from T using only primitive rules.

We transform it inductively; at each intermediate step of our induction we will have two derivations: a “normal” derivation π_{U} of some formula U from the axioms, and a derivation π_{U,1} of 1 from U using only the primitive rules.

We move the applications of the primitive rules from the first derivation to the second derivation one by one. Consider the last application of a primitive rule in π_{U}. Let S be a subformula to which this rule is applied. Note that if we omit this application, S will remain as a whole till the end of the proof, and this will be the only difference between the old final formula U of the proof and the new final formula U′. Let us apply the same rule to U′; we then obtain U and therefore have a derivation π_{U′,1} deriving 1 from U′. Observe that every step of this induction increases the proof size at most by the square of the size of the original proof.

Note that π_{T} is just the syntactic tree of the term T. We define the coefficients G_{i} of our F-N S proof ∑_{i=1}^{m} F_{i}G_{i} (see Subsection 2.2 above) inductively. The argument of M_{i}(·) is a subtree of π_{T}. For the axioms F_{i}, the formula M_{i}(F_{i}) is defined to be 1 if i = j, and 0 otherwise. If the root R of a subtree π_{R} is derived as the sum of two formulas P and Q, we define M_{i}(π_{R}) = (M_{i}(π_{P}) + M_{i}(π_{Q})), where π_{P} and π_{Q} are the subtrees corresponding to the proofs of P and Q respectively. If the root of π_{R} is derived as (P · Q), where P is an already derived formula, then M_{i}(π_{R}) = (M_{i}(π_{P}) · Q). Finally, we let the coefficient G_{i} be M_{i}(π_{T}).

Clearly, the size of every G_{i} is less or equal to the size of T. We must now present the proof of 1 from ∑_{i=1}^{m} F_{i}G_{i} using only the primitive rules.

If suffices to show that there is a derivation (of size polynomial in the size of T) of T from this sum using only the primitive rules. The proof is by induction on the construction of M_{i}’s. Suppose that we have derived the term T in which some subterms R_{j} are replaced by

(∑_{i=1}^{m} F_{i}M_{i}(π_{R_{j}})) . (4.1)

Then we rearrange one of such sums ∑_{i} F_{i}M_{i}(π_{R}). If M_{i}(π_{R})’s were obtained as (M_{i}(π_{P})·Q), we transform sum (4.1) into ((∑_{i} F_{i}M_{i}(π_{P}))·Q). If M_{i}(π_{R})’s were obtained as (M_{i}(π_{P})+M_{i}(π_{Q})), then we transform (4.1) into ((∑_{i} F_{i}M_{i}(π_{P}))+ (∑_{j} F_{j}M_{j}(π_{Q}))). If the argument of M_{i}’s is an axiom F_{j}, then we simplify (4.1) to F_{j}. □

Corollary 7 F-N S polynomially simulates Frege systems.

PROOF. Note that tree-like Frege systems polynomially simulate Frege systems [Kra95], and the proof of Theorem 3 translates tree-like Frege proofs into tree-like F-PC proofs. □

5 Constant-depth F-PC over ℤ_{p} simulates constant-depth Frege systems with MOD_{p} gates

In this section we show that constant-depth F-PC over ℤ_{p} polynomially simulates constant-depth Frege systems with MOD_{p} gates. (The depth of algebraic formulas may be bounded by a different constant than the depth of Boolean formulas).

We switch to the basis of ¬ and unbounded-arity ∨ (and sometimes ∧ which is a shorthand: ⋀_{i} x_{i} = ¬ ⋁_{i} ¬x_{i}) for this section (cf. Subsection 2.3). Note that the axioms of Hilbert’s system translate into the same polynomials in φ(Γ), φ(Δ), φ(Λ) as before, and so does modus ponens. It is easy to see that despite we modified φ for the constant-depth version of F-PC, still it translates Boolean formulas into Boolean polynomials, i.e., the analog of Lemma 4 still holds. We summarize that the proof of Theorem 3 still works for constantdepth Boolean formulas, and transforms constant-depth Frege proofs into constant-depth F-PC proofs.

A Frege system with MOD_{p} gates (see, e.g., [Kra95]) includes propositional connectives MOD_{p,i} of unbounded arity (0 ≤ i ≤ p − 1). Informally, MOD_{p,i}(x_{1}, …, x_{k}) means that the number of x_{i}’s having the value true equals i modulo p. We add the axiom schemes

MOD_{p,0}(∅)

and

¬MOD_{p,i}(∅)

for each i = 1, …, p−1. For each nonnegative integer k, we add also the axiom schemes

MOD_{p,i}(Φ_{1}, …, Φ_{k}, Φ_{k+1}) ≡
≡ ((MOD_{p,i}(Φ_{1}, …, Φ_{k}) ∧ ¬Φ_{k+1})
∨(MOD_{p, (i−1) mod p}(Φ_{1}, …, Φ_{k}) ∧ Φ_{k+1}).

(Here ≡ and ∧ are just shorthands). To translate formulas with MOD_{p} connectives into algebraic formulas over ℤ_{p} we extend φ to MOD_{p} gates by

φ(MOD_{p,i}(Φ_{1}, …, Φ_{k})) = (k − i − φ(Φ_{1}) − … − φ(Φ_{k}))^{p−1}.

To see that the obtained formula is Boolean, it is sufficient to prove A^{p} − A where A denotes k − i − φ(Φ_{1}) − … − φ(Φ_{k}) (then A^{2p−2} − A^{p−1} follows easily). Note that we can represent A as the sum of Boolean polynomials F_{1}, …, F_{k+((p−i) mod p)}, where F_{j} = 1 − φ(Φ_{j}) for 1 ≤ j ≤ k and F_{j} = 1 otherwise. When we open brackets in (∑_{j} F_{j})^{p} and group similar “monomials”, all summands except F_{j}^{p} cancel because p divides their coefficients. Since F_{j} are Boolean (by induction hypothesis), the claim follows, i.e., the analog of Lemma 4 holds even for constant-depth Boolean formulas with MOD_{p} gates. Namely, for such formula Φ, the algebraic formula (φ(Φ))^{2} − φ(Φ) has polynomial-size constant-depth F-PC proof over ℤ_{p}.

Theorem 8 Constant-depth F-PC over ℤ_{p} polynomially simulates constantdepth Frege systems with MOD_{p} gates.

PROOF. By the above discussion concerning the proofs of Lemma 4 and Theorem 3, it suffices to show that the axiom schemes for MOD_{p,i} connectives have short proofs in F-PC over ℤ_{p}.

The schemes for ∅ translate into trivial formulas involving no variables. The only non-trivial case is that of

1 − (1 − (1 − B)S) · (1 − (1 − S)B), (5.1)

where

B = (A + F)^{p−1},
S = (1 − (1 − A^{p−1})(1 − F))(1 − (1 − (A + 1)^{p−1})F),
A = k − i − φ(Φ_{1}) − … − φ(Φ_{k}),
and F = 1 − φ(Φ_{k+1}).

Note that (5.1) can be transformed into (B − S)^{2} (to verify, open all brackets and use B^{2} − B and S^{2} − S). Therefore, it suffices to prove B − S.

Using F^{2} − F the formula B can be transformed as follows:

(A + F)^{p−1} = A^{p−1} + F ∑_{j=0}^{p−2} \binom{p − 1}{j}A^{j} = A^{p−1} + F ((A + 1)^{p−1} − A^{p−1}).

On the other hand, opening the external brackets in S and using F^{2} − F gives

1 − (1 − A^{p−1})(1 − F) − (1 − (A + 1)^{p−1})F

= A^{p−1} + F ((A + 1)^{p−1} − A^{p−1}).

□

6 PHP

In this section we present a short proof of the propositional pigeon-hole principle in constant-depth F-PC over ℚ, moreover, this proof can be conducted in constant-depth F-N S.

PHP_{n} is usually formulated as

( ⋀_{i=1}^{n+1} ⋁_{k=1}^{n} p_{ik}) ⊃ ⋁_{k=1}^{n} ⋁_{1≤i<j≤n+1}(p_{ik} ∧ p_{jk}),

and its negation written in the basis {¬, ∨} is

¬(( ⋁_{i=1}^{n+1}¬ ⋁_{k=1}^{n} p_{ik}) ∨ ⋁_{k=1}^{n} ⋁_{1≤i<j≤n+1} ¬(¬p_{ik} ∨ ¬p_{jk})) .

We now give a short F-PC proof of the F-PC version of ¬PHP_{n}:

1 − ∏_{i=1}^{n+1}(1 − p_{i1}p_{i2}…p_{in}) · ∏_{1≤i<j≤n+1} ∏_{k=0}^{n}(1 − (1 − p_{ik})(1 − p_{jk}))  (6.1)

or, equivalently,

∀i, p_{i1}p_{i2}…p_{in}  (6.2)
∀i < j, ∀k, (1 − p_{ik})(1 − p_{jk}).  (6.3)

We start by (informally) switching to another set of variables

q_{ik} = (1 − p_{ik}) ∏_{1≤l<k} p_{il}.

In the real derivation, these variables are replaced by the corresponding formulas. We can easily prove

∀i, 1 − q_{i1} − q_{i2} − … − q_{in}  (6.4)
∀i, ∀j < i, ∀k, q_{ik}q_{jk}  (6.5)
∀i, ∀k, ∀l < k, q_{ik}q_{il}  (6.6)
∀i, k, q_{ik}^{2} − q_{ik}.  (6.7)

Indeed, all summands in (6.4) after opening brackets cancel except (6.2). Then, (6.5) is just (6.3) multiplied by ∏_{1≤l<k}(p_{il}p_{jl}). The formula (6.6) is a product containing p_{il}(1 − p_{il}). Finally, (6.7) follows from

q_{ik} = φ (¬p_{ik} ∨ ⋁_{1≤l<k} p_{il})

(see Lemma 4).

We sum (6.4) for all i’s and rearrange it as

(n + 1) − ∑_{k=1}^{n} x_{k}, (6.8)

where x_{k} = q_{1k} + … + q_{n+1,k}. Note that x_{k} is Boolean: open the brackets in

(q_{1k} + … + q_{n+1,k})^{2} − (q_{1k} + … + q_{n+1,k})

and use (6.5) and (6.7).

To derive 1 from (6.8) (which is an instance of the subset sum problem [IPS99]), we inductively derive the polynomial

S_{n}(S_{n} − 1)…(S_{n} − n), (6.9)

where S_{i} = x_{1} + x_{2} + … + x_{i}.

We start from S_{1}(S_{1} − 1) which is simply x_{1}^{2} − x_{1}. The induction step is to prove

S_{i}(S_{i} − 1)…(S_{i} − i) (6.10)

from

S_{i−1}(S_{i−1} − 1)…(S_{i−1} − (i − 1)). (6.11)

This derivation itself will be done inductively too. To stress the difference between the two induction arguments, we denote S_{i−1} by S and x_{i} by x. Multiply (6.11) by S + (i + 1)x − i. Opening brackets in the last two terms (S −(i−1))(S +(i+1)x−i) of the product, adding −i(x^{2} −x) and bracketing again, we get (S+ix−(i−1))(S+x−i) (to verify, open the brackets and notice that the difference is i(x^{2} − x)). We now turn our attention to the previous expression (S − (i − 2)) in brackets, open the brackets in (S − (i − 2))(S + (i − 1)x − (i − 2)) etc. Finally, we arrive at (6.10).

To derive 1 from (6.9), substitute in it n + 1 for S_{n} (use (6.8)) and multiply the result by 1/(n + 1)!.

Observe that this proof can be made tree-like and hence may be conducted in F-N S. On the other hand, observe that all the involved formulas in the proof are of depth bounded by a constant.

Remark 9 Note that the above version of PHP is given by polynomials of large degree (see (6.1)). On the other hand, in [Raz98] (see also [IPS99]) the injective PHP given by polynomials of degree at most two was studied. These are essentially the polynomials (6.4)–(6.7), where q_{ik} are treated as variables and not as shorthands for formulas. The paper [Raz98] establishes the lower bound Ω(n) on the degree of PC proofs of this set of polynomials. This implies an exponential lower bound [IPS99, Theorem 6.7] on the size of the shortest PC proof of this set of polynomials. Our short derivation of 1 from (6.4)–(6.7) demonstrates an exponential separation between PC and constant-depth F-PC (and also F-N S) as proof systems for the language of all insolvable systems of polynomial equations. However, it does not give a separation of these systems as propositional proof systems, because the formulation of PHP studied in [Raz98] may be not in the image of PC’s translation of Boolean formulas. The separation between propositional proof systems PC and constant-depth F-PC (and F-N S) is given in Section 7 by means of Tseitin’s tautologies.

By the same token, the subset sum problem provides the same separation result as the formulation of PHP from [Raz98] does, because [IPS99] gives an exponential lower bound on the size of the shortest PC proof of any instance of the subset sum problem, and we obtained a short constant-depth F-PC (and even F-N S) proof of its instance (6.8) (in the Boolean variables x_{i}).

7 Tseitin’s tautologies

In this section we show an exponential gap between lengths of proofs in PC and F-PC viewed as propositional proof systems. First, we show that Tseitin’s tautologies have short F-PC proofs while they have no PC proofs over any field of characteristic different from two. Afterwards, using the generalization of Tseitin’s tautologies given in [BGIP01], we show how to handle the remaining case; in fact, the generalization works for any field containing a p-th root of unity for some prime p. Our F-PC proof can be conducted even in constant-depth F-N S. This exhibits an exponential separation between the propositional proof systems PC and constant-depth F-N S over any field.

7.1 Fields of characteristic different from two

Let G = (V, E) by any undirected graph with an odd number of vertices and with expansion ε, i.e., for any subset S ⊆ V of cardinality at most |V |/2, the graph G has at least (1 + ε)|S| neighbors of S. For any number of vertices, there are such G’s of degree bounded by a constant c (see, e.g., [Alo86]).

Tseitin’s tautology for G is given by the Boolean formula

¬ ⋀_{v∈V} ⨁_{e∈E_{v}} x_{e} (7.1)

(where E_{v} is the set of edges incident to v) and its negation is the following formula in CNF:

⋀_{v∈V} ⋀_{i_{1},...,i_{deg(v)}∈{0,1},} ; i_{1}⊕...⊕i_{deg(v)}=0 ( ⋁_{k: i_{k}=0} x_{e(v,k)} ∨ ⋁_{l: i_{l}=1} ¬x_{e(v,l)}) ,  (7.2)

where e(v, i) denotes the i-th edge in E_{v}. There is one variable x_{e} for every edge e of G.

The PC translation of (7.2) is given by the polynomials

x_{e}^{2} − x_{e},  (7.3)
∏_{k: i_{k}=0} x_{e(v,k)} · ∏_{l: i_{l}=1}(1 − x_{e(v,l)})  (7.4)

where in (7.3) e ranges over E, in (7.4) v ranges over V and (i_{1}, …, i_{deg(v)}) ranges over {0, 1}^{deg(v)} and i_{1} ⊕ … ⊕ i_{deg(v)} = 0. (There are ∑_{v∈V} 2^{deg(v)−1} polynomials in (7.4), each of degree at most c).

In [BGIP01] a linear degree lower bound for another formulation of this problem is shown:

X_{e}^{2} − 1,  (7.5)
1 + ∏_{e∈E_{v}} X_{e},  (7.6)

where in (7.5) e ranges over E, and in (7.6) v ranges over V (note that there are no X_{e}^{2} − X_{e} polynomials). The following argument shows that this lower bound holds also for (7.3)–(7.4).

First, replace all occurrences of X_{e}’s in (7.5)–(7.6) by (2x_{e} − 1). We get

4(x_{e}^{2} − x_{e}),  (7.7)
1 + ∏_{e∈E_{v}}(2x_{e} − 1).  (7.8)

Note that any low degree PC proof of (7.3)–(7.4) can be easily extended to a low degree proof of (7.7)–(7.8): the polynomials (7.3) and (7.7) can be obtained from each other by multiplying by four, and, for a fixed v, (7.8) and the sum of (7.4) (for i_{1}, …, i_{deg(v)} ∈ {0, 1} such that i_{1} ⊕ … ⊕ i_{deg(v)} = 0) are two constant-degree polynomials that have the same values on {0, 1}^{|E_{v}|} and therefore differ by

∑_{e∈E_{v}}(G_{v,e}(x_{e}^{2} − x_{e})),

where G_{v,e} are some constant-degree polynomials.

Now consider any such low degree proof of (7.7)–(7.8) and replace in it all occurrences of x_{e}’s by (X_{e} + 1)/2. We obtain a low degree proof of (7.5)–(7.6). But such proofs do not exist [BGIP01]. Thus, our assumption that there is a low degree PC proof of (7.3)–(7.4) is false. Therefore, by [IPS99, Theorem 6.2] there are no polynomial-size proofs of Tseitin’s tautologies (7.2) in PC.

However, there are such proofs in F-PC. Consider the F-PC translation of (7.2). The system (7.3)–(7.4) can be obtained from it very easily. We already mentioned that we can derive (7.7)–(7.8) from it. Now change in these algebraic formulas all occurrences of x_{e}’s by (X_{e} + 1)/2, where X_{e} denotes the expression (\frac{1}{2} · (x_{e} + 1)). We arrive at (7.5)–(7.6).

Consider the polynomials (7.6) as equalities ∏_{e∈E_{v}} X_{e} = −1 and multiply them one by one, substituting 1 for X_{e}^{2}’s using (7.5) (cf. Subsection 2.1). Finally, we arrive at the equality 1 = (−1)^{|V |}, i.e., to the polynomial 2. It remains to divide it by two. One can verify that our F-PC proof can be conducted in constant-depth F-N S.

7.2 Fields of arbitrary characteristic

One could generalize this construction (see [BGIP01]) starting with a prime p and an expander G = (V, E) such that |V | ≡ 1 (mod p). Considering G as a directed (in arbitrary way) graph we assign to each its edge e a variable X_{e} which satisfy the following conditions. If ē is the edge with the orientation opposite to e, then we include the polynomial X_{e}Xē − 1 in the input system of polynomials. We also include the polynomials X_{e}^{p} − 1 (which replace (7.5)). Finally, for each vertex v we include the polynomial ∏ X_{e} − ω, where ω is a p-th root of unity (we assume that the ground field contain ω) and the product ranges over all the edges e emanating from v (this polynomial replaces (7.6)). The obtained system can be represented by a Boolean formula (cf. (7.1)) which we denote by Ψ_{p}.

Similarly to above, one could produce a constant-depth proof of Ψ_{p} in F-N S. On the other hand, a linear lower bound on the degree of the shortest PC proof of Ψ_{p} over any field of characteristic distinct from p is established in [BGIP01].

8 Further research

Since F-N S polynomially simulates Frege systems, proving lower bounds for it (and hence for F-PC) seems a hard problem. There is however a lot of apparently easier problems related to the constant-depth versions of F-PC and F-N S. For example, all we know about constant-depth F-PC over ℚ (resp., over ℤ_{p}) is that

• it polynomially simulates constant-depth Frege systems (resp., with MOD_{p} gates);

• it polynomially simulates PC over ℚ (resp., over ℤ_{p});

• it has polynomial-size proofs of PHP (over ℚ) and Tseitin’s tautologies.

What kind of Frege systems (without extension rules) could simulate constantdepth F-PC? We know even less about constant-depth F-N S. Does it simulate tree-like constant-depth F-PC? Finally, we do not know any lower bounds even for constant-depth F-N S over any field.

We have also introduced several extensions of F-PC. It would be interesting to clarify whether these extensions actually amplify F-PC. Observe that there is a degree two PC> (even N S>) proof of the subset sum problem with positive weights ∑ a_{i}x_{i} = m, where integers a_{i} > 0, m < 0 [Gri01]. Note that these integers are written in binary form. We ask whether there is a short proof of this problem in F-PC. Note that a linear lower bound Ω(n) on degrees of its PC proofs is shown in [IPS99]. This exhibits a gap between PC> and PC over ℚ (due to [IPS99, Theorem 6.2]).

Another extension of F-PC (considered in [Pit97]) emerges when one allows to replace an algebraic formula with arbitary algebraic formula representing the same polynomial without verification of their equivalence. Such verification of course could be done in BPP. As an example for which it is not clear how to verify quickly a formula in a deterministic way (say, using the primitive rules above, see Subsection 2.1, or some similar system of formula transformations) we can propose the Newton formula

∑_{j=0}^{k}(−1)^{j}σ_{j}τ_{k−j} = 0

where τ_{l} = ∑_{i=1}^{n} x_{i}^{l} and σ_{j} are elementary symmetric functions for which there are depth three formulas (over zero characteric fields) obtained from the Lagrange interpolation polynomial due to M. Ben-Or (see, e.g., [Shp01]).

Finally, we ask whether using other kinds of formulas can make F-PC or F-N S stronger, e.g., one may try using the exponentiation which would allow to use F^{d} for exponentially large d in a polynomial-size proof.

9 Acknowledgements

The second author would like to thank Boris Konev for useful discussions and V. P. Orevkov for providing multiple references.

References

[Alo86] N. Alon. Eigenvalues and expanders. Combinatorica, 6:83–96, 1986.

[AR01] M. Alekhnovich and A. A. Razborov. Lower bounds for polynomial calculus: Non-binomial case. In Proceedings of the 42nd Annual IEEE Symposium on Foundations of Computer Science, FOCS’01, pages 190– 199, 2001.

[BGIP01] S. Buss, D. Grigoriev, R. Impagliazzo, and T. Pitassi. Linear gaps between degrees for the polynomial calculus modulo distinct primes. Journal of Computing and System Sciences, 62:267–289, 2001.

[BIK^{+}96] P. Beame, R. Impagliazzo, J. Krajíček, T. Pitassi, and P. Pudlák. Lower bounds on Hilbert’s Nullstellensatz and propositional proofs. Proc. London Math. Soc., 73(3):1–26, 1996.

[BIK^{+}97] P. Beame, R. Impagliazzo, J. Krajíček, P. Pudlák, A. A. Razborov, and J. Sgall. Proof complexity in algebraic systems and bounded depth Frege systems with modular counting. Computational Complexity, 6(3):256–298, 1996/97.

[Bus87] S. Buss. Polynomial size proofs of the propositional pigeonhole principle. Journal of Symbolic Logic, 52:916–927, 1987.

[CEI96] M. Clegg, J. Edmonds, and R. Impagliazzo. Using the Groebner basis algorithm to find proofs of unsatisfiability. In Proceedings of the 28th Annual ACM Symposium on Theory of Computing, STOC’96, pages 174– 183, 1996.

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

[GHP01] Dima Grigoriev, Edward A. Hirsch, and Dmitrii V. Pasechnik. Complexity of semi-algebraic proofs. Technical Report 01-103, Electronic Colloquium on Computational Complexity, December 2001.

[GR00] D. Grigoriev and A. Razborov. Exponential lower bounds for depth 3 arithmetic circuits in algebras of functions over finite fields. Applicable Algebra in Engineering, Communication and Computing, 10(6):465–487, 2000.

[Gri01] D. Grigoriev. Complexity of Positivstellensatz proofs for the knapsack. Computational Complexity, 10:139–154, 2001.

[GV01] D. Grigoriev and N. Vorobjov. Complexity of Null- and Positivstellensatz proofs. Annals of Pure and Applied Logic, 113(1–3):153–160, 2001.

[IPS99] R. Impagliazzo, P. Pudlák, and J. Sgall. Lower bounds for the polynomial calculus. Computational Complexity, 8(2):127–144, 1999.

[KPW95] J. Krajíček, P. Pudlák, and A. Woods. Exponential lower bound to the size of bounded depth frege proofs of the pigeonhole principle. Random Structures and Algorithms, 7:15–39, 1995.

[Kra95] J. Krajíček. Bounded Arithmetic, Propositional Logic, and Complexity Theory, volume 60 of Encyclopedia of Mathematics and its Applications. Cambridge University Press, 1995.

[LMR96] H. Lombardi, N. Mnev, and M.-F. Roy. The Positivstellensatz and small deduction rules for systems of inequalities. Mathematische Nachrichten, 181:245–259, 1996.

[Lov94] L. Lovász. Stable sets and polynomials. Discrete Mathematics, 124:137– 153, 1994.

[LS91] L. Lovász and A. Schrijver. Cones of matrices and set-functions and 0–1 optimization. SIAM Journal on Optimization, 1:166–190, 1991.

[PBI93] T. Pitassi, P. Beame, and R. Impagliazzo. Exponential lower bounds for the pigeonhole principle. Computational Complexity, 3:97–140, 1993.

[Pit97] T. Pitassi. Algebraic propositional proof systems. In Neil Immerman and Phokion G. Kolaitis, editors, Descriptive Complexity and Finite Models, volume 31 of DIMACS Series in Discrete Mathematics and Theoretical Computer Science. American Mathematical Society, 1997.

[Raz98] A. A. Razborov. Lower bounds for the polynomial calculus. Computational Complexity, 7:291–324, 1998.

[Shp01] A. Shpilka. Affine projections of symmetric polynomials. In Proceedings of the 16th Annual IEEE Conference on Computational Complexity, pages 160–171, 2001.

[vdW31] B. L. van der Waerden. Moderne Algebra. Springer–Verlag, 1st edition, 1930/31.