# Gabriele Pulcini

## From complementary logic to proof-theoretic semantics

In the first part of my talk, I shall be concerned with $\overline{LK}$, a cut-free sequent calculus able to faithfully characterize classical (propositional) non-theorems, in the sense that a formula $A$ is provable in $\overline{LK}$ if, and only if, it is not provable in $LK$ (Tiomkin, 88; Goranko, 94). In particular, I will show how to enrich $\overline{LK}$ with two admissible (unary) cut-rules, which allow for a simple and efficient cut-elimination algorithm. I will then highlight two facts: 1) complementary cut-elimination always returns the simplest proof for any given invalid sequent, and 2) provable complementary sequents turn out to be deductively polarized by the empty sequent (Carnielli&Pulcini, 2017).

In the second part, I will provide a natural deduction system for complementary classical logic in terms of proof-nets and I will show how cut-elimination can be implemented directly on nets.

I will conclude the talk by observing how an alternative sequent system for complementary classical logic can be obtained by slightly modifying Gentzen-Schütte system $GS3$. This move could pave the way for a purely proof-theoretic account of multi-valuedness which, in turn, can be thought of as an alternative way to devise a proof-theoretic semantics for classical logic.