BRICS RS-99-29 S. Riis: A Complexity Gap for Tree-Resolution BRICS

Basic Research in Computer Science

A Complexity Gap for Tree-Resolution

Søren Riis BRICS Report Series RS-99-29 ISSN 0909-0878 September 1999 Copyright \begin{matrix}c \\ ◯ \end{matrix} 1999, Søren Riis.

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 BRICS Report Series publications. 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@brics.dk

BRICS publications are in general accessible through the World Wide Web and anonymous FTP through these URLs:

http://www.brics.dk
ftp://ftp.brics.dk

This document in subdirectory RS/99/29/

A Complexity gap for tree-resolution

Søren Riis ^{∗}

September 1999

Abstract

It is shown that any sequence ψ_{n} of tautologies which expresses the validity of a fixed combinatorial principle either is “easy” i.e. has polynomial size tree-resolution proofs or is “difficult” i.e requires exponential size tree-resolution proofs. It is shown that the class of tautologies which are hard (for tree-resolution) is identical to the class of tautologies which are based on combinatorial principles which are violated for infinite sets. Actually it is shown that the gap-phenomena is valid for tautologies based on infinite mathematical theories (i.e. not just based on a single proposition).

We clarify the link between translating combinatorial principles (or more general statements from predicate logic) and the recent idea of using the symmetrical group to generate problems of propositional logic.

Finally, we show that is undecidable whether a sequence ψ_{n} (of the kind we consider) has polynomial size tree-resolution proofs or requires exponential size tree-resolution proofs. Also we show that the degree of the polynomial in the polynomial size (in case it exists) is non-recursive, but semi-decidable.

Keywords: Logical aspects of Complexity, Propositional proof complexity, Resolution proofs.

1 Outline

In this paper we introduce a new kind of result for propositional logic. It is shown for a large class of uniform families of unsatisfiability problems C_{1}, C_{2}, …, C_{j}, … that the family either has polynomial size tree-resolution refutations or requires full exponential size tree-resolution refutations. For non-uniform families (where, for example, each C_{j} might express a different combinatorial principle) there is no complexity gap and any super-polynomial but sub-exponential growth-rate can appear. Somewhat informally our main result states that if the sequence C_{j} express the same combinatorial principle for each j then there is a complexity gap for tree-resolution.

1Basic Research in Computer Science, Department of Computer Science, University of Aarhus, Ny Munkegade, Building 540, 8000 Aarhus C, Denmark. Email: smriis@daimi.au.dk Phone: +45 89 42 32 85

In the section further perspectives we show how it is possible to assign a mathematical theory T_{P} (f) to any given propositional proof system P and any complexity f. This idea is new and places our main result in a larger perspective. For any propositional proof system P one can ask about the behaviour of T_{P} (f) when the resources f increase. This question is completely well defined and is closely linked to the complexity gap phenomena.

I hope the expert in propositional proof lower bound will seriously consider this approach. The paper raises a number of questions related to the theory T_{P}. The paper also raises a number of problems which seem to lie just outside the scope of current techniques.

The paper is however not only aimed at the expert. The major part of the paper is intended for a broad audience with a primary interest in complexity theory. We all know that a few complexities appear again and again, while other complexities virtually never appear. This is folklore knowledge which I think puzzles many of us from time to time. The present paper is partly motivated by this phenomena. The paper shows that there are contexts where it is possible to have a general complexity gap theorem. In the paper we focus almost entirely on tree-resolution and the most basic version of the complexity gap phenomena. This way we avoid any serious technical complications. More ambitious gap-theorems ([29], [30] joint work with Meera Sitharam) lead to highly interesting but also very serious technical problems. In the present paper we consider the base case which undoubtly also has the greatest general interest.

The reader who is interested in the resolution method (perhaps mostly for predicate logic) might find some of our proofs interesting and stimulating. To achieve our upper bound we show how it is possible to bring a given resolution refutation (for predicate logic) on a special but very natural normal form. The normal form allows one to read-off the unification directly from the abstract proof form.

Finally I think that the method of generating unsatisfiability problems by use of the symmetric group will be of general interest. This idea was introduced in [28], but in the present paper we develop the idea somewhat further.

An important motivation for studying propositional proof systems is tied up with the following basic question: Given a true statement (tautology) what is the length of the shortest proof of the statement. Here the answer of course depends on which axiomatic proof system is being used. From a Computer Science perspective the question is particularly fundamental for propositional logic. As formalised by Cook and Reckhow [13], there exists a propositional proof system in which any tautology ψ has a proof of size bounded by p(|ψ|) for a fixed polynomial p if and only if NP=co-NP. This question is far beyond current techniques. However Cook and Reckhow proposed a program of research which systematically tries to obtain non-polynomial lower bounds for stronger and stronger propositional proof systems. The hope is that this eventually will lead to a separation of NP from co-NP. In the section further perspectives we discuss this approach in the context of our results.

Tautologies expressing simple graph theoretic properties have been important test cases for obtaining bounds for the length of propositional resolution refutations. The first super-polynomial lower bound for resolution (satisfying a restriction called regularity) was obtained by Tseitin [32]. Subsequent work simplified Tseitin’s proof and improved the lower bounds for regular resolution [14], [33]. However great difficulty was experienced in extending Tseitin’s arguments to unrestricted resolution (=dag-resolution). In [16] Haken managed to give a super-polynomial lower bound for the pigeon-hole principle for dag-resolution. Later this result was improved considerably by Ajtai [1], [2] to a super-polynomial lower bound on bounded depth Frege proofs. Ajtai also used his approach to show independence results from Bounded Arithmetic. These results were later improved in various ways and generalities [3], [5], [8], [25], [26].

Informally we can state our result as follows: Let ψ_{n} denote a sequence of tautologies which expresses the validity of a fixed combinatorial principle P_{com}. Let C_{n} denote the negation of ψ_{n} on Conjunctive Normal Form. Our main result states that for any such sequence C_{n} either the sequence has polynomial size tree-resolution refutations or the sequence requires truly exponentially sizeed tree-resolution refutations. Furthermore, exponential size is required exactly when P_{com} is false as a principle of infinitary combinatorics.

The reason we consider tree-resolution, rather than dag-resolution is mainly technical. Ideally we would have preferred to have proved our results for dagresolution. Actually even stronger propositional systems might have complexity gaps, but for most propositional systems any proof of such a complexity gap would solve open problems which are beyond current techniques. In the case of tree-resolution we avoid any serious technical complications.

As already pointed out, we consider uniform sequences C_{n} of unsatisfiability problems. More specifically we consider uniformly S_{n}-generated sequences C_{n} of unsatisfiable clauses (here S_{n} denotes the symmetric group consisting of the permutations of {1, 2, …, n}). This approach was introduced in [28] (see also below for more details). The idea is to select a finite collection of generating clauses and then obtain C_{n} as the S_{n}-closure of the generating clauses. This method is interesting in its own right because it provides a very easy and feasible method for generating test problems for proof systems for propositional logic. Also it is easy to organise and classify the test problems.

The class of S_{n}-generated unsatisfiability problems consists of highly uniform sequences of unsatisfiability problems. How restrictive is this S_{n}-generated uniformity?

The class of S_{n}-generated sequences of C_{n} is quite rich and wide. The class is so rich that the decision problem of deciding whether a given S_{n}- generated sequence C_{n} has polynomial size tree-resolutions, is undecidable. Also the degree of the polynomial bounding the size might be tremendously large. Actually for any fast-growing total recursive function F, e.g. the Ackerman function, F_{ϵ_{0}}, F_{Γ_{0}} etc. (see for example [31] for a survey on fast growing functions), there exists a (small) finite list C_{gen} of generating clauses such that the sequence C_{n} has polynomial size tree-refutations, but the degree of the polynomial needed to bound the size of the smallest tree-refutations, is larger than F (|C_{gen}|) (where |C_{gen}| denotes the number of symbols in C_{gen}).

Another question we have to address is to what extent the class of S_{n}- generated unsatisfiability problems is relevant. It is certainly powerful enough to generate the hardest unsatisfiability problems which are known. Actually (assuming NEXP ≠ co-NEXP) the method is rich enough to generate a universally difficult sequence C_{n_{1}}, C_{n_{2}}, … of unsatisfiable collections of clauses which requires non-polynomial size refutations for any given propositional proof system [28].

The proof complexity of S_{n}-generated sequences C_{n}, which are unsatisfiable for all values of n, is open. We do not know whether there are propositional proof systems which have polynomial size refutations of any such S_{n}-generated sequence. We will return to this question in the section further perspectives towards the end of the paper.

Let us briefly compare the S_{n}-generation method with the most commonly used method of generating satisfiability problems. This method (which is outside the scope of this paper) is to consider randomly chosen 3-satisfiability problems and to consider the case where the ratio c of clauses and variables is kept constant, while the number of variables tends to infinity. Experiments suggest that there is a phase transition near c = c_{phase} ≈ 4.23.... Experimentally it is found that virtually all problems with c > c_{phase} are unsatisfiable, while virtually all problems with c < c_{phase} are satisfiable. Given a propositional refutation system P it seems to be possibile that there is a phase transition (for some constant c_{P}) in the following sense: For c_{phase} < c < c_{P} almost certainly long (e.g. exponential size) refutations are required, while for c_{P} < c there are almost certainly short (e.g. polynomial size) refutation size proofs. In such a case, where the threshold is sharp, it seems fair to say that a complexity gap occurs. Of course the situation could be much more complicated with various phase transitions and thresholds corresponding to different complexity classes, etc.

The only propositional refutation system for which the situation is well understood is the tree-resolution refutation system. It turns out that for this system there is no sharp phase transition (see [6]) and that the expected refutation complexity tails off very slowly as a function of c. This result does not contradict the complexity gap we show in this paper. This is because the S_{n}-generated test problems are very far from being random. I believe S_{n}- generated test problems are much superior to random test problems when it comes to discussing and analysing specific weaknesses of a given propositional proof system. It is in my opinion not a coincidence that the strongest known lower bounds - including Haken’s [16] (for resolution) and Beame et.al. [7] (for bounded depth frege proofs) - can be achieved by S_{n}-generated problems, rather than by random generated unsatisfiability problems.

Instead of considering randomly chosen unsatisfiability problems we consider uniformly S_{n}-generated sequences C_{n} of unsatisfiable clauses. Later in this paper we will notice how it is possible to assign a mathematical firstorder theory T to each uniformly S_{n}-generated sequence C_{n} of satisfiability problems. We also have the converse (which also follows from [28]) that for any first order theory (which might not be finitely axiomatisable and which might be highly non-recursive) there is a natural translation procedure which translates the question of whether T has a model of size n into a satisfiability problem SAT_{T,n}. This satisfiability problem is uniformly S_{n}-generated.

This shows that uniformly S_{n}-generated satisfiability problems can be viewed as being satisfiability problems (in propositional logic) which arise from translating satisfiability problems in predicate logic. The idea is (in its most general form) to take as input any first-order theory T, which then is used to generate a sequence of propositional formulas ψ_{1}, ψ_{2}, … in which ψ_{n} expresses that T does not have a model of size n. As already pointed out, this method of generating tautologies (even when T only consists of a single sentence) is very general. It covers a large and important class of sequences of tautologies. Many natural sequences of tautologies which express a general combinatorial principle belong to this class. The class also includes the tautologies defined in [28]. Let k_{T}^{rel} denote the maximal arity of a relation symbol in the language for T while k_{T}^{fun} denote the maximal arity of a function symbol in the language for T. For a given propositional proof system (refutation system) P it is natural to try to understand which mathematical theories T lead to difficult unsatisfiability problems. In the paper we show:

