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.

Markov's principle (MP) is an axiom in some varieties of constructive mathematics, stating that Σ01 propositions (i.e. existential quantification over a decidable predicate on N) are stable under double negation. However, there are various non-equivalent definitions of decidable predicates and thus Σ01 in constructive foundations, leading to non-equivalent Markov's principles. While this fact is well-reported in the literature, it is often overlooked, leading to wrong claims in standard references and published papers.

Continuity is a key principle of intuitionistic logic that is generally accepted by constructivists but is inconsistent with classical logic. Most commonly, continuity states that a function from the Baire space to numbers, only needs approximations of the points in the Baire space to compute. More recently, another formulation of the continuity principle was put forward. It states that for any function F from the Baire space to numbers, there exists a (dialogue) tree that contains the values of F at its leaves and such that the modulus of F at each point of the Baire space is given by the length of the corresponding branch in the tree. In this paper we provide the first internalization of this "inductive" continuity principle within a computational setting. Concretely, we present a class of intuitionistic theories that validate this formulation of continuity thanks to computations that construct such dialogue trees internally to the theories using effectful computations. We further demonstrate that this inductive continuity principle implies other forms of continuity principles.