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

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

Standard

The Inconsistency of a Brouwerian Continuity Principle with the Curry–Howard Interpretation. / Escardo, Martin; Xu, Chuangjie.

13th International Conference on Typed Lambda Calculi and Applications, Proceedings. ed. / Thorsten Altenkirch. Schloss Dagstuhl, 2015. p. 153-164 (LIPICS - Leibniz International Proceedings in Informatics; Vol. 38).

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

Harvard

Escardo, M & Xu, C 2015, The Inconsistency of a Brouwerian Continuity Principle with the Curry–Howard Interpretation. in T Altenkirch (ed.), 13th International Conference on Typed Lambda Calculi and Applications, Proceedings. LIPICS - Leibniz International Proceedings in Informatics, vol. 38, Schloss Dagstuhl, pp. 153-164, 13th International Conference on Typed Lambda Calculi and Applications, Warsaw, Poland, 1/07/15. https://doi.org/10.4230/LIPIcs.TLCA.2015.153

APA

Escardo, M., & Xu, C. (2015). The Inconsistency of a Brouwerian Continuity Principle with the Curry–Howard Interpretation. In T. Altenkirch (Ed.), 13th International Conference on Typed Lambda Calculi and Applications, Proceedings (pp. 153-164). (LIPICS - Leibniz International Proceedings in Informatics; Vol. 38). Schloss Dagstuhl. https://doi.org/10.4230/LIPIcs.TLCA.2015.153

Vancouver

Escardo M, Xu C. The Inconsistency of a Brouwerian Continuity Principle with the Curry–Howard Interpretation. In Altenkirch T, editor, 13th International Conference on Typed Lambda Calculi and Applications, Proceedings. Schloss Dagstuhl. 2015. p. 153-164. (LIPICS - Leibniz International Proceedings in Informatics). https://doi.org/10.4230/LIPIcs.TLCA.2015.153

Author

Escardo, Martin ; Xu, Chuangjie. / The Inconsistency of a Brouwerian Continuity Principle with the Curry–Howard Interpretation. 13th International Conference on Typed Lambda Calculi and Applications, Proceedings. editor / Thorsten Altenkirch. Schloss Dagstuhl, 2015. pp. 153-164 (LIPICS - Leibniz International Proceedings in Informatics).

Bibtex

@inproceedings{c5de9b04f3444356ba942ef5586a70ae,
title = "The Inconsistency of a Brouwerian Continuity Principle with the Curry–Howard Interpretation",
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{\textquoteright}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.",
author = "Martin Escardo and Chuangjie Xu",
year = "2015",
month = jul
day = "1",
doi = "10.4230/LIPIcs.TLCA.2015.153",
language = "English",
isbn = "9783939897873",
series = "LIPICS - Leibniz International Proceedings in Informatics",
publisher = "Schloss Dagstuhl",
pages = "153--164",
editor = "Thorsten Altenkirch",
booktitle = "13th International Conference on Typed Lambda Calculi and Applications, Proceedings",
address = "Germany",
note = "13th International Conference on Typed Lambda Calculi and Applications ; Conference date: 01-07-2015 Through 03-07-2015",

}

RIS

TY - GEN

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

AU - Escardo, Martin

AU - Xu, Chuangjie

PY - 2015/7/1

Y1 - 2015/7/1

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

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

U2 - 10.4230/LIPIcs.TLCA.2015.153

DO - 10.4230/LIPIcs.TLCA.2015.153

M3 - Conference contribution

SN - 9783939897873

T3 - LIPICS - Leibniz International Proceedings in Informatics

SP - 153

EP - 164

BT - 13th International Conference on Typed Lambda Calculi and Applications, Proceedings

A2 - Altenkirch, Thorsten

PB - Schloss Dagstuhl

T2 - 13th International Conference on Typed Lambda Calculi and Applications

Y2 - 1 July 2015 through 3 July 2015

ER -