Search

In this work we consider an extension MFcind of the Minimalist Foundation MF for predicative constructive mathematics with the addition of inductive and coinductive topological definitions sufficient to generate Sambin's Positive topologies, namely Martin-Löf-Sambin formal topologies (used to describe pointfree formal open subsets) equipped with a Positivity relation (used to describe pointfree formal closed subsets). In particular the intensional level of MFcind, called mTTcind, is defined by extending with coinductive topological definitions another theory mTTind extending the intensional level mTT of MF with the sole addition of inductive topological definitions. In previous work we have shown that mTTind is consistent with adding simultaneously formal Church's Thesis, CT, and the Axiom of Choice, AC, via an interpretation in Aczel's CZF +REA, namely Constructive Zermelo-Fraenkel Set Theory with the Regular Extension Axiom. Our aim is to show the expectation that the addition of coinductive topological definitions to mTTind does not increase its consistency strength by reducing the consistency of mTTcind+CT+AC to the consistency of CZF +REA through various interpretations. We reach our goal in two ways. One way consists in first interpreting mTTcind+CT+AC in the theory extending CZF with the Union Regular Extension Axiom, REAS, a strengthening of REA, and the Axiom of Relativized Dependent Choice, RDC. The theory CZF+REAS+RDC is then interpreted in MLS, a version of Martin-Löof's type theory with Palmgren's superuniverse S. The last step consists in interpreting MLS back into CZF +REA. The alternative way consists in first interpreting mTTcind+AC+CT directly in a version of Martin-Löf's type theory with Palmgren's superuniverse extended with CT, which is then interpreted back to CZF +REA. A key benefit of the first way is that the theory CZF + REAS + RDC also supports the intended set-theoretic interpretation of the extensional level of MFcind. Finally, all the theories considered to reach our goals, except mTTcind+AC + CT, are shown to be of the same proof-theoretic strength. [ABSTRACT FROM AUTHOR]

The Minimalist Foundation, MF for short, 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 content 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. • Interpretation of the intensional level of MF within HoTT through a careful management of proofs and their equalities. • Interpretation of the extensional level of MF within HoTT by adapting the notion of canonical isomorphisms of MF to HoTT. • Extension of Martin-Löf's interpretation of true judgements for logical constants to many-sorted extensional set theory. [ABSTRACT FROM AUTHOR]

Hyland's effctive topos offrs an important realizability model for constructive mathematics in the form of a category whose internal logic validates Church's Thesis. It also contains a boolean full sub-quasitopos of \assemblies" where only a restricted form of Church's Thesis survives. In the present paper we compare the effctive topos and the quasitopos of assemblies each as the elementary quotient completions of a Lawvere doctrine based on the partitioned assemblies. In that way we can explain why the two forms of Church's Thesis each category satisfies diffr by the way each is inherited from specific properties of the doctrine which determines the elementary quotient completion. [ABSTRACT FROM AUTHOR]

Consistency with the formal Church’s thesis, for short CT, and the axiom of choice, for short AC, was one of the requirements asked to be satisfied by the intensional level of a two-level foundation for constructive mathematics as proposed by Maietti and Sambin (in Crosilla, Schuster (eds) From sets and types to topology and analysis: practicable foundations for constructive mathematics, Oxford University Press, Oxford, 2005). Here we show that this is the case for the intensional level of the two-level Minimalist Foundation, for short MF, completed in 2009 by the second author. The intensional level of MF consists of an intensional type theory à la Martin-Löf, called mTT. The consistency of mTT with CT and AC is obtained by showing the consistency with the formal Church’s thesis of a fragment of intensional Martin-Löf’s type theory, called MLtt1, where mTT can be easily interpreted. Then to show the consistency of MLtt1 with CT we interpret it within Feferman’s predicative theory of non-iterative fixpoints ID1^ by extending the well known Kleene’s realizability semantics of intuitionistic arithmetics so that CT is trivially validated. More in detail the fragment MLtt1 we interpret consists of first order intensional Martin-Löf’s type theory with one universe and with explicit substitution rules in place of usual equality rules preserving type constructors (hence without the so called ξ-rule which is not valid in our realizability semantics). A key difficulty encountered in our interpretation was to use the right interpretation of lambda abstraction in the applicative structure of natural numbers in order to model all the equality rules of MLtt1 correctly. In particular the universe of MLtt1 is modelled by means of ID1^-fixpoints following a technique due first to Aczel and used by Feferman and Beeson. [ABSTRACT FROM AUTHOR]

The notion of overlap algebra introduced by G. Sambin provides a constructive version of complete Boolean algebra. Here we first show some properties concerning overlap algebras: we prove that the notion of overlap morphism corresponds classically to that of map preserving arbitrary joins; we provide a description of atomic set-based overlap algebras in the language of formal topology, thus giving a predicative characterization of discrete locales; we show that the power-collection of a set is the free overlap algebra join-generated from the set.Then, we generalize the concept of overlap algebra and overlap morphism in various ways to provide constructive versions of the category of Boolean algebras with maps preserving arbitrary existing joins. [ABSTRACT FROM AUTHOR]

Abstract: We present a two-level theory to formalize constructive mathematics as advocated in a previous paper with G. Sambin. One level is given by an intensional type theory, called Minimal type theory. This theory extends a previous version with collections. The other level is given by an extensional set theory that is interpreted in the first one by means of a quotient model. This two-level theory has two main features: it is minimal among the most relevant foundations for constructive mathematics; it is constructive thanks to the way the extensional level is linked to the intensional one which fulfills the “proofs-as-programs” paradigm and acts as a programming language. [Copyright &y& Elsevier]

The article presents an analysis of an extension of Martin-Löf's intensional set theory with the help of a power-set constructor. It demonstrates that Martin-Löf's set theory can not be extended to an intuitionistic theory of sets with power-sets, if sets and propositions are identified. It proves that even the weaker fragment containing only basic set constructors and the intensional equality cannot be extended with a power-set constructor.