Skip to main content
PRL Project

Bar Induction: The Good, the Bad, and the Ugly


More information can be found here.

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 trans-
finite 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 nontruncated
version of bar induction on monotone bars is
intuitionistically false (the Bad).