Por Gabriele Pulcini (FCT, Universidade Nova de Lisboa).

Abstract: In the first part of my talk, I'll consider 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, it is not provable in LK. I'll show how to enrich LK° with two admissible (unary) cut rules, which allow for a simple and efficient cut-elimination algorithm. I’ll then highlight two facts: 1) complementary cut-elimination always returns the simplest proof for any given provable sequent, and 2) provable complementary sequents turn out to be "deductively polarized" by the empty sequent.

In the second part, I'll observe how an alternative sequent system for complementary classical logic can be obtained by slightly modifying Kleene's system G4. I'll show how this move could pave the way for a new approach to many-valuedness and proof-theoretic semantics.