 Ad 2: Noncanonical proofs are justified by reducing them to canonical ones. Thus reduction procedures (detour reductions) as used in normalization proofs play a crucial role. As they justify arguments, they are also called “justifications” by Prawitz. This definition again only applies to closed proofs, corresponding to the introduction form property of closed normal derivations in natural deduction (see section  1.3).