Math 2.0

Mathematical logic and foundations Definition

Axiom of regularity

Builds on Zermelo–Fraenkel set theorySetElementWell-founded relationEmpty set

Definition

Work in first-order logic with the relation symbol ∈\in. The axiom of regularity, or axiom of foundation, is the axiom ∀x (x≠∅→∃y (y∈x∧y∩x=∅)).\forall x\, \bigl( x \ne \emptyset \to \exists y\, ( y \in x \wedge y \cap x = \emptyset ) \bigr). In words: every nonempty set xx has an element yy such that no element of yy is an element of xx.

Remarks

Example: let x={∅,{∅}}x = \set{\emptyset, \set{\emptyset}}. The element y=∅y = \emptyset satisfies y∩x=∅y \cap x = \emptyset, because the empty set has no elements. Non-example: a set aa with a={a}a = \set{a} would violate the axiom. The only element of x={a}x = \set{a} is aa, and a∩x=x∩x=x≠∅a \cap x = x \cap x = x \ne \emptyset. So in ZF, no set is an element of itself. The axiom says that ∈\in is a well-founded relation on every set. Over the other axioms of ZF, it is equivalent to the statement that every set lies in some level VαV_\alpha of the cumulative hierarchy. With the axiom of dependent choice, it is equivalent to the statement that there is no sequence (xn)(x_n) with xn+1∈xnx_{n+1} \in x_n for all nn. In Mathlib, the statement for ZFC sets is ZFSet.regularity.

Reading path

To understand this page from the ground up, read these 27 pages in order. The foundations come first.

Show the path as a graph
Element, definition, no evidence levelElementdefinitionProposition, concept, no evidence levelPropositionconceptSet, definition, no evidence levelSetdefinitionConjunction, definition, no evidence levelConjunctiondefinitionDisjunction, definition, no evidence levelDisjunctiondefinitionImplication, definition, no evidence levelImplicationdefinitionNegation, definition, no evidence levelNegationdefinitionPredicate, definition, no evidence levelPredicatedefinitionEmpty set, object, no evidence levelEmpty setobjectOrdered pair, definition, no evidence levelOrdered pairdefinitionBiconditional, definition, no evidence levelBiconditionaldefinitionUniversal quantifier, definition, no evidence levelUniversal quantifierdefinitionCartesian product, definition, no evidence levelCartesian productdefinitionAxiom of extensionality, statement, no evidence levelAxiom of extensionali…statementSubset, definition, no evidence levelSubsetdefinitionPropositional logic, concept, no evidence levelPropositional logicconceptBinary relation, definition, no evidence levelBinary relationdefinitionPredicate logic, concept, no evidence levelPredicate logicconceptAntisymmetric relation, definition, no evidence levelAntisymmetric relationdefinitionReflexive relation, definition, no evidence levelReflexive relationdefinitionTransitive relation, definition, no evidence levelTransitive relationdefinitionZermelo–Fraenkel set theory, concept, no evidence levelZermelo–Fraenkel set …conceptPreorder, definition, no evidence levelPreorderdefinitionPartial order, definition, no evidence levelPartial orderdefinitionMinimal element, definition, no evidence levelMinimal elementdefinitionWell-founded relation, definition, no evidence levelWell-founded relationdefinitionAxiom of regularity, definition, no evidence levelAxiom of regularitydefinition
Each page uses the pages above it. The colour of the bar on a box shows how strong the evidence is, and the box also gives it as text. The list has the same pages.
  • no evidence level
  1. Element definition
  2. Proposition concept
  3. Set definition
  4. Conjunction definition
  5. Disjunction definition
  6. Implication definition
  7. Negation definition
  8. Predicate definition
  9. Empty set object
  10. Ordered pair definition
  11. Biconditional definition
  12. Universal quantifier definition
  13. Cartesian product definition
  14. Axiom of extensionality statement
  15. Subset definition
  16. Propositional logic concept
  17. Binary relation definition
  18. Predicate logic concept
  19. Antisymmetric relation definition
  20. Reflexive relation definition
  21. Transitive relation definition
  22. Zermelo–Fraenkel set theory concept
  23. Preorder definition
  24. Partial order definition
  25. Minimal element definition
  26. Well-founded relation definition
  27. Axiom of regularity definition

Where this leads

1 page builds on this one.

Further reading

  1. Web https://en.wikipedia.org/wiki/Axiom_of_regularity
About this page
Tag6QXBY7J0M5
URIm2://6QXBY7J0M5
Kinddefinition
WritingW0 stub
MSC03E30
DefinesAxiom of regularity
UsesZermelo–Fraenkel set theory, Set, Element, Well-founded relation, Empty set
Changed2 November 2026

Markdown · JSON · Edit on GitHub

What this page needs for W1

  • a source with a locator (0 of 1)

The writing levels say how complete the text of a page is. They do not measure its truth.

What links here

Used by