A Closer Look at Some Recent Proof Compression-Related Claims
Michael C. Chavrimootoo, Ethan Ferland, Erin Gibson, Ashley, H. Wilson

TL;DR
This paper critically examines recent claims about proof compression in propositional logic, showing that previous proofs of polynomial size bounds are flawed, thus invalidating related complexity class equalities.
Contribution
The paper identifies gaps in prior proof compression arguments and demonstrates that their polynomial size bounds do not hold, challenging claims about NP=PSPACE.
Findings
Previous proof compression claims are incorrect.
Polynomial size bounds for minimal propositional logic proofs are not established.
Consequently, the proof that NP=PSPACE based on these bounds is invalid.
Abstract
Gordeev and Haeusler [GH19] claim that each tautology of minimal propositional logic can be proved with a natural deduction of size polynomial in . This builds on work from Hudelmaier [Hud93] that found a similar result for intuitionistic propositional logic, but for which only the height of the proof was polynomially bounded, not the overall size. They arrive at this result by transforming a proof in Hudelmaier's sequent calculus into an equivalent tree-like proof in Prawitz's system of natural deduction, and then compressing the tree-like proof into an equivalent DAG-like proof in such a way that a polynomial bound on the height and foundation implies a polynomial bound on the overall size. Our paper, however, observes that this construction was performed only on minimal implicational logic, which we show to be weaker than the minimal propositional logic for which they…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsLogic, Reasoning, and Knowledge · Advanced Algebra and Logic · Computability, Logic, AI Algorithms
