Non-strictly positive fixed points for classical natural deduction (Q1772778): Difference between revisions
From MaRDI portal
Created a new Item |
Added link to MaRDI item. |
||
links / mardi / name | links / mardi / name | ||
Revision as of 07:50, 1 February 2024
scientific article
Language | Label | Description | Also known as |
---|---|---|---|
English | Non-strictly positive fixed points for classical natural deduction |
scientific article |
Statements
Non-strictly positive fixed points for classical natural deduction (English)
0 references
21 April 2005
0 references
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.
0 references
classical \(\lambda\mu\)-calculus
0 references
strong normalization
0 references
fixed point operator
0 references