Constructivity, Computability and Continuity relative to the Minimalist Foundation

Constructivity, Computability and Continuity relative to the Minimalist Foundation Milly Maietti September 2025 Issues regarding constructivity, computability, and continuity are inevitable when developing a foundation for constructive mathematics, i.e., mathematics where the underlying logical reasoning has computational contents, sets are meant as data types, and the existence of objects is shown by construction. This tutorial aims to describe solved or still open issues of constructivity, computability, and continuity related to the Minimalist Foundation, for short MF, for constructive mathematics ideated in joint work with Giovanni Sambin in [8] and completed in [3]. First Lecture Regarding constructivity, the Minimalist Foundation provides a solution to the problem of finding a core foundation among the most relevant constructive and classical ones, often mutually incompatible between each other, including Martin-L¨of’s type theory, Aczel’s constructive set theory, the Calculus of Constructions, the internal theory of a topos, all shown in [3], and finally also Homotopy Type Theory, shown in [1]. To better achieve such a compatibility, MF is equipped with a two-level system, comprising an intensional level, an extensional one, and an interpretation of the latter on the former. Furthermore, MF distinguishes itself for being a predicative constructive foundation compatible with classical predicative mathematics `a la Weyl, especially for the treatment of the continuum. The key point is that the constructive MF has been shown in [7] to be equi-consistent with its classical version, a feature not shared by the other above-mentioned predicative foundations. Second Lecture Regarding computability, both levels of MF and its two-level extensions with inductive and coinductive definitions enjoy models validating the Formal Church thesis, where proofs can be seen as programs as devised in [2, 5, 6]. The key point is that such models are obtained by extending the usual Kleene realizability of intuitionistic arithmetic. They show that the intensional level of MF and its extensions are consistent with the axiom of choice, together with the Formal Church thesis, a property not shared by foundations validating extensionality of functions. Such realizability models provide the basic structure to build predicative effective toposes `a la Hyland, as in [4], where to interpret the extensional level of MF and extensions. Regarding continuity, MF opens the way to reconcile Markov’s constructivism with Brouwer’s intuitionism. The key point is the presence in MF of a primitive notion of function described by lambda-terms distinct from the usual notion of functional relation, used to interpret lawlike computable sequences and Brouwer’s choice sequences, respectively. As a consequence, MF Continuity, Computability, Constructivity 2025 From Logic to Algorithms has the peculiar property of being consistent with Brouwer’s continuity principles (which imply that all functions between real numbers are continuous) and Church’s thesis restricted to lambda-functions. References [1] M. Contente and M. E. Maietti. The compatibility of the Minimalist Foundation with Homotopy Type Theory. Theor. Comput. Sci., 2024. [2] H. Ishihara, M. E. Maietti, S. Maschio, T. Streicher. Consistency of the intensional level of the Minimalist Foundation with Church’s thesis and axiom of choice. Arch. Math. Log., 2018. [3] M. E. Maietti. A minimalist two-level foundation for constructive mathematics. Ann. of Pure and Applied Logic, 2009. [4] M. E. Maietti, S. Maschio. A Predicative variant of Hyland’s Effective Topos. J. Symb. Log., 2021. [5] M. E. Maietti, S. Maschio, M. Rathjen. A realizability semantics for inductive formal topologies, Church’s Thesis and Axiom of Choice. Log. Methods Comput. Sci., 2021. [6] M. E. Maietti, S. Maschio, M. Rathjen. Inductive and Coinductive Topological Generation with Church’s Thesis and the Axiom of Choice. Log. Methods Comput. Sci., 2022. [7] M. E. Maietti and P. Sabelli. Equiconsistency of the Minimalist Foundation with its classical version. Ann. of Pure and Applied Logic, 2024. [8] M. E. Maietti, G. Sambin. Toward a minimalist foundation for constructive mathematics. In: L. Crosilla and P. Schuster (eds.) From Sets and Types to Topology and Analysis: Practicable Foundations for Constructive Mathematics, no. 48, OUP, 2005.