Axiom Of Replacement
   HOME

TheInfoList



OR:

In
set theory Set theory is the branch of mathematical logic that studies Set (mathematics), sets, which can be informally described as collections of objects. Although objects of any kind can be collected into a set, set theory – as a branch of mathema ...
, the axiom schema of replacement is a
schema Schema may refer to: Science and technology * SCHEMA (bioinformatics), an algorithm used in protein engineering * Schema (genetic algorithms), a set of programs or bit strings that have some genotypic similarity * Schema.org, a web markup vocab ...
of
axiom An axiom, postulate, or assumption is a statement that is taken to be true, to serve as a premise or starting point for further reasoning and arguments. The word comes from the Ancient Greek word (), meaning 'that which is thought worthy or ...
s in
Zermelo–Fraenkel set theory In set theory, Zermelo–Fraenkel set theory, named after mathematicians Ernst Zermelo and Abraham Fraenkel, is an axiomatic system that was proposed in the early twentieth century in order to formulate a theory of sets free of paradoxes suc ...
(ZF) that asserts that the
image An image or picture is a visual representation. An image can be Two-dimensional space, two-dimensional, such as a drawing, painting, or photograph, or Three-dimensional space, three-dimensional, such as a carving or sculpture. Images may be di ...
of any
set Set, The Set, SET or SETS may refer to: Science, technology, and mathematics Mathematics *Set (mathematics), a collection of elements *Category of sets, the category whose objects and morphisms are sets and total functions, respectively Electro ...
under any definable mapping is also a set. It is necessary for the construction of certain infinite sets in ZF. The axiom schema is motivated by the idea that whether a
class Class, Classes, or The Class may refer to: Common uses not otherwise categorized * Class (biology), a taxonomic rank * Class (knowledge representation), a collection of individuals or objects * Class (philosophy), an analytical concept used d ...
is a set depends only on the
cardinality The thumb is the first digit of the hand, next to the index finger. When a person is standing in the medical anatomical position (where the palm is facing to the front), the thumb is the outermost digit. The Medical Latin English noun for thum ...
of the class, not on the rank of its elements. Thus, if one class is "small enough" to be a set, and there is a
surjection In mathematics, a surjective function (also known as surjection, or onto function ) is a function such that, for every element of the function's codomain, there exists one element in the function's domain such that . In other words, for a f ...
from that class to a second class, the axiom states that the second class is also a set. However, because ZFC only speaks of sets, not proper classes, the schema is stated only for definable surjections, which are identified with their defining
formulas In science, a formula is a concise way of expressing information symbolically, as in a mathematical formula or a ''chemical formula''. The informal use of the term ''formula'' in science refers to the general construct of a relationship betwe ...
.


Statement

