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

## by

2017

- Presented at
*LICS 2017, The Thirty-Second Annual ACM/IEEE Symposium on*. Reykjavik, Iceland, June 20-23, 2017.

Logic in Computer Science - Bar Induction: The Good, the Bad, and the Ugly (a long version with appendices is also available here.

More information can be found here.

**Abstract**

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).

.