Definition:Well-Founded Relation

From ProofWiki
Jump to navigation Jump to search


Let $\struct {S, \RR}$ be a relational structure.

Definition 1

$\RR$ is a well-founded relation on $S$ if and only if:

$\forall T \subseteq S: T \ne \O: \exists z \in T: \forall y \in T \setminus \set z: \tuple {y, z} \notin \RR$

where $\O$ is the empty set.

Definition 2

$\RR$ is a well-founded relation on $S$ if and only if:

for every non-empty subset $T$ of $S$, $T$ has a minimal element.


According to Strictly Well-Founded Relation is Well-Founded, the Axiom of Foundation implies that every strictly well-founded relation is well-founded.

As the definition quantifies over general subclasses, 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.

Also known as

The term well-founded relation is often used the literature for what on $\mathsf{Pr} \infty \mathsf{fWiki}$ we call a strictly well-founded relation.

In order to emphasise the differences between the two, at some point a $\mathsf{Pr} \infty \mathsf{fWiki}$ editor coined the term strongly well-founded relation.

However, $\mathsf{Pr} \infty \mathsf{fWiki}$ prefers the less unwieldy term well-founded relation in preference to others.

Some sources do not hyphenate, and present the name as wellfounded relation.

Also see

  • Results about well-founded relations can be found here.