| Index: > A B C D E F G H I J K L M N O P Q R S T U V W X Y Z |
|
|||||
| First Prev [ 1 2 ] Next Last |
In axiomatic set theory and the branches of logic, mathematics, and computer science that use it, the axiom schema of replacement is a schema of axioms in Zermelo-Fraenkel set theory.
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:
or in words:
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:
for each derived functional predicate F in one variable; or in words:
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:
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
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.)