Validating Brouwer's continuity principle for numbers using named exceptions

Research output: Contribution to journalArticlepeer-review

Authors

Colleges, School and Institutes

Abstract

This paper extends the Nuprl proof assistant (a system representative of the class of extensional type theories with dependent types) with named exceptions and handlers, as well as a nominal fresh operator. Using these new features, we prove a version of Brouwer's continuity principle for numbers. We also provide a simpler proof of a weaker version of this principle that only uses diverging terms. We prove these two principles in Nuprl's metatheory using our formalization of Nuprl in Coq and reflect these metatheoretical results in the Nuprl theory as derivation rules. We also show that these additions preserve Nuprl's key metatheoretical properties, in particular consistency and the congruence of Howe's computational equivalence relation. Using continuity and the fan theorem, we prove important results of Intuitionistic Mathematics: Brouwer's continuity theorem, bar induction on monotone bars and the negation of the law of excluded middle.

Details

Original languageEnglish
Pages (from-to)942-990
Number of pages49
JournalMathematical Structures in Computer Science
Volume28
Issue number6
Early online date2 Nov 2017
Publication statusPublished - 1 Jun 2018