It has long been known that (classical) Peano arithmetic is, in some strong sense, “equivalent” to the variant of (classical) Zermelo–Fraenkel set theory (including choice) in which the axiom of infinity is replaced by its negation. The intended model of the latter is the set of hereditarily finite sets. The connection between the theories is so tight that they may be taken as notational variants of each other. Our purpose here is to develop and establish a constructive version of this. (...) We present an intuitionistic theory of the hereditarily finite sets, and show that it is definitionally equivalent to Heyting Arithmetic, in a sense to be made precise. Our main target theory, the intuitionistic small set theory is remarkably simple, and intuitive. It has just one non-logical primitive, for membership, and three straightforward axioms plus one axiom scheme. We locate our theory within intuitionistic mathematics generally. (shrink)

This paper extends the axiomatic treatment of intuitionistic mereology introduced in Maffezioli and Varzi (_Synthese, 198_(S18), 4277–4302 2021 ) by examining the behavior of constructive notions of overlap and disjointness. We consider both (i) various ways of defining such notions in terms of other intuitionistic mereological primitives, and (ii) the possibility of treating them as mereological primitives of their own.

In this article I present a disagreement between classical and constructive approaches to predicativity regarding the predicative status of so-called generalised inductive definitions. I begin by offering some motivation for an enquiry in the predicative foundations of constructive mathematics, by looking at contemporary work at the intersection between mathematics and computer science. I then review the background notions and spell out the above-mentioned disagreement between classical and constructive approaches to predicativity. Finally, I look at possible ways of defending the constructive (...) predicativity of inductive definitions. (shrink)

Errett Bishop's work in constructive mathematics is overwhelmingly regarded as a turning point for mathematics based on intuitionistic logic. It brought new life to this form of mathematics and prompted the development of new areas of research that witness today's depth and breadth of constructive mathematics. Surprisingly, notwithstanding the extensive mathematical progress since the publication in 1967 of Errett Bishop's Foundations of Constructive Analysis, there has been no corresponding advances in the philosophy of constructive mathematics Bishop style. The aim of (...) this paper is to foster the philosophical debate about this form of mathematics. I begin by considering key elements of philosophical remarks by Bishop, especially focusing on Bishop's assessment of Brouwer. I then compare these remarks with ``traditional'' philosophical arguments for intuitionistic logic and argue that the latter are in tension with Bishop's views. ``Traditional'' arguments for intuitionistic logic turn out to be also in conflict with significant recent developments in constructive mathematics. This rises pressing questions for the philosopher of mathematics, especially with regard to the possibility of offering alternative philosophical arguments for constructive mathematics. I conclude with the suggestion to look anew at Bishop's own remarks for inspiration. (shrink)

ABSTRACT Theories of sets such as Zermelo Fraenkel set theory are usually presented as the combination of two distinct kinds of principles: logical and set-theoretic principles. The set-theoretic principles are imposed ‘on top’ of first-order logic. This is in agreement with a traditional view of logic as universally applicable and topic neutral. Such a view of logic has been rejected by the intuitionists, on the ground that quantification over infinite domains requires the use of intuitionistic rather than classical logic. In (...) the following, I consider constructive set theories, which use intuitionistic rather than classical logic, and argue that they manifest a distinctive interdependence or an entanglement between sets and logic. In fact, Martin-Löf type theory identifies fundamental logical and set-theoretic notions. Remarkably, one of the motivations for this identification is the thought that classical quantification over infinite domains is problematic, while intuitionistic quantification is not. The approach to quantification adopted in Martin-Löf’s type theory is subtly interconnected with its predicativity. I conclude by recalling key aspects of an approach to predicativity inspired by Poincaré, which focuses on the issue of correct quantification over infinite domains and relate it back to Martin-Löf type theory. (shrink)

