Natural deduction systems are historically and conceptually connected to assumption formation. Proofs are defined as derivations where all assumptions are discharged. In Prawitz’ Natural Deduction the systems for classical, intuitionistic and minimal logic are first defined with no discharging strategy (or with the so-called “savage” discharging strategy). Discharging functions were not used before the chapter devoted to modal logic. We know that although there is no difference in deductive power, the adoption of no discharging strategy/function has undesirable proof-theoretical consequences:

[a] No strong normalization; [b] No unicity of normal form; [c] No Curry-Howard.

The aim of this presentation is twofold:

[1] To examine the general role of dependency relations and discharging functions in proof-theory.

[2] (together with E, Hermann Haeusler) In a recent [still unpublished] paper, Prawitz was able to use, “in a seemingly magical way”, the techniques introduced by Gentzen in the second consistency proof in order to prove a normalization theorem directly for a natural deduction formulation of Peano’s Arithmetic. Prawitz’s proof solved a problem that resisted a satisfactory solution for more than 35 years: how to extend Gentzen’s proof to natural deduction, in particular, how to define the notion of level line, so fundamental in the case of sequent calculus, directly for natural deduction. Our second aim is to explore the way Prawitz’ result deals with the problem of assumption-substitution in order to obtain a new proof of strong normalization.