In this article, we consider LK, a cut-free sequent calculus able to faithfully characterize classical (propositional) nontheorems, in the sense that a formula φ is provable in LK if, and only if, φ is not provable in LK, i.e., φ is not a classical tautology. The LK calculus is here enriched with two admissible (unary) cut rules, which allow for a simple and efficient cut-elimination algorithm. We observe two facts: (i) complementary cut-elimination always returns the simplest proof for a given provable sequent, and (ii) provable complementary sequents turn out to be deductively polarized by the empty sequent.
Carnielli, W.a., Pulcini, G. (2017). Cut-elimination and deductive polarization in complementary classical logic. LOGIC JOURNAL OF THE IGPL, 25(3), 273-282 [10.1093/jigpal/jzx006].
Cut-elimination and deductive polarization in complementary classical logic
Pulcini G.
2017-01-01
Abstract
In this article, we consider LK, a cut-free sequent calculus able to faithfully characterize classical (propositional) nontheorems, in the sense that a formula φ is provable in LK if, and only if, φ is not provable in LK, i.e., φ is not a classical tautology. The LK calculus is here enriched with two admissible (unary) cut rules, which allow for a simple and efficient cut-elimination algorithm. We observe two facts: (i) complementary cut-elimination always returns the simplest proof for a given provable sequent, and (ii) provable complementary sequents turn out to be deductively polarized by the empty sequent.I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.