Suppose P is a definable binary relation (which may be a
proper class Proper may refer to: Mathematics * Proper map, in topology, a property of continuous function between topological spaces, if inverse images of compact subsets are compact * Proper morphism, in algebraic geometry, an analogue of a proper map f ...
) such that for every set x there is a unique set y such that P(x,y) holds. There is a corresponding definable function F_P, where F_P(x)=y
if and only if In logic and related fields such as mathematics and philosophy, "if and only if" (often shortened as "iff") is paraphrased by the biconditional, a logical connective between statements. The biconditional is true in two cases, where either bo ...
P(x,y). Consider the (possibly proper) class B defined such that for every set y, y\in B if and only if there is an x\in A with F_P(x)=y. B is called the image of A under F_P, and denoted F_P /math> or (using
set-builder notation In mathematics and more specifically in set theory, set-builder notation is a notation for specifying a set by a property that characterizes its members. Specifying sets by member properties is allowed by the axiom schema of specification. Th ...
) \. The axiom schema of replacement states that if F is a definable class function, as above, and A is any set, then the image F /math> is also a set. This can be seen as a principle of smallness: the axiom states that if A is small enough to be a set, then F /math> is also small enough to be a set. It is implied by the stronger axiom of limitation of size. Because it is impossible to quantify over definable functions in first-order logic, one instance of the schema is included for each formula \phi in the language of set theory with free variables among w_1,\dotsc,w_n,A,x,y; but B is not free in \phi. In the formal language of set theory, the axiom schema is: :\begin \forall w_1,\ldots,w_n \, \forall A \, ( \forall x \in A &\, \exists ! y \, \phi(x, y, w_1, \ldots, w_n, A) \Longrightarrow\ \exists B \, \forall y \, \in B \Leftrightarrow \exists x \in A \, \phi(x, y, w_1, \ldots, w_n, A) ) \end For the meaning of \exists!, see
uniqueness quantification In mathematics and logic, the term "uniqueness" refers to the property of being the one and only object satisfying a certain condition. This sort of quantification is known as uniqueness quantification or unique existential quantification, and i ...
. For clarity, in the case of no variables w_i, this simplifies to: :\begin \forall A \, ( \forall x \in A &\, \exists ! y \, \phi(x, y, A) \Longrightarrow\ \exists B \, \forall y \, \in B \Leftrightarrow \exists x \in A \, \phi(x, y, A) ) \end So whenever \phi specifies a unique x-to-y correspondence, akin to a function F on A, then all y reached this way can be collected into a set B, akin to F /math>.


Applications

