Cut-elimination and deductive polarization in complementary classical logic

Walter A. Carnielli, Gabriele Pulcini

Research output: Contribution to journalArticlepeer-review

7 Citations (Scopus)


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.

Original languageEnglish
Pages (from-to)273-282
Number of pages10
JournalLogic Journal of the IGPL
Issue number3
Publication statusPublished - 1 Jan 2017


  • Complementary classical logic
  • Cut-elimination theorem
  • Refutation calculi


Dive into the research topics of 'Cut-elimination and deductive polarization in complementary classical logic'. Together they form a unique fingerprint.

Cite this