On definition trees of ordinal recursive functionals: Reduction of the recursion orders by means of type level raising

DOI10.2307/2273149zbMath0488.03030OpenAlexW2103403562MaRDI QIDQ3949042

Jan Terlouw

Publication date: 1982

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

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

zbMATH Keywords

definability of functionalsfunctional of type level nfunctionals of finite typesnumber-theoretic functions definable by nested recursionscheme of degree nwell-ordering of the set of natural numbers

Mathematics Subject Classification ID

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

Related Items

Constructing recursion operators in intuitionistic type theory ⋮ How to assign ordinal numbers to combinatory terms with polymorphic types ⋮ Characterizing complexity classes by higher type primitive recursive definitions ⋮ Reduction of higher type levels by means of an ordinal analysis of finite terms

Cites Work

• Nested recursion
• Beweisbarkeit und Unbeweisbarkeit von Anfangsfällen der transfiniten Induktion in der reinen Zahlentheorie
• Eine Klassifikation der ε₀‐Rekursiven Funktionen
• Ordinal recursion, and a refinement of the extended Grzegorczyk hierarchy
• On n-quantifier induction