Cut-elimination and deductive polarization in complementary classical logic. (10th April 2017)

• Record Type: Journal Article
• Authors: Carnielli, Walter A.; Pulcini, Gabriele
• Is Part Of: Logic journal of the IGPL. Volume 25:Number 3(2017:Jun.)
• Page Start: 273
• Page End: 282
• Publication Date: 2017-04-10
• Subjects: Complementary classical logic -- refutation calculi -- cut-elimination theorem; Logic, Symbolic and mathematical -- Periodicals; 511.3
• DOI: 10.1093/jigpal/jzx006
• Languages: English
• ISSNs: 1367-0751

Abstract

Abstract: In this article, we consider $\overline{\mathsf{LK}}$, a cut-free sequent calculus able to faithfully characterize classical (propositional) non-theorems, in the sense that a formula $\varphi$ is provable in $\overline{\mathsf{LK}}$ if, and only if, $\varphi$ is not provable in $\mathsf{LK}$, i.e., $\varphi$ is not a classical tautology. The $\overline{\mathsf{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.