一句话：为 Nuprl 扩展 bar induction，在 Coq 中证明其可靠性与一致性，并发现单调 bar 的非截断版本直觉主义下不成立。
本文为 Nuprl 证明助手的计算系统与逻辑引入直觉主义原理，即若干版本的 Brouwer bar induction（等价于超限归纳）。作者在 Coq 中大幅扩展 Nuprl 类型论的形式化，证明两类 bar induction 原理相对 Nuprl 语义可靠：针对数序列的版本只需对系统作少量修改；针对无名字封闭项序列的更一般版本则需在模型的项语法中加入 limit 构造子。形式化还证明这些扩展保持一致性等关键元理论性质。此外，作者发现单调 bar 的非截断 bar induction 在直觉主义下为假，澄清了该原理的适用边界。
We present an extension of the computation system and logic of the Nuprl proof assistant with intuitionistic principles, namely versions of Brouwer's bar induction principle, which is equivalent to transfinite induction. We have substantially extended the formalization of Nuprl's type theory within the Coq proof assistant to show that two such bar induction principles are valid w.r.t. Nuprl's semantics (the Good): one for sequences of numbers that involved only minor changes to the system, and a more general one for sequences of name-free (the Ugly) closed terms that involved adding a limit constructor to Nuprl's term syntax in our model of Nuprl's logic. We have proved that these additions preserve Nuprl's key metatheoretical properties such as consistency. Finally, we show some new insights regarding bar induction, such as the non-truncated version of bar induction on monotone bars is intuitionistically false (the Bad).