On relativisation and complexity gap for resolution-based proof systems

Abstract

We study the proof complexity of Taut, the class of Second-Order Existential (SO∃) logical sentences which fail in all finite models. The Complexity-Gap theorem for Tree-like Resolution says that the shortest Tree-like Resolution refutation of any such sentence Φ is either fully exponential, 2Ω(n), or polynomial, nO(1), where n is the size of the finite model. Moreover, there is a very simple model-theoretics criteria which separates the two cases: the exponential lower bound holds if and only if Φ holds in some infinite model. In the present paper we prove several generalisations and extensions of the Complexity-Gap theorem. For a natural subclass of Taut, Rel(Taut), there is a gap between polynomial Tree-like Resolution proofs and sub-exponential, 2Ω(nε), general (DAG-like) Resolution proofs, whilst the separating model-theoretic criteria is the same as before. Rel(Taut) is the set of all sentences in Taut, relativised with respect to a unary predicate. The gap for stronger systems, Res∗(k), is between polynomial and exp(Ω(logkkn)) for every k, 1≤ k≤ n. Res∗(k) is an extension of Tree-like Resolution, in which literals are replaced by terms (i.e. conjunctions of literals) of size at most k. The lower bound is tight. There is (as expected) no gap for any propositional proof system (including Tree-like Resolution) if we enrich the language of SO logic by a built-in order.