Continuity of gödel's system T definable functionals via effectful forcing

Research output: Contribution to journalArticlepeer-review

Colleges, School and Institutes

Abstract

It is well-known that the Gödel's system T definable functions (N→N)→N are continuous, and that their restrictions from the Baire type (N→N) to the Cantor type (N→2) are uniformly continuous. We offer a new, relatively short and self-contained proof. The main technical idea is a concrete notion of generic element that doesn't rely on forcing, Kripke semantics or sheaves, which seems to be related to generic effects in programming. The proof uses standard techniques from programming language semantics, such as dialogues, monads, and logical relations. We write this proof in intensional Martin-Löf type theory (MLTT) from scratch, in Agda notation. Because MLTT has a computational interpretation and Agda can be seen as a programming language, we can run our proof to compute moduli of (uniform) continuity of T-definable functions.

Details

Original languageEnglish
Pages (from-to)119-141
Number of pages23
JournalElectronic Notes in Theoretical Computer Science
Volume298
Publication statusPublished - 4 Nov 2013

Keywords

  • Agda, Baire space, Cantor space, continuity, dialogue, Gödel's system T, intensional Martin-Löf theory, logical relation, semantics, uniform continuity