UNSOUND INFERENCES MAKE PROOFS SHORTER
Juan P. Aguilera, MATTHIAS BAAZ · Journal of Symbolic Logic · 2019
Abstract We give examples of calculi that extend Gentzen’s sequent calculusLKby unsound quantifier inferences in such a way that (i) derivations lead only to true sequents, and (ii) proofs therein are nonelementarily shorter thanLK-proofs.