{"history":[],"article":{"id":"2bd9122a-7656-48de-9a4d-9315b72688c6","title":"Well-founded relation","slug":"well-founded-relation","content":":::summary\n:::\n\n# \nIn [mathematics](https://bliptext.com/articles/mathematics), a [binary relation](https://bliptext.com/articles/binary-relation) R is called **well-founded** (or **wellfounded** or **foundational** ) on a [set](https://bliptext.com/articles/set-mathematics) or, more generally, a [class](https://bliptext.com/articles/class-set-theory) X if every [non-empty](https://bliptext.com/articles/non-empty) sub[set](https://bliptext.com/articles/set-mathematics)\nS ⊆ X\nhas a [minimal element](https://bliptext.com/articles/minimal-element) with respect to R; that is, there exists an\nm ∈ S\nsuch that, for every\ns ∈ S\n, one does not have\ns R m\n. In other words, a relation is well-founded if:\nSome authors include an extra condition that R is [set-like](https://bliptext.com/articles/set-like-relation), i.e., that the elements less than any given element form a set.\nEquivalently, assuming the [axiom of dependent choice](https://bliptext.com/articles/axiom-of-dependent-choice), a relation is well-founded when it contains no [infinite descending chains](https://bliptext.com/articles/infinite-descending-chain), which can be proved when there is no infinite sequence\nx0, x1, x2, ...\nof elements of X such that\nxn+1 R xn\nfor every natural number n.\nIn [order theory](https://bliptext.com/articles/order-theory), a [partial order](https://bliptext.com/articles/partial-order) is called well-founded if the corresponding [strict order](https://bliptext.com/articles/strict-order) is a well-founded relation.\nIf the order is a [total order](https://bliptext.com/articles/total-order) then it is called a [well-order](https://bliptext.com/articles/well-order).\nIn [set theory](https://bliptext.com/articles/set-theory), a set x is called a **well-founded set** if the [set membership](https://bliptext.com/articles/element-mathematics) relation is well-founded on the [transitive closure](https://bliptext.com/articles/transitive-closure-set) of x. The [axiom of regularity](https://bliptext.com/articles/axiom-of-regularity), which is one of the axioms of Zermelo–Fraenkel [set theory](https://bliptext.com/articles/set-theory), asserts that all sets are well-founded.\nA relation R is **converse well-founded**, **upwards well-founded** or **Noetherian** on X, if the [converse relation](https://bliptext.com/articles/converse-relation)\nR−1\nis well-founded on X. In this case R is also said to satisfy the [ascending chain condition](https://bliptext.com/articles/ascending-chain-condition).\nIn the context of [rewriting](https://bliptext.com/articles/rewriting) systems, a Noetherian relation is also called **terminating**.\n\n# Induction and recursion\nAn important reason that well-founded relations are interesting is because a version of [transfinite induction](https://bliptext.com/articles/transfinite-induction) can be used on them: if (\nX, R\n) is a well-founded relation,\nP(x)\nis some property of elements of X, and we want to show that\nP(x)\nholds for all elements x of X,\nit suffices to show that:\nP(y)\nis true for all y such that\ny R x\n, then\nP(x)\nmust also be true.\nThat is,\nWell-founded induction is sometimes called Noetherian induction, after [Emmy Noether](https://bliptext.com/articles/emmy-noether).\nOn par with induction, well-founded relations also support construction of objects by [transfinite recursion](https://bliptext.com/articles/transfinite-recursion).\nLet\n(X, R)\nbe a [set-like](https://bliptext.com/articles/binary-relation) well-founded relation and F a function that assigns an object\nF(x, g)\nto each pair of an element\nx ∈ X\nand a function g on the [initial segment](https://bliptext.com/articles/initial-segment)\n{y: y R x}\nof X. Then there is a unique function G such that for every\nx ∈ X\n,\nThat is, if we want to construct a function G on X, we may define\nG(x)\nusing the values of\nG(y)\nfor\ny R x\n.\nAs an example, consider the well-founded relation\n(N, S)\n, where\nN\nis the set of all [natural numbers](https://bliptext.com/articles/natural-numbers), and S is the graph of the successor function\nx ↦ x+1\n. Then induction on S is the usual [mathematical induction](https://bliptext.com/articles/mathematical-induction), and recursion on S gives [primitive recursion](https://bliptext.com/articles/primitive-recursive-functions).\nIf we consider the order relation\n(N, <)\n, we obtain [complete induction](https://bliptext.com/articles/complete-induction), and [course-of-values recursion](https://bliptext.com/articles/course-of-values-recursion).\nThe statement that\n(N, <)\nis well-founded is also known as the [well-ordering principle](https://bliptext.com/articles/well-ordering-principle).\nThere are other interesting special cases of well-founded induction.\nWhen the well-founded relation is the usual ordering on the class of all [ordinal numbers](https://bliptext.com/articles/ordinal-numbers), the technique is called [transfinite induction](https://bliptext.com/articles/transfinite-induction).\nWhen the well-founded set is a set of recursively-defined data structures, the technique is called [structural induction](https://bliptext.com/articles/structural-induction).\nWhen the well-founded relation is set membership on the universal class, the technique is known as [∈-induction](https://bliptext.com/articles/induction).\nSee those articles for more details.\n\n# Examples\nWell-founded relations that are not totally ordered include:\n{1, 2, 3, ...}\n, with the order defined by\na < b\n[if and only if](https://bliptext.com/articles/if-and-only-if) a [divides](https://bliptext.com/articles/divisor) b and\na ≠ b\n.\ns < t\nif and only if s is a proper substring of t.\nN × N\nof [pairs](https://bliptext.com/articles/cartesian-product) of [natural numbers](https://bliptext.com/articles/natural-number), ordered by\n(n1, n2) < (m1, m2)\nif and only if\nn1 < m1\nand\nn2 < m2\n.\na R b\nif and only if there is an edge from a to b. Examples of relations that are not well-founded include:\n{−1, −2, −3, ...}\n, with the usual order, since any unbounded subset has no least element.\n\n# Other properties\nIf\n(X, <)\nis a well-founded relation and x is an element of X, then the descending chains starting at x are all finite, but this does not mean that their lengths are necessarily bounded.\nConsider the following example:\nLet X be the union of the positive integers with a new element ω that is bigger than any integer.\nThen X is a well-founded set, but\nthere are descending chains starting at ω of arbitrary great (finite) length;\nthe chain\nω, n − 1, n − 2, ..., 2, 1\nhas length n for any n.\nThe [Mostowski collapse lemma](https://bliptext.com/articles/mostowski-collapse) implies that set membership is a universal among the extensional well-founded relations: for any set-like well-founded relation R on a class X that is extensional, there exists a class C such that\n(X, R)\nis isomorphic to\n(C, ∈)\n.\n\n# Reflexivity\nA relation R is said to be [reflexive](https://bliptext.com/articles/reflexive-relation) if\na R a\nholds for every a in the domain of the relation.\nEvery reflexive relation on a nonempty domain has infinite descending chains, because any constant sequence is a descending chain.\nFor example, in the natural numbers with their usual order ≤, we have 1 ≥ 1 ≥ 1 ≥ ....\nTo avoid these trivial descending sequences, when working with a partial order ≤, it is common to apply the definition of well foundedness (perhaps implicitly) to the alternate relation < defined such that\na < b\nif and only if\na ≤ b\nand\na ≠ b\n. More generally, when working with a [preorder](https://bliptext.com/articles/preorder) ≤, it is common to use the relation < defined such that\na < b\nif and only if\na ≤ b\nand\nb ≰ a\n. In the context of the natural numbers, this means that the relation <, which is well-founded, is used instead of the relation ≤, which is not.\nIn some texts, the definition of a well-founded relation is changed from the definition above to include these conventions.","current_revision":null,"created_by":"kACnuQmH5k9Nr5VNVEpVeg7XpvUmMctD","created_at":"2025-01-25T19:09:46.664Z","updated_at":"2025-01-25T19:09:46.664Z","search_vector":"'found':3 'relat':4 'well':2 'well-found':1","search_content":" \n \n\n# \nIn [mathematics](https://bliptext.com/articles/mathematics), a [binary relation](https://bliptext.com/articles/binary-relation) R is called **well-founded** (or **wellfounded** or **foundational** ) on a [set](https://bliptext.com/articles/set-mathematics) or, more generally, a [class](https://bliptext.com/articles/class-set-theory) X if every [non-empty](https://bliptext.com/articles/non-empty) sub[set](https://bliptext.com/articles/set-mathematics)\nS ⊆ X\nhas a [minimal element](https://bliptext.com/articles/minimal-element) with respect to R; that is, there exists an\nm ∈ S\nsuch that, for every\ns ∈ S\n, one does not have\ns R m\n. In other words, a relation is well-founded if:\nSome authors include an extra condition that R is [set-like](https://bliptext.com/articles/set-like-relation), i.e., that the elements less than any given element form a set.\nEquivalently, assuming the [axiom of dependent choice](https://bliptext.com/articles/axiom-of-dependent-choice), a relation is well-founded when it contains no [infinite descending chains](https://bliptext.com/articles/infinite-descending-chain), which can be proved when there is no infinite sequence\nx0, x1, x2, ...\nof elements of X such that\nxn+1 R xn\nfor every natural number n.\nIn [order theory](https://bliptext.com/articles/order-theory), a [partial order](https://bliptext.com/articles/partial-order) is called well-founded if the corresponding [strict order](https://bliptext.com/articles/strict-order) is a well-founded relation.\nIf the order is a [total order](https://bliptext.com/articles/total-order) then it is called a [well-order](https://bliptext.com/articles/well-order).\nIn [set theory](https://bliptext.com/articles/set-theory), a set x is called a **well-founded set** if the [set membership](https://bliptext.com/articles/element-mathematics) relation is well-founded on the [transitive closure](https://bliptext.com/articles/transitive-closure-set) of x. The [axiom of regularity](https://bliptext.com/articles/axiom-of-regularity), which is one of the axioms of Zermelo–Fraenkel [set theory](https://bliptext.com/articles/set-theory), asserts that all sets are well-founded.\nA relation R is **converse well-founded**, **upwards well-founded** or **Noetherian** on X, if the [converse relation](https://bliptext.com/articles/converse-relation)\nR−1\nis well-founded on X. In this case R is also said to satisfy the [ascending chain condition](https://bliptext.com/articles/ascending-chain-condition).\nIn the context of [rewriting](https://bliptext.com/articles/rewriting) systems, a Noetherian relation is also called **terminating**.\n\n# Induction and recursion\nAn important reason that well-founded relations are interesting is because a version of [transfinite induction](https://bliptext.com/articles/transfinite-induction) can be used on them: if (\nX, R\n) is a well-founded relation,\nP(x)\nis some property of elements of X, and we want to show that\nP(x)\nholds for all elements x of X,\nit suffices to show that:\nP(y)\nis true for all y such that\ny R x\n, then\nP(x)\nmust also be true.\nThat is,\nWell-founded induction is sometimes called Noetherian induction, after [Emmy Noether](https://bliptext.com/articles/emmy-noether).\nOn par with induction, well-founded relations also support construction of objects by [transfinite recursion](https://bliptext.com/articles/transfinite-recursion).\nLet\n(X, R)\nbe a [set-like](https://bliptext.com/articles/binary-relation) well-founded relation and F a function that assigns an object\nF(x, g)\nto each pair of an element\nx ∈ X\nand a function g on the [initial segment](https://bliptext.com/articles/initial-segment)\n{y: y R x}\nof X. Then there is a unique function G such that for every\nx ∈ X\n,\nThat is, if we want to construct a function G on X, we may define\nG(x)\nusing the values of\nG(y)\nfor\ny R x\n.\nAs an example, consider the well-founded relation\n(N, S)\n, where\nN\nis the set of all [natural numbers](https://bliptext.com/articles/natural-numbers), and S is the graph of the successor function\nx ↦ x+1\n. Then induction on S is the usual [mathematical induction](https://bliptext.com/articles/mathematical-induction), and recursion on S gives [primitive recursion](https://bliptext.com/articles/primitive-recursive-functions).\nIf we consider the order relation\n(N, <)\n, we obtain [complete induction](https://bliptext.com/articles/complete-induction), and [course-of-values recursion](https://bliptext.com/articles/course-of-values-recursion).\nThe statement that\n(N, <)\nis well-founded is also known as the [well-ordering principle](https://bliptext.com/articles/well-ordering-principle).\nThere are other interesting special cases of well-founded induction.\nWhen the well-founded relation is the usual ordering on the class of all [ordinal numbers](https://bliptext.com/articles/ordinal-numbers), the technique is called [transfinite induction](https://bliptext.com/articles/transfinite-induction).\nWhen the well-founded set is a set of recursively-defined data structures, the technique is called [structural induction](https://bliptext.com/articles/structural-induction).\nWhen the well-founded relation is set membership on the universal class, the technique is known as [∈-induction](https://bliptext.com/articles/induction).\nSee those articles for more details.\n\n# Examples\nWell-founded relations that are not totally ordered include:\n{1, 2, 3, ...}\n, with the order defined by\na < b\n[if and only if](https://bliptext.com/articles/if-and-only-if) a [divides](https://bliptext.com/articles/divisor) b and\na ≠ b\n.\ns < t\nif and only if s is a proper substring of t.\nN × N\nof [pairs](https://bliptext.com/articles/cartesian-product) of [natural numbers](https://bliptext.com/articles/natural-number), ordered by\n(n1, n2) < (m1, m2)\nif and only if\nn1 < m1\nand\nn2 < m2\n.\na R b\nif and only if there is an edge from a to b. Examples of relations that are not well-founded include:\n{−1, −2, −3, ...}\n, with the usual order, since any unbounded subset has no least element.\n\n# Other properties\nIf\n(X, <)\nis a well-founded relation and x is an element of X, then the descending chains starting at x are all finite, but this does not mean that their lengths are necessarily bounded.\nConsider the following example:\nLet X be the union of the positive integers with a new element ω that is bigger than any integer.\nThen X is a well-founded set, but\nthere are descending chains starting at ω of arbitrary great (finite) length;\nthe chain\nω, n − 1, n − 2, ..., 2, 1\nhas length n for any n.\nThe [Mostowski collapse lemma](https://bliptext.com/articles/mostowski-collapse) implies that set membership is a universal among the extensional well-founded relations: for any set-like well-founded relation R on a class X that is extensional, there exists a class C such that\n(X, R)\nis isomorphic to\n(C, ∈)\n.\n\n# Reflexivity\nA relation R is said to be [reflexive](https://bliptext.com/articles/reflexive-relation) if\na R a\nholds for every a in the domain of the relation.\nEvery reflexive relation on a nonempty domain has infinite descending chains, because any constant sequence is a descending chain.\nFor example, in the natural numbers with their usual order ≤, we have 1 ≥ 1 ≥ 1 ≥ ....\nTo avoid these trivial descending sequences, when working with a partial order ≤, it is common to apply the definition of well foundedness (perhaps implicitly) to the alternate relation < defined such that\na < b\nif and only if\na ≤ b\nand\na ≠ b\n. More generally, when working with a [preorder](https://bliptext.com/articles/preorder) ≤, it is common to use the relation < defined such that\na < b\nif and only if\na ≤ b\nand\nb ≰ a\n. In the context of the natural numbers, this means that the relation <, which is well-founded, is used instead of the relation ≤, which is not.\nIn some texts, the definition of a well-founded relation is changed from the definition above to include these conventions.","revisionCount":0},"hasMore":false,"nextCursor":null}

History