Working in constructive set theory we formulate notions of constructive topological space and set-generated locale so as to get a good constructive general version of the classical Galois adjunction between topological spaces and locales. Our notion of constructive topological space allows for the space to have a class of points that need not be a set. Also our notion of locale allows the locale to have a class of elements that need not be a set. Class sized mathematical structures need (...) to be allowed for in constructive set theory because the powerset axiom and the full separation scheme are necessarily missing from constructive set theory. We also consider the notion of a formal topology, usually treated in Intuitionistic type theory, and show that the category of set-generated locales is equivalent to the category of formal topologies. We exploit ideas of Palmgren and Curi to obtain versions of their results about when the class of formal points of a set-presentable formal topology form a set. (shrink)

The glueing of (sequentially, pointwise, or uniformly) continuous functions that coincide on the intersection of their closed domains is examined in the light of Bishop-style constructive analysis. This requires us to pay attention to the way that the two domains intersect.

This thesis articulates the resonances between J. M. Coetzee's lifelong engagement with mathematics and his practice as a novelist, critic, and poet. Though the critical discourse surrounding Coetzee's literary work continues to flourish, and though the basic details of his background in mathematics are now widely acknowledged, his inheritance from that background has not yet been the subject of a comprehensive and mathematically- literate account. In providing such an account, I propose that these two strands of his intellectual trajectory not (...) only developed in parallel, but together engendered several of the characteristic qualities of his finest work. The structure of the thesis is essentially thematic, but is also broadly chronological. Chapter 1 focuses on Coetzee's poetry, charting the increasing involvement of mathematical concepts and methods in his practice and poetics between 1958 and 1979. Chapter 2 situates his master's thesis alongside archival materials from the early stages of his academic career, and thus traces the development of his philosophical interest in the migration of quantificatory metaphors into other conceptual domains. Concentrating on his doctoral thesis and a series of contemporaneous reviews, essays, and lecture notes, Chapter 3 details the calculated ambivalence with which he therein articulates, adopts, and challenges various statistical methods designed to disclose objective truth. Chapter 4 explores the thematisation of several mathematical concepts in Dusklands and In the Heart of the Country. Chapter Five considers Waiting for the Barbarians and Foe in the context provided by Coetzee's interest in the attempts of Isaac Newton to bridge the gap between natural language and the supposedly transparent language of mathematics. Finally, Chapter 6 locates in Elizabeth Costello and Diary of a Bad Year a cognitive approach to the use of mathematical concepts in ethics, politics, and aesthetics, and, by analogy, a central aspect of the challenge Coetzee's late fiction poses to the contemporary literary landscape. (shrink)

Constructive and intuitionistic Zermelo-Fraenkel set theories are axiomatic theories of sets in the style of Zermelo-Fraenkel set theory (ZF) which are based on intuitionistic logic. They were introduced in the 1970's and they represent a formal context within which to codify mathematics based on intuitionistic logic. They are formulated on the basis of the standard first order language of Zermelo-Fraenkel set theory and make no direct use of inherently constructive ideas. In working in constructive and intuitionistic ZF we can thus (...) to some extent rely on our familiarity with ZF and its heuristics. -/- Notwithstanding the similarities with classical set theory, the concepts of set defined by constructive and intuitionistic set theories differ considerably from that of the classical tradition; they also differ from each other. The techniques utilised to work within them, as well as to obtain metamathematical results about them, also diverge in some respects from the classical tradition because of their commitment to intuitionistic logic. In fact, as is common in intuitionistic settings, a plethora of semantic and proof-theoretic methods are available for the study of constructive and intuitionistic set theories. -/- The entry introduces the main features of Constructive and Intuitionistic ZF and offers links to the relevant bibliography. (shrink)

Gödel's dialectica interpretation of Heyting arithmetic HA may be seen as expressing a lack of confidence in our understanding of unbounded quantification. Instead of formally proving an implication with an existential consequent or with a universal antecedent, the dialectica interpretation asks, under suitable conditions, for explicit 'interpreting' instances that make the implication valid. For proofs in constructive set theory CZF-, it may not always be possible to find just one such instance, but it must suffice to explicitly name a set (...) consisting of such interpreting instances. The aim of eliminating unbounded quantification in favor of appropriate constructive functionals will still be obtained, as our ∧-interpretation theorem for constructive set theory in all finite types CZFω- shows. By changing to a hybrid interpretation ∧q, we show closure of CZFω- under rules that – in stronger forms – have already been studied in the context of Heyting arithmetic. In a similar spirit, we briefly survey modified realizability of CZFω- and its hybrids. Central results of this paper have been proved by Burr 2000a and Schulte 2006, however, for different translations. We use a simplified interpretation that goes back to Diller and Nahm 1974. A novel element is a lemma on absorption of bounds which is essential for the smooth operation of our translation. (shrink)

