On Relativisation and Complexity Gap

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^{\Omega \left(n\right)}\), or polynomial, \(n^{O\left(1\right)}\), 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. 1 For a natural subclass of Taut, \(Rel\left(Taut\right)\), there is a gap between polynomial Tree-like Resolution proofs and sub-exponential, \(2^{\Omega \left(n^{\varepsilon }\right)}\), general (DAG-like) Resolution proofs, whilst the separating model-theoretic criteria is the same as before. \(Rel\left(Taut\right)\) is the set of all sentences in Taut, relativised with respect to a unary predicate. 2 The gap for stronger systems, \(\textrm{Res}^{*}\left(k\right)\), is between polynomial and \(\exp \left(\Omega \left(\frac{\log k}{k}n\right)\right)\) for every k, 1≤ k ≤ n. \(\textrm{Res}^{*}\left(k\right)\) 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. 3 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.

Authors

• Stefan S. Dantchev
• Søren Riis

Keywords

No keywords are indexed for this paper.