Normal proofs, cut free derivations and structural rules

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.