Theorem: (informal version) Let T be a first order theory (which might not be finitely axiomatisable and which might be highly non-recursive). There is a natural translation procedure which translates the question of whether T has a model of size n into a satisfiability problem SAT_{T,n}. There are two possibilities:

(1) For each value of n for which SAT_{T,n} is unsatisfiable, the smallest tree-resolution refutations has size at least 2^{n/max(k_{T}^{rel},1+k_{T}^{fun})}

(2) Asymptotically (i.e when n tends to infinity) SAT_{T,n} has polynomial size (in n) tree-resolution refutations.

Possibility (1) happens if and only if T has an infinite model. The lower bound in (1) also holds if SAT_{T,n′} is satisfiable for some n′ > n.

In general - even when T only consists of a single sentence ψ - it is undecidable whether SAT_{ψ,n} has polynomial size tree-refutations or require exponential size tree-refutations. The collection of ψ which have polynomial size tree-refutations is recursively enumerable (but not recursive). There is no total recursive function which given input ψ outputs u ∈ N such that if SAT_{ψ,n} has polynomial size tree-refutations then it has ≤ n^{u}-size tree-refutations.

The theorem gives a complete classification of the theories T for which SAT_{T,n} requires large tree-resolution refutations (if there are any at all - SAT_{T,n} could be satisfiable). More specifically, a theory T leads to hard (for tree-resolution) tautologies if and only if T has an infinite model.

Let me point out that the philosophy behind this result first was articulated in [23] where it was shown (in the context of Bounded Arithmetic) that combinatorial principles which fail as infinitary combinatorics in a sense (which can be made precise) are harder (to prove) than combinatorial principles which also are valid as part of infinitary combinatorics. More specifically in [23] we showed that combinatorial principles which fails for infinite sets never can be proved on the first tree levels S_{2}^{1}(α) ⊆ T_{2}^{1}(α) ⊆ S_{2}^{2}(α) of Sam Buss hierarchy of Bounded Arithmetic, while such combinatorial principle in certain cases can be proved on the fourth level T_{2}^{2}(α). It is well known that provability in fragments of Bounded Arithmetic is closely related to propositional proof complexity (for more details see [17]). The results in the present paper are, however, technically unrelated to the results in [23]. The proof technique in the current paper is different from the rudimentary forcing technique which was employed in [23]. Jan Krajicek has pointed out (personal communication) that our exponential lower bound follows by a modification of his proof of Theorem 11.3.2 in [17] (which essentially is the main result in [23]). See also Lemma 9.5.2 in [17] where this is stated explicitly.

I am aware of only one other result which gives a complexity gap between polynomial complexity and exponential complexity. A beautiful result [15] which relates the Vapnik-Chervonenkis (VC) dimension to the growth rate of the complexity of learning the concept class C. It states that this growth rate is either polynomial or exponential. Furthermore, it is polynomial if and only if the VC-dimension of C is finite. The underlying mathematics in this result are completely different from ours. It is however remarkable that the dichotomy of finite versus infinite plays a crucial role in both the VC-complexity gap theorem as well as in our complexity gap theorem.

2 Background and Notation

A literal is a propositional variable or the negation of a propositional variable. A clause C := {l_{1}, l_{2}, …, l_{u}} is a collection of literals, and it is satisfied if l_{1} ∨l_{2} ∨…∨l_{u} holds. In the famous NP-complete problem 3-SAT, the decision problem is to decide if a given collection of clauses (which each contain at most 3 literals) is satisfiable.

Resolution is a refutation system designed to provide certificates (i.e. proofs) that a system of clauses is unsatisfiable. A given formula is shown to be a tautology by showing that its negation, put into conjunctive normal form (i.e. clausal form) is unsatisfiable. This is done by means of the resolution rule

Resolution rule :  \frac{C_{1} ∪ \{p\} C_{2} ∪ \{¬p\}}{C_{1} ∪ C_{2}}

The given clauses are often referred to as axioms, and the task it to derive the empty clause (the contradiction) from the axioms. In tree-resolution the proof is organised as a binary tree with the axioms in the leaves and the empty clause in the root.

As comparison in unrestricted resolution (dag-resolution) the derived clauses are listed in a linear fashion C_{1}, C_{2}, …, C_{u}, and any clause C_{l} is either an axiom or appears by resolving two clauses C_{i}, C_{j}, i, j < l. Such a derivation can also be represented as a dag which explains the terminology dag-resolution. In dag-resolution a derived clause can be reused, while this is not the case in tree-resolution.

As already noted, Haken considered a sequence of tautologies expressing the so-called pigeonhole principle. It can be shown that Haken’s tautologies require tree-resolution proofs of size ≥ n2^{n} [11]. In this paper we will show that an exponential lower bound actually follows from the simple fact that the pigeon-hole principle fails as a principle of infinite combinatorics.

Haken’s tautologies (Γ_{n}) can be written as follows: ∪_{j=1}^{n} {a_{ij}}, where i = 1, 2, …, n {ā_{ij}, ā_{ik}}, where i, j, k = 1, 2, …, n and j ≠ k ∪_{j=1}^{n} {a_{0j}}, {ā_{0i}, ā_{0j}}, where i, j = 1, 2, …, n and i ≠ j {ā_{ik}, ā_{jk}}, where i, j, k = 1, 2, …, n {ā_{ij}, ā_{0j}}, where i, j = 1, 2, …, n This collection is, in a rather obvious way, finitely generated by the symmetric group S_{n}. More specifically each Γ_{n} is generated by taking the S_{n}-closure of the clauses: ∪_{j} {a_{1j}}, {ā_{12}, ā_{13}}, {ā_{11}, ā_{12}}, ∪_{j} {a_{0j}}, {ā_{01}, ā_{02}}, {ā_{13}, ā_{23}}, {ā_{12}, ā_{02}}, {ā_{12}, ā_{22}}, {ā_{11}, ā_{01}} For future reference let us denote this collection of generators by Γ_{Haken}. For any n let C_{n} denote the collection of clauses which appear by closing Γ_{Haken} under the natural action of the symmetrical group S_{n} (permuting {1, 2, 3, …, n} while keeping 0 fixed). This system of clauses is equivalent to the system for which Haken obtained his famous super-polynomial lower bound.

2.1 S_{n}-generated unsatisfiability problems

The translation of many combinatorial principles into a system of unsatisfiable clauses naturally leads to clauses which are generated by applying the symmetric group S_{n} to a collection of generators. The S_{n}-symmetry arises naturally when the combinatorial problem is independent from the underlying representation. Consider, for example, a combinatorial principle K which is valid for some graph G. The principle K is also valid when the enumeration of the vertices is permuted by an element π ∈ S_{n}. It turns out that this S_{n}-symmetry survives (as will become clear) when we reformulate the combinatorial principle in terms of an (un)satisfiability problem.

Before we move on we will be slightly more general and consider hypergraphs; For fixed r = 0, 1, 2, … we can consider the collection a_{n_{1},n_{2},...,n_{r}} of boolean variables for which n_{1}, n_{2}, …, n_{r} ∈ {1, 2, …} = N. Actually we might also have other boolean variables b_{n_{1},n_{2},...,n_{r}} for which n_{1}, n_{2}, …, n_{r} ∈ {1, 2, …, }, or more generally we might fix a collection a_{n_{1},n_{2},...,n_{r_{i}}}^{i} i = 1, 2, … of boolean variables of different variable types (one for each i). The support of a boolean variable a_{n_{1},n_{2},...,n_{r_{i}}}^{i} is {n_{1}, n_{2}, …, n_{r_{i}}}. We consider two kind of clauses. An ordinary clause is a collection {p_{1}, p_{2}, …, p_{l}} of literals (i.e. boolean variables or negations of boolean variables). An abstract clause is a formal expression of the form ∪_{j} {a_{n_{1},n_{2},...,n_{r_{i}−1},j}^{i}}. In the case of Γ_{Haken} the generators ∪_{j} {a_{1j}} and ∪_{j} {a_{0j}} were the only abstract clauses - all other clauses were ordinary clauses. In the example of Γ_{Haken} we can view boolean variables which contain a zero (e.g. a_{02}) as variables of a different variable type than variables which do not contain a zero (e.g. a_{12}).

Now let Γ_{gen} be a collection of clauses (normal clauses as well as abstract clauses). Assume that all boolean variables which appear in Γ_{gen} have support contained in {1, 2, …, l}. For each n ≥ l we get a collection Γ_{n} of clauses by taking the S_{n}-closure of the clauses in Γ_{gen} in the obvious fashion. The sequence Γ_{n} is S_{n}-generated if there exists a collection Γ_{gen} (not necessarily finite) such that Γ_{n} is the S_{n}-closure of Γ_{gen}. The sequence Γ_{n} is finitely S_{n}- generated if there exists a finite collection Γ_{gen} which generates the sequence Γ_{n}. Notice that Γ must involve infinitely many variable types in the case where Γ is infinite.

In [28] we showed how one could obtain a finite collection of generators (like the list above) whenever given an existential second order sentence Ψ. If Ψ is second order existential which is on prenex normal form with its first order part purely universal, then the translation into propositional logic does not involve the introduction of skolem functions. In this case we simply translate the question of whether a purely universal first order sentence Ψ′ has a model (of size n) into a satisfiability problem Γ_{Ψ,n}. As we showed in [28] there is a one-to-one correspondence between the satisfying assignments of Γ_{Ψ,n} and the models of size n of Ψ′.

The converse is essentially (see later for the exact result) also true: For any collection Γ of generators there exists a universal first order theory T such that there is a one-to-one correspondence between satisfying assignments of Γ_{n} (the S_{n}-closure of Γ) and the models M_{n} of T which have size n. Furthermore, if Γ is finite, then T can be replaced by a single universal first order sentence Ψ.

Again there is a one-to-one correspondence between the satisfying assignments of Γ_{n} and the models of size n of T (Ψ).

2.2 Link to predicate logic

Consider the system Γ_{gen} := Γ_{Haken}. We claim (and it is essentially just a matter of changing notation) that the satisfiability problem Γ_{n} is equivalent to the question of whether a sentence (theory) in predicate logic has a model of size n. The sentence is the following predicate formula expressing the negation of the pigeon-hole principle:

∀x f(x) ≠ c ∧ ∀x, y, z (f(x) = y ∧ x ≠ z) → (f(z) ≠ y)

We can write this sentence in clausal form as a satisfiability problem in predicate logic. This problem consists of the clauses

{¬f(x) = c}, and {¬f(x) = z, ¬f(y) = z, x = y}

as well as the usual clauses for axioms of equality (see [19] or below for more details). To these clauses we add the clauses {¬c_{i} = c_{j}} for i ≠ j, i, j ≤ n as well as the clause {x = c_{1}, x = c_{2}, …, x = c_{n}} (see below for a discussion of this choice). The collection these clauses gives us a system C_{n} of clauses in predicate logic. The satisfiability problems Γ_{n} and C_{n} are (not surprisingly) closely related.

We will now focus on the case of translating satisfiability problems in predicate logic into a satisfiability problem in propositional logic (Our translation should NOT be confused with the usual Herbrand-style (or Henkin-style) translation in which sentences are viewed as propositional variables).

