A new normalization strategy for the implicational fragment of classical propositional logic (Q708929)

This paper gives a normalization theorem for the implicational fragment of classical logic in natural deduction, augmented by Pierce's Law \(((A\rightarrow B)\rightarrow A)\rightarrow A\) (the addition of Pierce's law is needed, since the purely implicational fragment of natural deduction is not complete). The normalization strategy in this paper is based on the method used by Seldin.