Well-foundedness & well-orders
Parent: order-theory
Well-founded / well-order
- Well-founded — no infinite descending chain
… < a₂ < a₁(equivalently: every nonempty subset has a minimal element).- Well-order — a total order that is well-founded (every nonempty subset has a least element).
Why it matters:
- well-founded ⟹ well-founded recursion/induction — you may recurse "toward minimal elements," which always bottoms out. This is the abstract form of [[pc-well-founded-recursion|
P×C-well-founded recursion]] (and of structural induction). - well-order ⟹ transfinite induction; the order-types of well-orders are the ordinals (
0,1,2,…,ω,ω+1,…). "Every set can be well-ordered" is the well-ordering theorem (= AC).
Examples: < on ℕ (a well-order); the subterm relation, ⊂ on finite sets (well-founded, not total). Not well-founded: < on ℤ or ℝ (… < −2 < −1 < 0), or ⊂ on infinite sets.