The aim of this article is to give an introduction to functional interpretations of set theory given by the authorin Burr (2000a). The first part starts with some general remarks on Gödel's functional interpretation with a focus on aspects related to problems that arise in the context of set theory. The second part gives an insight in the techniques needed to perform a functional interpretation of systems of set theory. However, the first part of this article is not intended to (...) be a complete survey of functional interpretations and here we recommend, for example, Avigad and Feferman (1998),Troelstra (1990) and Troelstra (1973). (shrink)

Should weak forms of the axiom of choice really be accepted within constructive mathematics? A critical view of the Brouwer-Heyting-Kolmogorov interpretation, accompanied by the intention to include nondeterministic algorithms, leads us to subscribe to Richman's appeal for dropping countable choice. As an alternative interpretation of intuitionistic logic, we propose to renew dialogue semantics.

The first part of the paper introduces the varieties of modern constructive mathematics, concentrating on Bishop's constructive mathematics (BISH). it gives a sketch of both Myhill's axiomatic system for BISH and a constructive axiomatic development of the real line R. The second part of the paper focusses on the relation between constructive mathematics and programming, with emphasis on Martin-L6f 's theory of types as a formal system for BISH.

We see the defining properties of constructive mathematics as being the proof interpretation of the logical connectives and the definition of function as rule or method. We sketch the development of intuitionist type theory as an alternative to set theory. We note that the axiom of choice is constructively valid for types, but not for sets. We see the theory of types, in which proofs are directly algorithmic, as a more natural setting for constructive mathematics than set theories like IZF. (...) Church’s thesis provides an objective definition of effective computability. It cannot be proved mathematically because it is a conjecture about what kinds of mechanisms are physically possible, for which we have scientific evidence but not proof. We consider the idea of free choice sequences and argue that they do not undermine Church’s Thesis. (shrink)

An axiomatic development of the theory of apartness and nearness of a point and a set is introduced as a framework for constructive topology. Various notions of continuity of mappings between apartness spaces are compared; the constructive independence of one of the axioms from the others is demonstrated; and the product apartness structure is defined and analysed.

Constructive theories usually have interesting metamathematical properties where explicit witnesses can be extracted from proofs of existential sentences. For relational theories, probably the most natural of these is the existence property, EP, sometimes referred to as the set existence property. This states that whenever ϕϕ is provable, there is a formula χχ such that ϕ∧χϕ∧χ is provable. It has been known since the 80s that EP holds for some intuitionistic set theories and yet fails for IZF. Despite this, it has (...) remained open until now whether EP holds for the most well known constructive set theory, CZF. In this paper we show that EP fails for CZF. (shrink)

The paper aims to provide precise proof theoretic characterizations of Myhill–Friedman-style “weak” constructive extensional set theories and Aczel–Rathjen analogous constructive set theories both enriched by Mostowski-style collapsing axioms and/or related anti-foundation axioms. The main results include full intuitionistic conservations over the corresponding purely arithmetical formalisms that are well known in the reverse mathematics – which strengthens analogous results obtained by the author in the 80s. The present research was inspired by the more recent Sato-style “weak weak” classical extensional set theories (...) whose proof theoretic strengths are shown to strongly exceed the ones of the intuitionistic counterparts in the presence of the collapsing axioms. (shrink)