Let C be a collection of clauses for predicate logic over some fixed language L in which function symbols and relation symbols have arities bound by fixed constants k_{C}^{rel} and k_{C}^{fun}. The collection C might be infinite. Any universal theory can be written as a collection of clauses. In general any theory T′ can be replaced by a logical equivalent universal theory T (this process of introducing skolem-functions is not unique).

Let C_{eq} denote the collection C extended with clauses expressing the axioms of equality. More specifically let C_{eq} consists of the clauses in C together with the clauses {x = x}, {¬x = y, y = x}, {¬x = y, ¬y = z, x = z} and a clause {¬x_{1} = y_{1}, ¬x_{2} = y_{2}, …, ¬x_{k} = y_{k}, ¬R(x_{1}, x_{2}, …, x_{k}), R(y_{1}, y_{2}, …, y_{k})} for each k-ary relation symbol R (k = 1, 2, …, k_{C}^{rel}) and a clause {¬x_{1} = y_{1}, ¬x_{2} = y_{2}, …, ¬x_{k} = y_{k}, f(x_{1}, x_{2}, …, x_{k}) = f(y_{1}, y_{2}, …, y_{k})} for each k-ary function symbol f (k = 1, 2, …, k_{C}^{fun}). Now let n ∈ N be given. Let c_{1}, c_{2}, …, c_{n} be new constants which does not appear in C. Consider the following collection (of clauses):

C_{≥n} := {{¬c_{1} = c_{2}}, {¬c_{1} = c_{3}}, …, {¬c_{n−1} = c_{n}}}

If we add these clauses to C_{eq}, any model which satisfies the clauses must have size ≥ n. A little care is needed when we add clauses expressing that there are at most n elements in the domain. One could, for example, add the clause, {x_{1} = x_{2}, x_{1} = x_{3}, …, x_{n} = x_{n+1}}. The presence of this clause, however, smuggles in a version of the pigeon-hole principle which is not available as a rule in propositional resolution proofs. Instead we chose the collection:

C_{≤n} := {{x = c_{1}, x = c_{2}, …, x = c_{n}}}

The collection of the clauses in C_{eq} together with the clauses axiomatising nness is denoted C_{n} (i.e. C_{n} := C_{eq} ∪ C_{≥n} ∪ C_{≤n}). We also introduce a slightly weaker axiomatisation of n-ness. In this axiomatisation we replace the clause {x = c_{1}, x = c_{2}, …, x = c_{n}} by the schema C_{≤n}^{weak} which consists of the clauses {f(c_{i_{1}}, c_{i_{2}}, …, c_{i_{k}}) = c_{1}, f(c_{i_{1}}, c_{i_{2}}, …, c_{i_{k}}) = c_{2}, …, f(c_{i_{1}}, c_{i_{2}}, …, c_{i_{k}}) = c_{n}}. There is one such clause for each function symbol and for each i_{1}, i_{2}, …, i_{k} ∈ {1, 2, …, n}. For each constant symbol c the schema contain the clause {c = c_{1}, c = c_{2}, …, c = c_{n}}. This system of clauses is denoted C_{n}^{weak} (i.e. C_{n}^{weak} := C_{eq} ∪ C_{≥n} ∪ C_{≤n}^{weak}).

To get propositional tautologies like the ones which have already been extensively examined in the literature ([2], [11], [13], [16], [28]) we proceed as follows: We are given a system C_{n} (or C_{n}^{weak}). We want to ensure that each literal (=atomic formula or negation of atomic formula) is of the form: R(x_{1}, x_{2}, …, x_{k}) or f(x_{1}, x_{2}, …, x_{k}) = x_{k+1} or c = x_{1}. To achieve this we rewrite the clauses in the obvious way. Assume, for example, that we want to rewrite the clause: {R(x, S(S(x))), f(S(x), y) = x}. We do this in steps, getting {R(x, z), ¬z = S(S(x)), ¬w = S(x), f(w, y) = x} , {R(x, z), ¬z = S(u), ¬u = S(x), ¬w = S(x), f(w, y) = x}, and then finally {R(x, z), ¬S(u) = z, ¬S(x) = u, ¬S(x) = w, f(w, y) = x}. The resulting system is denoted C_{n}^{∗} (C_{n}^{weak,∗} (C_{eq,n}^{∗} in the case of C_{eq})). Finally consider all clauses which can appear by replacing each of its variables by a constant from c_{1}, c_{2}, …, c_{n}. We denote the resulting system of clauses C_{n}^{prop} (C_{n}^{prop,weak}).

Notice that each clause in C_{≤n}^{weak} is a substitution instance of the clause {x = c_{1}, x = c_{2}, …, x = c_{n}} in C_{≤n}. On the other hand {fff(c_{1}) = c_{1}, fff(c_{1}) = c_{2}, …, fff(c_{1}) = c_{n}} (which is a substitution instance of {x = c_{1}, x = c_{2}, …, x = c_{n}}) becomes {¬f(c_{1}) = x, ¬f(x) = y, f(y) = c_{1}, f(y) = c_{2}, …, f(y) = c_{n}} and thus when constants c_{i}, c_{j} are substituted for x and y {¬f(c_{1}) = c_{i}, ¬f(c_{i}) = c_{j}, f(c_{j}) = c_{1}, f(c_{j}) = c_{2}, …, f(c_{j}) = c_{n}}. But clauses of this form are just weakenings of the clauses in C_{≤n}^{weak}. Actually it is not difficult to see that this always is the case. Thus from now on we do not distinguish between C_{n}^{prop,weak} and C_{n}^{prop}. From now on C_{n}^{prop} denotes the same system as C_{n}^{prop,weak} (except we might be allowed to include weakenings of the clauses to be refuted to the unsatisfiability problem).

Notice that the size of C_{n}^{prop} is bounded by a polynomial in n. It should, however, be emphasised that our translation procedure - naively speaking - typically translates combinatorial principles (like the pigeon-hole principle) into an infinite system of clauses. This is because, besides the “usual” clauses, we also get clauses which, for example, express properties and behaviour of the terms (including skolem-functions). In the case of the pigeonhole principle we have, for example, clauses expressing properties which involve the iteration of the function symbol. We have already seen that this is irrelevant when it occurs in {x = c_{1}, x = c_{2}, …, x = c_{n}} and that we essentially get the same clauses whether we allow iterations of terms or only allow atomic terms to be substituted. This is also (trivially) the case for a general clause in C. This is because substitution in a clause (e.g. x ← f(x), y ← g(y) in {R(x, y)}) always leads to a weakening of the original clause ({R(f(x), g(y))} which turns into the form {R(z, u), ¬f(x) = z, ¬g(y) = u}).

These considerations show that the translation C_{n}^{prop} (after having discarded irrelevant weakenings) always contains only polynomially (in n) many clauses. The translation corresponds (except from the treatment of constants in the original language for C) to the informal procedure which seems to have been used when considering a principle like the pigeonhole principle [13] or the parity principle [3]. This translation also agrees with (and extends) the procedure defined in [28].

Let S_{C}(n) denote the size of the smallest tree-resolution refutation of C_{n}^{prop}. If there is no such refutation, we let S_{C}(n) = ∞. Usually proof complexity is measured in the size of the satisfiability problem, however we get cleaner results if we use n as input parameter. Also there exist polynomials p_{1}, p_{2} such that p_{1}(n) ≤ |C_{n}| ≤ p_{2}(n) so our complexity gap agrees with the usual conventions. For our purposes it is most sensible to use the model size n as the relevant parameter.

Finally let me briefly mention the treatment of constants. In the case where L has finitely many constants c^{(1)}, c^{(2)}, …, c^{(u)} and where we assume that these are distinct, it is natural (mostly for cosmetic reasons) to replace the clauses {c^{(i)} = c_{1}, c^{(i)} = c_{2}, …, c^{(i)} = c_{n}} by the clauses {c^{(1)} = c_{1}}, {c^{(2)} = c_{2}}, …, {c^{(u)} = c_{u}} and to let the symmetric group S_{n−u} act on {u + 1, u + 2, …, n}. Notice that this modification of C_{n}^{prop} only affects our lower bounds mildly (at most by a polynomial factor n^{u}).

3 Main Results

Theorem 1: (Gap theorem) The following are equivalent:

(1) For any polynomial P (n), there exists n such that S_{C}(n) > P (n).

(2) For each n, S_{C}(n) ≥ 2^{n/max(k_{C}^{rel},1+k_{C}^{fun})}.

(3) C is satisfied in an infinite model. The decision problem of deciding whether C satisfies (1),(2) and (3) is undecidable. The collection of finite collections C of clauses for which there exists a polynomial P such that P (n) > S_{C}(n) for all n ∈ N is recursively enumerable (but not recursive). There is no total recursive function, which given input C, outputs u ∈ N such that n^{u} > S_{C}(n) whenever (1),(2) or (3) fails.

