---
tag: 55WD0H03CZ
kind: concept
name: Well-founded order
msc: [06A06, "03E20"]
specializes: [0DQPNJNPYK]
sources:
  - url: https://en.wikipedia.org/wiki/Well-founded_relation
---

## Summary

A well-founded order is a partial order in which every nonempty subset has a minimal element.
Equivalently, assuming the axiom of dependent choice, there is no infinite strictly decreasing sequence.
It is the order case of a [[well-founded relation|0DQPNJNPYK]].
It is exactly what is needed for proofs by well-founded induction and definitions by well-founded recursion.
A [[well-order|01CGSJ0GNQ]] is a well-founded order that is also total.

## Explanations

### L1 human

In a well-founded order you cannot keep stepping down forever: every descent stops after finitely many steps.
The natural numbers with the usual order are the basic example.
The order need not be total: the positive integers ordered by divisibility are well-founded.
Indeed, a sequence in which each term is a proper divisor of the previous one must stop.
The integers with the usual order are not well-founded, since $0 > -1 > -2 > \cdots$ never stops.