The Inconsistency of a Brouwerian Continuity Principle with the Curry–Howard Interpretation

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

Authors

Colleges, School and Institutes

Abstract

If all functions (N -> N) -> N are continuous then 0 = 1. We establish this in intensional (and hence also in extensional) intuitionistic dependent-type theories, with existence in the formulation of continuity expressed as a Sigma type via the Curry-Howard interpretation. But with an intuitionistic notion of anonymous existence, defined as the propositional truncation of Sigma, it is consistent that all such functions are continuous. A model is Johnstone’s topological topos. On the other hand, any of these two intuitionistic conceptions of existence give the same, consistent, notion of uniform continuity for functions (N -> 2) -> N, again valid in the topological topos. It is open whether the consistency of (uniform) continuity extends to homotopy type theory. The theorems of type theory informally proved here are also formally proved in Agda, but the development presented here is self-contained and doesn't show Agda code.

Details

Original languageEnglish
Title of host publication13th International Conference on Typed Lambda Calculi and Applications, Proceedings
EditorsThorsten Altenkirch
Publication statusPublished - 1 Jul 2015
Event13th International Conference on Typed Lambda Calculi and Applications - Warsaw, Poland
Duration: 1 Jul 20153 Jul 2015

Publication series

NameLIPICS - Leibniz International Proceedings in Informatics
PublisherDagstuhl Publishing
Volume38
ISSN (Print)1868-8969

Conference

Conference13th International Conference on Typed Lambda Calculi and Applications
CountryPoland
CityWarsaw
Period1/07/153/07/15