In this paper we provide a detailed proof-theoretical analysis of a natural deduction system for classical propositional logic that (i) represents classical proofs in a more natural way than standard Gentzen-style natural deduction, (ii) admits of a simple normalization procedure such that normal proofs enjoy the Weak Subformula Property, (iii) provides the means to prove a Non-contamination Property of normal proofs that is not satisfied by normal proofs in the Gentzen tradition and is useful for applications, especially in formal argumentation, (iv) naturally leads to defining a notion of depth of a proof, to the effect that, for every fixed natural k, normal k-depth deducibility is a tractable problem and converges to classical deducibility as k tends to infinity.
Normality, Non-contamination and Logical Depth in Classical Natural Deduction / M. D’Agostino, D. Gabbay, S. Modgil. - In: STUDIA LOGICA. - ISSN 0039-3215. - 108:2(2020 Apr 01), pp. 291-357.
Titolo: | Normality, Non-contamination and Logical Depth in Classical Natural Deduction |
Autori: | |
Parole Chiave: | Natural deduction; Classical propositional logic; Normal proofs; Non-contamination; Tractable reasoning |
Settore Scientifico Disciplinare: | Settore M-FIL/02 - Logica e Filosofia della Scienza Settore MAT/01 - Logica Matematica |
Data di pubblicazione: | 1-apr-2020 |
Rivista: | |
Tipologia: | Article (author) |
Data ahead of print / Data di stampa: | 23-mar-2019 |
Digital Object Identifier (DOI): | http://dx.doi.org/10.1007/s11225-019-09847-4 |
Appare nelle tipologie: | 01 - Articolo su periodico |
File in questo prodotto:
File | Descrizione | Tipologia | Licenza | |
---|---|---|---|---|
DAgostino2019_Article_NormalityNon-contaminationAndL.pdf | Publisher's version/PDF | Administrator Richiedi una copia | ||
NNC_rev2.pdf | Post-print, accepted manuscript ecc. (versione accettata dall'editore) | Open Access Visualizza/Apri |