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.

Carnielli, W.a., Pulcini, G. (2017). Cut-elimination and deductive polarization in complementary classical logic. LOGIC JOURNAL OF THE IGPL, 25(3), 273-282 [10.1093/jigpal/jzx006].

Cut-elimination and deductive polarization in complementary classical logic

Pulcini G.
2017-01-01

Abstract

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.
2017
Pubblicato
Rilevanza internazionale
Articolo
Esperti anonimi
Settore M-FIL/02 - LOGICA E FILOSOFIA DELLA SCIENZA
English
Complementary classical logic
Cut-elimination theorem
Refutation calculi
Carnielli, W.a., Pulcini, G. (2017). Cut-elimination and deductive polarization in complementary classical logic. LOGIC JOURNAL OF THE IGPL, 25(3), 273-282 [10.1093/jigpal/jzx006].
Carnielli, Wa; Pulcini, G
Articolo su rivista
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/2108/261228
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 8
  • ???jsp.display-item.citation.isi??? 5
social impact