Ordinal analysis of terms of finite type

DOI10.2307/2273417zbMath0444.03029OpenAlexW2030975201MaRDI QIDQ3887455

William Alvin Howard

Publication date: 1980

Published in: Journal of Symbolic Logic (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.2307/2273417

zbMATH Keywords

ordinal notationsSkolem arithmetictransfinite recursioncomputation treeterms for primitive recursive functionals of finite type

Mathematics Subject Classification ID

Functionals in proof theory (03F10) Recursive ordinals and ordinal notations (03F15)

Related Items

Continuity of Gödel's system T definable functionals via effectful forcing, Upper bounds for standardizations and an application, Combinatory logic with polymorphic types, An upper bound for reduction sequences in the typed \(\lambda\)-calculus, Strong normalization from weak normalization in typed \(\lambda\)-calculi, Term extraction and Ramsey's theorem for pairs, Representing definable functions of \(\mathrm{HA}^{\omega}\) by neighbourhood functions, Unnamed Item, Primitive recursion and the chain antichain principle, How to assign ordinal numbers to combinatory terms with polymorphic types, On the Cantor–Bendixson rank of a set that is searchable in Gödel’s T, Reduction of higher type levels by means of an ordinal analysis of finite terms, Ordinal analysis of simple cases of bar recursion, Perpetual reductions in \(\lambda\)-calculus

Cites Work

• Functionals defined by recursion