Alphabeta Math
DefinitionDefinition: Literature-sourcedProof: Not applicableverified 2026-09-26 (gpt-6-sol)
How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

  • Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
  • AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
  • AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Well-order and well-ordered set

Definition

Let W be a set. A well-order on W is a total order ≤ on W (Partial order and partially ordered set) with the property that

every nonempty S⊆W has a least element, i.e. an ℓ∈S with ℓ≤s for all s∈S.

The pair (W,≤) is then a well-ordered set, and W is well-ordered by ≤.

A least element of S is unique when it exists: two of them are below each other, hence equal by antisymmetry (Partial order and partially ordered set). We may therefore write min⁡S for it.

Strict form. Everything on this page is more convenient in terms of the associated strict order x<y:  ⟺  (x≤y and x≠y) (Partial order and partially ordered set). Spelled out strictly, a well-order on W is a relation < that is

  • irreflexive: x<x holds for no x∈W;
  • transitive: x<y and y<z imply x<z;
  • trichotomous: for all x,y∈W exactly one of x<y, x=y, y<x holds;
  • and such that every nonempty S⊆W has an element ℓ with no s∈S satisfying s<ℓ.

The two presentations determine each other by x≤y  ⟺  (x<y or x=y), and we write (W,<) or (W,≤) as convenient.

Remarks

  • Totality is not an extra hypothesis. If ≤ is a partial order on W in which every nonempty subset has a least element, then ≤ is already total: apply the hypothesis to the two element subset {x,y}, whose least element is below the other. Totality is nevertheless stated, because in the strict presentation trichotomy has to be written down explicitly.
  • A well-order is total, so every subset of a well-ordered set is a chain (Chain in a poset), and W itself is one. Chains are therefore not the interesting invariant here; the least element property is.
  • The model case is (N,≤), which is a linear order (≤ is a linear order on N) in which every nonempty subset has a least element (The well-ordering principle). Ordinals, defined later on this page, are the exact generalisation of that picture.
  • (Z,≤) and (R,≤) are total orders but not well-orders: Z has no least element at all, and the bounded set {x∈R:0<x<1} has none either. Being bounded below does not help, which is exactly why well-ordering is a strong condition.
  • The empty set carries exactly one well-order, the empty relation, vacuously. Every one element set carries exactly one.
  • A well-order admits no infinite strictly decreasing sequence x0>x1>x2>⋯, since the set of its terms would have no least element. This direction follows directly from the definition; no converse is used here.

Depends on

Dependency tree · 2 levels

Sources