Iterated lower bound formulas: a diagonalization-based approach to proof complexity
File(s)
Accepted version
Author(s)
Santhanam, Rahul
Tzameret, Iddo
Type
Journal Article
Abstract
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 (Ideal Proof System) and in the context of propositional proof systems more generally. We give an explicit sequence of formulas in conjuctive normal form (CNF) {𝜙𝑛} such that 𝖵𝖭𝖯 ≠𝖵𝖯 iff there are no polynomial-size IPS proofs for the formulas 𝜙𝑛. This provides a natural equivalence between proof size 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 𝜙𝑛 themselves assert the nonexistence of short IPS proofs for formulas encoding 𝖵𝖭𝖯 ≠𝖵𝖯 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 𝑅 we propose a new explicit hard candidate, the iterated 𝑅 -lower bound formulas, which inductively asserts the nonexistence of short 𝑅 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 favor of this hypothesis for other proof systems.
Date Issued
2025-06-10
Date Acceptance
2025-03-05
Citation
SIAM Journal on Computing, 2025, pp.313-349
ISSN
0097-5397
Publisher
Society for Industrial and Applied Mathematics
Start Page
313
End Page
349
Journal / Book Title
SIAM Journal on Computing
Copyright Statement
© 2025 Society for Industrial and Applied Mathematics. This is the author’s accepted manuscript made available under a CC-BY licence in accordance with Imperial’s Research Publications Open Access policy (www.imperial.ac.uk/oa-policy)
License URL
Publication Status
Published online
Date Publish Online
2025-06-10