Bruno da Rocha Paiva (University of Birmingham), Internalising effectful forcing in System T

Programme

Résumé

Gödel first introduced System T in his dialectica interpretation to prove consistency of arithmetic. As a higher-order analogue of primitive recursive functions, computability in System T has been studied extensively. For example, it is known that all functions F : (ℕ → ℕ) → ℕ are continuous, in the sense that their output must only rely on a finite amount of their input. Moreover, it can even be shown if F is a System T function, then the amount of input that required to compute F(α) can itself be computed via a function m : (ℕ → ℕ) → ℕ in System T. While the former result has a succinct semantic proof using a model based in dialogue trees, the latter result seemed out of reach. In this talk we will see how to rephrase this model as a syntactic translation using Church-encodings of dialogue trees, allowing us to prove that the stronger result about moduli of continuity.