Axiom of regularity: Difference between revisions

From Wikipedia
Jump to navigation Jump to search
Browse history interactively
VisualWikitext
imported>Citation bot
Altered template type. Add: class, arxiv, doi, pages, issue, volume, journal, authors 1-1. Removed parameters. Some additions/deletions were parameter name changes. | Use this bot. Report bugs. | Suggested by Headbomb | Category:Articles with missing Cite arXiv inputs | #UCB_Category 1/25
 
imported>Mechanikin
: fixed redirect
 
Line 2: Line 2:
In [[mathematics]], the '''axiom of regularity''' (also known as the '''axiom of foundation''') is an axiom of [[Zermelo–Fraenkel set theory]] that states that every [[Empty set|non-empty]] [[Set (mathematics)|set]] ''A'' contains an element that is [[Disjoint sets|disjoint]] from ''A''. In [[first-order logic]], the axiom reads:
In [[mathematics]], the '''axiom of regularity''' (also known as the '''axiom of foundation''') is an axiom of [[Zermelo–Fraenkel set theory]] that states that every [[Empty set|non-empty]] [[Set (mathematics)|set]] ''A'' contains an element that is [[Disjoint sets|disjoint]] from ''A''. In [[first-order logic]], the axiom reads:


<math display="block">\forall x\,(x \neq \varnothing \rightarrow (\exists y \in x) (y \cap x = \varnothing)).</math>
<math display="block">\forall x\,(x \neq \varnothing \rightarrow (\exists y \in x) (x \cap y = \varnothing)).</math>


