 The central metatheorem about natural deduction is the Normalization theorem, to the effect that proofs in a natural deduction system can be transformed into a “normal form”, informally characterized by Gentzen as “not being roundabout”. This theorem applies to the full systems for first order logic, though in what follows we will, in order to give a “flavour” of the result and the method of proving it, describe only the propositional fragment.