一句话：用效应强制证明 System T 中可实现的 bar 满足 Brouwer 单调 bar 定理，并以对话树刻画其构造。
本文旨在为 Brouwer 单调 bar 定理给出新证明：若一个 bar 可由 Gödel System T 中类型为 (ℕ→ℕ)→ℕ 的泛函实现，则该 bar 满足该定理。作者扩展 Martín Escardó 的 effectful forcing 技术，将 System T 程序解释为良基对话树；树节点对 ℕ→ℕ 的 oracle 进行查询，并沿 call-by-name 翻译提升到高阶类型。该解释使用计算效应、monad、call-by-name λ-演算的代数解释以及逻辑关系等编程语言思想，为通常的层论强制论证提供初等替代。最后，作者表明 Brouwer 关于 barhood 的“心智构造”构成这些对话树的不变形式：其中对 oracle 的查询以最大方式且按序进行。由此定理得证。
Abstract Extending Martín Escardó’s effectful forcing technique, we give a new proof of a well-known result: Brouwer’s monotone bar theorem holds for any bar that can be realized by a functional of type (ℕ→ℕ)→ℕ in Gödel’s System T . Effectful forcing is an elementary alternative to standard sheaf-theoretic forcing arguments, using ideas from programming languages, including computational effects, monads, the algebra interpretation of call-by-name λ-calculus, and logical relations. Our argument proceeds by interpreting System T programs as well-founded dialogue trees whose nodes branch on a query to an oracle of type ℕ→ℕ, lifted to higher type along a call-by-name translation. To connect this interpretation to the bar theorem, we then show that Brouwer’s famous “mental constructions” of barhood constitute an invariant form of these dialogue trees in which queries to the oracle are made maximally and in order.