In mathematical logic

Mathematical logic

Mathematical logic is a subfield of mathematics with close connections to foundations of mathematics, theoretical computer science and philosophical logic. The field includes both the mathematical study of logic and the applications of formal logic to other areas of mathematics...

, the Mostowski collapse lemma is a statement in set theory

Set theory

Set theory is the branch of mathematics that studies sets, which are collections of objects. Although any type of object can be collected into a set, set theory is applied most often to objects that are relevant to mathematics...

 named for Andrzej Mostowski

Andrzej Mostowski

Andrzej Mostowski was a Polish mathematician. He is perhaps best remembered for the Mostowski collapse lemma....

.

Statement

Suppose that R is a binary relation on a class X such that

• R is set-like: R⁻¹[x] = {y : y R x} is a set for every x,
• R is well-founded
  Well-founded relation
  In mathematics, a binary relation, R, is well-founded on a class X if and only if every non-empty subset of X has a minimal element with respect to R; that is, for every non-empty subset S of X, there is an element m of S such that for every element s of S, the pair is not in R:\forall S...
  
  : every nonempty subset S of X contains an R-minimal element (i.e. an element x ∈ S such that R⁻¹[x] ∩ S is empty),
• R is extensional
  Axiom of extensionality
  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.- Formal statement :...
  
  : R⁻¹[x] ≠ R⁻¹[y] for every distinct elements x and y of X

The Mostowski collapse lemma states that for any such R there exists a unique transitive

Transitive set

In set theory, a set A is transitive, if* whenever x ∈ A, and y ∈ x, then y ∈ A, or, equivalently,* whenever x ∈ A, and x is not an urelement, then x is a subset of A....

 class (possibly proper) whose structure under the membership relation is isomorphic to (X, R), and the isomorphism is unique. The isomorphism maps each element x of X to the set of images of elements y of X such that y R x (Jech 2003:69).

Generalizations

Every well-founded set-like relation can be embedded into a well-founded set-like extensional relation. This implies the following variant of the Mostowski collapse lemma: every well-founded set-like relation is isomorphic to set-membership on a (non-unique, and not necessarily transitive) class.

A mapping F such that F(x) = {F(y) : y R x} for all x in X can be defined for any well-founded set-like relation R on X by well-founded recursion

Well-founded relation

In mathematics, a binary relation, R, is well-founded on a class X if and only if every non-empty subset of X has a minimal element with respect to R; that is, for every non-empty subset S of X, there is an element m of S such that for every element s of S, the pair is not in R:\forall S...

. It provides a homomorphism of R onto a (non-unique, in general) transitive class. The homomorphism F is an isomorphism if and only if R is extensional.

The well-foundedness assumption of the Mostowski lemma can be alleviated or dropped in non-well-founded set theories

Non-well-founded set theory

Non-well-founded set theories are variants of axiomatic set theory which allow sets to contain themselves and otherwise violate the rule of well-foundedness...

. In Boffa's set theory, every set-like extensional relation is isomorphic to set-membership on a (non-unique) transitive class. In set theory with Aczel's anti-foundation axiom

Aczel's anti-foundation axiom

Aczel's anti-foundation axiom is an axiom set forth by Peter Aczel in . It states that every accessible pointed directed graph corresponds to a unique set. In particular, the graph consisting of a single vertex with a loop corresponds to a set which contains only itself as element, i.e...

, every set-like relation is bisimilar

Bisimulation

In theoretical computer science a bisimulation is a binary relation between state transition systems, associating systems which behave in the same way in the sense that one system simulates the other and vice-versa....

 to set-membership on a unique transitive class, hence every bisimulation-minimal set-like relation is isomorphic to a unique transitive class.

Application

Every set model

Model theory

In mathematics, model theory is the study of mathematical structures using tools from mathematical logic....

 of ZF

Zermelo–Fraenkel set theory

In mathematics, Zermelo–Fraenkel set theory with the axiom of choice, named after mathematicians Ernst Zermelo and Abraham Fraenkel and commonly abbreviated ZFC, is one of several axiomatic systems that were proposed in the early twentieth century to formulate a theory of sets without the paradoxes...

 is set-like and extensional. If the model is well-founded, then by the Mostowski collapse lemma it is isomorphic to a transitive model of ZF and such a transitive model is unique.

Note that the saying the membership relation of some model of ZF is well-founded is stronger than saying that the axiom of regularity

Axiom of regularity

In mathematics, the axiom of regularity is one of the axioms of Zermelo-Fraenkel set theory and was introduced by...

is true in the model. There exists a model M (assuming the consistency of ZF) whose domain has a subset A with no R-minimal element, but this set A is not a "set in the model" (A is not in the domain of the model, even though all of its members are). More precisely, for no such set A there exists x in M such that A = R⁻¹[x]. So M satisfies the axiom of regularity (it is "internally" well-founded) but it is not well-founded and the collapse lemma does not apply to it.