Iterated lower bound formulas: a diagonalization-based approach to proof complexity

We propose a diagonalization-based approach to several important questions in proof complexity. We illustrate this approach in the context of the algebraic proof system IPS and in the context of propositional proof systems more generally.

We give an explicit sequence of CNF formulas φ n such that VNP = VP iff there are no polynomial-size IPS proofs for the formulas φ n . This provides the first natural equivalence between proof complexity lower bounds and standard algebraic complexity lower bounds. Our proof of this fact uses the implication from IPS lower bounds to algebraic complexity lower bounds due to Grochow and Pitassi together with a diagonalization argument: the formulas φ n themselves assert the non-existence of short IPS proofs for formulas encoding VNP = VP at a different input length. Our result also has meta-mathematical implications: it gives evidence for the difficulty of proving strong lower bounds for IPS within IPS.

More generally, for any strong enough propositional proof system R we propose a new explicit hard candidate, the iterated R-lower bound formulas, which inductively asserts the non-existence of short R proofs for formulas encoding this same statement at a different input length. We show that these formulas are unconditionally hard for Resolution following recent results of Atserias and Müller and of Garlik. We further give evidence in favour of this hypothesis for other proof systems.