Abstract
The work presented in this thesis is a contribution to the area of type theory and semantics for programming languages in that we develop and study new models for type theories and programming logics. It is also a contribution to the area of logic in computer science, in that our categorical analysis provides us with new insights into functional interpretations. Functional interpretations have proved highly effective in the area of proof mining, which is the enterprise of extracting constructive (computable) contents from nonconstructive proofs.
When Gödel published his functional interpretation in the journal Dialectica, hence the name “Dialectica Interpretation”, in 1958, it was as a contribution to Hilbert’s program. The Dialectica interpretation reduces consistency of Heyting arithmetic (and combined with the double negation translation, also Peano arithmetic) to consistency of Gödel’s system T, a quantifier-free theory of computable finite-type functionals. Nowadays, fifty years later, the interest in Gödel’s functional interpretation as well as other functional interpretations (e.g. Kleene’s number realizability, Kreisel’s modified realizability, the Diller-Nahm interpretation) is much less philosophical, and much more oriented toward (theoretical) computer science.
The Dialectica interpretations are remarkable syntactic constructions, We use these constructions to develop new mathematical structures such as the Dialectica categories, the Dialectica- and Diller-Nahm triposes, and the Dialectica- and Diller-Nahm toposes. The benefits work in both directions. The mathematical structures created from the functional interpretations provides us with new models for type theories and programming logics. And from studying the mathematical structures we also gain new insights into the syntactical constructions, in particular we present a new Dialectica variant for higher typed Heyting arithmetic: the Copenhagen interpretation, which is a product of the categorical analysis of the original Dialectica interpretation.
When Gödel published his functional interpretation in the journal Dialectica, hence the name “Dialectica Interpretation”, in 1958, it was as a contribution to Hilbert’s program. The Dialectica interpretation reduces consistency of Heyting arithmetic (and combined with the double negation translation, also Peano arithmetic) to consistency of Gödel’s system T, a quantifier-free theory of computable finite-type functionals. Nowadays, fifty years later, the interest in Gödel’s functional interpretation as well as other functional interpretations (e.g. Kleene’s number realizability, Kreisel’s modified realizability, the Diller-Nahm interpretation) is much less philosophical, and much more oriented toward (theoretical) computer science.
The Dialectica interpretations are remarkable syntactic constructions, We use these constructions to develop new mathematical structures such as the Dialectica categories, the Dialectica- and Diller-Nahm triposes, and the Dialectica- and Diller-Nahm toposes. The benefits work in both directions. The mathematical structures created from the functional interpretations provides us with new models for type theories and programming logics. And from studying the mathematical structures we also gain new insights into the syntactical constructions, in particular we present a new Dialectica variant for higher typed Heyting arithmetic: the Copenhagen interpretation, which is a product of the categorical analysis of the original Dialectica interpretation.
| Originalsprog | Engelsk |
|---|---|
| Kvalifikation | Ph.d. |
| Vejleder(e) |
|
| Udgiver | |
| ISBN'er, trykt | 978-87-7949-180-9 |
| Status | Udgivet - 2008 |