Normal proofs, cut free derivations and structural rules

Greg Restall*

*Corresponding author for this work

Research output: Contribution to journalArticlepeer-review


Different natural deduction proof systems for intuitionistic and classical logic -and related logical systems-differ in fundamental properties while sharing significant family resemblances. These differences become quite stark when it comes to the structural rules of contraction and weakening. In this paper, I show how Gentzen and JaA > kowski's natural deduction systems differ in fine structure. I also motivate directed proof nets as another natural deduction system which shares some of the design features of Genzen and JaA > kowski's systems, but which differs again in its treatment of the structural rules, and has a range of virtues absent from traditional natural deduction systems.

Original languageEnglish
Pages (from-to)1143-1166
Number of pages24
JournalStudia Logica
Issue number6
Publication statusPublished - Dec 2014


  • Natural deduction
  • Normal proof
  • Sequent calculus
  • Structural rule
  • Proof net


Dive into the research topics of 'Normal proofs, cut free derivations and structural rules'. Together they form a unique fingerprint.

Cite this