In recent years the question of whether adding the limited principle of omniscience, LPO, to constructive Zermelo–Fraenkel set theory, CZF, increases its strength has arisen several times. As the addition of excluded middle for atomic formulae to CZF results in a rather strong theory, i.e. much stronger than classical Zermelo set theory, it is not obvious that its augmentation by LPO would be proof-theoretically benign. The purpose of this paper is to show that CZF+RDC+LPO has indeed the same strength as (...) CZF, where RDC stands for relativized dependent choice. In particular, these theories prove the same Π02 theorems of arithmetic. (shrink)

An axiomatic development of the theory of apartness and nearness of a point and a set is introduced as a framework for constructive topology. Various notions of continuity of mappings between apartness spaces are compared; the constructive independence of one of the axioms from the others is demonstrated; and the product apartness structure is defined and analysed.

In the present paper we give a functional interpretation of Aczel's constructive set theories CZF − and CZF in systems T ∈ and T ∈ + of constructive set functionals of finite types. This interpretation is obtained by a translation × , a refinement of the ∧ -translation introduced by Diller and Nahm 49–66) which again is an extension of Gödel's Dialectica translation. The interpretation theorem gives characterizations of the definable set functions of CZF − and CZF in terms of (...) constructive set functionals. In a second part we introduce constructive set theories in all finite types. We expand the interpretation to these theories and give a characterization of the translation × . We further show that the simplest non-trivial axiom of extensionality is not interpretable by functionals of T ∈ and T ∈ + . We obtain this result by adapting Howard's notion of hereditarily majorizable functionals to set functionals. Subject of the last section is the translation ∨ that is defined in Burr for an interpretation of Kripke-Platek set theory with infinity. (shrink)

This paper is the first in a series whose objective is to study notions of large sets in the context of formal theories of constructivity. The two theories considered are Aczel's constructive set theory and Martin-Löf's intuitionistic theory of types. This paper treats Mahlo's π-numbers which give rise classically to the enumerations of inaccessibles of all transfinite orders. We extend the axioms of CZF and show that the resulting theory, when augmented by the tertium non-datur, is equivalent to ZF plus (...) the assertion that there are inaccessibles of all transfinite orders. Finally, the theorems of that extension of CZF are interpreted in an extension of Martin-Löf's intuitionistic theory of types by a universe. (shrink)

The standard construction of quotient spaces in topology uses full separation and power sets. We show how to make this construction using only the predicative methods available in constructive type theory and constructive set theory.

Constructive Zermelo–Fraenkel set theory, CZF, can be interpreted in Martin-Löf type theory via the so-called propositions-as-types interpretation. However, this interpretation validates more than what is provable in CZF. We now ask ourselves: is there a reasonably simple axiomatization of the set-theoretic formulae validated in Martin-Löf type theory? The answer is yes for a large collection of statements called the mathematical formulae. The validated mathematical formulae can be axiomatized by suitable forms of the axiom of choice.The paper builds on a self-interpretation (...) of CZF IOS Press, Amsterdam, 2004 ]) that provides an “inner” model of CZF which also validates the so-called -axiom of choice, . The crucial technical step taken in the present paper is to investigate the absoluteness properties of this model under the hypothesis .It is also shown that CZF plus the -axiom of choice possesses the disjunction property, the numerical existence property and the existence property for an important group of formulae. (shrink)

Continuing the study of apartness in lattices, begun in [8], this paper deals with axioms for a product a-frame and with their consequences. This leads to a reasonable notion of proximity in an a-frame, abstracted from its counterpart in the theory of set-set apartness.

Constructive set theory started with Myhill's seminal 1975 article [8]. This paper will be concerned with axiomatizations of the natural numbers in constructive set theory discerned in [3], clarifying the deductive relationships between these axiomatizations and the strength of various weak constructive set theories.

Bar Induction occupies a central place in Brouwerian mathematics. This note is concerned with the strength of Bar Induction on the basis of Constructive Zermelo-Fraenkel Set Theory, CZF. It is shown that CZF augmented by decidable Bar Induction proves the 1-consistency of CZF. This answers a question of P. Aczel who used Bar Induction to give a proof of the Lusin Separation Theorem in the constructive set theory CZF.

