Well-founded relation

Y indicates that the column's property is always true for the row's term (at the very left), while ✗ indicates that the property is not guaranteed
in general (it might, or might not, hold). For example, that every equivalence relation is symmetric, but not necessarily antisymmetric,
is indicated by Y in the "Symmetric" column and ✗ in the "Antisymmetric" column, respectively.

All definitions tacitly require the homogeneous relation${\displaystyle R}$ be transitive: for all ${\displaystyle a,b,c,}$ if ${\displaystyle aRb}$ and ${\displaystyle bRc}$ then ${\displaystyle aRc.}$
A term's definition may require additional properties that are not listed in this table.

In mathematics, a binary relationR is called well-founded (or wellfounded or foundational) on a set or, more generally, a classX if every non-emptysubset (or subclass) S ⊆ X has a minimal element with respect to R; that is, there exists an m ∈ S such that for every s ∈ S, one does not have sRm. More formally, a relation is well-founded if: $${\displaystyle (\forall S\subseteq X)\;[S eq \varnothing \implies (\exists m\in S)(\forall s\in S)\lnot (s\mathrel {R} m)].}$$ Some authors include an extra condition that R is set-like, i.e., that the elements less than any given element form a set.

Equivalently, assuming the axiom of dependent choice, a relation is well-founded when it contains no infinite descending chains, meaning there is no infinite sequence x₀, x₁, x₂, ... of elements of X such that x_n+1Rx_n for every natural number n.

In order theory, a partial order is called well-founded if the corresponding strict order is a well-founded relation. If the order is a total order, then it is called a well-order.

In set theory, a set x is called a well-founded set if the set membership relation is well-founded on the transitive closure of x. The axiom of regularity, which is one of the axioms of Zermelo–Fraenkel set theory, asserts that all sets are well-founded.

A relation R is converse well-founded, upwards well-founded, or Noetherian on X, if the converse relationR is well-founded on X. In this case R is also said to satisfy the ascending chain condition. In the context of rewriting systems, a Noetherian relation is also called terminating.