Definition:Strongly Well-Founded Relation

From ProofWiki
Jump to: navigation, search


Let $A$ be a class.

Let $\mathcal R$ be a relation on $A$.

Then $A$ is strongly well-founded if and only if:

whenever $B$ is a non-empty subclass of $A$, $B$ has an $\mathcal R$-minimal element.

Also known as

Most sources that define this concept simply call it well-founded. However, that term is most commonly defined in a weaker sense.

Thus on $\mathsf{Pr} \infty \mathsf{fWiki}$ we have invented the term "strongly well-founded" to avoid ambiguity.


According to Well-Founded Relation Determines Minimal Elements, the Axiom of Foundation implies that every foundational relation is strongly well-founded.

As the definition quantifies over general subclasses, strong well-foundedness is not a first-order property. Thus it cannot be used in a formula of a theory, like NBG class-set theory, that only allow quantification over sets; for example it cannot be used with the axiom schema of specification in NBG set theory, and statements using it must generally be framed as schemas. A higher-order theory such as Morse-Kelley set theory allows it to be used more freely and directly.

A concrete example:

Let $A$ be a class, and let $\mathcal R$ be a relation on $A$.

One cannot directly use the axiom schema of specification in NBG theory to form the class of all subsets $x$ of $A$ such that the restriction of $\mathcal R$ to $A \setminus x$ is a strongly well-founded relation.

Also see

Weaker properties