Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedjudge pass (gpt-5.6-terra)audited 2026-09-14
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.

The ordered Mostowski model

Statement

For densely ordered atoms, order automorphisms and finite supports, the order relation belongs to the permutation model and every symmetric set has a unique least finite support. The atom set is linearly ordered but not well-orderable, so AC fails.

Facts & Assumptions

Given: A countable atom set A with a dense linear order without endpoints, its full order-automorphism group, and finite supports.

[F2]

The Axiom of Choice is used only in the final failure inference.

Proof

1.1F1

The order relation is fixed by every order automorphism, so it has empty support. We first verify the finite-support intersection fact used below. If E1,E2⊆A are finite and E=E1∩E2, then fix⁡(E)=⟨fix⁡(E1)∪fix⁡(E2)⟩.(*) Indeed, cut A at the points of E. In each resulting open interval the two finite sets E1∖E and E2∖E are disjoint. List their points and the images of those points under a given π∈fix⁡(E). Move the image points into their required successive cuts, one at a time. To cross a point of E1∖E, use an increasing finite partial bijection which fixes E2; to cross a point of E2∖E, use one which fixes E1. The point being crossed is not in the fixed set, and density and the absence of endpoints provide a fresh point on the required side. Each such finite increasing partial bijection extends, by the usual interval-by-interval back-and-forth for a countable dense order without endpoints, to an automorphism in the indicated pointwise stabilizer. There are only finitely many marked and image points, so after finitely many moves the residual automorphism fixes E1 (and the last correction may be taken to fix E2). This proves (∗) on each component; joining the component automorphisms proves it on A. If E1,E2 support x, every factor on the right of (∗) fixes x. Thus every element of fix⁡(E) fixes x, and E1∩E2 supports x.

2.1step 1.1

All supports contained in one fixed finite support form a finite family. Repeated intersection therefore gives a support Ex contained in every support; it is the unique least support. Conjugating shows gEx is the least support of gx, so the least-support assignment is itself symmetric.

3.1F2step 1.1∎

Suppose a well-order ◃ of A belonged to the model, and let E be a finite support for it. The nonempty set A∖E has a ◃-least element a. It lies in one of the open intervals cut out by E; choose b≠a in that interval. The finite increasing partial map fixing E and sending a to b extends by back-and-forth to an order automorphism π∈fix⁡(E). Because E supports ◃, π preserves ◃ and maps A∖E to itself. It must therefore fix that subset's unique ◃-least element, contradicting π(a)=b. Hence A is linearly ordered by the empty-supported dense order but is not well-orderable. Since F2 implies well-orderability of every set, AC fails.

Depends on

Used by

Dependency tree · two levels

4 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources