TY - GEN

T1 - A constructive model of uniform continuity

AU - Xu, Chuangjie

AU - Escardó, Martín

PY - 2013

Y1 - 2013

N2 - We construct a continuous model of Gödel's system T and its logic HAω in which all functions from the Cantor space 2 ℕ to the natural numbers are uniformly continuous. Our development is constructive, and has been carried out in intensional type theory in Agda notation, so that, in particular, we can compute moduli of uniform continuity of T-definable functions 2ℕ → ℕ. Moreover, the model has a continuous Fan functional of type (2ℕ → ℕ) → ℕ that calculates moduli of uniform continuity. We work with sheaves, and with a full subcategory of concrete sheaves that can be presented as sets with structure, which can be regarded as spaces, and whose natural transformations can be regarded as continuous maps.

AB - We construct a continuous model of Gödel's system T and its logic HAω in which all functions from the Cantor space 2 ℕ to the natural numbers are uniformly continuous. Our development is constructive, and has been carried out in intensional type theory in Agda notation, so that, in particular, we can compute moduli of uniform continuity of T-definable functions 2ℕ → ℕ. Moreover, the model has a continuous Fan functional of type (2ℕ → ℕ) → ℕ that calculates moduli of uniform continuity. We work with sheaves, and with a full subcategory of concrete sheaves that can be presented as sets with structure, which can be regarded as spaces, and whose natural transformations can be regarded as continuous maps.

KW - Constructive mathematics

KW - Fan functional

KW - Gödel's system T

KW - HA

KW - intuitionistic type theory

KW - sheaves

KW - topological models

KW - topos theory

KW - uniform continuity

UR - http://www.scopus.com/inward/record.url?scp=84884513912&partnerID=8YFLogxK

U2 - 10.1007/978-3-642-38946-7_18

DO - 10.1007/978-3-642-38946-7_18

M3 - Conference contribution

AN - SCOPUS:84884513912

SN - 9783642389450

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 236

EP - 349

BT - Typed Lambda Calculi and Applications - 11th International Conference, TLCA 2013, Proceedings

T2 - 11th International Conference on Typed Lambda Calculi and Applications, TLCA 2013

Y2 - 26 June 2013 through 28 June 2013

ER -