Now let Ψ be a universal sentence in first order logic. In the previous section we showed that we can express the claim that Ψ does not have a model of size n as a boolean tautology Ψ_{n} (see also [28]). We may even consider the case where Ψ is a Π_{2}-sentence (i.e. not just a Π_{1}-sentence). In this case we can translate the sentence into propositional logic by means of abstract clauses very similar to the abstract clauses described earlier (the existential quantifier get translated into clauses like ∪_{j_{1},j_{2},...,j_{r}} {a_{i_{1},i_{2},...,i_{s_{1}−1},j_{1},i_{s_{1}+1},...,i_{s_{k}−1},j_{k},i_{s_{k}+1},...,i_{m}}}. In general (for arbitrary first order formulas) we can introduce skolem functions (see [28] for details) to rewrite the sentence as a Π_{1}-sentence (or just a Π_{2}-sentence) which then can be translated into a satisfiability problem in propositional logic. One way which leads to the same result is to translate Ψ into a satisfiability problem C_{Ψ} (the usual way by introducing skolem functions etc. see for example [19]) and then proceed as described the the previous section. The collection of clauses C_{Ψ,eq} (which contains the clauses for equality) is satisfiable if and only if Ψ has a model. If Ψ does not have a model, there exists (by Herbrands Theorem) a finite collection of clauses (from C_{Ψ,eq}) together with a suitable unification, such that the resulting system is unsatisfiable in the sense of propositional logic. Let Ψ_{n} denote the tautology which express the unsatisfiability of C_{Ψ,n}^{prop}. With this notation we get:

Corollary 1: Assume Ψ is a sentence of first order logic. Assume Ψ does not have models of size n for infinitely many values n_{1}, n_{2}, n_{3}, … of n. Then the following are equivalent:

(1) Ψ_{n} has a tree-resolution refutation of sub-exponential size.

(2) Ψ_{n} has a tree-resolution refutation of polynomial size.

(3) Ψ has no infinite model. Furthermore if (1), (2) or (3) holds, there exists n_{0} such that Ψ_{n} is a tautology for all n ≥ n_{0}.

Corollary 2: If Ψ_{n} has a tree-resolution refutation of size < 2^{n_{0}/max(k_{T}^{rel},1+k_{T}^{fun})} just for one value n = n_{0}, then there exists a polynomial P (n) such that each Ψ_{n}, for n ≥ n_{0} have tree-refutations of size ≤ P (n).

Given our main result there is nothing mystical in this Corollary. A treeresolution of size < 2^{n/max(k_{T}^{rel},1+k_{T}^{fun})} witness the fact that C_{eq} ∩ {{c_{1} ≠ c_{2}}, … {c_{n−1} ≠ c_{n}}} is unsatisfiable, and that C is not satisfied in any infinite model. It is well known that predicate logic is decidable in an oracle which provide an upper bound on the Herbrand Complexity for a logical valid formula. This shows that there is no general computable method for computing the degree of the polynomial P in Corollary 1.

As a by-product and somewhat related we get a complexity gap for the Herbrand complexity:

Theorem 3: (Complexity gap for Herbrand Complexity) Let C be a satisfiability problem (for predicate logic). Assume that the underlying language has all functions and relations of arity bounded by a constant. Consider C_{n} := C_{eq} ∪ C_{≥n} ∪ C_{≤n} and let us only consider the values of n for which C_{n} is unsatisfiable.

Then either C_{n} has a Herbrand Complexity bounded by a constant, or C_{n} has Herbrand Complexity which is linear in n.

Furthermore, the first case appears exactly when C is unsatisfiable.

We noticed (after Corollary 2) that there is no general computable method for computing the degree of the polynomial P in Corollary 1. The same observation shows that there is no general computable method for bounding the constant in Theorem 3. Also there is, given input C, no computational method which can decide whether the sequence C_{n}^{prop} (C_{n}) requires superpolynomial tree-resolution refutations (has non-constant Herband Complexity) or has polynomial size tree-resolution refutations (have constant Herband Complexity)

The argument for the polynomial upper bound can be broadened somewhat further. We present these results in the section further perspectives .

4 Examples

Now let us illustrate the main ideas in this paper by a few examples:

Example 1: Let Θ ≡ ∀x∃yR(x, y) ∨ ∃x∀y¬R(x, y). This sentence is logically valid. To show this (by the resolution method for predicate logic) we first consider Ψ ≡ ¬Θ ≡ ∃x∀y¬R(x, y) ∧ ∀x∃y¬R(x, y) and rephrase this (by introducing skolem-functions) as ∀y¬R(c, y) ∧ ∀xR(x, f(x)). This translation method is standard and is, for example, described in [19]. To show Θ is equivalent to showing that the system of clauses {{¬R(c, y)}_{y}, {R(x, f(x))}_{x}} is unsatisfiable. The unsatisfiability follows from the fact that we have a unification of (R(c, y), R(x, f(x)) by x → c, y → f(c) which leads to the refutation \frac{\{¬R(c,f(c))\} \{R(c,f(c))\}}{∅}.

For a given n, the clauses in C_{n} consist of the clauses {¬R(c, y)}_{y}, {R(x, f(x))}_{x} together with the clauses for equality and the clauses {¬c_{1} = c_{2}}, …, {¬c_{n−1} = c_{n}}, as well as the schema: {c = c_{1}, c = c_{2}, …, c = c_{n}}, and {f(c_{i}) = c_{1}, f(c_{i}) = c_{2}, …, f(c_{i}) = c_{n}}. Now to get the system C_{n}^{prop} we rewrite {¬R(c, y)}_{y} and {R(x, f(x))}_{x} as {¬c = x, ¬R(x, y)}_{x,y} and {R(x, y), ¬f(x) = y}_{x,y}.

Finally, after taking the union of all clauses which appear by replacing free variables by constants c_{1}, c_{2}, …, c_{n}, we arrive at C_{n}^{prop} the following clauses, where f_{ij} is shorthand for f(c_{i}) = c_{j} and where d_{i} is shorthand for c = c_{i}:

{¬r_{ik}, ¬d_{i}} for i, k ∈ {1, 2, …, n}, {r_{ik}, ¬f_{ik}} for i, k ∈ {1, 2, …, n},

{d_{1}, d_{2}, …, d_{n}}, {f_{i1}, f_{i2}, …, f_{in}} for i ∈ {1, 2, …, n}.

The system C_{n}^{prop} has the following tree-resolution refutation proof:

B_{n} \frac{.... \frac{B_{4} \frac{B_{3} \frac{B_{2} \frac{B_{1} \{d_{1}, d_{2}, …, d_{n}\}}{\{d_{2}, d_{3}, …, d_{n}\}}}{\{d_{3}, …, d_{n}\}}}{....}}{........}}{\{d_{n}\}}

∅

where

B_{i} := \frac{A_{in} \frac{.... \frac{A_{i4} \frac{A_{i3} \frac{A_{i2} \frac{A_{i1} \{f_{i1}, f_{i2}, …, f_{in}\}}{\{¬d_{i}, f_{i2}, f_{i3}, …, f_{in}\}}}{\{¬d_{i}, f_{i3}, …, f_{in}\}}}{....}}{........}}{\{¬d_{i}, f_{in}\}}}{\{¬d_{i}\}}

and where

A_{ik} := \frac{\{¬r_{ik}, ¬d_{i}\} \{r_{ik}, ¬f_{ik}\}}{\{¬d_{i}, ¬f_{ik}\}}

It is not hard to verify that this proof consists of 4n^{2} +2n+1 clauses (which is optimal because any tree-resolution refutation must have each of the 2n^{2}+n+1 clauses appearing in the some leaf). ♣

This example illustrate how the fact that Ψ has no models (of size n) can be translated into a “test-case” unsatisfiability problem for propositional logic. In the example ¬Ψ is logically valid so Ψ has no infinite model. According to our main result this implies (what we just verified) that C_{n}^{prop} has polynomial size tree-resolution refutations.

Example 2: Let T denote the first order theory axiomatised by the single axiom ψ := ∀i, j( i ≠ j → s(i) ≠ s(j)) ∧ ∀j s(j) ≠ c. The theory T is an axiomatisation of the first order theory of a constant and a successor function. The clauses in C consist of {x = y, ¬S(x) = S(y)}_{x,y}, and {¬S(x) = c}_{x}. To make the translation into propositional logic we rewrite these clauses as {x = y, ¬S(x) = z, ¬S(y) = z}_{x,y,z} and {¬S(x) = y, ¬c = y}_{x,y}. To simplify the readability we abbreviate S(c_{i}) = c_{j} as s_{ij}, and c = c_{j} as d_{j}. This gives us a satisfiability problem C_{n}^{prop} in the boolean variables s_{11}, s_{12}, …, s_{nn}, d_{1}, d_{2}, …, d_{n} and with the following clauses:

(1) {s_{i1}, s_{i2}, …, s_{in}} for i = 1, 2, …, n.

(2) {s̄_{ik}, s̄_{jk}} for i ≠ j, where i, j, k ∈ {1, 2, …, n}

(3) {d_{1}, d_{2}, …, d_{n}}

(4) {d̄_{i}, d̄_{j}} for i ≠ j, where i, j ∈ {1, 2, …, n}

(5) {d̄_{i}, s̄_{ji}} for i, j ∈ {1, 2, …, n}.

The theory T has infinite models so, according to our main result, C_{n}^{prop} requires tree-resolution refutations of size ≥ 2^{n/max(k_{T}^{rel},1+k_{T}^{fun})} = 2^{n/2}.

♣

Example 3: Let T be the theory which is axiomatised by a single axiom stating that there exists a injective map from the universe onto the universe minus one point. More specifically let T be axiomatised by the sentence:

∀x, y x ≠ y → f(x) ≠ f(y) ∧ ∀x f(x) ≠ c.

In clausal form we have C := {{x = y, ¬f(x) = f(y)}_{x,y}, {¬f(x) = c}_{x}}. Then C^{∗} := {{x = y, ¬f(x) = z, ¬f(y) = z}_{x,y,z}, {¬f(x) = z, c = z}_{x,z}}. Let e_{ij} be short hand for f(i) = j and let d_{j} be short hand c = j. Let C_{n}^{prop′} := {{ē_{ik}, ē_{jk}} for i ≠ j, {ē_{ik}, d_{k}}, {e_{i1}, e_{i2}, …, e_{in}}, i = 1, 2, …, n}.

The clauses in C_{n}^{prop} involve other substitution instances of C. As we already noticed these substitutions play no role. For example substituting f(x) → x and f(y) → y in {x = y, ¬f(x) = f(y)}_{x,y} gives us the clause {f(x) = f(y), ¬f(f(x)) = f(f(y))}_{x,y}. If we rewrite this on the (*)-form we get the clause {¬f(y) = z, f(x) = z, ¬f(x) = u, ¬f(y) = v, ¬f(u) = w, ¬f(v) = w}. Thus C_{n}^{prop} includes the clause {¬f(c_{j}) = c_{k}, f(c_{i}) = c_{k}, ¬f(c_{i}) = c_{u}, ¬f(c_{j}) = c_{v}, ¬f(c_{u}) = c_{w}, ¬f(c_{v}) = c_{w}} for i ≠ j and i, j, k, v, w, z ∈ {1, 2, …, n} with i ≠ j. In our shorthand notation these clauses are of the form {ē_{jk}, e_{ik}, ē_{iu}, ē_{jv}, ē_{uw}, ē_{vw}} where i ≠ j. These clause are weakenings of {ē_{uw}, ē_{vw}} which is already (when u ≠ v) in C_{n}^{prop}. When u = v, the clause is a weakening of {ē_{iu}, ē_{jv}} which is already (when i ≠ j) in C_{n}^{prop}. Thus these clause are redundant. Other substitution instances produce even more clauses, but these clauses are redundant. Thus C_{n}^{prop} = C_{n}^{prop′}.

There exists an infinite model in which T is valid. Thus C_{n}^{prop} require tree-resolution refutations of size ≥ 2^{\frac{n}{2}} . The usual version of the pigeon-hole principle is obtained by treating c as a fixed element (for example c_{1}). In this case we get the clauses C_{n}^{prop^{∗}} := {{ē_{ik}, ē_{jk}} for i ≠ j, {ē_{i1}, d}, {e_{i1}, e_{i2}, …, e_{in}}, i = 1, 2, …, n}. Clearly this give a lower bound of 2^{\frac{n}{2}} /n on refuting C_{n}^{prop^{∗}}. Actually it is not hard to see that we can modify our main theorem to the case where the symmetrical group S_{n−1} acts on {c_{2}, c_{3}, …, c_{n}} (and where we let c = c_{1}). This gives a lower bound of 2^{\frac{(n−1)}{2}} . The best known lower bound on this propositional version of the pigeon-hole principle is (n − 1)2^{n−1} (see [11]).

♣

Example 4: It is well known that each finite division ring is a field. There are various ways to rephrase the statement that the universe is a division ring which is not a field as a satisfiability problem (for predicate logic). Let C be one of these satisfiability problems. Then for each n, C_{n}^{prop} is an unsatisfiable set of clauses expressing the fact that there are no non-commutative division rings with n elements.

There are infinite divisions rings which not are fields (for example Hamilton’s famous quaternions). Thus, according to our main result the sequence C_{n}^{prop}; n = 1, 2, .... requires exponential size tree-resolution refutations. It is not clear if C_{n}^{prop} is hard for stronger propositional proof systems like for example the extended Frege proof system. ♣

The final example is somewhat curious. It shows a case where the so-called weak propositional pigeonhole principle appears somewhat unexpected: Example 5: Let T be the first order theory in the language L(=, d_{i}; i ∈ N) of equality plus infinitely many constants. Assume that the theory T is axiomatised by a conjunction of the axioms {¬d_{i} = d_{j}} where i ≠ j, i, j ∈ N. Notice that T not is finitely axiomatisable. Our main theorem include this situation. Let C_{T} = {{¬d_{i} = d_{j}} : i ≠ j, i, j ∈ N}}. The system C_{n}^{weak} = C_{n} consists of the clauses: {¬d_{i} = d_{j}} for i ≠ j, i, j ∈ N and {¬c_{i} = c_{j}} and {d_{i} = c_{1}, …, d_{i} = c_{n}}, i ∈ N as well as the clauses for equality. Thus C_{n}^{prop} consists of the clauses {ē_{k}^{(i)}, ē_{k}^{(j)}} and {e_{1}^{(i)}, e_{2}^{(i)}, …, e_{n}^{(i)}}, where e_{k}^{(i)} is shorthand for d_{i} = c_{k}. So C_{n}^{prop} is (essentially) a boolean version of the pigeonhole principle (stating that there is no injective map from an infinite set onto a set with n elements). A priori T has an infinite model, so according to our main result, C_{n}^{prop} requires exponential size tree-refutations. ♣

5 The polynomial size upper bound

As before let C be a collection of clauses (in the sense of predicate logic). The clauses in C consists of atomic formulas and negations of atomic formulas.

The system C can be rewritten on a normal form C^{∗} where all (negations of) atomic formulas are (negation of) basic atomic formulas i.e. each atomic formula is either of the form R(x_{i_{1}}, x_{i_{2}}, …, x_{i_{r}}) where R is a r-ary (r ∈ {1, 2, …}) relation symbol or is of the form f(x_{i_{1}}, x_{i_{2}}, …, x_{i_{r}}) = x_{i_{r+1}} where f is a r-ary (r ∈ {1, 2, …}) function symbol. Constants are treated as 0-ary function symbols. Here are some examples of basic atomic formulas: R(x, z, x), f(x, y, z) = z and U(x, y). On the other hand the atomic formulas R(g(y), x) and f(x, g(y), z) = h(z, x) are not basic.

Now it is clear we can rewrite any clause C, containing atomic formulas, as an equivalent clause C^{∗} containing only basic atomic formulas. In the case where C = {{¬R(c, y)}_{y}, {R(x, f(x))}_{x}} we can rewrite this as C^{∗} := {¬R(x, y), ¬c = x}_{x,y}, {R(x, y), ¬f(x) = y}_{x,y}}.

