Bar induction: The good, the bad, and the ugly

Vincent Rahli, Mark Bickford, Robert L. Constable

Research output: Chapter in Book/Report/Conference proceedingConference contribution

5 Citations (Scopus)

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 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).
Original languageEnglish
Title of host publication32nd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2017
PublisherInstitute of Electrical and Electronics Engineers (IEEE)
ISBN (Print)9781509030187
DOIs
Publication statusPublished - 18 Aug 2017
Event32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2017) - Reykjavik, Iceland
Duration: 20 Jun 201723 Jun 2017

Conference

Conference32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2017)
Country/TerritoryIceland
CityReykjavik
Period20/06/1723/06/17

Fingerprint

Dive into the research topics of 'Bar induction: The good, the bad, and the ugly'. Together they form a unique fingerprint.

Cite this