Abstract
In [Tro77], Troelstra showed that on Heyting arithmetic with finite types, the axiom of choice together with extensionality of functions contradict Brouwer’s Local Continuity principle (LCP).
In [EX15], Martín Escardó and Chuangjie Xu refined such a result by showing that on Heyting arithmetic with finite types, it is enough to take the xi-rule of definitional equality between typed terms to show that the axiom of choice contradicts LCP. In particular, Martin-Löf’s intensional type theory contradicts LCP and is therefore incompatible with Brouwer’s intuitionism.
We show that there are dependent type theories compatible with Brouwer’s intuitionism, and these include Coquand-Huet-Paulin’s Calculus of Constructions (CC_rocq) as implemented in the proof-assistant Rocq, and the two-level Minimalist Foundation (MF) in [MS05] and [M09].
Indeed, by modeling both foundations within constructive quasi-toposes of assemblies in [MST25], we show that CC_rocq and each level of MF are consistent with all Brouwer’s intuitionistic principles, including LCP, the Zermelo (or relational) instance of the axiom of choice from the Baire space to the natural numbers; extensionality of functions; and a restricted form of Church’s thesis establishing that all lambda-terms between natural numbers are computable, with the proviso that choice sequences are interpreted as functional relations.
This result is drawn as a consequence of the following other key facts:
- a suitable extensional version of CC_rocq, called eCC_rocq, is “the internal language of arithmetic solid quasi-toposes”;
- CC_rocq can be interpreted in eCC_rocq (and it is equi-consistent with it) by using the same technique in [MS24];
- the intensional/extensional levels of MF are respectively predicative variants of CC_rocq and eCC_rocq without any large elimination of propositions.
This is joint work with Pietro Sabelli (Czech Academy of Sciences).
Talk Details
Speaker: Maria Emilia Maietti (University of Padua, Italy)
Event: Types and Topology Workshop in Honour of Martin Escardo’s 60th Birthday
Date: Wednesday 17 December 2025
Time: 09:00
Slides: Available
Key Topics
- Brouwer’s intuitionism
- Local Continuity Principle (LCP)
- Dependent type theory
- Martin-Löf type theory
- Calculus of Constructions
- Minimalist Foundation
- Quasi-toposes of assemblies
- Axiom of choice
- Church’s thesis
- Choice sequences
Collaborators
- Pietro Sabelli (Czech Academy of Sciences)
References
- [EX15] M. Escardó, C. Xu. “The Inconsistency of a Brouwerian Continuity Principle with the Curry-Howard Interpretation.” TLCA, 2015
- [M09] Maietti, M.E. “A minimalist two-level foundation for constructive mathematics.” Annals of Pure and Applied Logic, 2009
- [MS24] M. E. Maietti, P. Sabelli. “Equiconsistency of the Minimalist Foundation with its classical version.” Annals of Pure and Applied Logic, 2025
- [MS05] M. E. Maietti, G. Sambin. “Toward a minimalist foundation for constructive mathematics”. Oxford Logic Guides, 2005
- [MST25] M. E. Maietti, P. Sabelli, D. Trotta. “Effectiveness and Continuity in Intuitionistic Quasi-toposes of Assemblies”. Submitted, 2025
- [Tro77] A.S. Troelstra. “A note on non-extensional operations in connection with continuity and recursiveness.” Indagationes Mathematicae, 1977