Predicative functionals and an interpretation of \({\widehat{\text{ID}}_{<\omega}}\)
From MaRDI portal
Publication:1295369
DOI10.1016/S0168-0072(97)00045-6zbMath0945.03084MaRDI QIDQ1295369
Publication date: 16 August 1999
Published in: Annals of Pure and Applied Logic (Search for Journal in Brave)
fixed pointDialectica interpretationequational theoryextension of first-order arithmeticMartin-Löf's universes of transfinite types
First-order arithmetic and fragments (03F30) Functionals in proof theory (03F10) Recursive ordinals and ordinal notations (03F15) Relative consistency and interpretations (03F25)
Related Items (3)
Logical problems of functional interpretations ⋮ Functional interpretation and inductive definitions ⋮ Functional interpretation of Aczel's constructive set theory
Cites Work
- Type-theoretic interpretation of iterated, strictly positive inductive definitions
- Realizability and intuitionistic logic
- On the syntax of Martin-Löf's type theories
- Iterated inductive definitions and subsystems of analysis: recent proof-theoretical studies
- What's so special about Kruskal's theorem and the ordinal \(\Gamma{}_ 0\)? A survey of some results in proof theory
- Constructivism in mathematics. An introduction. Volume II
- Metamathematical investigation of intuitionistic arithmetic and analysis. With contributions by C. A. Smorynski, J. I. Zucker and W. A. Howard
- ÜBER EINE BISHER NOCH NICHT BENÜTZTE ERWEITERUNG DES FINITEN STANDPUNKTES
- Recursive models for constructive set theories
- Eine Variante zur Dialectica-Interpretation der Heyting-Arithmetik endlicher Typen
- On the relationship between ATR0 and
- On the interpretation of non-finitist proofs–Part II
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
This page was built for publication: Predicative functionals and an interpretation of \({\widehat{\text{ID}}_{<\omega}}\)
