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.

Prikry forcing preserves every cardinal

Statement

Prikry forcing at a measurable cardinal κ preserves every ground-model cardinal while changing cf⁡(κ) to ω.

Facts & Assumptions

Given: The forcing-theorem setting over a transitive ZFC ground model M, a normal measure on κ, and a generic extension M[G].

[F1]

Prikry forcing adds no bounded subsets of kappa: Every subset of an ordinal below κ appearing in the extension is already in the ground model.

[F2]

Prikry forcing is kappa-plus-cc but not ccc: Prikry forcing is κ+-cc.

[F3]

Measurable cardinals are inaccessible: A measurable κ is inaccessible, hence in particular an uncountable regular limit cardinal.

[F4]

Chain conditions preserve high cofinalities and ccc preserves cardinals: A θ-cc forcing for regular θ preserves all ground cardinals at least θ.

[F6]

Absorption: for cardinals κ,λ with κ infinite and λ≤κ, κ⊕λ=κ, and κ⊗λ=κ when λ≠0: Products of nonzero infinite cardinals with cardinals no larger than them are absorbed by the larger cardinal.

[F8]

The Prikry generic sequence changes cofinality to omega: The generic stem union is an omega-sequence cofinal in κ.

Proof

1.1F1F6F7

Every ground cardinal λ<κ remains a cardinal. Otherwise in M[G] some ordinal α<λ would be bijective with λ, by F7. In M, cardinal absorption supplies a bijection coding α×λ by an ordinal ρ<κ (the finite cases are immediate and the infinite case uses F6). The graph of the alleged bijection therefore codes a new subset of ρ, but F1 says that subset, and hence the graph, belongs to M. This contradicts that λ was a ground cardinal. Choice is used only through the ground cardinal comparisons and coding already stated in F6 and F7.

2.1F3F7step 1.1

The ordinal κ also remains a cardinal. If it were equinumerous in M[G] with some α<κ, let μ=∣α∣M<κ and obtain an injection e:κ→μ. Since F3 makes κ a limit cardinal, the ground successor cardinal μ+ is still below κ; it remains a cardinal by step 1.1. Restricting e to μ+ would inject that preserved successor cardinal into μ, contradicting the defining minimality in F7.

3.1F2F4F5F7step 1.1step 2.1

Write the infinite cardinal κ as ℵα using F5. Then κ+=ℵα+1 by the successor convention in F7, and F5 makes κ+ regular under Choice. F2 and F4 now imply that every ground cardinal at least κ+ is preserved. Together with steps 1.1 and 2.1, this covers every ground cardinal.

4.1F8step 2.1step 3.1∎

Cardinal preservation is not cofinality preservation at κ: F8 supplies in M[G] a cofinal map from ω into the still-cardinal ordinal κ, and proves cf⁡(κ)=ω. Thus the two promised conclusions coexist without treating the cofinality change as a collapse.

Depends on

Used by

Dependency tree · two levels

49 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