Any good recomendations for an introduction to functional interpretations? I understand this is a little vague but i haven't had much contact with the area. I am particularly interested in the intuitionistic logic and wanted to get to know (possibly with some historical context also) some classical interpretations, namely: Modified Realizability, Gödel's functional interpretation and Diller-Nahm interpretation.
1 Answer
$\begingroup$ $\endgroup$
You could try Ulrich Kohlenbach: "Applied Proof Theory: Proof Interpretations and their Use in Mathematics". Springer Monographs in Mathematics, 2008. Probably it is a big shot for your question, but it addresses
- Systems of intuitionistic logic and arithmetic
- No-Counterexample Interpretation (Kreisel)
- Modified Realizability (Kreisel)
- Functional (Dialectica) Interpretation (Gödel)
- Applications of Functional Interpretation in mathematics
The historical context is usually outlined at the end of the respective chapters.