Normal Proofs, Cut Free Derivations and Structural Rules

from blog Home on consequently.org, | ↗ original
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 Jaśkowski’s...