Functional interpretation and inductive definitions

DOI10.2178/jsl/1254748682zbMath1193.03082arXiv0802.1938OpenAlexW1970069956MaRDI QIDQ3655246

Henry Towsner, Jeremy Avigad

Publication date: 7 January 2010

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

Full work available at URL: https://arxiv.org/abs/0802.1938

zbMATH Keywords

functional interpretationwell-founded treeinductive definition

Mathematics Subject Classification ID

Functionals in proof theory (03F10)

Related Items

A herbrandized functional interpretation of classical first-order logic ⋮ Intuitionistic fixed point logic ⋮ The metamathematics of ergodic theory ⋮ Iterated Inductive Definitions Revisited ⋮ On Some Semi-constructive Theories Related to Kripke–Platek Set Theory

Cites Work

• Unnamed Item
• Unnamed Item
• Iterated inductive definitions and subsystems of analysis: recent proof-theoretical studies
• Predicative functionals and an interpretation of \({\widehat{\text{ID}}_{<\omega}}\)
• A Diller-Nahm-style functional interpretation of \(\text{KP}\omega\)
• Bounded functional interpretation
• Interpreting classical theories in constructive ones
• Hierarchies of number-theoretic predicates
• ÜBER EINE BISHER NOCH NICHT BENÜTZTE ERWEITERUNG DES FINITEN STANDPUNKTES
• Shoenfield is Gödel after Krivine
• Interpretationen der Heyting-Arithmetik endlicher Typen
• Eine Variante zur Dialectica-Interpretation der Heyting-Arithmetik endlicher Typen
• Some logical metatheorems with applications in functional analysis
• Applied Proof Theory: Proof Interpretations and Their Use in Mathematics
• A system of abstract constructive ordinals