Working within Bishop’s constructive framework, we examine the connection between a weak version of the Heine–Borel property, a property antithetical to that in Specker’s theorem in recursive analysis, and the uniform continuity theorem for integer-valued functions. The paper is a contribution to the ongoing programme of constructive reverse mathematics.

In the informal setting of Bishop-style constructive reverse mathematics we discuss the connection between the antithesis of Specker’s theorem, Ishihara’s principle BD-N, and various types of equicontinuity. In particular, we prove that the implication from pointwise equicontinuity to uniform sequential equicontinuity is equivalent to the antithesis of Specker’s theorem; and that, for a family of functions on a separable metric space, the implication from uniform sequential equicontinuity to uniform equicontinuity is equivalent to BD-N.

Two new notions of compactness, each classically equivalent to the standard classical one of sequential compactness, for apartness spaces are examined within Bishop-style constructive mathematics.

We show how to interpret the language of first-order set theory in an elementary topos endowed with, as extra structure, a directed structural system of inclusions (dssi). As our main result, we obtain a complete axiomatization of the intuitionistic set theory validated by all such interpretations. Since every elementary topos is equivalent to one carrying a dssi, we thus obtain a first-order set theory whose associated categories of sets are exactly the elementary toposes. In addition, we show that the full (...) axiom of Separation is validated whenever the dssi is superdirected. This gives a uniform explanation for the known facts that cocomplete and realizability toposes provide models for Intuitionistic Zermelo—Fraenkel set theory (IZF). (shrink)

The aim of this paper is to describe from a semantic perspective the problem of conservativity of classical first-order theories over their intuitionistic counterparts. In particular, we describe a class of formulae for which such conservativity results can be proven in case of any intuitionistic theory T which is complete with respect to a class of T-normal Kripke models. We also prove conservativity results for intuitionistic theories which are closed under the Friedman translation and complete with respect to a class (...) of conversely well-founded Kripke models. The results can be applied to a wide class of intuitionistic theories and can be viewed as generalization of the results obtained by syntactic methods. (shrink)

We show how to interpret the language of first-order set theory in an elementary topos endowed with, as extra structure, a directed structural system of inclusions . As our main result, we obtain a complete axiomatization of the intuitionistic set theory validated by all such interpretations. Since every elementary topos is equivalent to one carrying a dssi, we thus obtain a first-order set theory whose associated categories of sets are exactly the elementary toposes. In addition, we show that the full (...) axiom of Separation is validated whenever the dssi is superdirected. This gives a uniform explanation for the known facts that cocomplete and realizability toposes provide models for Intuitionistic Zermelo-Fraenkel set theory. (shrink)

The von Neumann hierarchy of sets is heavily used as a basic tool in classical set theory, being an underlying ingredient in many proofs and concepts. In constructive set theories like without the powerset axiom however, it loses much of its potency by ceasing to be a hierarchy of sets as its single stages become only classes. This article proposes an alternative cumulative hierarchy which does not have this drawback and provides examples of how it can be used to prove (...) new theorems in. (shrink)

CZF is an intuitionistic set theory that does not contain Power Set, substituting instead a weaker version, Subset Collection. In this paper a Kripke model of CZF is presented in which Power Set is false. In addition, another Kripke model is presented of CZF with Subset Collection replaced by Exponentiation, in which Subset Collection fails.

In the article [4], a new constructive set theoretic principle called Refinement was introduced and analysed. While it seemed to be significantly weaker than its alternative, the more established axiom of Fullness , it was shown to suffice to imply many of the mathematically important consequences. In this article, we will define for each set A a set of truth values which measures the complexity of the equality relation on A. Using these sets we will show that Refinement is actually (...) equivalent to Fullness on the basis of the other axioms of constructive Zermelo-Fraenkel set theory. (shrink)

The anti-Specker property, a constructive version of sequential compactness, is used to prove constructively that a pointwise continuous, order-dense preference relation on a compact metric space is uniformly sequentially continuous. It is then shown that Ishihara's principle BD-ℕ implies that a uniformly sequentially continuous, order-dense preference relation on a separable metric space is uniformly continuous. Converses of these two theorems are also proved.