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

Martín Escardó*

*Corresponding author for this work

Research output: Contribution to journalArticlepeer-review

10 Citations (Scopus)


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.

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


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

ASJC Scopus subject areas

  • Theoretical Computer Science
  • General Computer Science


Dive into the research topics of 'Continuity of gödel's system T definable functionals via effectful forcing'. Together they form a unique fingerprint.

Cite this