Internal Effectful Forcing in System T
Martı́n Hötzel Escardó, Bruno Da Rocha Paiva, Rahli, Vincent, Tosun, Ayberk · DROPS (Schloss Dagstuhl – Leibniz Center for Informatics) · 2025
The effectful forcing technique allows one to show that the denotation of a closed System T term of type (ι ⇒ ι) ⇒ ι in the set-theoretical model is a continuous function (N → N) → 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.