Normality, Non-contamination and Logical Depth in Classical Natural Deduction

Marcello D’Agostino*, Dov Gabbay, Sanjay Modgil

*Corresponding author for this work

Research output: Contribution to journalArticlepeer-review

7 Citations (Scopus)
132 Downloads (Pure)


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.

Original languageEnglish
Pages (from-to)291–357
Number of pages67
JournalStudia Logica
Issue number2
Early online date18 Feb 2019
Publication statusPublished - 30 Apr 2020


  • Classical propositional logic
  • Natural deduction
  • Non-contamination
  • Normal proofs
  • Tractable reasoning


Dive into the research topics of 'Normality, Non-contamination and Logical Depth in Classical Natural Deduction'. Together they form a unique fingerprint.

Cite this