Functional interpretation and inductive definitions
From MaRDI portal
Abstract: Extending G"odel's emph{Dialectica} interpretation, we provide a functional interpretation of classical theories of positive arithmetic inductive definitions, reducing them to theories of finite-type functionals defined using transfinite recursion on well-founded trees.
Recommendations
- scientific article; zbMATH DE number 1215497
- Functional interpretations. From the Dialectica interpretation to interpretations of classical and constructive set theory
- Predicative functionals and an interpretation of \({\widehat{\text{ID}}_{<\omega}}\)
- scientific article; zbMATH DE number 6307929
- Functional interpretations of classical systems
Cites work
- A Diller-Nahm-style functional interpretation of \(\text{KP}\omega\)
- A system of abstract constructive ordinals
- Applied Proof Theory: Proof Interpretations and Their Use in Mathematics
- Bounded functional interpretation
- Eine Variante zur Dialectica-Interpretation der Heyting-Arithmetik endlicher Typen
- Hierarchies of number-theoretic predicates
- scientific article; zbMATH DE number 4039890 (Why is no real title available?)
- Interpretationen der Heyting-Arithmetik endlicher Typen
- Interpreting classical theories in constructive ones
- Iterated inductive definitions and subsystems of analysis: recent proof-theoretical studies
- Mathematical logic.
- Predicative functionals and an interpretation of \({\widehat{\text{ID}}_{<\omega}}\)
- Shoenfield is Gödel after Krivine
- Some logical metatheorems with applications in functional analysis
- ÜBER EINE BISHER NOCH NICHT BENÜTZTE ERWEITERUNG DES FINITEN STANDPUNKTES
Cited in
(20)- The metamathematics of ergodic theory
- Induktive Definitionen und Dilatoren. (Inductive definitions and dilators)
- Predicative functionals and an interpretation of \({\widehat{\text{ID}}_{<\omega}}\)
- Realizability interpretation of generalized inductive definitions
- \(\mathbf L^i \mathbf D^Z_\lambda\) as a basis for PRA
- Intuitionistic fixed point logic
- A herbrandized functional interpretation of classical first-order logic
- Another reduction of classical ID_ to constructive ID^i_
- Functional interpretations of classical systems
- Functional interpretation and the existence property
- Spielquantorinterpretation unstetiger Funktionale der höheren Analysis
- scientific article; zbMATH DE number 3873314 (Why is no real title available?)
- scientific article; zbMATH DE number 3954904 (Why is no real title available?)
- scientific article; zbMATH DE number 176201 (Why is no real title available?)
- The bounded functional interpretation of bar induction
- A functional functional interpretation
- Gödel's functional interpretation and the concept of learning
- Iterated inductive definitions revisited
- On some semi-constructive theories related to Kripke-Platek set theory
- Herbrandized modified realizability
This page was built for publication: Functional interpretation and inductive definitions
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3655246)
