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

Forcing preserves ordinals

Statement

In ambient ZF, if M is a transitive ZF ground model and G is M-generic for a nonempty forcing preorder in M, then

Ord⁡∩M[G]=Ord⁡∩M.

This is preservation of ordinals as sets; no preservation of their cardinality or cofinality is asserted.

Facts & Assumptions

Given: The stated ground model and generic extension.

[F1]

Generic extensions satisfy ZF and preserve ground-model Choice gives transitive ZF M[G] containing M; only its ZF branch is used.

[F2]

Transitivity and a valuation rank bound gives rank⁡(τG)≤rk⁡P(τ).

[F3]

Names for pairs, functions and ordinals gives check names for ground ordinals with their original values.

[F4]

Absoluteness of names and their ranks identifies the name rank of a ground name as an ordinal belonging to M.

Proof

1.1

If γ∈Ord⁡∩M, F3 gives a ground name whose value is gamma, so γ∈M[G]. Its being an actual ordinal is unchanged. Thus Ord⁡∩M⊆Ord⁡∩M[G].

F1F3
1.2

If γ∈Ord⁡∩M[G], write γ=τG for a name τ∈M. By F4, β=rk⁡P(τ) is an actual ordinal in M. Since an ordinal has membership rank equal to itself, F2 gives γ≤β. If γ=β it is in M directly; if γ<β, transitivity of M puts γ∈M. This includes gamma zero.

F1F2F4
2.1

The inclusions in steps 1.1 and 1.2 prove the equality. The upper-bound argument compares actual ordinal sets and uses no enumeration, cardinal arithmetic, cofinal map or AC; it therefore makes no claim that the extension has the same cardinals or cofinalities.

step 1.1step 1.2∎

Depends on

Used by

Dependency tree · two levels

15 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