Abstract It is well known that over Heyting arithmetic with finite types, the effective principle of the formal Church thesis, stating that all number-theoretic functional relations are computable, is inconsistent with Brouwer’s intuitionistic principles on the continuum, in particular, the fan theorem. Here, we build two arithmetic quasi-toposes, validating on the one hand Brouwer’s continuity principles, including the Fan theorem, and on the other hand, a restricted form of Church’s Thesis, called the Type-theoretic Church Thesis and written TCT, expressing that all morphisms of the considered quasi-topos are computable. One quasi-topos is constructed by formalizing the category of assemblies Asm within Hyland’s effective topos using intuitionistic Zermelo-Fraenkel set theory IZF extended with Brouwer’s continuity principles as our meta-theory. The other quasi-topos is obtained as an elementary quotient completion in the same intuitionistic meta-theory. While in previous work by the first author with F. Pasquali and G. Rosolini, it has been shown that these two quasi-toposes are equivalent when working within the classical ZFC set theory; here, we show that this is no longer the case when working within IZF. We also observe that the aforementioned inconsistency is resolved in such quasi-toposes by the non-validity of the axiom of unique choice on the natural numbers and that no non-trivial topos can validate the effective principle TCT together with Brouwer’s continuity principles altogether.
Maietti et al. (Thu,) studied this question.