Internal Effectful Forcing in System T

Abstract

The effectful forcing technique allows one to show that the denotation of a closed System T term of type $({\hat{I}}^1\to {\hat{I}}^1)\to {\hat{I}}^1$ 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.

To appear in the proceedings of FSCD'2025