The axiom schema of replacement is not necessary for the proofs of most theorems of ordinary mathematics. Indeed, Zermelo set theory (Z) already can interpret
second-order arithmetic In mathematical logic, second-order arithmetic is a collection of axiomatic systems that formalize the natural numbers and their subsets. It is an alternative to axiomatic set theory as a foundation of mathematics, foundation for much, but not all, ...
and much of
type theory In mathematics and theoretical computer science, a type theory is the formal presentation of a specific type system. Type theory is the academic study of type systems. Some type theories serve as alternatives to set theory as a foundation of ...
in finite types, which in turn are sufficient to formalize the bulk of mathematics. Although the axiom schema of replacement is a standard axiom in set theory today, it is often omitted from systems of
type theory In mathematics and theoretical computer science, a type theory is the formal presentation of a specific type system. Type theory is the academic study of type systems. Some type theories serve as alternatives to set theory as a foundation of ...
and foundation systems in
topos In mathematics, a topos (, ; plural topoi or , or toposes) is a category that behaves like the category of sheaves of sets on a topological space (or more generally, on a site). Topoi behave much like the category of sets and possess a notio ...
theory. At any rate, the axiom schema drastically increases the strength of ZF, both in terms of the theorems it can prove—for example the sets shown to exist—and also in terms of its proof-theoretic consistency strength, compared to Z. Some important examples follow: * Using the modern definition due to von Neumann, proving the existence of any
limit ordinal In set theory, a limit ordinal is an ordinal number that is neither zero nor a successor ordinal. Alternatively, an ordinal λ is a limit ordinal if there is an ordinal less than λ, and whenever β is an ordinal less than λ, then there exists a ...
greater than \omega requires the replacement axiom. The
ordinal number In set theory, an ordinal number, or ordinal, is a generalization of ordinal numerals (first, second, th, etc.) aimed to extend enumeration to infinite sets. A finite set can be enumerated by successively labeling each element with the leas ...
\omega+\omega is the first such ordinal. Indeed, the
axiom of infinity In axiomatic set theory and the branches of mathematics and philosophy that use it, the axiom of infinity is one of the axioms of Zermelo–Fraenkel set theory. It guarantees the existence of at least one infinite set, namely a set containing ...
asserts the existence of an infinite set \omega=\. One may hope to define \omega+\omega as the union of the sequence \. However, arbitrary such classes of ordinals need not be sets; for example, the class of all ordinals is not a set. Replacement now allows one to replace each finite number n in \omega with the corresponding \omega+n, and thus guarantees that this class is a set. As a clarification, note that one can easily construct a
well-ordered set In mathematics, a well-order (or well-ordering or well-order relation) on a set is a total ordering on with the property that every non-empty subset of has a least element in this ordering. The set together with the ordering is then called a ...
that is isomorphic to \omega+\omega without resorting to replacement: simply take the
disjoint union In mathematics, the disjoint union (or discriminated union) A \sqcup B of the sets and is the set formed from the elements of and labelled (indexed) with the name of the set from which they come. So, an element belonging to both and appe ...
of two copies of \omega, with the second copy greater than the first; however, that is not an ordinal since it is not totally ordered by inclusion. * Larger ordinals rely on replacement less directly. For example, \omega_1, the
first uncountable ordinal In mathematics, the first uncountable ordinal, traditionally denoted by \omega_1 or sometimes by \Omega, is the smallest ordinal number that, considered as a set, is uncountable. It is the supremum (least upper bound) of all countable ordinals. Whe ...
, can be constructed as follows: the set of countable well orders exists as a subset of P(\times ) by the axioms of separation and
power set In mathematics, the power set (or powerset) of a set is the set of all subsets of , including the empty set and itself. In axiomatic set theory (as developed, for example, in the ZFC axioms), the existence of the power set of any set is po ...
(a relation on A is a subset of A\times A, and so an element of P(A\times A). A set of relations is thus a subset of P(A\times A)). Replace each well-ordered set with its ordinal. This is the set of countable ordinals \omega_1, which can itself be shown to be uncountable. The construction uses replacement twice; once to ensure an ordinal assignment for each well ordered set and again to replace well ordered sets by their ordinals. This is a special case of the result of Hartogs number, and the general case can be proved similarly. * In light of the above, the existence of an assignment of an ordinal to every well-ordered set requires replacement as well. Similarly the
von Neumann cardinal assignment The von Neumann cardinal assignment is a cardinal assignment that uses ordinal numbers. For a well-orderable set ''U'', we define its cardinal number to be the smallest ordinal number equinumerous to ''U'', using the von Neumann definition of a ...
which assigns a
cardinal number In mathematics, a cardinal number, or cardinal for short, is what is commonly called the number of elements of a set. In the case of a finite set, its cardinal number, or cardinality is therefore a natural number. For dealing with the cas ...
to each set requires replacement, as well as
axiom of choice In mathematics, the axiom of choice, abbreviated AC or AoC, is an axiom of set theory. Informally put, the axiom of choice says that given any collection of non-empty sets, it is possible to construct a new set by choosing one element from e ...
. * For sets of tuples recursively defined as A^n=A^\times A and for large A, the set \ has too high of a rank for its existence to be provable from set theory with just the axiom of power set, choice and without replacement. * Similarly, Harvey Friedman showed that at least some instances of replacement are required to show that Borel games are determined. The proven result is Donald A. Martin's Borel determinacy theorem. A later, more careful analysis by Martin of the result showed that it only requires replacement for functions with domain an arbitrary countable ordinal. * ZF with replacement proves the
consistency In deductive logic, a consistent theory is one that does not lead to a logical contradiction. A theory T is consistent if there is no formula \varphi such that both \varphi and its negation \lnot\varphi are elements of the set of consequences ...
of Z, as the set V_ is a
model A model is an informative representation of an object, person, or system. The term originally denoted the plans of a building in late 16th-century English, and derived via French and Italian ultimately from Latin , . Models can be divided in ...
of Z whose existence can be proved in ZF. The
cardinal number In mathematics, a cardinal number, or cardinal for short, is what is commonly called the number of elements of a set. In the case of a finite set, its cardinal number, or cardinality is therefore a natural number. For dealing with the cas ...
\aleph_\omega is the first one which can be shown to exist in ZF but not in Z. For clarification, note that Gödel's second incompleteness theorem shows that each of these theories contains a sentence, "expressing" the theory's own consistency, that is unprovable in that theory, if that theory is consistent - this result is often loosely expressed as the claim that neither of these theories can prove its own consistency, if it is consistent.


