Unsound Inferences Make Proofs Shorter
Juan P. Aguilera, Matthias Baaz
TL;DR
This paper presents calculi extending Gentzen's LK with unsound quantifier inferences that still produce only true sequents and result in significantly shorter proofs, challenging traditional proof complexity assumptions.
Contribution
It introduces new calculi with unsound inferences that maintain truthfulness and drastically reduce proof lengths compared to LK.
Findings
Derivations lead only to true sequents
Proofs are non-elementarily shorter than LK-proofs
Extends Gentzen's sequent calculus with unsound inferences
Abstract
We give examples of calculi that extend Gentzen's sequent calculus LK by unsound quantifier inferences in such a way that (i) derivations lead only to true sequents, and (ii) proofs therein are non-elementarily shorter than LK-proofs.
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.