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

From MaRDI portal
Importer (talk | contribs)
Created a new Item
 
Added link to MaRDI item.
links / mardi / namelinks / 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
    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

    Identifiers