Cuts and cut-elimination for complementary classical logic

  • Walter Carnielli
  • Gabriele Pulcini


 This paper introduces LK, a cut-free sequent calculus able to faithfully characterize classical (propositional) non-theorems, in the sense that a formula a is provable in LK if, and only if, a is not provable in LK (i.e. a is not a tautology) [Tiomkin(1988), Bonatti(1993)]. This calculus is enriched with a set of admissible cut rules, which provide a cut-elimination algorithm. The calculus is also proved to be strong normalizing and strongly confluent.