Strong normalization of a symmetric lambda calculus for second-order classical logic (Q1407527)

We extend \textit{F. Barbanera} and \textit{S. Berardi}'s symmetric lambda calculus [Inf. Comput. 125, 103-117 (1996; Zbl 0853.68159)] to second-order propositional logic and prove its strong normalizability. The proof proceeds by extending Barbanera and Berardi's construction of reducibility to infinitary propositional logic, and reducibility candidates are defined as the class closed under such construction. A similar proof was found independently by \textit{M. Parigot} [Lect. Notes Comput. Sci. 1974, 442-453 (2000)].