3 ms·

For comparison, here are the natural deduction rules expressed in modern notation: https://leanprover.github.io/logic_and_proof/nd_quickref.html https://leanpr

• chalst 7y ago
  The most significant difference between Gentzen's original calculus and the way it is most often given today is that discharge of assumptions are associated with labels in modern calculus, so each discharged assumption is tied to a rule, whereas in Gentzen's calculus, all instances of that proposition are discharged. The innovation is essential to the Curry-Howard correspondence, because this labelling of assumptions matches variable bindings in typed lambda calculus.