History and Philosophy
The axiom schema of replacement was not 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 invented by Thoralf Skolem later in the same year. Although it is Skolem's final 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 axiom schema of replacement drastically increases the strength of ZF, both in terms of the theorems it can prove and in terms of its proof-theoretic consistency strength, compared to Z. In particular, ZF proves the consistency of Z, as the set Vω·2 is a model of Z constructible in ZF. (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, but the work of Solomon Feferman shows that care must be taken in stating the content of the second incompleteness theorem.) The cardinal number is the first one which can be shown to exist in ZF but not in Z.
The axiom schema of replacement is not necessary for the proofs of most theorems of ordinary mathematics. Indeed, Zermelo set theory already can interpret second-order arithmetic and much of type theory in finite types, which in turn are sufficient to formalize the bulk of mathematics. A notable mathematical theorem that requires the axiom of replacement to be proved in ZF is the Borel determinacy theorem.
The axiom of replacement does have an important role in the study of set theory itself. For example, the replacement schema is needed to construct the von Neumann ordinals from ω·2 onwards; without replacement, it would be necessary to find some other representation for ordinal numbers.
Although the axiom schema of replacement is a standard axiom in set theory today, it is often omitted from systems of type theory and foundation systems in topos theory.
Read more about this topic: Axiom Schema Of Replacement
Famous quotes containing the words history and, history and/or philosophy:
“We don’t know when our name came into being or how some distant ancestor acquired it. We don’t understand our name at all, we don’t know its history and yet we bear it with exalted fidelity, we merge with it, we like it, we are ridiculously proud of it as if we had thought it up ourselves in a moment of brilliant inspiration.”
—Milan Kundera (b. 1929)
“All history attests that man has subjected woman to his will, used her as a means to promote his selfish gratification, to minister to his sensual pleasures, to be instrumental in promoting his comfort; but never has he desired to elevate her to that rank she was created to fill. He has done all he could to debase and enslave her mind; and now he looks triumphantly on the ruin he has wrought, and say, the being he has thus deeply injured is his inferior.”
—Sarah M. Grimke (1792–1873)
“Histories make men wise; poets witty; the mathematics subtle; natural philosophy deep; moral grave; logic and rhetoric able to contend.”
—Francis Bacon (1561–1626)