Non-strictly positive fixed points for classical natural deduction (Q1772778): Difference between revisions

The object of investigation of this paper is the classical second-order \(\lambda\mu\)-calculus with disjunction and the rule RAA (reductio ad absurdum). The author presents two proofs of strong normalization; every reduction of a typed term terminates in a finite number of steps. These proofs are of dual nature. The first is ``introduction-based'', and of the nature of \textit{W. W. Tait}'s realizability interpretation [Lect. Notes Math. 453, 240--251 (1975; Zbl 0328.02014)]; while the second is ``elimination-based'', and of \textit{M. Parigot}'s approach with reducibility candidates [J. Symb. Log. 62, 1461--1479 (1997; Zbl 0941.03063)]. In the first approach, the author's notion of saturated sets (of terms) is new, and he further shows that this approach works for the extended system with the non-strictly positive fixed points operator. Throughout the paper, the author gives abundant reference to the literature, with comments and comparisons. So, this paper has the flavor of being a survey.