This article serves to present a large mathematical perspective and historical basis for the Axiom of Replacement as well as to affirm its importance as a central axiom of modern set theory.

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)

We present a generalisation of the type-theoretic interpretation of constructive set theory into Martin-Löf type theory. The original interpretation treated logic in Martin-Löf type theory via the propositions-as-types interpretation. The generalisation involves replacing Martin-Löf type theory with a new type theory in which logic is treated as primitive. The primitive treatment of logic in type theories allows us to study reinterpretations of logic, such as the double-negation translation.

In the present note, we study a generalization of Dedekind cuts in the context of constructive Zermelo–Fraenkel set theory CZF. For this purpose, we single out an equivalent of CZF's axiom of fullness and show that it is sufficient to derive that the Dedekind cuts in this generalized sense form a set. We also discuss the instance of this equivalent of fullness that is tantamount to the assertion that the class of Dedekind cuts in the rational numbers, in the customary (...) constructive sense including locatedness, is a set. This is to be compared with the situation for the partial reals, a generalization in a different direction: if one drops locatedness from the notion of a Dedekind real, then it becomes inherently impredicative. We make this precise, and further present the curiosity that the irrational Dedekind reals form a set already with exponentiation. (shrink)