From the usual completeness theorem it follows that C has a model if and only if C_{eq} is satisfiable. And this only holds if and only if C_{eq}^{∗} is satisfiable (has a model).

Assume C has no model. Then C_{eq} (and C_{eq}^{∗}) is unsatisfiable and according to Herbrands Theorem there exists a unification τ and a finite subset C′ ⊆ C_{eq} (C′ ⊆ C_{eq}^{∗}) such that τ(C′) is unsatisfiable in the sense of propositional logic.

Actually in the case of C_{eq}^{∗} we can write the refutation on a special normal form. We will use this normal form in the proof of our upper bound.

Let me illustrate this by an example. Consider the “proof-form”

\frac{\{¬R(c, y)\}_{y} \{R(x, f(x))\}_{x}}{∅}

The substitution x → c, y → f(c) turns this into a valid resolution. Now we can rewrite the proof-form as

\frac{\{¬R(x, y), ¬c = x\}_{x,y} \{R(x, y), ¬f(x) = y\}_{x,y}}{\{¬c = x, ¬f(x) = y\}_{x,y}}

This is a valid proof (though in many formalisms only closed terms, and not variables are allowed). The final clause {¬c = x, ¬f(x) = y}_{x,y} can be refuted by the unification x → c, y → f(c).

This leads to the proof:

\frac{\{f(c) = f(c)\} \frac{\{c = c\} \frac{\frac{\{¬R(x, y), ¬c = x\}_{x,y} \{R(x, y), ¬f(x) = y\}_{x,y}}{\{¬c = x, ¬f(x) = y\}_{x,y} (= D)}}{\{¬c = c, ¬f(c) = f(c)\}}}{\{¬f(c) = f(c)\}}}{∅}

The refutation consists of two parts. The first part ends with the clause = D. The unification is uniquely determined from this clause, and the next step (leading to the clause {¬c = c, ¬f(c) = f(c)}) is the only place in the refutation where a substitution takes place. The final part of the refutation only uses clauses expressing the axioms of equality.

This idea works in general. For any refutation of C_{eq}, we can rewrite this as a tree-refutation of C_{eq}^{∗} which is of a normal form such that:

(1) The first part of the refutation consists solely of basic atomic formulas and negation of basic atomic formulas.

(2) The last clause D in this part uniquely determines the unification which is required to refute the clause.

(3) The clause D consists solely of negations of atomic equations.

(4) The last part of the proof refutes the unification (of D) using only applications of substitutions of equality axioms.

To illustrate these ideas further let C := {{P (0)}, {¬P (x), P (S(x))}_{x}, {¬P (S(S(0)))}}. This statement is written in the language L = L(0, P, S) of predicate logic which contains a unary relation symbol P, a constant 0 and a unary function symbol S. Clearly C_{eq} is unsatisfiable. Any refutation requires Herbrand complexity HC = 3 (if {¬P (S(S(0)))} is replaced by {¬P (S^{(k)}(0)))} it requires Herbrand Complexity HC = k). Clearly C^{∗} = {{P (x), ¬0 = x}_{x}, {¬P (x), P (y), ¬S(x) = y}_{x,y}, {¬P (z), ¬S(z_{1}) = z_{2}, ¬S(z_{2}) = z, ¬0 = z_{1}}_{z,z_{1},z_{2}}}. The corresponding propositional unsatisfiability problem C_{n}^{prop} consists of the clauses:

(1) A clause {p_{i}} for i = 1, 2, …, n.

(2) A clause {¬p_{i}, p_{j}, ¬s_{ij}} for each i, j ∈ {1, 2, …, n}.

(3) A clause {¬p_{i}, ¬s_{jk}, ¬s_{ki}, ¬o_{j}} for each i, j, k ∈ {1, 2, …, n}.

(4) The clause {o_{1}, o_{2}, …, o_{n}}.

(5) A clause {s_{i1}, s_{i2}, …, s_{in}} for each i ∈ {1, 2, …, n}.

This system is (a priori as we know) finitely S_{n}-generated. The generators are {p_{1}}, {¬p_{1}, p_{2}, ¬s_{12}}, {¬p_{1}, ¬s_{23}, ¬s_{31}, ¬o_{2}} as well as the degenerate versions of these (i.e. {¬p_{1}, ¬s_{21}, ¬s_{11}, ¬o_{2}} etc.). The axioms for C_{≤n} are generated by the two abstract generators ∨_{j}{o_{j}} and ∨_{j}{s_{1j}}.

The clauses C have no model so we want to show (this is the issue in this section) that the sequence n → C_{n}^{prop} has polynomial size tree-resolution refutations. The clauses in C_{eq} have the following refutation:

\{¬P (S(S(0)))\} \frac{\{¬P (S(0)), P (S(S(0)))\} \frac{\{P (0)\} \{¬P (0), P (S(0))\}}{\{P (S(0))\}}}{\{P (S(S(0)))\}}

∅

This can be translated into the normal form (which is a refutation of C_{eq}^{∗}). The first part of this refutation is

\frac{\{P (z), ¬0 = x, ¬S(x) = y, ¬S(y) = z\} U}{\{¬0 = x, ¬S(x) = y, ¬S(y) = z\} (= D)}

where

U := \frac{\{¬P (y), P (z), ¬0 = x, ¬S(x) = y, ¬S(y) = z\} V}{\{P (z), ¬0 = x, ¬S(x) = y, ¬S(y) = z\}}

and where

V := \frac{\{P (x), ¬0 = x\} \{¬P (x), P (y), ¬0 = x, ¬S(x) = y\}}{\{P (y), ¬0 = x, ¬S(x) = y\}}

The last clause D determines the unification x ← 0, y ← S(0) and z ← S(S(0)). The last part of the refutation consists of the obvious refutation of the clause {¬0 = 0, ¬S(0) = S(0), ¬S(S(0)) = S(S(0))}.

Now let us show how we can turn the abstract derivation of D into propositional refutations of C_{n}^{prop}. For any i, j, k we have a derivation A_{i,j,k}:

\{¬p_{k}, ¬o_{i}, ¬s_{ij}, ¬s_{jk}\} \frac{\{¬p_{j}, p_{k}, ¬s_{ij}, ¬o_{i}, ¬s_{jk}\} \frac{\{p_{i}, ¬o_{i}\} \{¬p_{i}, p_{j}, ¬o_{i}, ¬s_{ij}\}}{\{p_{j}, ¬o_{i}.¬s_{ij}\}}}{\{p_{k}, ¬o_{i}, ¬s_{ij}, ¬s_{jk}\}}

{¬o_{i}, ¬s_{ij}, ¬s_{jk}} (= D_{ijk})

These derivations can now be resolved using the axioms in (4) and (5). First we derive {¬o_{i}, ¬s_{ij}} from the clauses {¬o_{i}, ¬s_{ij}, ¬s_{jk}} k = 1, 2, …, n and {s_{j1}, s_{j2}, …, s_{jn}}. Then we derive the clauses {¬o_{i}} from {¬o_{i}, ¬s_{ij}} j = 1, 2, …, n and {s_{i1}, s_{i2}, …, s_{in}}. Finally we derive the empty clause from {¬o_{i}} and {o_{1}, o_{2}, …, o_{n}}.

In this derivation each clause in (1)-(5) was used exactly once so C_{n}^{prop} has refutation which has n^{3} + n^{2} + 2n + 1 leaves. The derivation tree is a binary tree so the derivation uses 2n^{3} + 2n^{2} + 4n + 1 clause.

These considerations leads to Lemma 1: Assume C_{eq} is unsatisfiable. Then there exists l ∈ N such that for each n ≥ 2, there exists a tree-resolution refutation of C_{n}^{prop} of size ≤ n^{l}

Proof: Assume C_{eq} is unsatisfiable . Then C_{eq}^{∗} is unsatisfiable. According to Herbrand’s Theorem (see for example [19]) there exists a finite refutation of a suitable substitution instance. Actually there exists a finite tree-refutation on the normal form (described above). The first part of this refutation leads to a clause D of the form;

{¬h_{1}(z_{11}, …, z_{1r_{1}}) = z_{1,r_{1}+1}, ¬h_{2}(z_{21}, …, z_{2r_{2}}) = z_{2,r_{2}+1}, …,
…, ¬h_{u}(z_{u1}, …, z_{ur_{u}}) = z_{u,r_{u}+1}}

where each h_{j} denotes one of the function symbols f_{1}, f_{2}, …, f_{l} and where each z_{ij} denotes a variable (i.e. x, y, z, x_{ij}, y_{i_{1},i_{2},i_{3},...,i_{r}} etc). All the variables which are not among the variables on the right hand sides (i.e. the variables not among z_{1,r_{1}+1}, z_{2,r_{2}+1}, …, z_{u,r_{u}+1}) can be substituted with anything (for example c_{1}).

Consider all substitutions where the variables on the right hand sides (i.e. the variables z_{1,r_{1}+1}, z_{2,r_{2}+1}, …, z_{u,r_{u}+1}) are replaced by for constants in {c_{1}, c_{2}, …, c_{n}}. If there are u different atomic term equations in D, there are exactly n^{u} different derivations A_{i_{1},i_{2},...,i_{u}}. All together these derivations use at most HC(C_{eq}^{∗}) n^{u} different axioms.

