Internal Effectful Forcing in System T
Martin H. Escardo, Bruno da Rocha Paiva, Vincent Rahli, Ayberk Tosun
TL;DR
This work addresses whether System T-definable functionals on the Baire space are continuous and whether their moduli of continuity can be defined inside System T. It advances a constructive program by developing an oracle-free effectful forcing framework based on dialogue-tree semantics and proving, via a logical relation, that these trees are themselves definable in System T through Church encodings. The authors establish the internal translations and prove correctness results for both moduli of continuity and uniform moduli of continuity, eliminating the need for external oracle extensions. The results extend the understanding of constructive continuity for higher-type functionals and hint at applications in characterising System T-definable functionals through the structure of their interaction trees, with potential implications for ordinal analyses of tree heights.
Abstract
The effectful forcing technique allows one to show that the denotation of a closed System T term of type $(ι\to ι) \to ι$ in the set-theoretical model is a continuous function $(\mathbb{N} \to \mathbb{N}) \to \mathbb{N}$. For this purpose, an alternative dialogue-tree semantics is defined and related to the set-theoretical semantics by a logical relation. In this paper, we apply effectful forcing to show that the dialogue tree of a System T term is itself System T-definable, using the Church encoding of trees.