---
tag: 0230ECX1Q5
kind: definition
name: Well-founded relation
msc: ["03E20"]
defines: 0DQPNJNPYK
uses: [08EJC6Q25H, 0MCR8ZAXQD]
sources:
  - url: https://en.wikipedia.org/wiki/Well-founded_relation
    locator: lead section
---

## Definition

Let $R$ be a [[binary relation|08EJC6Q25H]] on a set $A$.
The relation $R$ is well-founded when each nonempty subset $S$ of $A$ has an element $m$ such that no $s \in S$ satisfies $s \mathrel{R} m$.

## Remarks

The relation $<$ on $\mathbb{N}$ is well-founded. The relation $<$ on $\mathbb{Z}$ is not, because $\mathbb{Z}$ itself has no minimal element.
If $R$ is well-founded, there is no sequence $x_0, x_1, x_2, \dots$ with $x_{n+1} \mathrel{R} x_n$ for each $n$. The converse needs the axiom of dependent choice.
Well-founded relations allow proofs by [[transfinite induction|0ZHQMQ2C1N]].

## Explanations

### L1 human

In a well-founded relation, you cannot go down forever.
Each strictly decreasing sequence of natural numbers stops after finitely many steps.