The derivation A_{i_{1},i_{2},...,i_{u}} derives some clause D_{i_{1},i_{2},...,i_{u}}. Each clause D_{i_{1},i_{2},...,i_{u}} expresses the propositional version of a list of negations of basic atomic formulas. And each of these basic equations has all free variables replaced by constants from {c_{1}, c_{2}, …, c_{n}}.

Now we use the fact that D has an unification. The unification problem is to unify a list of the form

h_{1}(z_{11}, z_{12}, …, z_{1r_{1}}) = z_{1,r_{1}+1}, h_{2}(z_{21}, z_{22}, …, z_{2r_{2}}) = z_{2,r_{2}+1}, …,
…, h_{u}(z_{u1}, z_{u2}, …, z_{ur_{u}}) = z_{u,r_{u}+1}

All variables z_{ij} which do not appear among the variables z_{1,r_{1}+1}, z_{2,r_{2}+1}, …, z_{u,r_{u}+1} are substituted with c_{1} (or any other constant). Next notice that there is a natural partial ordering on the remaining variables. We define the ordering by defining z_{i,r_{1}+1} to dominate the variable z_{ij} if z_{ij} appears in h_{i}(z_{i1}, z_{i2}, …, z_{ir_{i}}) (as well as on the right hand side somewhere).

The fact that D has an unification ensures this is a well defined ordering ≺. Without loss of generality we can assume that the u variables in the notation of A_{i_{1},i_{2},...,i_{u}} have been displayed according to some total ordering which extends ≺.

The clause D_{i_{1},i_{2},...,i_{u}} (in the propositional notation) is of the form

{¬h_{i_{11},i_{12},...,i_{1r_{1}},i_{1}}^{1}, ¬h_{i_{21},i_{22},...,i_{2r_{2}},i_{2}}^{2}, …, ¬h_{i_{u1},i_{u2},...,i_{uru},i_{u}}^{u}}

Resolving with the clause {h_{i_{11},i_{12},...,i_{1r_{1}},1}^{1}, h_{i_{11},i_{12},...,i_{1r_{1}},2}^{1}, …, h_{i_{11},i_{12},...,i_{1r_{1}},n}^{1}} we derive the clauses D′_{i_{2},...,i_{u}}.

{¬h_{i_{21},i_{22},...,i_{2r_{2}},i_{2}}^{2}, …, ¬h_{i_{u1},i_{u2},...,i_{uru},i_{u}}^{u}}

Notice that the variable i_{1} does not appear elsewhere because the variable z_{1,r_{1}+1} was dominating all other terms. Now we precede and resolve the clauses D′_{i_{2},...,i_{u}} for i_{2} = 1, 2, 3, …, n with the clause {h_{i_{21},i_{22},...,i_{2r_{2}},1}^{2}, h_{i_{21},i_{22},...,i_{2r_{2}},2}^{2}, …, h_{i_{21},i_{22},...,i_{2r_{2}},n}^{2}} and derive the clauses D′′_{i_{3},...,i_{u}}

{¬h_{i_{31},i_{32},...,i_{3r_{3}},i_{3}}^{3}, …, ¬h_{i_{u1},i_{u2},...,i_{uru},i_{u}}^{u}}

We continue this procedure. Eventually we derive the empty clause. The number of clauses used in the leaves is at most HC(C) n^{u} where u is the number of atomic term equations in the clause D. The number u is bound by the number of function symbols which appear in the unification needed to refute C_{eq}. □ Please notice that it is the non circular relationship between the variables on the right hand sides of D which allows this procedure to go through. If D, for example, happens to be {¬S(x) = y, ¬S(y) = x} it would be impossible to translate {¬s_{ij}, ¬s_{ji}}_{ij} (as well as {s_{i1}, s_{i2}, …, s_{in}}_{i}) into a (polynomial size) resolution refutation. Well, the point of course is, that D can never be of the form {¬S(x) = y, ¬S(y) = x} because S(x) = y and S(y) = x (and thus S(S(x)) = x) have no unification.

Lemma 2: Assume C is not satisfied in any infinite model. Then there exists l ∈ N such that for each n ≥ 2, there exists a tree-refutation of C_{n}^{prop} of size ≤ n^{l}

Proof: If C has no infinite model according to the compactness theorem, it cannot have arbitrary large finite models. Assume C has no models of size ≥ n_{0}. Introduce constants c_{1}, c_{2}, …, c_{n_{0}} together with axioms {¬c_{i} = c_{j}} for i ≠ j. It is clear that the system C_{n_{0}}^{prop} is unsatisfiable. Now consider a general n ≥ n_{0}. According to Lemma 1 (with the obvious treatment of the constants c_{1}, c_{2}, …, c_{n_{0}}) there exists a tree-refutation of C_{n}^{prop} of size ≤ n^{l}. □

Corollary: In theorem 1, (1) implies (3) and (2) implies (3).

6 The exponential size lower bounds

For the lower bound it is convenient to view a tree-resolution refutation as a decision tree. This is essentially done by turning the refutation tree on its head (see for example [20]). On an input (i.e. a truth assignment) the decision tree outputs an unsatisfied clause. To illustrate the idea consider for example the tree-refutation:

\frac{\frac{\{p, r\} \{p̄, s\}}{\{r, s\}} \{r̄, s\}}{\{s\}} \{s̄\}

∅

The refutation shows that {{s̄}, {p, r}, {p̄, s}, {r̄, s}} is unsatisfiable. If we turn the refutation on its head we get the binary decision tree.

[figure: s?; r?; p?; {s’}; {r’, s}; 0; 1; 0; 0; 1; 1; {p , r}; {p’, s}; Decision tree refuting {{s’},{r’, s},{p’, s},{p , r}}]

For any truth assignment of the variables (s, p and r) the decision tree uniquely determines a clause which is unsatisfiable.

We want to give a lower bound on the number of clauses needed to refute C_{n}^{prop} in a tree-refutation. This is equivalent of giving a lower bound of the number of nodes required by a decision tree which output an unsatisfied clause.

Now the variables in the clauses in C_{n}^{prop} are basic atomic sentences where the variables are substituted by concrete constants chosen from {c_{1}, c_{2}, …, c_{n}}. Thus, we can view the decision tree as a decision tree which as input takes a model M of the language of C_{eq} extended by the constants {c_{1}, c_{2}, …, c_{n}}. The decision tree outputs a clause which is unsatisfied by M.

If we restrict the inputs to models M which satisfy the clauses in C, the decision tree never needs to output the clauses appearing from C_{eq}. Only clauses expressing ≤ n-ness and ≥ n-ness are needed because all other clauses are automatically satisfied. If we further restrict the input to only include such models M for which the constants c_{1}, c_{2}, …, c_{n} are interpreted as different elements, the decision tree only needs to output clauses expressing ≤ n-ness. These are clauses of the form {f(a_{1}, a_{2}, …, a_{r}) = c_{1}, …, f(a_{1}, a_{2}, …, a_{r}) = c_{n}}.

All output nodes which do not output a clause expressing ≤ n-ness can be cancelled and the decision tree can be simplified until it is a binary decision tree T where all leaves have been assigned an axiom of ≤ n-ness.

Now we approach the key idea for the lower bound. We restrict the inputs further. We only consider inputs which are models M which have size ≥ n′ (n′ > n), which satisfy the clauses in C, and which have the constants c_{1}, c_{2}, …, c_{n}, c_{n+1}, … interpreted as different elements. Also we require that each element in M has a name c_{j} for some j. This extra requirement is permitted because if there is a model of C which has size n′ then there is also such a model for which each of the constants c_{1}, c_{2}, ..... denotes its elements (skolem-lowenheims theorem is needed if we only want to consider at most countable many constants c_{α}, α ∈ I).

This restriction on the inputs allows us to simplify the decision tree T further. All nodes which correspond to outputs which can never be achieved can be removed. This leads to a decision tree T′.

Now the lower bound is almost trivial. Suppose that C has a model of size ≥ n′. The model might be finite or infinite. We want to see what impact this has on the size of tree-resolution refutations of C_{n}^{prop}.

The key observation is that each constant c_{1}, c_{2}, …, c_{n} must appear along each computational path through T′.

Lemma 3: Assume there are models M of C which have size > n. Then each computational path through T′ must involves each of the constants c_{1}, c_{2}, …, c_{n}.

Proof: Assume some branch does not involve the constant c′ ∈ {c_{1}, c_{2}, …, c_{n}}. The branch leads to a leaf l which has been assigned a clause on the form {f(c_{i_{1}}, c_{i_{2}}, …, c_{i_{r}}) = c_{1}, f(c_{i_{1}}, c_{i_{2}}, …, c_{i_{r}}) = c_{2}, …, f(c_{i_{1}}, c_{i_{2}}, …, c_{i_{r}}) = c_{n}}.

None of the inputs M which lead to the leaf l will have f(c_{i_{1}}, c_{i_{2}}, …, c_{i_{r}}) = c′. The decision tree T′ does not involve any of the constants c_{n+1}, c_{n+2}, …, c_{n′} ( or c_{n+1}, c_{n+2}, … if n′ = ∞) so none of the inputs M which lead to the leaf l will have f(c_{i_{1}}, c_{i_{2}}, …, c_{i_{r}}) = c_{j} for some j = n + 1, n + 2, …, n′ (if this was the case, we get a contradiction by replacing the input M with a model M′ in which the interpretation of c′ and c_{j} is interchanged). But then all models M which lead to the leaf l fail to satisfy f(c_{i_{1}}, c_{i_{2}}, …, c_{i_{r}}) = c for any constant c. Now we only considered inputs being models M for which each element has a name. Thus each model M which leads to the leaf l must have ∀x ¬f(c_{i_{1}}, c_{i_{2}}, …, c_{i_{r}}) = x. This sentence is a logical contradiction. This is a contradiction to the fact that T′ was constructed in such a way that there actually was some permissible input M leading to l. □

From this we get:

Lemma 4: Assume n is given, and that there is a model of C which has size n′ for some n′ > n. Here n′ = ∞ if C has an infinite model. Then there is no tree-refutation of C_{n}^{prop} which has size < 2^{n/max(k_{C}^{rel},1+k_{C}^{fun})}.

Thus (3) implies (1) and (2) in Theorem 1. This, in conjunction with the upper bounds, complete the proof of the first part of Theorem 1. The remaining part follows from the fact that the set of finite satisfiability problem C (for predicate logic) which is satisfiable in an infinite model is non-recursive. Actually the complement - the set of finite satisfiability problems C which has no infinite model - is r.e. complete.

Finally - to complete the proof of the Gap Theorem - we have to show that there is no total recursive function which given input C, outputs u ∈ N such that n^{u} > S_{C}(n) whenever (1),(2) or (3) fails. If such total recursive function existed, we could use property (2) to provide a bound on smallest n_{0} with C_{n}^{prop} unsatisfiable for each n ≥ n_{0}. This would give us a decision procedure to decide whether C has an infinite model. It is well known that the existence of such a decision procedure leads to a contradiction. This completes the proof of the Gap Theorem.

7 Further perspectives

Up to this point we have considered uniform sequences C_{n}^{prop} of unsatisfiability problems. Notice however that our polynomial upper bound was achieved by highly uniform families of tree-refutations. This raises a crucial question. Given a propositional proof system P. When does P have the property that uniform generated (i.e. S_{n}-generated) sequences of tautologies which have short P -proofs have short uniformly (here used in an informal sense) generated P -proofs? In this paper we have seen that tree-resolution has this property.

