Reference for normalization of propositional logic natural deduction.

Question

I'm looking for a reference for the normalization of classical propositional logic natural deduction. I have heard that D.Prawitz's book Natural Deduction is a good reference on the FOL. But first I want to study this on classical propositional logic. If you know any kind of reference, please let me know.

Answer 1

In Prawitz's Natural Deduction (1965) you can find a proof of normalization in classical natural deduction for the fragment $\bot, \land, \to, \forall$ of first-order logic. The presence of the universal quantifier $\forall$ does not complicate the proof of normalization, so you can read his proof and just forget about the case of $\forall$, so that you get a proof of normalization for the fragment $\bot, \land, \to$ of propositional logic.

As far as I know, the first proof of strong normalization for the full propositional classical natural deduction (including the disjunction $\lor$) is due to Stalmark's Normalization theorems for full first order classical natural deduction. Actually, in this paper there is a proof of normalization for full first-order classical natural deduction, including also the existential quantifier $\exists$. The kind of problems to manage normalization with $\exists$ are analogous to the ones to manage normalization with $\lor$, so as before, you can read his proof and just forget about the cases with $\forall $ and $\exists$ to have a proof of strong normalization for full propositional classical natural deduction.

Easy and recent proofs of strong normalization for full propositional classical natural deduction are due to David and Nour and to Nakazawa and Tastuta, both of them are essentially based on some variant of Parigot's $\lambda\mu$-calculus. The introductions and bibliographies of these papers are also a source for other references.