Relation to other axiom schemas


Simplifications

Some simplifications may be made to the axiom schema of replacement to obtain different equivalent versions.
Azriel Lévy Azriel Lévy (; born c. 1934) is an Israeli mathematician, logician, and a professor emeritus at the Hebrew University of Jerusalem. Biography Lévy obtained his Ph.D. at the Hebrew University of Jerusalem in 1958, under the supervision of Abr ...
showed that a version of replacement with parameters removed, i.e. the following schema, is equivalent to the original form. In particular the equivalence holds in the presence of the axioms of extensionality, pairing, union and powerset. : \forall A \, ( \forall x \, \exists ! y \, \phi(x, y, A) \Longrightarrow\ \exists B \, \forall y \, \in B \Leftrightarrow \exists x \in A \, \phi(x, y, A) )


Collection

The axiom schema of collection is closely related to and frequently confused with the axiom schema of replacement. Over the remainder of the ZF axioms, it is equivalent to the axiom schema of replacement. The axiom of collection is stronger than replacement in the absence of the power set axiom or its constructive counterpart of ZF and is used in the framework of IZF, which lacks the
law of excluded middle In logic, the law of excluded middle or the principle of excluded middle states that for every proposition, either this proposition or its negation is true. It is one of the three laws of thought, along with the law of noncontradiction and t ...
, instead of Replacement which is weaker. While replacement can be read to say that the image of a function is a set, collection speaks about images of relations and then merely says that some superclass of the relation's image is a set. In other words, the resulting set B has no minimality requirement, i.e. this variant also lacks the uniqueness requirement on \phi. That is, the relation defined by \phi is not required to be a function—some x\in A may correspond to many y's in B. In this case, the image set B whose existence is asserted must contain at least one such y for each x in the original set, with no guarantee that it will contain only one. Suppose that the free variables of \phi are among w_1,\dotsc,w_n,x,y; but neither A nor B is free in \phi. Then the axiom schema is: : \forall w_1,\ldots,w_n \, \forall x\, \exists\, y \phi(x, y, w_1, \ldots, w_n)) \Rightarrow \forall A\, \exists B\, \forall x \in A\, \exists y \in B\, \phi(x, y, w_1, \ldots, w_n) The axiom schema is sometimes stated without prior restrictions (apart from B not occurring free in \phi) on the predicate, \phi: : \forall w_1,\ldots,w_n \, \forall A\, \exists B\,\forall x \in A\, \exists y \phi(x, y, w_1, \ldots, w_n) \Rightarrow \exists y \in B\,\phi(x, y, w_1, \ldots, w_n) In this case, there may be elements x in A that are not associated to any other sets by \phi. However, the axiom schema as stated requires that, if an element x of A is associated with at least one set y, then the image set B will contain at least one such y. The resulting axiom schema is also called the axiom schema of boundedness.


Separation