Let T_{total} denote the mathematical theory which is axiomatised by all existential sentences ψ which are valid in all finite models (the sentences are written in an infinite language with an arbitrary number of function and relation symbols of each arity). This theory consists of the class of first order formulas which hold in all finite models. Notice that T_{total} is a well-defined theory because the property of being valid in all finite models is closed under logical deduction. The list of sentences in T_{total} forms a complete co-recursively enumerable set. Thus T_{total} is not recursively axiomatisable.

Given a propositional proof system P. In general we let T_{P} ⊆ T_{total} denote the collection of existential sentences ψ ∈ T_{total} for which the sequence ψ_{n} has polynomial size (or for example n^{log(n)^{o(1)}}-size) P -proofs.

Let ψ be a sentence (formula) in predicate logic. Assume for example ψ :≡ ∀x∃y∀zR(x, y, z). The sentence (formula) ψ′ :≡ ∃yR(c, y, f(y)) is a skolemisation of ψ. Clearly ψ implies ψ′ while ψ′ does not implies ψ in general. In our context, things are very nice because we consider validity in a class of models (rather than validity in a single model). Notice that ψ holds in the class of all finite models if and only if ψ′ holds in the class of all finite models. Often a sentence has more than one skolemisation. Using [4] it is possible to show that there exists a sequence of sentences ψ_{u} (in predicate logic) as well as two sequences ψ′_{u} and ψ′′_{u} such that ψ′_{u} and ψ′′_{u} both are skolemisations of ψ_{u} and such that the term-complexity as well as the Herbrand complexity of ψ′′_{u} is 2_{u}-times larger than the term complexity as well as the Herbrand complexity of ψ′_{u} (here 2_{l+1} := 2^{2_{l}} and 2_{0} = 1). The function 2_{u} has a non-elementary growth rate.

Theorem 4: For any reasonable (see proof for details) propositional system P, T_{p} is a well defined mathematical theory closed under logical deduction. More specifically T_{p} is closed under logical deduction in the following sense: Let ψ be an arbitrary sentence (not necessarily an existential sentence) which is a logical consequence of T_{p}. Then for any skolemisation of ψ turning it into an equivalent existential sentence ψ′, the sequence ψ′_{n} have polynomial size P -proofs (i.e. ψ′ ∈ T_{p}). If ψ′′ is another skolemisation there are examples which show that the polynomial tree-resolution refutation complexity of (ψ′′)_{n} might have a degree which is non-elementarily larger than the degree of the tree-resolution refutation complexity of (ψ′)_{n}. Thus the polynomial complexity of the sequence tautologies arising from different skolemisations can vary grossly. Still the translation procedure leads to robust complexity results: Either all translations produce sequences which all have polynomial size treeresolution refutations or none of the translations produce sequences which have polynomial size tree-resolution refutations.

Proof:(outline) The property of having polynomial size propositional proofs is closed under logical deduction. We showed this for tree-resolution, but for stronger systems (which polynomially simulate tree-resolution) this property follows as a corollary. More specifically the skolemisation ψ′ is a logical consequence of ψ, and ψ is by assumption a logical consequence of T_{P}. Thus there exists a finite collection of axioms θ_{1}, θ_{2}, …, θ_{u} ∈ T_{P} such that η, a skolemisation of (θ_{1} ∧ θ_{2} ∧ … ∧ θ_{u} → ψ′), is a logical tautology as well as an appropriate existential sentence of the form we consider.

Our polynomial upper bound ensures that the sequence η_{n} has polynomial size P -proofs. By assumption, the sequences (θ_{1})_{n}, (θ_{2})_{n} … (θ_{k})_{n} each have polynomial size P -proofs. The intuition tells us that in a reasonable propositional proof system this implies (η)_{n} ≡ (θ_{1})_{n} ∧ (θ_{2})_{n} ∧ … ∧ (θ_{k})_{n} → (ψ′)_{n} and thus the sequence ψ′_{n} has polynomial size P -proofs.

Some care is however needed at this stage, and we need to extend our upper bound result slightly. Let us assume that P is a refutation system which is at least as efficient as tree-resolution. The situation can then be described as follows: By assumption we have polynomial size refutations of the translation of the clauses {{l_{111}, l_{112}, …, l_{11k}}, {l_{121}, l_{122}, …, l_{12k}}, …, {l_{1k1}, l_{1k2}, …, l_{1kk}}} (the refutations of (¬θ_{1})_{n}). Here each literal l_{ijm} denotes a basic atomic sentence or the negation of a basic atomic sentence. To simplify the notation we have assumed (and we can clearly do this without loss of generality) that all index run between 1 and k. We also assume we have polynomial size P -refutations of the clauses {{l_{i11}, l_{i12}, …, l_{i1k}}, {l_{i21}, l_{i22}, …, l_{i2k}}, …, {l_{ik1}, l_{ik2}, …, l_{ikk}}} when i = 2, 3, …, k (refutations of (¬θ_{i})_{n} where i = 2, 3, …, k). By assumption we can refute the CNF formula θ :≡ ∧_{j=1}^{k} ∧_{π∈S_{k}} {¬l_{j1π(1)}, ¬l_{j2π(2)}, …, ¬l_{jkπ(k)}} ∧ ∧_{i=1}^{k} {m_{i1}, m_{i2}, …, m_{ik}} (θ is a CNF sentence (in predicate logic) which is logically equivalent to ¬η). According to our main result (the upper bound) there exists polynomial size tree-refutations of the propositional translations of θ. We want to show we can obtain polynomial size P -refutations of the CNF ∧_{i=1}^{k} {m_{i1}, m_{i2}, …, m_{ik}} (i.e. a refutation of ¬(ψ′)_{n}). To show this we need to assume P satisfies the following natural condition: Assumption (slightly informal): If A_{1} ∧ A_{2} … A_{k} → B has a derivation of size s, then the CNF of A_{1} ∧ A_{2} … A_{k−1} → (B ∨ ¬A_{k}) has a derivation of size s^{O(1)}.

This assumption suffices (we leave the rather tedious details to the reader) and ensures that it is possible to construct polynomial size P -refutation proofs of the propositional translations of ∧_{i=1}^{k} {m_{i1}, m_{i2}, …, m_{ik}}. This construction is very similar to the construction in our polynomial upper bound. We call a propositional system P as reasonable if it satisfies the polynomial upper bound for translations of tautologies (this happens, in particular, for all propositional proof systems which are stronger than tree-resolution) and satisfies the assumption above. This concludes the proof that T_{P} is a well defined and a well-behaved theory.

There exists a sequences of sentences ψ which have skolemisations ψ′ and ψ′′ which leads to unsatisfiability problems C_{ψ′} and C_{ψ′′} (of predicate logic) such that the Herbrand Complexity of the two systems differ with a nonelementary function (see [4] for details). Also the term complexity might differ by a non-elementary function. The canonical translation (we used for our upper bound) thus leads to tree-resolution refutations in which the degree in the polynomial complexity differs by a non-elementary function.

The final part of the theorem follows from the extension of our upper bound we already discussed. □

Notice that the assumption that P is a reasonable propositional system is a harmless assumption. Only reasonable propositional proof systems are relevant for complexity theory. An unreasonable propositional system can always be strengthened (by adding a few extra deduction rules) such that it becomes reasonable. All standard propositional systems are reasonable.

To show a super-polynomial lower bound for the propositional system P it suffices to show that T_{P} ≠ T_{total}. In this paper we showed that when P is tree-resolution then T_{P} is the minimal theory i.e. just predicate logic. For tree-resolution T_{P} is recursively axiomatisable (axiomatised by the empty set (!) of axioms over predicate logic). In general for stronger propositional proof systems T_{P} need not be recursively axiomatisable. It is a mistake to equate T_{P} with IΔ_{0}(α) (resp. V_{1}^{1} or U_{1}^{1}) when P is polynomial size bounded depth Frege proofs (resp. polynomial size extended Frege proofs or n^{log(n)^{o}(1)}-size Frege proofs) [remark: for readers who are not familiar with the theories IΔ_{0}(α), V_{1}^{1} or U_{1}^{1} it suffices to know that these are all recursively axiomatisable by universal axioms (see [17])]. The theory T_{P} is axiomatised by purely existential axioms and thus it behaves different from the theories (IΔ_{0}(α), V_{1}^{1} or U_{1}^{1}) which not are axiomatisable by purely existential axioms.

It is possible to formulate various interesting conjectures [27] concerning general properties of the axiomatisations of T_{P}. Here we only state the most general of these conjectures:

Conjecture: For any propositional proof system T_{P} ≠ T_{total}.

Using Cook’s and Reckhow’s reformulation of the NP ≠ co-NP question [13] we get:

Proposition: The conjecture implies NP ≠ co-NP.

The main aim in this section was to define the theory T_{P} (where P is an arbitrary propositional proof system). Our main result can now be stated as follows:

Theorem 5: Let P denote tree-resolution and let T_{P} (f) ⊆ T_{total} denote the theory of principles ψ ∈ T_{total} which have f(n)-size tree proofs (refutations).

The theory T_{P} (f) is well-defined as well as well-behaved (Theorem 4). Furthermore T_{P} (f) is the same theory (namely predicate logic) for any superpolynomial but sub-exponential function f(n).

8 General considerations

Consider the theory T_{P} (f) defined in the previous section. When the growth rate of f changes the theory T_{P} (f) might of course also change. The question is whether this change happens in a continuous manner or - as we have shown for tree-resolution - happens in jumps.

This touches a fundamental question in complexity theory. It is an empirical fact that only a relative small number of complexities appears in practice (e.g. θ(1), θ(\sqrt{log(n)/loglog(n)}), θ(log(n)/loglog(n)), θ(n), θ(nlogn), θ(n^{2}), 2^{n^{θ(1)}}). This phenomena is folklore, but to my knowledge there is at present no heuristic explanations of this.

Theoretically, virtually any complexity is possible, so why do so few complexities appear in practice? One feature of real world computational problems is that they in some sense involve the same general computational problem. It would, for example, be highly unnatural to consider a computational problem where certain lists have to be sorted for some values of n while certain bin-packing problems have to be solved for other values of n. Uniformity is clearly a feature of real world problems as we meet them in theoretical computer science. I hope the reader will forgive me these pure speculations, but perhaps uniformly (here used informally) given computational problems always have worst case complexities belonging to a finite list (including e.g. θ(1), θ(\sqrt{log(n)/loglog(n)}), θ(log(n)/loglog(n)), θ(n), θ(nlogn), θ(n^{2}), 2^{n^{θ(1)}}) of possibilities? Perhaps the fact that so few complexities appear in complexity theory are the shadows of a master theorem - a theorem which states that uniform complexity questions only can have certain possible answers (among finitely many possibilities). Or does this phenomena only reflect our limitations in showing matching upper and lower bounds? In the setting of propositional logic perhaps T_{P} (f) always makes at most finitely many jumps. Clearly (using Cook’s and Reckhow’s result [13]) if there is a complexity gap for any propositional system P we must have NP ≠ co-NP.

It is, of course, also possible that our gap-theorem is a rather singular phenomena which only occur for weak propositional proof systems (like treeresolution) where certain versions of the so-called weak pigeon-hole principle fails.

Let me point out that it is possible to extend the complexity gap theorem to a wider class of tautologies. In the present paper we solely focused on the propositional versions of the first finitisation principle [23]. This was mainly done to keep the proofs as simple as possible. It is possible to achieve a polynomial ↔ exponential complexity gap related to the propositional version of the second finitisation principle [23]. In order to keep the application of mathematical logic to a pleasant minimum we will not discuss this extension in the present paper.

