Content deleted Content added
→Relation to the axiom schema of replacement: Added a source |
Citation bot (talk | contribs) Altered url. URLs might have been anonymized. | Use this bot. Report bugs. | #UCB_CommandLine |
||
| (16 intermediate revisions by 6 users not shown) | |||
Line 2:
{{redirect|Axiom of separation|the separation axioms in topology|separation axiom}}
In many popular versions of [[axiomatic set theory]], the '''axiom schema of specification''',<ref name=":1" /> also known as the '''axiom schema of separation''' (''Aussonderungsaxiom''),<ref name="SuppesAxiomatic">{{Cite book |last=Suppes |first=Patrick |url=https://books.google.com/books?id=sxr4LrgJGeAC |title=Axiomatic Set Theory |date=1972-01-01 |publisher=Courier Corporation |isbn=978-0-486-61630-8 |pages=6,19,21,237 |language=en |quote=}}</ref> '''subset axiom<ref name=":0" />''', '''axiom of class construction''',<ref>{{Cite book |last=Pinter |first=Charles C. |url=https://books.google.com/books?id=iUT_AwAAQBAJ |title=A Book of Set Theory |date=2014-06-01 |publisher=Courier Corporation |isbn=978-0-486-79549-2 |pages=27 |language=en}}</ref> or '''axiom schema of restricted comprehension''' is an [[axiom schema]]. Essentially, it says that any definable [[subclass (set theory)|subclass]] of a set is a set.
Some mathematicians call it the '''axiom schema of comprehension''', although others use that term for '''''unrestricted'' comprehension''', discussed below.
Line 9:
== Statement ==
One instance of the schema is included for each [[Well-formed formula|formula]] <math>\varphi(x)</math> in the language of set theory with <math>x</math> as a free variable. So ''<math>S</math>'' does not occur free in <math>\varphi(x)</math>.<ref name=":0">{{Cite book |last=Cunningham |first=Daniel W. |title=Set theory: a first course |date=2016 |publisher=Cambridge University Press |isbn=978-1-107-12032-7 |series=Cambridge mathematical textbooks |location=New York, NY |pages=22,24-25,29}}</ref><ref name="SuppesAxiomatic" /><ref name=":2">{{Cite book |last1=DeVidi |first1=David |url=https://books.google.com/books?id=z39HwYEekPEC |title=Logic, Mathematics, Philosophy, Vintage Enthusiasms: Essays in Honour of John L. Bell |last2=Hallett |first2=Michael |last3=Clark |first3=Peter |date=2011-03-23 |publisher=Springer Science & Business Media |isbn=978-94-007-0214-1 |pages=206 |language=en}}</ref> In the formal language of set theory, the axiom schema is:
:<math>\forall A \, \exists S \, \forall x \, \big( x \in S \iff (x \in A \wedge \varphi(x)) \big)</math><ref name=":0" /><ref name=":1">{{Cite web |title=AxiomaticSetTheory |url=https://www.cs.yale.edu/homes/aspnes/pinewiki/AxiomaticSetTheory.html |access-date=2024-06-08 |website=www.cs.yale.edu |at=Axiom Schema of Specification}}</ref><ref name=":2" />
or in words:
Line 17:
Note that there is one axiom for every such [[predicate (mathematics)|predicate]] <math>\varphi(x)</math>; thus, this is an [[axiom schema]].<ref name=":0" /><ref name=":1" />
To understand this axiom schema, note that the set ''
: Every [[Subclass (set theory)|subclass]] of a set that is defined by a predicate is itself a set.
The preceding form of separation was introduced in 1930 by [[Thoralf Skolem]] as a refinement of a previous, non-first-order<ref>F. R. Drake, ''Set Theory: An Introduction to Large Cardinals (1974), pp.12--13. ISBN 0 444 10535 2.</ref> form by Zermelo.<ref>W. V. O. Quine, ''Mathematical Logic'' (1981), p.164. Harvard University Press, 0-674-55451-5</ref> The axiom schema of specification is characteristic of systems of [[axiomatic set theory]] related to the usual set theory [[ZFC]], but does not usually appear in radically different systems of [[alternative set theory]]. For example, [[New Foundations]] and [[positive set theory]] use different restrictions of the [[#Unrestricted comprehension|axiom of comprehension]] of [[naive set theory]]. The [[Alternative Set Theory]] of Vopenka makes a specific point of allowing proper subclasses of sets, called [[semiset]]s. Even in systems related to ZFC, this scheme is sometimes restricted to formulas with bounded quantifiers, as in [[Kripke–Platek set theory with urelements]].
== Relation to the axiom schema of replacement ==
The axiom schema of specification is implied by the [[axiom schema of replacement]] together with the [[axiom of empty set]].<ref name="GaborMath">{{Cite book |last=Toth |first=Gabor |url=https://books.google.com/books?id=bJhEEAAAQBAJ
▲The axiom schema of specification is implied by the [[axiom schema of replacement]] together with the [[axiom of empty set]].<ref>{{Cite book |last=Toth |first=Gabor |url=https://books.google.com/books?id=bJhEEAAAQBAJ&newbks=0 |title=Elements of Mathematics: A Problem-Centered Approach to History and Foundations |date=2021-09-23 |publisher=Springer Nature |isbn=978-3-030-75051-0 |pages=32 |language=en}}</ref>
The ''axiom schema of replacement'' says that, if a function <math>f</math> is definable by a formula <math>\varphi(x, y, p_1, \ldots, p_n)</math>, then for any set <math>A</math>, there exists a set <math>B = f(A) = \{ f(x) \mid x \in A \}</math>:
:<math>\begin{align}
:<math>\forall A \, \exists B \, \forall C \, ( C \in B \iff \exists D \, [ D \in A \land C = F(D) ] )</math>▼
&\forall x \, \forall y \, \forall z \, \forall p_1 \ldots \forall p_n [ \varphi(x, y, p_1, \ldots, p_n) \wedge \varphi(x, z, p_1, \ldots, p_n) \implies y = z ] \implies \\
▲
\end{align}</math>.<ref name="GaborMath" />
To derive the axiom schema of specification, let <math>\varphi(x, p_1, \ldots, p_n)</math> be a formula and <math>z</math> a set, and define the function <math>f</math> such that <math>f(x) = x</math> if <math>\varphi(x, p_1, \ldots, p_n)</math> is true and <math>f(x) = u</math> if <math>\varphi(x, p_1, \ldots, p_n)</math> is false, where <math>u \in z</math> such that <math>\varphi(u, p_1, \ldots, p_n)</math> is true. Then the set <math>y</math> guaranteed by the axiom schema of replacement is precisely the set <math>y</math> required in the axiom schema of specification. If <math>u</math> does not exist, then <math>f(x)</math> in the axiom schema of specification is the empty set, whose existence (i.e., the axiom of empty set) is then needed.<ref name="GaborMath" />
For this reason, the axiom schema of specification is left out of some axiomatizations of [[Zermelo–Fraenkel set theory|ZF (Zermelo-Frankel) set theory]],<ref name=":3">{{Cite book |last=Bajnok |first=Béla |url=https://books.google.com/books?id=ZZUFEAAAQBAJ |title=An Invitation to Abstract Mathematics |date=2020-10-27 |publisher=Springer Nature |isbn=978-3-030-56174-1 |pages=138 |language=en}}</ref> although some authors, despite the redundancy, include both.<ref>{{Cite book |last=Vaught |first=Robert L. |url=https://books.google.com/books?id=sqxKHEwb5FkC |title=Set Theory: An Introduction |date=2001-08-28 |publisher=Springer Science & Business Media |isbn=978-0-8176-4256-3 |pages=67 |language=en}}</ref> Regardless, the axiom schema of specification is notable because it was in [[Ernst Zermelo|Zermelo]]'s original 1908 list of axioms, before [[Abraham Fraenkel|Fraenkel]] invented the axiom of replacement in 1922.<ref name=":3" /> Additionally, if one takes [[ZFC set theory]] (i.e., ZF with the axiom of choice), removes the axiom of replacement and the [[axiom of collection]], but keeps the axiom schema of specification, one gets the weaker system of axioms called '''ZC''' (i.e., Zermelo's axioms, plus the axiom of choice).<ref>{{Cite book |last1=Kanovei |first1=Vladimir |url=https://books.google.com/books?id=GfDtCAAAQBAJ |title=Nonstandard Analysis, Axiomatically |last2=Reeken |first2=Michael |date=2013-03-09 |publisher=Springer Science & Business Media |isbn=978-3-662-08998-9 |pages=21 |language=en}}</ref>
== Unrestricted comprehension<!--'Unrestricted comprehension' and 'Axiom schema of unrestricted comprehension' redirect here--> ==
Line 89:
==References==
{{reflist}}
==Further reading==
{{refbegin}}
* {{cite book | last1=Crossley | first1=J.bN. | last2=Ash | first2=C. J. | last3=Brickhill | first3=C. J. | last4=Stillwell | first4=J. C. | last5=Williams | first5=N. H. | title=What is mathematical logic? | zbl=0251.02001 | location=London-Oxford-New York | publisher=[[Oxford University Press]] | year=1972 | isbn=0-19-888087-1 }}
Line 95 ⟶ 97:
*Kunen, Kenneth, 1980. ''Set Theory: An Introduction to Independence Proofs''. Elsevier. {{ISBN|0-444-86839-9}}.
{{refend}}
==
{{reflist|group=lower-alpha}}
{{Set theory}}
| |||