The axiom of regularity together with the [[axiom of pairing]] implies that [[Russell paradox|no set is an element of itself]], and that there is no infinite [[sequence]] <math>(a_n)</math> such that <math>a_{i+1}</math> is an element of <math>a_i</math> for all <math>i</math>. With the [[axiom of dependent choice]] (which is a weakened form of the [[axiom of choice]]), this result can be reversed: if there are no such infinite sequences, then the axiom of regularity is true. Hence, in this context the axiom of regularity is equivalent to the sentence that there are no downward infinite membership chains.
The axiom of regularity together with the [[axiom of pairing]] implies that [[Russell's paradox|no set is an element of itself]], and that there is no infinite [[sequence]] <math>(a_n)</math> such that <math>a_{i+1}</math> is an element of <math>a_i</math> for all <math>i</math>. With the [[axiom of dependent choice]] (which is a weakened form of the [[axiom of choice]]), this result can be reversed: if there are no such infinite sequences, then the axiom of regularity is true. Hence, in this context the axiom of regularity is equivalent to the sentence that there are no downward infinite membership chains.


The axiom was originally formulated by von Neumann;{{sfn|von Neumann|1925}} it was adopted in a formulation closer to the one found in contemporary textbooks by Zermelo.{{sfn|Zermelo|1930}} Virtually all results in the branches of mathematics based on set theory hold even in the absence of regularity.{{sfn|Kunen|1980|loc=ch. 3}} However, regularity makes some properties of [[Ordinal number|ordinals]] easier to prove; and it not only allows induction to be done on [[well-ordering|well-ordered sets]] but also on proper classes that are [[well-founded relation|well-founded relational structures]] such as the [[lexicographical ordering]] on <math display="inline">\{ (n, \alpha) \mid n \in \omega \land \alpha \text{ is an ordinal } \} \,.</math>
The axiom was originally formulated by [[John von Neumann|von Neumann]];{{sfn|von Neumann|1925}} it was adopted in a formulation closer to the one found in contemporary textbooks by [[Zermelo]].{{sfn|Zermelo|1930}} Virtually all results in the branches of mathematics based on set theory hold even in the absence of regularity.{{sfn|Kunen|1980|loc=ch. 3}} However, regularity makes some properties of [[Ordinal number|ordinals]] easier to prove; and it not only allows induction to be done on [[well-ordering|well-ordered sets]] but also on [[proper class]]es that are [[well-founded relation|well-founded relational structures]] such as the [[lexicographical ordering]] on <math display="inline">\{ (n, \alpha) \mid n \in \omega \land \alpha \text{ is an ordinal } \} \,.</math>


Given the other axioms of Zermelo–Fraenkel set theory, the axiom of regularity is equivalent to the [[epsilon-induction|axiom of induction]]. The axiom of induction tends to be used in place of the axiom of regularity in [[intuitionism|intuitionistic]] theories (ones that do not accept the [[law of the excluded middle]]), where the two axioms are not equivalent.
Given the other axioms of Zermelo–Fraenkel set theory, the axiom of regularity is equivalent to the [[epsilon-induction|axiom of induction]]. The axiom of induction tends to be used in place of the axiom of regularity in [[intuitionism|intuitionistic]] theories (ones that do not accept the [[law of the excluded middle]]), where the two axioms are not equivalent.
Line 18: Line 18:


===No infinite descending sequence of sets exists===
===No infinite descending sequence of sets exists===
Suppose, to the contrary, that there is a [[function (mathematics)|function]], ''f'', on the [[natural number]]s with ''f''(''n''+1) an element of ''f''(''n'') for each ''n''. Define ''S'' = {''f''(''n''): ''n'' a natural number}, the range of ''f'', which can be seen to be a set from the [[axiom schema of replacement]]. Applying the axiom of regularity to ''S'', let ''B'' be an element of ''S'' which is disjoint from ''S''. By the definition of ''S'', ''B'' must be ''f''(''k'') for some natural number ''k''. However, we are given that ''f''(''k'') contains ''f''(''k''+1) which is also an element of ''S''. So ''f''(''k''+1) is in the [[Intersection (set theory)|intersection]] of ''f''(''k'') and ''S''. This contradicts the fact that they are disjoint sets. Since our supposition led to a contradiction, there must not be any such function, ''f''.
Suppose, to the contrary, that there is a [[function (mathematics)|function]], ''f'', on the [[natural number]]s with ''f''(''n''+1) an element of ''f''(''n'') for each ''n''. Define ''S'' = {''f''(''n''): ''n'' a natural number}, the range of ''f'', which can be seen to be a set from the [[axiom schema of replacement]]. Applying the axiom of regularity to ''S'', let ''B'' be an element of ''S'', which is disjoint from ''S''. By the definition of ''S'', ''B'' must be ''f''(''k'') for some natural number ''k''. However, we are given that ''f''(''k'') contains ''f''(''k''+1), which is also an element of ''S''. So ''f''(''k''+1) is in the [[Intersection (set theory)|intersection]] of ''f''(''k'') and ''S''. This contradicts the fact that they are disjoint sets. Since our supposition led to a contradiction, there must not be any such function, ''f''.


The nonexistence of a set containing itself can be seen as a special case where the sequence is infinite and constant.
The nonexistence of a set containing itself can be seen as a special case where the sequence is infinite and constant.


Notice that this argument only applies to functions ''f'' that can be represented as sets as opposed to undefinable classes. The [[hereditarily finite set]]s, ''V''<sub>ω</sub>, satisfy the axiom of regularity (and all other axioms of [[ZFC]] except the [[axiom of infinity]]). So if one forms a non-trivial [[ultraproduct|ultrapower]] of V<sub>ω</sub>, then it will also satisfy the axiom of regularity. The resulting [[model (logic)|model]] <!--WHAT model?--> will contain elements, called non-standard natural numbers, that satisfy the definition of natural numbers in that model but are not really natural numbers.{{dubious|date=February 2023|reason=They satisfy the first-order Peano axioms, so it seems dubious to claim that they are not actually natural numbers. They presumably do not satisfy the second-order Peano axioms with respect to the subset relation of the "ambient" set theory inside of which the model is constructed. But don't they actually satisfy the second-order Peano axioms with respect to the internal subset relation of the model?}} They are "fake" natural numbers which are "larger" than any actual natural number. This model will contain infinite descending sequences of elements.{{clarification needed|date=February 2023|reason=Is the set membership relation in this infinite descending chain the "internal" set membership relation of the model? (I.e. the model's interpretation of the set membership relation?) Or is what follows referring to the set membership relation of the "ambient" set theory in which the model is constructed? Presumably it can't be the latter, because the fact that the latter has a von Neumann cumulative hierarchy, e.g. V_omega, seems to presuppose that it satisfies regularity, and thus otherwise this section would be describing a contradiction. If so, then this section ideally would clarify that what follows refers to the model's interpretation of the set membership relation, and that this is necessarily distinct from (in particular not the restriction of) the ambient set theory's set membership relation.}} For example, suppose ''n'' is a non-standard natural number, then <math display="inline">(n-1) \in n</math> and <math display="inline">(n-2) \in (n-1)</math>, and so on. For any actual natural number ''k'', <math display="inline">(n-k-1) \in (n-k)</math>. This is an unending descending sequence of elements. But this sequence is not definable in the model and thus not a set.  So no contradiction to regularity can be proved.
Notice that this argument only applies to functions ''f'' that can be represented as sets as opposed to undefinable classes. The [[hereditarily finite set]]s, ''V''<sub>ω</sub>, satisfy the axiom of regularity (and all other axioms of [[ZFC]] except the [[axiom of infinity]]). So if one forms a non-trivial [[ultraproduct|ultrapower]] of ''V''<sub>ω</sub>, then it will also satisfy the axiom of regularity. The resulting [[structure (logic)|structure]] <!--WHAT model?--> will contain elements, called non-standard natural numbers, that satisfy the definition of natural numbers in that structure but are not really natural numbers. They are "fake" natural numbers that are "larger" than any actual natural number. This structure will contain infinite descending (with respect to the interpretation of <math>\in</math> in the structure) sequences of elements. For example, suppose ''n'' is a non-standard natural number, then <math display="inline">(n-1) \in n</math> and <math display="inline">(n-2) \in (n-1)</math>, and so on. For any actual natural number ''k'', <math display="inline">(n-k-1) \in (n-k)</math>. This is an unending descending sequence of elements. But this sequence is not definable in the structure and thus not a set.  So no contradiction to regularity can be proved.


===Simpler set-theoretic definition of the ordered pair===
===Simpler set-theoretic definition of the ordered pair===
Line 30: Line 30:
This was actually the original form of the axiom in von Neumann's axiomatization.
This was actually the original form of the axiom in von Neumann's axiomatization.


Suppose ''x'' is any set. Let ''t'' be the [[transitive closure (set)|transitive closure]] of {''x''}. Let ''u'' be the subset of ''t'' consisting of unranked sets. If ''u'' is empty, then ''x'' is ranked and we are done. Otherwise, apply the axiom of regularity to ''u'' to get an element ''w'' of ''u'' which is disjoint from ''u''. Since ''w'' is in ''u'', ''w'' is unranked. ''w'' is a subset of ''t'' by the definition of transitive closure. Since ''w'' is disjoint from ''u'', every element of ''w'' is ranked. Applying the axioms of replacement and union to combine the ranks of the elements of ''w'', we get an ordinal rank for ''w'', to wit <math display="inline">\textstyle \operatorname{rank} (w) = \cup \{ \operatorname{rank} (z) + 1 \mid z \in w \}</math>. This contradicts the conclusion that ''w'' is unranked. So the assumption that ''u'' was non-empty must be false and ''x'' must have rank.
To prove it from the axiom of regularity, suppose ''x'' is any set. Let ''t'' be the [[transitive closure (set)|transitive closure]] of {''x''}. Let ''u'' be the subset of ''t'' consisting of unranked sets. If ''u'' is empty, then ''x'' is ranked and we are done. Otherwise, apply the axiom of regularity to ''u'' to get an element ''w'' of ''u'' that is disjoint from ''u''. Since ''w'' is in ''u'', ''w'' is unranked. ''w'' is a subset of ''t'' by the definition of transitive closure. Since ''w'' is disjoint from ''u'', every element of ''w'' is ranked. Applying the axioms of replacement and [[axiom of union|union]] to combine the ranks of the elements of ''w'', we get an ordinal rank for ''w'', to wit <math display="inline">\textstyle \operatorname{rank} (w) = \cup \{ \operatorname{rank} (z) + 1 \mid z \in w \}</math>. This contradicts the conclusion that ''w'' is unranked. So the assumption that ''u'' was non-empty must be false and ''x'' must have rank.


=== For every two sets, only one can be an element of the other ===
=== For every two sets, only one can be an element of the other ===
Let ''X'' and ''Y'' be sets. Then apply the axiom of regularity to the set {''X'',''Y''} (which exists by the axiom of pairing). We see there must be an element of {''X'',''Y''} which is also disjoint from it. It must be either ''X'' or ''Y''. By the definition of disjoint then, we must have either ''Y'' is not an element of ''X'' or vice versa.
Let ''X'' and ''Y'' be sets. Then apply the axiom of regularity to the set {''X'',''Y''} (which exists by the axiom of pairing). We see there must be an element of {''X'',''Y''} that is also disjoint from it. It must be either ''X'' or ''Y''. By the definition of disjoint then, we must have either ''Y'' is not an element of ''X'' or vice versa.


==The axiom of dependent choice and no infinite descending sequence of sets implies regularity==
==The axiom of dependent choice and no infinite descending sequence of sets implies regularity==
Line 39: Line 39:


== Regularity and the rest of ZF(C) axioms ==
== Regularity and the rest of ZF(C) axioms ==
Regularity was shown to be relatively consistent with the rest of ZF by Skolem{{sfn|Skolem|1923}} and von Neumann,{{sfn|von Neumann|1929}} meaning that if ZF without regularity is consistent, then ZF (with regularity) is also consistent.<ref>For his{{ambiguous|reason=Skolem or Von Neumann?|date=December 2024}} proof in modern notation, see {{harvtxt|Vaught|2001|loc=§10.1}} for instance.</ref>
Regularity was shown to be relatively consistent with the rest of ZF by [[Thoralf Skolem|Skolem]]{{sfn|Skolem|1923}} and von Neumann,{{sfn|von Neumann|1929}} meaning that if ZF without regularity is consistent, then ZF (with regularity) is also consistent.<ref>For his{{ambiguous|reason=Skolem or Von Neumann?|date=December 2024}} proof in modern notation, see {{harvtxt|Vaught|2001|loc=§10.1}} for instance.</ref>


The axiom of regularity was also shown to be [[Independence (mathematical logic)|independent]] from the other axioms of ZFC, assuming they are consistent. The result was announced by [[Paul Bernays]] in 1941, although he did not publish a proof until 1954. The proof involves (and led to the study of) Rieger-Bernays [[permutation model]]s (or method), which were used for other proofs of independence for non-well-founded systems.{{sfn|Rathjen|2004|p=193}}{{sfn|Forster|2003|pp=210–212}}
The axiom of regularity was also shown to be [[Independence (mathematical logic)|independent]] from the other axioms of ZFC, assuming they are consistent. The result was announced by [[Paul Bernays]] in 1941, although he did not publish a proof until 1954. The proof involves (and led to the study of) Rieger–Bernays [[permutation model]]s (or method), which were used for other proofs of independence for non-well-founded systems.{{sfn|Rathjen|2004|p=193}}{{sfn|Forster|2003|pp=210–212}}


== Regularity in ordinary mathematics ==
== Regularity in ordinary mathematics ==


The axiom of regularity is rarely useful outside of set theory; A. A. Fraenkel, Y. Bar-Hillel and A. Levy noted that<ref>{{cite book | last1=Fraenkel | first1=A.A. | last2=Bar-Hillel | first2=Y. | last3=Levy | first3=A. | title=Foundations of Set Theory | publisher=North Holland | publication-place=Amsterdam | date=1973 | isbn=0-7204-2270-1}}</ref> “its omission will not incapacitate any field of mathematics”. Its inclusion, therefore, can be considered as chiefly a clarification of what one means by “set”, as elaborated on by the [[Mostowski collapse lemma]] (which provides the converse: that not only is membership on every set a well-founded and extensional relation, but that any such relation admits a corresponding set). If one performs mathematics in a more structural setting, for example by using a [[Type theory|type theory]] or [[Structural set theory|structural set theory]] like ETCS, the axiom is not used at all, since it is not needed to prove that '''Set''', the category of sets, forms an [[elementary topos]].<ref>{{cite journal|last=Shulman|first=Michael|date=2018|title=Comparing material and structural set theories|journal=Annals of Pure and Applied Logic |volume=170 |issue=4 |pages=465–504 |doi=10.1016/j.apal.2018.11.002 |arxiv=1808.05204}}</ref>
The axiom of regularity is rarely useful outside of set theory; A. A. Fraenkel, Y. Bar-Hillel and A. Levy noted that<ref>{{cite book | last1=Fraenkel | first1=A.A. | last2=Bar-Hillel | first2=Y. | last3=Levy | first3=A. | title=Foundations of Set Theory | publisher=North Holland | publication-place=Amsterdam | date=1973 | isbn=0-7204-2270-1}}</ref> “its omission will not incapacitate any field of mathematics”. Its inclusion, therefore, can be considered as chiefly a clarification of what one means by “set”, as elaborated on by the [[Mostowski collapse lemma]] (which provides the converse: that not only is membership on every set a well-founded and extensional relation, but that any such relation admits a corresponding set). If one performs mathematics in a more structural setting, for example by using a [[type theory]] or [[structural set theory]] like [[elementary theory of the category of sets|ETCS]], the axiom is not used at all, since it is not needed to prove that '''Set''', the category of sets, forms an [[elementary topos]].<ref>{{cite journal|last=Shulman|first=Michael|date=2018|title=Comparing material and structural set theories|journal=[[Annals of Pure and Applied Logic]] |volume=170 |issue=4 |pages=465–504 |doi=10.1016/j.apal.2018.11.002 |arxiv=1808.05204}}</ref>


However, it does have practical uses, especially in the absence of the [[Axiom of choice|axiom of choice]]. One application is [[Scott's trick]] for constructing equivalence classes of a relation defined on proper classes, as an alternative to postulating a [[Grothendieck universe]]; it may also be used as an alternative to choice in the proof of [[Frucht's theorem]] for infinite groups.<ref>{{cite arXiv|last=Pinsky|first=Brian|date=2023|title=Frucht's Theorem without Choice|class=math.LO |eprint=2305.11382}}</ref>
However, it does have practical uses, especially in the absence of the [[axiom of choice]]. One application is [[Scott's trick]] for constructing equivalence classes of a relation defined on proper classes, as an alternative to postulating a [[Grothendieck universe]]; it may also be used as an alternative to choice in the proof of [[Frucht's theorem]] for infinite groups.<ref>{{cite arXiv|last=Pinsky|first=Brian|date=2023|title=Frucht's Theorem without Choice|class=math.LO |eprint=2305.11382}}</ref>


== Regularity and Russell's paradox ==
== Regularity and Russell's paradox ==
[[Naive set theory]] (the axiom schema of [[unrestricted comprehension]] and the [[axiom of extensionality]]) is inconsistent due to [[Russell's paradox]]. In early formalizations of sets, mathematicians and logicians have avoided that contradiction by replacing the axiom schema of comprehension with the much weaker [[axiom schema of separation]]. However, this step alone takes one to theories of sets which are considered too weak.{{clarification needed|date=January 2023|reason=This seems to have in mind a specific result or interpretation, however what that might be is not stated. Ideally that would be given, along with a citation of at least one reference stating/explaining the corresponding result/interpretation.}}{{citation needed|date=January 2023}} So some of the power of comprehension was added back via the other existence axioms of ZF set theory (pairing, union, powerset, replacement, and infinity) which may be regarded as special cases of comprehension.{{citation needed|date=January 2023}}{{clarification needed|date=January 2023|reason=Interpreting this literally, if these axioms were all special cases of the particular comprehension axiom, then adding them back would neither strengthen nor weaken the theory. So clearly something slightly different is what the author had in mind, and expressed it this way heuristically. Fine. But a reference to a more precise explanation/result could still be helpful.}} So far, these axioms do not seem to lead to any contradiction. Subsequently, the axiom of choice and the axiom of regularity were added to exclude models with some undesirable properties. These two axioms are known to be relatively consistent.
[[Naive set theory]] (the axiom schema of [[unrestricted comprehension]] and the [[axiom of extensionality]]) is inconsistent due to [[Russell's paradox]]. In early formalizations of sets, mathematicians and logicians avoided that contradiction by simply replacing the axiom schema of comprehension with the much weaker [[axiom schema of separation]]. However, this step alone takes one to theories of sets that are considered too weak.{{clarification needed|date=January 2023|reason=This seems to have in mind a specific result or interpretation, however what that might be is not stated. Ideally that would be given, along with a citation of at least one reference stating/explaining the corresponding result/interpretation.}}{{citation needed|date=January 2023}} So some of the power of comprehension was added back via the other existence axioms of ZF set theory (pairing, union, [[powerset axiom|powerset]], replacement, and infinity), which may be regarded as special cases of comprehension.{{citation needed|date=January 2023}} So far, these axioms do not seem to lead to any contradiction. Subsequently, the axiom of choice and the axiom of regularity were added to exclude models with some undesirable properties. These two axioms are known to be relatively consistent.


In the presence of the axiom schema of separation, Russell's paradox becomes a proof that there is no [[universal set|set of all sets]]. The axiom of regularity together with the axiom of pairing also prohibit such a universal set. However, Russell's paradox yields a proof that there is no "set of all sets" using the axiom schema of separation alone, without any additional axioms. In particular, ZF without the axiom of regularity already prohibits such a universal set.
In the presence of the axiom schema of separation, Russell's paradox becomes a proof that there is no [[universal set|set of all sets]]. The axiom of regularity together with the axiom of pairing also prohibit such a universal set. However, Russell's paradox yields a proof that there is no "set of all sets" using the axiom schema of separation alone, without any additional axioms. In particular, ZF without the axiom of regularity already prohibits such a universal set.


If a theory is extended by adding an axiom or axioms, then any (possibly undesirable) consequences of the original theory remain consequences of the extended theory. In particular, if ZF without regularity is extended by adding regularity to get ZF, then any contradiction (such as Russell's paradox) which followed from the original theory would still follow in the extended theory.
If a theory is extended by adding an axiom or axioms, then any (possibly undesirable) consequences of the original theory remain consequences of the extended theory. In particular, if ZF without regularity is extended by adding regularity to get ZF, then any contradiction that followed from the original theory would still follow in the extended theory.


The existence of [[Quine atom]]s (sets that satisfy the formula equation ''x''&nbsp;=&nbsp;{''x''}, i.e. have themselves as their only elements) is consistent with the theory obtained by removing the axiom of regularity from ZFC. Various [[non-well-founded set theory|non-wellfounded set theories]] allow "safe" circular sets, such as Quine atoms, without becoming inconsistent by means of Russell's paradox.{{sfn|Rieger|2011|pp=175,178}}
The existence of [[Quine atom]]s (sets that satisfy the formula equation ''x''&nbsp;=&nbsp;{''x''}, i.e. have themselves as their only elements) is consistent with the theory obtained by removing the axiom of regularity from ZFC. Various [[non-well-founded set theory|non-wellfounded set theories]] allow "safe" circular sets, such as Quine atoms, without becoming inconsistent by means of Russell's paradox.{{sfn|Rieger|2011|pp=175,178}}


== Regularity, the cumulative hierarchy, and types ==
== Regularity, the cumulative hierarchy, and types ==
In ZF it can be proven that the class <math display="inline"> \bigcup_{\alpha} V_\alpha </math>, called the [[von Neumann universe]], is equal to the class of all sets. This statement is even equivalent to the axiom of regularity (if we work in ZF with this axiom omitted). From any model which does not satisfy the axiom of regularity, a model which satisfies it can be constructed by taking only sets in <math display="inline"> \bigcup_{\alpha} V_\alpha </math>.
In ZF it can be proven that the class <math display="inline"> \bigcup_{\alpha} V_\alpha </math>, called the [[von Neumann universe]], is equal to the class of all sets. This statement is even equivalent to the axiom of regularity (if we work in ZF with this axiom omitted). From any model that does not satisfy the axiom of regularity, a model that satisfies it can be constructed by taking only sets in <math display="inline"> \bigcup_{\alpha} V_\alpha </math>.


Herbert Enderton{{sfn|Enderton|1977|loc=p. 206}} wrote that "The idea of rank is a descendant of Russell's concept of ''type''". Comparing ZF with [[type theory]], [[Alasdair Urquhart]] wrote that "Zermelo's system has the notational advantage of not containing any explicitly typed variables, although in fact it can be seen as having an implicit type structure built into it, at least if the axiom of regularity is included.<ref>The details of this implicit typing are spelled out in {{harvnb|Zermelo|1930}}, and again in {{harvnb|Boolos|1971}}.</ref>{{sfn|Urquhart|2003|p=305}}
[[Herbert Enderton]]{{sfn|Enderton|1977|loc=p. 206}} wrote that "The idea of rank is a descendant of Russell's concept of ''type''". Comparing ZF with [[type theory]], [[Alasdair Urquhart]] wrote that "Zermelo's system has the notational advantage of not containing any explicitly typed variables, although in fact it can be seen as having an implicit type structure built into it, at least if the axiom of regularity is included.<ref>The details of this implicit typing are spelled out in {{harvnb|Zermelo|1930}}, and again in {{harvnb|Boolos|1971}}.</ref>{{sfn|Urquhart|2003|p=305}}


Dana Scott{{sfn|Scott|1974}} went further and claimed that:
[[Dana Scott]]{{sfn|Scott|1974}} went further and claimed that:


{{Blockquote|The truth is that there is only one satisfactory way of avoiding the paradoxes: namely, the use of some form of the ''theory of types''. That was at the basis of both Russell's and Zermelo's intuitions. Indeed the best way to regard Zermelo's theory is as a simplification and extension of Russell's. (We mean Russell's ''simple'' theory of types, of course.) The simplification was to make the types ''cumulative''. Thus mixing of types is easier and annoying repetitions are avoided. Once the later types are allowed to accumulate the earlier ones, we can then easily imagine ''extending'' the types into the transfinite&mdash;just how far we want to go must necessarily be left open. Now Russell made his types ''explicit'' in his notation and Zermelo left them ''implicit''. [emphasis in original]}}
{{Blockquote|The truth is that there is only one satisfactory way of avoiding the paradoxes: namely, the use of some form of the ''theory of types''. That was at the basis of both Russell's and Zermelo's intuitions. Indeed the best way to regard Zermelo's theory is as a simplification and extension of Russell's. (We mean Russell's ''simple'' theory of types, of course.) The simplification was to make the types ''cumulative''. Thus mixing of types is easier and annoying repetitions are avoided. Once the later types are allowed to accumulate the earlier ones, we can then easily imagine ''extending'' the types into the transfinite&mdash;just how far we want to go must necessarily be left open. Now Russell made his types ''explicit'' in his notation and Zermelo left them ''implicit''. [emphasis in original]}}
Line 73: Line 73:
The concept of well-foundedness and [[Von Neumann universe|rank]] of a set were both introduced by [[Dmitry Mirimanoff]].{{sfn|Mirimanoff|1917}}<ref>cf. {{harvnb|Lévy|2002|p=68}} and {{harvnb|Hallett|1996|loc=§4.4, esp. p. 186, 188}}.</ref> Mirimanoff called a set ''x'' "regular" ({{langx|fr|ordinaire}}) if every descending chain ''x'' ∋ ''x''<sub>1</sub> ∋ ''x''<sub>2</sub>  ∋ ... is finite. Mirimanoff however did not consider his notion of regularity (and well-foundedness) as an axiom to be observed by all sets;{{sfn|Halbeisen|2012|pp=62–63}} in later papers Mirimanoff also explored what are now called [[non-well-founded set theory|non-well-founded sets]] ({{lang|fr|extraordinaire}} in Mirimanoff's terminology).{{sfn|Sangiorgi|2011|pp=17–19, 26}}
The concept of well-foundedness and [[Von Neumann universe|rank]] of a set were both introduced by [[Dmitry Mirimanoff]].{{sfn|Mirimanoff|1917}}<ref>cf. {{harvnb|Lévy|2002|p=68}} and {{harvnb|Hallett|1996|loc=§4.4, esp. p. 186, 188}}.</ref> Mirimanoff called a set ''x'' "regular" ({{langx|fr|ordinaire}}) if every descending chain ''x'' ∋ ''x''<sub>1</sub> ∋ ''x''<sub>2</sub>  ∋ ... is finite. Mirimanoff however did not consider his notion of regularity (and well-foundedness) as an axiom to be observed by all sets;{{sfn|Halbeisen|2012|pp=62–63}} in later papers Mirimanoff also explored what are now called [[non-well-founded set theory|non-well-founded sets]] ({{lang|fr|extraordinaire}} in Mirimanoff's terminology).{{sfn|Sangiorgi|2011|pp=17–19, 26}}


Skolem{{sfn|Skolem|1923}} and von Neumann{{sfn|von Neumann|1925}} pointed out that non-well-founded sets are superfluous{{sfn|van Heijenoort|1967|p=404}} and in the same publication von Neumann gives an axiom{{sfn|van Heijenoort|1967|p=412}} which excludes some, but not all, non-well-founded sets.{{sfn|Rieger|2011|p=179}} In a subsequent publication, von Neumann{{sfn|von Neumann|1929|p=231}} gave an equivalent but more complex version of the axiom of class foundation:<ref>cf. {{harvnb|Suppes|1972|p=53}} and {{harvnb|Lévy|2002|p=72}}</ref>
Skolem{{sfn|Skolem|1923}} and von Neumann{{sfn|von Neumann|1925}} pointed out that non-well-founded sets are superfluous{{sfn|van Heijenoort|1967|p=404}} and in the same publication von Neumann gives an axiom{{sfn|van Heijenoort|1967|p=412}} that excludes some, but not all, non-well-founded sets.{{sfn|Rieger|2011|p=179}} In a subsequent publication, von Neumann{{sfn|von Neumann|1929|p=231}} gave an equivalent but more complex version of the axiom of class foundation:<ref>cf. {{harvnb|Suppes|1972|p=53}} and {{harvnb|Lévy|2002|p=72}}</ref>


<math display="block"> A \neq \emptyset \rightarrow \exists x \in A\,(x \cap A = \emptyset).</math>
<math display="block"> A \neq \emptyset \rightarrow \exists x \in A\,(x \cap A = \emptyset).</math>
Line 92: Line 92:


==Sources==
==Sources==
* {{cite journal |first=Paul Isaac|last= Bernays|author-link=Paul Bernays| title= A system of axiomatic set theory. Part II |journal= The Journal of Symbolic Logic| volume= 6 |issue= 1| year = 1941 | pages = 1–17 | doi=10.2307/2267281 | jstor=2267281|s2cid= 250344277}}
* {{cite journal |first=Paul Isaac|last= Bernays|author-link=Paul Bernays| title= A system of axiomatic set theory. Part II |journal= [[The Journal of Symbolic Logic]]| volume= 6 |issue= 1| year = 1941 | pages = 1–17 | doi=10.2307/2267281 | jstor=2267281|s2cid= 250344277}}
* {{cite journal | first= Paul Isaac|last = Bernays|author-link=Paul Bernays| title= A system of axiomatic set theory. Part VII |journal = The Journal of Symbolic Logic| volume = 19 |issue = 2| year = 1954 | pages = 81–96 | doi=10.2307/2268864 | jstor=2268864| s2cid=250351655 | url = http://doc.rero.ch/record/301843/files/S0022481200087570.pdf}}
* {{cite journal | first= Paul Isaac|last = Bernays|author-link=Paul Bernays| title= A system of axiomatic set theory. Part VII |journal = The Journal of Symbolic Logic| volume = 19 |issue = 2| year = 1954 | pages = 81–96 | doi=10.2307/2268864 | jstor=2268864| s2cid=250351655 | url = http://doc.rero.ch/record/301843/files/S0022481200087570.pdf}}
*{{cite journal|last=Boolos|first= George |author-link=George Boolos | year= 1971 | title = The iterative conception of set | journal = Journal of Philosophy | volume = 68 |issue= 8 |pages= 215–231 | doi=10.2307/2025204 | jstor=2025204}} Reprinted in {{cite book|last=Boolos|first= George |year=1998|title=Logic, Logic and Logic|pages=13–29|publisher=Harvard University Press}}
*{{cite journal|last=Boolos|first= George |author-link=George Boolos | year= 1971 | title = The iterative conception of set | journal = [[Journal of Philosophy]] | volume = 68 |issue= 8 |pages= 215–231 | doi=10.2307/2025204 | jstor=2025204}} Reprinted in {{cite book|last=Boolos|first= George |year=1998|title=Logic, Logic and Logic|pages=13–29|publisher=Harvard University Press}}
*{{cite book | last= Enderton | first = Herbert B. | title = Elements of Set Theory | publisher = Academic Press | year=1977}}
*{{cite book | last= Enderton | first = Herbert B. | title = Elements of Set Theory | publisher = Academic Press | year=1977}}
*{{cite book|title = Logic, induction and sets| last = Forster | first = T. | publisher = Cambridge University Press | year = 2003}}
*{{cite book|title = Logic, induction and sets| last = Forster | first = T. | publisher = Cambridge University Press | year = 2003}}
Line 127: Line 127:
*{{cite journal|last = von Neumann|first = John| author-link=John von Neumann |year= 1928|title= Über die Definition durch transfinite Induktion und verwandte Fragen der allgemeinen Mengenlehre|language=de| journal= Mathematische Annalen|volume = 99 |pages=373–391|doi=10.1007/BF01459102|s2cid = 120784562}}
*{{cite journal|last = von Neumann|first = John| author-link=John von Neumann |year= 1928|title= Über die Definition durch transfinite Induktion und verwandte Fragen der allgemeinen Mengenlehre|language=de| journal= Mathematische Annalen|volume = 99 |pages=373–391|doi=10.1007/BF01459102|s2cid = 120784562}}
*{{cite journal| last = von Neumann |first = John| author-link=John von Neumann| year = 1929 | title= Über eine Widerspruchfreiheitsfrage in der axiomatischen Mengenlehre|language=de| journal = Journal für die Reine und Angewandte Mathematik |volume = 1929 |issue = 160|pages = 227–241 | doi=10.1515/crll.1929.160.227|s2cid = 199545822}}
*{{cite journal| last = von Neumann |first = John| author-link=John von Neumann| year = 1929 | title= Über eine Widerspruchfreiheitsfrage in der axiomatischen Mengenlehre|language=de| journal = Journal für die Reine und Angewandte Mathematik |volume = 1929 |issue = 160|pages = 227–241 | doi=10.1515/crll.1929.160.227|s2cid = 199545822}}
*{{cite journal |last=Zermelo|first= Ernst |author-link=Ernst Zermelo | year= 1930 | title = Über Grenzzahlen und Mengenbereiche. Neue Untersuchungen über die Grundlagen der Mengenlehre |language=de| journal = Fundamenta Mathematicae | volume = 16 |pages= 29–47|url=http://matwbn.icm.edu.pl/ksiazki/fm/fm16/fm1615.pdf |archive-url=https://ghostarchive.org/archive/20221009/http://matwbn.icm.edu.pl/ksiazki/fm/fm16/fm1615.pdf |archive-date=2022-10-09 |url-status=live|doi= 10.4064/fm-16-1-29-47 |doi-access= free }} Translation in {{cite book | editor-last= Ewald |editor-first= W. B. | year = 1996| title = From Kant to Hilbert: A Source Book in the Foundations of Mathematics |volume=2 | publisher= Clarendon Press |pages = 1219–1233}}
*{{cite journal |last=Zermelo|first= Ernst |author-link=Ernst Zermelo | year= 1930 | title = Über Grenzzahlen und Mengenbereiche. Neue Untersuchungen über die Grundlagen der Mengenlehre |language=de| journal = [[Fundamenta Mathematicae]] | volume = 16 |pages= 29–47|url=http://matwbn.icm.edu.pl/ksiazki/fm/fm16/fm1615.pdf |archive-url=https://ghostarchive.org/archive/20221009/http://matwbn.icm.edu.pl/ksiazki/fm/fm16/fm1615.pdf |archive-date=2022-10-09 |url-status=live|doi= 10.4064/fm-16-1-29-47 |doi-access= free }} Translation in {{cite book | editor-last= Ewald |editor-first= W. B. | year = 1996| title = From Kant to Hilbert: A Source Book in the Foundations of Mathematics |volume=2 | publisher= Clarendon Press |pages = 1219–1233}}


==External links==
==External links==

Latest revision as of 22:03, 11 May 2026

In mathematics, the axiom of regularity (also known as the axiom of foundation) is an axiom of Zermelo–Fraenkel set theory that states that every non-empty set A contains an element that is disjoint from A. In first-order logic, the axiom reads:

Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \forall x\,(x \neq \varnothing \rightarrow (\exists y \in x) (x \cap y = \varnothing)).}

The axiom of regularity together with the axiom of pairing implies that no set is an element of itself, and that there is no infinite sequence Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle (a_n)} such that Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle a_{i+1}} is an element of Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle a_i} for all Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle i} . With the axiom of dependent choice (which is a weakened form of the axiom of choice), this result can be reversed: if there are no such infinite sequences, then the axiom of regularity is true. Hence, in this context the axiom of regularity is equivalent to the sentence that there are no downward infinite membership chains.

The axiom was originally formulated by von Neumann;[1] it was adopted in a formulation closer to the one found in contemporary textbooks by Zermelo.[2] Virtually all results in the branches of mathematics based on set theory hold even in the absence of regularity.[3] However, regularity makes some properties of ordinals easier to prove; and it not only allows induction to be done on well-ordered sets but also on proper classes that are well-founded relational structures such as the lexicographical ordering on Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\textstyle \{ (n, \alpha) \mid n \in \omega \land \alpha \text{ is an ordinal } \} \,.}

Given the other axioms of Zermelo–Fraenkel set theory, the axiom of regularity is equivalent to the axiom of induction. The axiom of induction tends to be used in place of the axiom of regularity in intuitionistic theories (ones that do not accept the law of the excluded middle), where the two axioms are not equivalent.

In addition to omitting the axiom of regularity, non-standard set theories have indeed postulated the existence of sets that are elements of themselves.

Elementary implications of regularity

No set is an element of itself

Let Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle A} be a set, and apply the axiom of regularity to Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \{A\}} , which is a set by the axiom of pairing. By this axiom, there must be an element of Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \{A\}} which is disjoint from Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \{A\}} . Since the only element of Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \{A\}} is Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle A} , it must be that Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle A} is disjoint from Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \{A\}} . So, since Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\textstyle A \cap \{A\} = \varnothing} , we cannot have Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle A} an element of Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle A} (by the definition of disjointness).

No infinite descending sequence of sets exists

Suppose, to the contrary, that there is a function, f, on the natural numbers with f(n+1) an element of f(n) for each n. Define S = {f(n): n a natural number}, the range of f, which can be seen to be a set from the axiom schema of replacement. Applying the axiom of regularity to S, let B be an element of S, which is disjoint from S. By the definition of S, B must be f(k) for some natural number k. However, we are given that f(k) contains f(k+1), which is also an element of S. So f(k+1) is in the intersection of f(k) and S. This contradicts the fact that they are disjoint sets. Since our supposition led to a contradiction, there must not be any such function, f.

The nonexistence of a set containing itself can be seen as a special case where the sequence is infinite and constant.

Notice that this argument only applies to functions f that can be represented as sets as opposed to undefinable classes. The hereditarily finite sets, Vω, satisfy the axiom of regularity (and all other axioms of ZFC except the axiom of infinity). So if one forms a non-trivial ultrapower of Vω, then it will also satisfy the axiom of regularity. The resulting structure will contain elements, called non-standard natural numbers, that satisfy the definition of natural numbers in that structure but are not really natural numbers. They are "fake" natural numbers that are "larger" than any actual natural number. This structure will contain infinite descending (with respect to the interpretation of Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \in} in the structure) sequences of elements. For example, suppose n is a non-standard natural number, then Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\textstyle (n-1) \in n} and Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\textstyle (n-2) \in (n-1)} , and so on. For any actual natural number k, Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\textstyle (n-k-1) \in (n-k)} . This is an unending descending sequence of elements. But this sequence is not definable in the structure and thus not a set. So no contradiction to regularity can be proved.

Simpler set-theoretic definition of the ordered pair

The axiom of regularity enables defining the ordered pair (a,b) as {a,{a,b}}; see ordered pair for specifics. This definition eliminates one pair of braces from the canonical Kuratowski definition (a,b) = {{a},{a,b}}.

Every set has an ordinal rank

This was actually the original form of the axiom in von Neumann's axiomatization.

To prove it from the axiom of regularity, suppose x is any set. Let t be the transitive closure of {x}. Let u be the subset of t consisting of unranked sets. If u is empty, then x is ranked and we are done. Otherwise, apply the axiom of regularity to u to get an element w of u that is disjoint from u. Since w is in u, w is unranked. w is a subset of t by the definition of transitive closure. Since w is disjoint from u, every element of w is ranked. Applying the axioms of replacement and union to combine the ranks of the elements of w, we get an ordinal rank for w, to wit Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\textstyle \textstyle \operatorname{rank} (w) = \cup \{ \operatorname{rank} (z) + 1 \mid z \in w \}} . This contradicts the conclusion that w is unranked. So the assumption that u was non-empty must be false and x must have rank.

For every two sets, only one can be an element of the other

Let X and Y be sets. Then apply the axiom of regularity to the set {X,Y} (which exists by the axiom of pairing). We see there must be an element of {X,Y} that is also disjoint from it. It must be either X or Y. By the definition of disjoint then, we must have either Y is not an element of X or vice versa.

The axiom of dependent choice and no infinite descending sequence of sets implies regularity

Let the non-empty set S be a counter-example to the axiom of regularity; that is, every element of S has a non-empty intersection with S. We define a binary relation R on S by Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\textstyle aRb :\Leftrightarrow b \in S \cap a} , which is entire by assumption. Thus, by the axiom of dependent choice, there is some sequence (an) in S satisfying anRan+1 for all n in N. As this is an infinite descending chain, we arrive at a contradiction and so, no such S exists.

Regularity and the rest of ZF(C) axioms

Regularity was shown to be relatively consistent with the rest of ZF by Skolem[4] and von Neumann,[5] meaning that if ZF without regularity is consistent, then ZF (with regularity) is also consistent.[6]

The axiom of regularity was also shown to be independent from the other axioms of ZFC, assuming they are consistent. The result was announced by Paul Bernays in 1941, although he did not publish a proof until 1954. The proof involves (and led to the study of) Rieger–Bernays permutation models (or method), which were used for other proofs of independence for non-well-founded systems.[7][8]

Regularity in ordinary mathematics

The axiom of regularity is rarely useful outside of set theory; A. A. Fraenkel, Y. Bar-Hillel and A. Levy noted that[9] “its omission will not incapacitate any field of mathematics”. Its inclusion, therefore, can be considered as chiefly a clarification of what one means by “set”, as elaborated on by the Mostowski collapse lemma (which provides the converse: that not only is membership on every set a well-founded and extensional relation, but that any such relation admits a corresponding set). If one performs mathematics in a more structural setting, for example by using a type theory or structural set theory like ETCS, the axiom is not used at all, since it is not needed to prove that Set, the category of sets, forms an elementary topos.[10]

However, it does have practical uses, especially in the absence of the axiom of choice. One application is Scott's trick for constructing equivalence classes of a relation defined on proper classes, as an alternative to postulating a Grothendieck universe; it may also be used as an alternative to choice in the proof of Frucht's theorem for infinite groups.[11]

Regularity and Russell's paradox

Naive set theory (the axiom schema of unrestricted comprehension and the axiom of extensionality) is inconsistent due to Russell's paradox. In early formalizations of sets, mathematicians and logicians avoided that contradiction by simply replacing the axiom schema of comprehension with the much weaker axiom schema of separation. However, this step alone takes one to theories of sets that are considered too weak.[clarification needed][citation needed] So some of the power of comprehension was added back via the other existence axioms of ZF set theory (pairing, union, powerset, replacement, and infinity), which may be regarded as special cases of comprehension.[citation needed] So far, these axioms do not seem to lead to any contradiction. Subsequently, the axiom of choice and the axiom of regularity were added to exclude models with some undesirable properties. These two axioms are known to be relatively consistent.

In the presence of the axiom schema of separation, Russell's paradox becomes a proof that there is no set of all sets. The axiom of regularity together with the axiom of pairing also prohibit such a universal set. However, Russell's paradox yields a proof that there is no "set of all sets" using the axiom schema of separation alone, without any additional axioms. In particular, ZF without the axiom of regularity already prohibits such a universal set.

If a theory is extended by adding an axiom or axioms, then any (possibly undesirable) consequences of the original theory remain consequences of the extended theory. In particular, if ZF without regularity is extended by adding regularity to get ZF, then any contradiction that followed from the original theory would still follow in the extended theory.

The existence of Quine atoms (sets that satisfy the formula equation x = {x}, i.e. have themselves as their only elements) is consistent with the theory obtained by removing the axiom of regularity from ZFC. Various non-wellfounded set theories allow "safe" circular sets, such as Quine atoms, without becoming inconsistent by means of Russell's paradox.[12]

Regularity, the cumulative hierarchy, and types

In ZF it can be proven that the class Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\textstyle \bigcup_{\alpha} V_\alpha } , called the von Neumann universe, is equal to the class of all sets. This statement is even equivalent to the axiom of regularity (if we work in ZF with this axiom omitted). From any model that does not satisfy the axiom of regularity, a model that satisfies it can be constructed by taking only sets in Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\textstyle \bigcup_{\alpha} V_\alpha } .

Herbert Enderton[13] wrote that "The idea of rank is a descendant of Russell's concept of type". Comparing ZF with type theory, Alasdair Urquhart wrote that "Zermelo's system has the notational advantage of not containing any explicitly typed variables, although in fact it can be seen as having an implicit type structure built into it, at least if the axiom of regularity is included.[14][15]

Dana Scott[16] went further and claimed that:

The truth is that there is only one satisfactory way of avoiding the paradoxes: namely, the use of some form of the theory of types. That was at the basis of both Russell's and Zermelo's intuitions. Indeed the best way to regard Zermelo's theory is as a simplification and extension of Russell's. (We mean Russell's simple theory of types, of course.) The simplification was to make the types cumulative. Thus mixing of types is easier and annoying repetitions are avoided. Once the later types are allowed to accumulate the earlier ones, we can then easily imagine extending the types into the transfinite—just how far we want to go must necessarily be left open. Now Russell made his types explicit in his notation and Zermelo left them implicit. [emphasis in original]

In the same paper, Scott shows that an axiomatic system based on the inherent properties of the cumulative hierarchy turns out to be equivalent to ZF, including regularity.[17]

History

The concept of well-foundedness and rank of a set were both introduced by Dmitry Mirimanoff.[18][19] Mirimanoff called a set x "regular" (Script error: The function "langx" does not exist.) if every descending chain x ∋ x1 ∋ x2 ∋ ... is finite. Mirimanoff however did not consider his notion of regularity (and well-foundedness) as an axiom to be observed by all sets;[20] in later papers Mirimanoff also explored what are now called non-well-founded sets (extraordinaire in Mirimanoff's terminology).[21]

Skolem[4] and von Neumann[1] pointed out that non-well-founded sets are superfluous[22] and in the same publication von Neumann gives an axiom[23] that excludes some, but not all, non-well-founded sets.[24] In a subsequent publication, von Neumann[25] gave an equivalent but more complex version of the axiom of class foundation:[26]

Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle A \neq \emptyset \rightarrow \exists x \in A\,(x \cap A = \emptyset).}

The contemporary and final form of the axiom is due to Zermelo.[2]

Regularity in the presence of urelements

Urelements are objects that are not sets, but which can be elements of sets. In ZF set theory, there are no urelements, but in some other set theories such as ZFA, there are. In these theories, the axiom of regularity must be modified. The statement "Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\textstyle x \neq \emptyset} " needs to be replaced with a statement that Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\textstyle x} is not empty and is not an urelement. One suitable replacement is Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\textstyle (\exists y)[y \in x]} , which states that x is inhabited.

See also

References

  1. ↑ 1.0 1.1 von Neumann 1925.
  2. ↑ 2.0 2.1 Zermelo 1930.
  3. ↑ Kunen 1980, ch. 3.
  4. ↑ 4.0 4.1 Skolem 1923.
  5. ↑ von Neumann 1929.
  6. ↑ For hisTemplate:Ambiguous proof in modern notation, see Vaught (2001, §10.1) for instance.
  7. ↑ Rathjen 2004, p. 193.
  8. ↑ Forster 2003, pp. 210–212.
  9. ↑ Fraenkel, A.A.; Bar-Hillel, Y.; Levy, A. (1973). Foundations of Set Theory. Amsterdam: North Holland. ISBN 0-7204-2270-1.
  10. ↑ Shulman, Michael (2018). "Comparing material and structural set theories". Annals of Pure and Applied Logic. 170 (4): 465–504. arXiv:1808.05204. doi:10.1016/j.apal.2018.11.002.
  11. ↑ Pinsky, Brian (2023). "Frucht's Theorem without Choice". arXiv:2305.11382 [math.LO].
  12. ↑ Rieger 2011, pp. 175, 178.
  13. ↑ Enderton 1977, p. 206.
  14. ↑ The details of this implicit typing are spelled out in Zermelo 1930, and again in Boolos 1971.
  15. ↑ Urquhart 2003, p. 305.
  16. ↑ Scott 1974.
  17. ↑ Lévy 2002, p. 73.
  18. ↑ Mirimanoff 1917.
  19. ↑ cf. Lévy 2002, p. 68 and Hallett 1996, §4.4, esp. p. 186, 188.
  20. ↑ Halbeisen 2012, pp. 62–63.
  21. ↑ Sangiorgi 2011, pp. 17–19, 26.
  22. ↑ van Heijenoort 1967, p. 404.
  23. ↑ van Heijenoort 1967, p. 412.
  24. ↑ Rieger 2011, p. 179.
  25. ↑ von Neumann 1929, p. 231.
  26. ↑ cf. Suppes 1972, p. 53 and Lévy 2002, p. 72

Sources

Template:Set theory

Retrieved from "https://wiki.tachyony.co.uk/w/index.php?title=Axiom_of_regularity&oldid=34472"