Let me point out that there also is a complexity gap for the so-called Nullstellensatz proof system as well as for the Polynomial calculus. The exact size of this gap is still not completely settled. From [18] and [29] it is however clear that we essentially have a complexity jump from polynomial size NSproof (PS-proof) to at least n^{log(n)}. We suggest that the actual jump is from polynomial size to size 2^{o(n)}. This was claimed (with incomplete proof) in [30].

A very interesting question is to classify the collection of propositions Ψ which have polynomial size refutations for different propositional proof systems (or equivalently to characterise the theory T_{P}). Consider for example the NS-proof system (over fields of characteristic 0). This is a very interesting propositional proof system which has been studied intensively in the recent years. The system was first introduced in [5] and has many nice features [12]. We finish the paper by showing that the Nullstellensatz proof system proves the following version of the pigeon-hole principle.

For fixed n ∈ N consider the class Poly_{n} of polynomials in the variables x_{ij} where i ∈ {0, 1, 2, …, n} and j ∈ {1, 2, …, n}.

Consider the following polynomial equations:

( ∑_{j=1,j≠i}^{n} x_{ij}) + x_{ii} − 1 = 0 for i = 1, 2, …, n, ( ∑_{j=1}^{n} x_{0j}) − 1 = 0.

( ∑_{j=1,j≠i}^{n} x_{ji}) + x_{ii} + x_{0i} − 1 = 0 for i = 1, 2, …, n.

These equations have no 0/1-solution as such a solution would define a bijection from {0, 1, …, n} onto {1, 2, …, n}. Actually we show:

Proposition: The equations do not have any solutions over any ring.

Proof: Notice that

∑_{i=1}^{n}(( ∑_{j=1,j≠i}^{n} x_{ij})+x_{ii} +x_{0i} −1)− ∑_{i=1}^{n}(( ∑_{j=1,j≠i}^{n} x_{ji})+x_{ii} −1)−(∑_{j=1}^{n} x_{0j})−1 = 1

and that 1 thus can be written as a linear combination of the polynomials which appear in the polynomial equations. □

The tautologies for the usual pigeonhole principle is an extension of the above equations. Besides the equations above, they include:

x_{ij}^{2} − x_{ij} = 0, where i ∈ {0, 1, 2, …, n} and j ∈ {1, 2, …, n}. x_{ij}x_{ik} = 0 for i ∈ {0, 1, 2, …, n} and j, k ∈ {1, 2, …, n} with j ≠ k.

x_{ji}x_{ki} = 0 for i ∈ {1, 2, …, n} and j, k ∈ {0, 1, 2, …, n} with j ≠ k.

It is well known that the bijective pigeon-hole principle requires exponential size bounded depth Frege proofs [7]. Thus we have:

Theorem 6: There exists a sequence of tautologies which has linear size Nullstellensatz proofs, but require exponential size bounded depth Frege Proofs.

This shows that the strength of the NS-proof system is incompatible to Bounded Depth Frege. It also shows that the complexity gap for the NS-proof system does not take place at the same place as for tree-resolution (i.e. T_{TR} ⊂ T_{NS} with T_{TR} ≠ T_{NS}). An exact characterisation of T_{NS}, i.e. an exact characterisation of the class of C_{n}’s which have polynomial size NS-proofs, is open. Is the theory T_{NS} recursively axiomatisable? Also the size of the complexity jump for the NS-proof system is open although some special cases has been settled [29]. The same questions for bounded depth Frege are open, and any answer has to involve ideas beyond current techniques. Does the cutting plane propositional proof system have a complexity gap? Does unrestricted resolution? Does the unrestricted resolution system have a gap-theorem similar to that for tree-resolution?

To end I would like to thank Peter Bro Miltersen and Ulrich Kohlenbach for their useful comments related to this paper.

References

[1] Ajtai, M.: The complexity of the pigeonhole principle. In 29th Annual Symposium on Foundations of Computer Science, IEEE (1988) pp. 346-355.

[2] Ajtai, M.: The complexity of the pigeonhole principle. Combinatorica, 14(4) (1994) pp. 417-433.

[3] Ajtai, M.: The independence of the modulo p counting principles. In Proceedings of the 26th ACM STOC, (1994) 402-411

[4] Baaz, M.,Leitsch, A.: On Slolemization and proof complexity. Fund. Inform. 20 no. 4 (1994) 353-379

[5] Beame, P., Impagliazzo, R., Krajicek, J., Pitassi, T., Pudlak, P.: Lower bounds on Hilbert’s Nullstellensatz and propositional proofs. Proceedings of the London Mathematical Society 73(3) 1-26 (1996)

[6] Beame, P.,Karp R., Pitassi T., Saks M.: On the complexity of Unsatisfiability Proofs for Random k-CNF Formulas. STOC 98. The 30th ACM STOC, (1998)

[7] Beame, P.,Impagliazzo, R.,Krajicek, J., Pitassi,T.,Pudlak,P., Woods,A.: Exponential lower bounds for the pigeonhole principle, In the proceedings of the 24th ACM STOC 200-221 (1992)

[8] Beame, P., Riis, S.: More on the relative strength of counting principles. In: Proceedings of the DIMACS workshop on Feasible Arithmetic and Complexity of Proofs, (1996)

[9] Buss, S.: The propositional pigeonhole principle has polynomial size Frege proofs, J. of Symbolic Logic, 52 (1987) 916-927

[10] Buss, S.: Propositional consistency proofs, Annals of Pure and Applied Logic 52 (1991) 3-29

[11] Buss, S., Pitassi, T.: Resolution and the weak Pigeonhole Principle (notes).

[12] Buss, S., Krajicek, j,. Pitassi, T., Razborov, A., Sergal, J.: Polynomial bound on Nullstellensatz for counting principles. To appear in Computational Complexity (1997)

[13] Cook, S., Reckhow, R.: The relative efficiency of propositional proof systems, Journal of Symbolic Logic, 44 (1979) 36-50.

[14] Galil, Z.: On the complexity of regular resolution and the Davis-Putnam procedure. Theoretical Computer Science, 4 (1977) 23-46

[15] Kearns, Vazirani: An Introduction to Computational Learning Theory, MIT Press, (1994)

[16] Haken, A.: The intractability of resolution, Theoretical Computer Science, 39 (1985), 297-308.

[17] Krajicek, J.:Bounded Arithmetic, propositional logic, and complexity theory, Encyclopedia of Mathematics and Its Applications, Vol. 60, Cambridge University Press (1995)

[18] Krajicek, J.: On the degree of ideal membership proofs from uniform families of polynomials over a finite field (manuscript)

[19] Leitsch, A.: The resolution Calculus. Book in the series of Texts in Theoretical Computer Science, Ed. Brauer, W., Rozenberg, G., Salomaa, A. Springer / Heidelberg (1996)

[20] Lovasz, L. Naor,M., Newman,I.,Wigderson,A. Search problems in the decision tree model. In Proceedings of the 32th ACM STOC, (1991) 576-585

[21] Pudlak, P.: On the length of proofs of finitistic consistency statements in first order theories, in: J.B. Paris et al., eds, Logic Colloquium ’84 North-Holland, Amsterdam (1986) 165-196

[22] Pudlak, P.: Improved bounds to the lengths of proofs of finitistic consistency statements, in: Logic and combinatorics, Contemporary Math. 65 (Amer. Math. Soc., Providence, RI (1987) 309-331.

[23] Riis, S.: Making infinite structures finite in models of Second Order Bounded Arithmetic. In: Arithmetic, proof theory and computorial complexity, 289-319, Oxford: Oxford University Press 1993

[24] Riis, S.: Independence in Bounded Arithmetic. DPhil dissertation, Oxford University (1993)

[25] Riis, S.: Count(q) does not imply Count(p) Annals of Pure and Applied Logic, 90(1-3) (1997) 1-56

[26] Riis, S.: Count(q) versus the pigeon-hole principle. Archive for Mathematical Logic 36 (1997) 157-188

[27] Riis, S.: (manuscript in preparation)

[28] Riis, S., Sitharam, M: Generating hard tautologies using logic and the symmetric group. BRICS RS-98-19.

[29] Riis, S., Sitharam, M: Uniformly Generated Submodules of Permutation Modules. BRICS RS-98-20.

[30] Riis, S., Sitharam, M: (manuscript in preparation). Incomplete version appear as: Non-constant Degree Lower Bounds imply Linear Degree Lower Bounds, Technical report TR97-048 of the Electronic Colloquium on Computational Complexity, http://www.eccc.uni-trier.de/pub/eccc (1997)

[31] Simpson,S.: Unprovable theorem and fast growing functions. Contempora Mathematics Vol 65 (1987) 359-394

[32] Tseitin, G.S.: On the complexity of derivations in the propositional Calculus. In A.O. Slisenko, editor, Studies in Constructive Mathematics and Mathematical Logic, Part II (1968)

[33] Urquhart, A.: Hard examples for resolution. Journal of the ACM, 34(1) (1987) 209-219.

[34] Urquhart, A.: The Complexity of Propositional Proofs. The Bulletin of Symbolic Logic, 1 (1995) 425-467

Recent BRICS Report Series Publications

RS-99-29 Søren Riis. A Complexity Gap for Tree-Resolution. September 1999. 33 pp.

RS-99-28 Thomas Troels Hildebrandt. A Fully Abstract Presheaf Semantics of SCCS with Finite Delay. September 1999. 37 pp. To appear in Category Theory and Computer Science: 8th International Conference, CTCS ’99 Proceedings, ENTCS, 1999.

RS-99-27 Olivier Danvy and Ulrik P. Schultz. Lambda-Dropping: Transforming Recursive Equations into Programs with Block Structure. September 1999. 57 pp. To appear in the November 2000 issue of Theoretical Computer Science. This revised report supersedes the earlier BRICS report RS-98-54.

RS-99-26 Jesper G. Henriksen. An Expressive Extension of TLC. September 1999. 20 pp. To appear in Thiagarajan and Yap, editors, Fifth Asian Computing Science Conference, ASIAN ’99 Proceedings, LNCS, 1999.

RS-99-25 Gerth Stølting Brodal and Christian N. S. Pedersen. Finding Maximal Quasiperiodicities in Strings. September 1999. 20 pp.

RS-99-24 Luca Aceto, Willem Jan Fokkink, and Chris Verhoef. Conservative Extension in Structural Operational Semantics. September 1999. 23 pp. To appear in the Bulletin of the EATCS.

RS-99-23 Olivier Danvy, Belmina Dzafic, and Frank Pfenning. On proving syntactic properties of CPS programs. August 1999. 14 pp. To appear in Gordon and Pitts, editors, 3rd Workshop on Higher Order Operational Techniques in Semantics, HOOTS ’99 Proceedings, ENTCS, 1999.

RS-99-22 Luca Aceto, Zoltán Ésik, and Anna Ingólfsdóttir. On the Two-Variable Fragment of the Equational Theory of the Max-Sum Algebra of the Natural Numbers. August 1999. 22 pp.

RS-99-21 Olivier Danvy. An Extensional Characterization of Lambda-Lifting and Lambda-Dropping. August 1999. 13 pp. Extended version of an article to appear in Fourth Fuji International Symposium on Functional and Logic Programming, FLOPS ’99 Proceedings (Tsukuba, Japan, November 11–13, 1999). This report supersedes the earlier BRICS report RS-98-2.