Palestrado: Prof. Gabriele Pulcini (16/05/17)

[Bruno Lopes]

Caros,

Amanhã, na PUC-Rio, haverá a palestra abaixo descrita do Prof. Gabriele Pulcini (Universidade Nova de Lisboa)

16/05/2017  - 10:00 Sala: 511

FROM COMPLEMENTARY LOGIC TO PROOF-THEORETIC SEMANTICS

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 to a new approach to proof-theoretic semantics.

Abraços,

Bruno.

-- 
Bruno Lopes
http://www.ic.uff.br/~bruno