Reduction of higher type levels by means of an ordinal analysis of finite terms
type: Item
instance of: scholarly article
title: Reduction of higher type levels by means of an ordinal analysis of finite terms
zbMATH Open document ID: 0554.03024
DOI: 10.1016/0168-0072(85)90031-4
author: Jan Terlouw
published in: Annals of Pure and Applied Logic
publication date: 1985-01-01T00:00:00Z
full work available at URL: 1 s2.0 0168007285900314 main.pdf
review text: The main contribution of this paper is a new method to obtain assignments of ordinals to all finite terms (in extensions of Gödel's T by transfinite recursion) with the property that successors of a term (in the style of Sanchis) always get smaller ordinals. Although the author states on p. 2 that his work has been strongly inspired by Howard's approach [\textit{W. A. Howard}, J. Symb. Logic 45, 493-504 (1980; Zbl 0444.03029)], in my opinion he really has achieved something new, which is technically highly non-trivial. The usefulness of the result is documented by just one application (elimination of higher type levels) but it seems likely that further applications of his method can be found. The only criticism I have is that the author's approach is rather formal when compared with Howard's. Howard has succeeded to combine the intuitive clarity of Tait's analysis using infinite terms, where the associated ordinal is just the length of the term, with the simplicity of a system of finite terms. In Howard's paper the fact that reducing the degree of a term by one corresponds to raising its ordinal \(\alpha\) to \(\omega^{\alpha}\) is clearly explained by an analysis, where finite sequences of certain subterms come up naturally. In the paper under review I could not find an equally convincing explanation of this phenomenon. Technically, the paper is written very carefully and all proofs I have checked are given with just the right amount of detail.
reviewed by: Helmut Schwichtenberg
Mathematics Subject Classification ID: 03D65
Mathematics Subject Classification ID: 03D20
Mathematics Subject Classification ID: 03F05
zbMATH DE Number: 3882416
zbMATH Keywords: ordinal assignments
zbMATH Keywords: finite terms
zbMATH Keywords: elimination of higher type levels
MaRDI profile type: MaRDI publication profile
OpenAlex ID: W2133262398
cites work: The lambda calculus, its syntax and semantics
cites work: Ordinal analysis of terms of finite type
cites work: Recursion on the countable functionals
cites work: Q5533181
cites work: Functionals defined by recursion
cites work: Q4079601
cites work: Nested recursion
cites work: On definition trees of ordinal recursive functionals: Reduction of the recursion orders by means of type level raising
Recommended article: Q4218926
Recommended article: A proof of strongly uniform termination for Gödel's \(T\) by methods from local predicativity
Recommended article: How is it that infinitary methods can be applied to finitary mathematics? Gödel's T: a case study
Recommended article: Tarskian and Kripkean truth
Recommended article: Complexity of Gödel’s T in λ-Formulation
Recommended article: Derivation lengths classification of Gödel's T extending Howard's assignment
Recommended article: Consistency proof via pointwise induction
Recommended article: Q4934564
Recommended article: Techniques of admissible recursion theory
Recommended article: Ptykes in Gödels T und Definierbarkeit von Ordinalzahlen. (Ptykes in Gödel's T and definability of ordinal numbers)
description: scientific article; zbMATH DE number 3882416