The
axiom schema of separation In many popular versions of axiomatic set theory, the axiom schema of specification, also known as the axiom schema of separation (''Aussonderungsaxiom''), subset axiom, axiom of class construction, or axiom schema of restricted comprehension is ...
, the other axiom schema in ZFC, is implied by the axiom schema of replacement and the
axiom of empty set In axiomatic set theory, the axiom of empty set, also called the axiom of null set and the axiom of existence, is a statement that asserts the existence of a set with no elements. It is an axiom of Kripke–Platek set theory and the variant of g ...
. Recall that the axiom schema of separation includes :\forall A\, \exists B\, \forall C\, (C \in B \Leftrightarrow \in A \land \theta(C) for each formula \theta in the language of set theory in which B is not free, i.e. \theta that does not mention B. The proof is as follows: Either A contains some element a validating \theta(a), or it does not. In the latter case, taking the empty set for B fulfills the relevant instance of the axiom schema of separation and one is done. Otherwise, choose such a fixed a in A that validates \theta(a). Now define \phi(x, y):=(\theta(x)\land y=x)\lor(\neg\theta(x)\land y=a) for use with replacement. Using function notation for this predicate \phi, it acts as the identity F_a(x)=x wherever \theta(x) is true and as the constant function F_a(x)=a wherever \theta(x) is false. By case analysis, the possible values y are unique for any x, meaning F_a indeed constitutes a class function. In turn, the image B := \ of A under F_a, i.e. the class A\cap\, is granted to be a set by the axiom of replacement. This B precisely validates the axiom of separation. This result shows that it is possible to axiomatize ZFC with a single infinite axiom schema. Because at least one such infinite schema is required (ZFC is not finitely axiomatizable), this shows that the axiom schema of replacement can stand as the only infinite axiom schema in ZFC if desired. Because the axiom schema of separation is not independent, it is sometimes omitted from contemporary statements of the Zermelo-Fraenkel axioms. Separation is still important, however, for use in fragments of ZFC, because of historical considerations, and for comparison with alternative axiomatizations of set theory. A formulation of set theory that does not include the axiom of replacement will likely include some form of the axiom of separation, to ensure that its models contain a sufficiently rich collection of sets. In the study of models of set theory, it is sometimes useful to consider models of ZFC without replacement, such as the models V_\delta in von Neumann's hierarchy. The proof given above assumes the
law of excluded middle In logic, the law of excluded middle or the principle of excluded middle states that for every proposition, either this proposition or its negation is true. It is one of the three laws of thought, along with the law of noncontradiction and t ...
for the proposition that A is inhabited by a set validating \theta, and for any \theta(x) when stipulating that the relation \phi is functional. The axiom of separation is explicitly included in
constructive set theory Constructivism may refer to: Art and architecture * Constructivism (art), an early 20th-century artistic movement that extols art as a practice for social purposes * Constructivist architecture, an architectural movement in the Soviet Union in ...
, or a bounded variant thereof.


Reflection

Lévy's reflection principle for ZFC is equivalent to the axiom of replacement, assuming the axiom of infinity. Lévy's principle is as follows: : For any x_1,\ldots,x_n and any first-order formula \phi(x_1,\ldots,x_n), there exists an \alpha such that \phi(x_1,\ldots,x_n)\iff\phi^(x_1,\ldots,x_n). This is a schema that consists of countably many statements, one for each formula \phi. Here, \phi^M means \phi with all quantifiers bounded to M, i.e. \phi but with every instance of \exists x and \forall x replaced with \exists(x\in V_\alpha) and \forall(x\in V_\alpha) respectively.


History

The axiom schema of replacement was not part of
Ernst Zermelo Ernst Friedrich Ferdinand Zermelo (; ; 27 July 187121 May 1953) was a German logician and mathematician, whose work has major implications for the foundations of mathematics. He is known for his role in developing Zermelo–Fraenkel set theory, Z ...
's 1908 axiomatisation of set theory (Z). Some informal approximation to it existed in
Cantor A cantor or chanter is a person who leads people in singing or sometimes in prayer. Cantor as a profession generally refers to those leading a Jewish congregation, although it also applies to the lead singer or choir director in Christian contexts. ...
's unpublished works, and it appeared again informally in Mirimanoff (1917).. Maddy cites two papers by Mirimanoff, "Les antinomies de Russell et de Burali-Forti et le problème fundamental de la théorie des ensembles" and "Remarques sur la théorie des ensembles et les antinomies Cantorienne", both in ''L'Enseignement Mathématique'' (1917). Its publication by
Abraham Fraenkel Abraham Fraenkel (; 17 February, 1891 – 15 October, 1965) was a German-born Israeli mathematician. He was an early Zionist and the first Dean of Mathematics at the Hebrew University of Jerusalem. He is known for his contributions to axiomatic ...
in 1922 is what makes modern set theory Zermelo-''Fraenkel'' set theory (ZFC). The axiom was independently discovered and announced by
Thoralf Skolem Thoralf Albert Skolem (; 23 May 1887 – 23 March 1963) was a Norwegian mathematician who worked in mathematical logic and set theory. Life Although Skolem's father was a primary school teacher, most of his extended family were farmers. Skole ...
later in the same year (and published in 1923). Zermelo himself incorporated Fraenkel's axiom in his revised system he published in 1930, which also included as a new axiom von Neumann's axiom of foundation.Ebbinghaus, p. 92. Although it is Skolem's first order version of the axiom list that we use today, he usually gets no credit since each individual axiom was developed earlier by either Zermelo or Fraenkel. The phrase “Zermelo-Fraenkel set theory” was first used in print by von Neumann in 1928.Ebbinghaus, p. 189. Zermelo and Fraenkel had corresponded heavily in 1921; the axiom of replacement was a major topic of this exchange.Ebbinghaus, pp. 135-138. Fraenkel initiated correspondence with Zermelo sometime in March 1921. However, his letters before the one dated 6 May 1921 are lost. Zermelo first admitted to a gap in his system in a reply to Fraenkel dated 9 May 1921. On 10 July 1921, Fraenkel completed and submitted for publication a paper (published in 1922) that described his axiom as allowing arbitrary replacements: "If ''M'' is a set and each element of ''M'' is replaced by set or an urelementthen ''M'' turns into a set again" (parenthetical completion and translation by Ebbinghaus). Fraenkel's 1922 publication thanked Zermelo for helpful arguments. Prior to this publication, Fraenkel publicly announced his new axiom at a meeting of the
German Mathematical Society The German Mathematical Society (, DMV) is the main professional society of German mathematicians and represents German mathematics within the European Mathematical Society (EMS) and the International Mathematical Union (IMU). It was founded in ...
held in
Jena Jena (; ) is a List of cities and towns in Germany, city in Germany and the second largest city in Thuringia. Together with the nearby cities of Erfurt and Weimar, it forms the central metropolitan area of Thuringia with approximately 500,000 in ...
on 22 September 1921. Zermelo was present at this meeting; in the discussion following Fraenkel's talk he accepted the axiom of replacement in general terms, but expressed reservations regarding its extent. Thoralf Skolem made public his discovery of the gap in Zermelo's system (the same gap that Fraenkel had found) in a talk he gave on 6 July 1922 at the 5th Congress of Scandinavian Mathematicians, which was held in
Helsinki Helsinki () is the Capital city, capital and most populous List of cities and towns in Finland, city in Finland. It is on the shore of the Gulf of Finland and is the seat of southern Finland's Uusimaa region. About people live in the municipali ...
; the proceedings of this congress were published in 1923. Skolem presented a resolution in terms of first-order definable replacements: "Let ''U'' be a definite proposition that holds for certain pairs (''a'', ''b'') in the domain ''B''; assume further, that for every ''a'' there exists at most one ''b'' such that ''U'' is true. Then, as ''a'' ranges over the elements of a set ''Ma'', ''b'' ranges over all elements of a set ''Mb''." In the same year, Fraenkel wrote a review of Skolem's paper, in which Fraenkel simply stated that Skolem's considerations correspond to his own. Zermelo himself never accepted Skolem's formulation of the axiom schema of replacement. At one point he called Skolem's approach “set theory of the impoverished”. Zermelo envisaged a system that would allow for
large cardinal In the mathematical field of set theory, a large cardinal property is a certain kind of property of transfinite cardinal numbers. Cardinals with such properties are, as the name suggests, generally very "large" (for example, bigger than the least ...
s.Ebbinghaus, p. 184. He also objected strongly to the philosophical implications of countable models of set theory, which followed from Skolem's first-order axiomatization. According to the biography of Zermelo by Heinz-Dieter Ebbinghaus, Zermelo's disapproval of Skolem's approach marked the end of Zermelo's influence on the developments of set theory and logic.


References

*. *. *. *.


Citations

{{Set theory Axioms of set theory