License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.TLCA.2015.153
URN: urn:nbn:de:0030-drops-51618
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2015/5161/
Go to the corresponding LIPIcs Volume Portal

Hötzel Escardó, Martín ; Xu, Chuangjie

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

pdf-format:
16.pdf (0.3 MB)

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.

BibTeX - Entry

@InProceedings{htzelescard_et_al:LIPIcs:2015:5161,
  author =	{Mart{\'i}n H{\"o}tzel Escard{\'o} and Chuangjie Xu},
  title =	{{The Inconsistency of a Brouwerian Continuity Principle with the Curry–Howard Interpretation}},
  booktitle =	{13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015)},
  pages =	{153--164},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-87-3},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{38},
  editor =	{Thorsten Altenkirch},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2015/5161},
  URN =		{urn:nbn:de:0030-drops-51618},
  doi =		{10.4230/LIPIcs.TLCA.2015.153},
  annote =	{Keywords: Dependent type, intensional Martin-L{\"o}f type theory, Curry-Howard interpretation, constructive mathematics, Brouwerian continuity axioms, anonymous exi}
}

Keywords: Dependent type, intensional Martin-Löf type theory, Curry-Howard interpretation, constructive mathematics, Brouwerian continuity axioms, anonymous exi
Collection: 13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015)
Issue Date: 2015
Date of publication: 15.06.2015

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI