-
On the Compatibility of Constructive Predicative Mathematics with Weyl's Classical Predicativity
Authors:
Michele Contente,
Maria Emilia Maietti
Abstract:
It is well known that most foundations for Bishop's constructive mathematics are incompatible with a classical predicative development of analysis as put forward by Weyl in his $\textit{Das Kontinuum}$. Here, we first recall how this incompatibility arises from the possibility, present in most constructive foundations, to define sets by quantifying over (the exponentiation of) functional relations…
▽ More
It is well known that most foundations for Bishop's constructive mathematics are incompatible with a classical predicative development of analysis as put forward by Weyl in his $\textit{Das Kontinuum}$. Here, we first recall how this incompatibility arises from the possibility, present in most constructive foundations, to define sets by quantifying over (the exponentiation of) functional relations. This possibility is not allowed in modern formulations of Weyl's logical system. Then, we argue how a possible way out is offered by foundations, such as the Minimalist Foundation, where exponentiation is limited to a primitive notion of function defined by $λ$-terms as in dependent type theory. The price to pay is to renounce the so-called rule of unique choice identifying functional relations with $λ$-terms, and to number-theoretic choice principles, characteristic of foundations aimed to formalize Bishop's constructive analysis. This restriction calls for a point-free constructive development of topology as advocated by P. Martin-Löf and G. Sambin with the introduction of Formal Topology. Hence, we conclude that the Minimalist Foundation promises to be a natural crossroads between Bishop's constructivism and Weyl's classical predicativity provided that a point-free reformulation of classical analysis is viable.
△ Less
Submitted 4 July, 2024;
originally announced July 2024.
-
The Compatibility of the Minimalist Foundation with Homotopy Type Theory
Authors:
Michele Contente,
Maria Emilia Maietti
Abstract:
The Minimalist Foundation, for short MF, is a two-level foundation for constructive mathematics ideated by Maietti and Sambin in 2005 and then fully formalized by Maietti in 2009. MF serves as a common core among the most relevant foundations for mathematics in the literature by choosing for each of them the appropriate level of MF to be translated in a compatible way, namely by preserving the mea…
▽ More
The Minimalist Foundation, for short MF, is a two-level foundation for constructive mathematics ideated by Maietti and Sambin in 2005 and then fully formalized by Maietti in 2009. MF serves as a common core among the most relevant foundations for mathematics in the literature by choosing for each of them the appropriate level of MF to be translated in a compatible way, namely by preserving the meaning of logical and set-theoretical constructors. The two-level structure consists of an intensional level, an extensional one, and an interpretation of the latter in the former in order to extract intensional computational contents from mathematical proofs involving extensional constructions used in everyday mathematical practice. In 2013 a completely new foundation for constructive mathematics appeared in the literature, called Homotopy Type Theory, for short HoTT, which is an example of Voevodsky's Univalent Foundations with a computational nature. So far no level of MF has been proved to be compatible with any of the Univalent Foundations in the literature. Here we show that both levels of MF are compatible with HoTT. This result is made possible thanks to the peculiarities of HoTT which combines intensional features of type theory with extensional ones by assuming Voevodsky's Univalence Axiom and higher inductive quotient types. As a relevant consequence, MF inherits entirely new computable models.
△ Less
Submitted 29 January, 2024; v1 submitted 8 July, 2022;
originally announced July 2022.
-
Overlap Algebras: a Constructive Look at Complete Boolean Algebras
Authors:
Francesco Ciraulo,
Michele Contente
Abstract:
The notion of a complete Boolean algebra, although completely legitimate in constructive mathematics, fails to capture some natural structures such as the lattice of subsets of a given set. Sambin's notion of an overlap algebra, although classically equivalent to that of a complete Boolean algebra, has powersets and other natural structures as instances. In this paper we study the category of over…
▽ More
The notion of a complete Boolean algebra, although completely legitimate in constructive mathematics, fails to capture some natural structures such as the lattice of subsets of a given set. Sambin's notion of an overlap algebra, although classically equivalent to that of a complete Boolean algebra, has powersets and other natural structures as instances. In this paper we study the category of overlap algebras as an extension of the category of sets and relations, and we establish some basic facts about mono-epi-isomorphisms and (co)limits; here a morphism is a symmetrizable function (with classical logic this is just a function which preserves joins). Then we specialize to the case of morphisms which preserve also finite meets: classically, this is the usual category of complete Boolean algebras. Finally, we connect overlap algebras with locales, and their morphisms with open maps between locales, thus obtaining constructive versions of some results about Boolean locales.
△ Less
Submitted 12 February, 2020; v1 submitted 30 April, 2019;
originally announced April 2019.
