Unsound Inferences Make Proofs Shorter
J. Symb. Log., Volume abs/1608.07703, 2019.
We give examples of calculi that extend Gentzenu0027s 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.
PPT (Upload PPT)