Axiom Schema Of Replacement Axiom Of Choice Axiom

Suppose P is any predicate in two variables that doesn't use the symbol B. Then in the formal language of the Zermelo-Fraenkel axioms, the axiom schema reads:

Note that there is one axiom for every such predicate P; thus, this is an axiom schemaIn symbolic logic, it is sometimes inconvenient or impossible to express an axiomatic system in a finite number of axioms. For this reason, an axiom schema is used. Formally, an axiom schema is a set (usually infinite) of well formed formulae, each of whi.

To understand this axiom, first note that the clause in the first set of parentheses above is exactly what one needs to construct a functional predicateModel theory In formal logic and related branches of mathematics, a functional predicate or function symbol is a logical symbol that may be applied to an object term to produce another object term. Functional predicates are also sometimes called mappings F in one variable such that F(X) = Y if and only if P(X,Y). Indeed, if one formalises the language of predicate logic to allow the use of derived functional predicates in axiom schemas, then the axiom schema may be rewritten as:

Next, note that the clause in parentheses in the reformulation above (equivalent to the second clause in parentheses in the original statement) simply states that C is the value of F at some member D of A. Thus, what the axiom schema is really saying is that, given a set A, we can find a set B whose members are precisely the values of F at the members of A.

We can use the axiom of extensionalitySet theory In axiomatic set theory and the branches of logic, mathematics, and computer science that use it, the axiom of extensionality or axiom of extension is one of the axioms of Zermelo-Fraenkel set theory. In the formal language of the Zermelo-Fraen to show that this set B is unique. We call the set B the image of A under F, and denote it F(A) or (using a form of set-builder notation) {F(D) : D in A}. Thus the essence of the axiom schema is:

1 History and philosophy

Most of the applications to which replacement might naïvely be put in fact do not require it. For example, suppose that f is a function from a set S to a set T. Then we may construct a functional predicate F such that F(x) = f(x) whenever x is a member of S, letting F(x) be anything we like otherwise (it won't matter for this application). Then given a subset A of S, applying the axiom schema of replacement to F constructs the image f(A) of the subset A under the function f; it is just F'(A). However, replacement is in fact not needed here, because f(A) is a subset of T, so we could instead construct this image using the axiom schema of specification as the set {y in T : for some x in A, y = f(x)}. In general, specification will suffice when the values of F at the members of A all belong to some previously constructed set T; replacement is needed only when such a T isn't already available.

According to some philosophies, it's preferable to apply specification to a set like T in the example above, since specification is logically weaker than replacement (as explained in the next section). Indeed, replacement is arguably unnecessary in ordinary mathematics, needed only for certain features of axiomatic set theory. For example, you need replacement to construct the von Neumann ordinals from ω2 onwards, and the von Neumann ordinals are necessary for certain set-theoretic results. However, you don't need replacement to construct these ordinal numbers in other ways that are sufficient for applications to the theory of well-ordered sets. Some mathematicians working on the foundations of mathematics, particularly those that focus on type theory as opposed to set theory, find this axiom unnecessary for any purpose and therefore do not include it (nor a type-theoretic analogue) in their foundations. Replacement is difficult to express at all in foundations built upon topos theory, so it's usually left out there as well. Nevertheless, replacement is not controversial in the sense that some people find its consequences to be necessarily false (a sense in which the axiom of choice, for example, is controversial); it's just that they find it unnecessary.

The axiom schema of replacement wasn't part of Ernst Zermelo's 1908 axiomatisation of set theory (Z); its introduction by Adolf Fraenkel in 1922 is what makes modern set theory Zermelo-Fraenkel set theory (ZF). The axiom was independently discovered by Thoralf Skolem later in the same year, and it is in fact Skolem's final version of the axiom list that we use today -- but he usually gets no credit since each individual axiom was developed earlier by either Zermelo or Fraenkel. Including replacement makes a big difference from the proof-theoretic point of view; adding this schema to Zermelo's axioms makes for a much stronger system logically, allowing one to prove more statements. In particular, in ZF one can prove the consistency of Z by constructing the von Neumann universe V_ω2 as a model. (Of course, Gödel's second incompleteness theorem shows that neither of these theories can prove its own consistency, if it is consistent.)

2 Relation to the axiom schema of specification

The axiom schema of specification can almost be derived from the axiom schema of replacement.

First, recall this axiom schema:

for any predicate P in one variable that doesn't use the symbol B. Given such a predicate P, define the mapping F by F(D) = D if P(D) is true and F(D) = E if P(D) is false, where E is any member of A such that P(E) is true. Then the set B guaranteed by the axiom of replacement is precisely the set B required for the axiom of specification. The only problem is if no such E exists. But in this case, the set B required for the axiom of specification is the empty set, so the axiom schema follows in general using also the axiom of empty set.

For this reason, the axiom schema of specification is often left out of modern lists of the Zermelo-Fraenkel axioms. However, specification is still important for historical considerations, and for comparison with alternative axiomatisations of set theory. For example, the argument above used the law of excluded middle, so specification can't be left out of an intuitionistic set theory. And any formulation of set theory that excludes replacement as unnecessary certainly will want to keep specification.

<Hide>

Home > Axiom schema of replacement

1 History and philosophy

2 Relation to the axiom schema of specification

Topics: Axiom Schema Of Replacement, Axiom Of Choice, Axiom...