Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passaudited 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.

Small forcing does not create measurable cardinals

Statement

Assume ZFC. Let P be a forcing notion in V, let GP be V-generic, and let κ be an uncountable cardinal such that PV<κ. If V[G] regards κ as measurable, then V already regards κ as measurable.

Here, locally, measurable means that κ is uncountable and carries a nonprincipal ultrafilter closed under intersections of length less than κ. The proof also establishes the auxiliary equivalence it uses: such an ultrafilter yields a definable elementary embedding into a transitive class with critical point κ, and any such embedding yields a measure by the seed κ.

Facts & Assumptions

Given: The ground model V, forcing P, generic G, and cardinal κ in the statement. ZFC, including Choice, is assumed in both the ground and its forcing extension.

[F1]

Ultrafilter and Characterisation of ultrafilters: every set or its complement give the properness, complement-decision, finite-intersection, upward-closure, principality, and nonprincipality laws. In this item, κ-complete means closed under intersections indexed by every ordinal below κ, including the empty intersection.

[F2]

Forcing theorem supplies the definable forcing relation, truth lemma, and persistence used in the restriction argument.

[F3]

The Axiom of Choice supplies the cardinal comparisons, enumerations, elementary submodels, and ultrapowers used below.

Proof

Proof technique: the no-new-measurables half of the Lévy--Solovay theorem, proved through the small-forcing case of the gap-forcing restriction argument.

1.1

The trivial-forcing case is immediate, so suppose P is nontrivial and replace it by an isomorphic forcing on an ordinal of size μ=PV. A measure on κ is uniform: if A in the measure had size λ<κ, intersecting the complements of its λ singletons would both retain A and make the intersection empty. Uniformity and κ-completeness make κ regular, since the bounded pieces of a cofinal partition of length below κ would all be measure-small. They also make κ a strong limit: if κ2λ for λ<κ, choose κ distinct binary subsets of λ; for every coordinate take the bit occurring on a measure-one set and intersect these fewer than κ sets. The intersection has at most one member, contradicting uniformity. Thus κ is strongly inaccessible in V[G]. Forcing of size μ is μ+-cc and preserves cardinals at and above μ+, so κ is also a ground cardinal. Choose a regular ground cardinal δ with μ<δ<δ+<κ.

F1F3
1.2

We give the ultrapower facts needed later. From a nonprincipal κ-complete ultrafilter U on κ, form the ultrapower using functions κV[G]. Łoś's induction uses F1 and the witness choices supplied by F3. It is well-founded: an external descending omega-sequence would, by countable completeness, give one coordinate carrying an infinite descending sequence of ordinals. After transitive collapse, the constant-function map j:V[G]M is elementary, fixes every ordinal below κ, and moves κ, so its critical point is κ. The derived measure W={Aκ:κj(A)} is normal: for a regressive f on a W-large set, j(f)(κ)<κ is fixed by j, and its fibre is W-large. Take the ultrapower by W and again call its collapsed map j. Its target is closed under κ-sequences from V[G]: given xα=[fα]W for α<κ, use F3 to choose the representatives and define F(ξ)=fα(ξ):α<ξ. Normality identifies the seed [id]W with κ, and j(F)(κ)(α)=xα for every α<κ, so the entire sequence belongs to the target. Conversely, for any definable elementary j into a transitive class with critical point κ, the same seed formula defines a set-sized nonprincipal κ-complete ultrafilter: elementarity gives complement decision and intersections, and j fixes all singleton indices below κ.

F1F3construct
2.1

Thus forcing by P is forcing with a gap at δ: the initial forcing has size below δ and the tail forcing is trivial, hence δ-strategically closed.

F1F3step 1.1
3.1

By step 1.2, in V[G] take a normal-measure ultrapower j:V[G]M with critical point κ. The transitive target is closed under κ-sequences of the extension and hence under δ-sequences. As in the general setup of the Gap Forcing Theorem, define the ground part M=αOrdj(VαV), taking the transitive collapse implicit in this notation. Then jV:VM, j(G) is M-generic, and M=M[j(G)]. By the ordinal presentation chosen in step 1.1, PVκ, so j(P)=P; the image-filter calculation gives j(G)=G, and consequently M=M[G]. The critical-point calculation also gives agreement below κ, Vκ=Mκ, in the two ground parts. The remaining task is to prove that M and the restricted map actually belong to the ground model, not merely to the forcing extension.

step 1.1step 1.2step 2.1
4.1

First record the fresh-sequence obstruction specialized to small forcing. If cf(θ)>μ, P adds no sequence s:θOrd which is new while every proper initial segment is in V. Indeed, for each α<θ the truth lemma gives a condition pαG and a ground sequence sα such that pαs˙α=sˇα. One condition pG occurs for an unbounded set of α, because there are at most μ conditions and cf(θ)>μ. Persistence then makes p decide all of s˙ as the union of those compatible ground initial segments, contrary to newness. The same argument works over M for the forcing j(P)=P.

F2step 1.1step 3.1
4.2

We next prove the common-cover claim used by the restriction. If σ is a set of ordinals of extension-cardinality δ, there is a set τMV of cardinality δ with στ. First, a δ-enumeration of σ is a δ-sequence of ordinals, so the closure from step 3.1 puts it, and hence σ, in M[G]. A P-name for such an enumeration has at most δμ=δ possible ordinal values, so σ has a V-cover of size δ; the same name calculation in M gives an M-cover. Alternate these two operations for δ stages, taking increasing covers, and let τ be their union. The resulting sequence belongs to M[G] by its δ-closure. On the cofinally many stages whose values lie in V, a single condition of G decides unboundedly many values, because P<δ and δ is regular; monotonicity of the sequence makes that condition decide the union, so τV. Repeating this argument with an M-name at the cofinally many M-stages gives τM.

F2F3step 1.1step 3.1
5.1

It follows that M and V have the same δ-sequences of ordinals. For a size-δ set of ordinals σ in either class, take the common cover τ from step 4.2 and enumerate it increasingly in both classes as βξ:ξ<γ, where γ<δ+<κ. The index set A={ξ<γ:βξσ} lies below κ. The agreement Vκ=Mκ from step 3.1 puts A, and hence σ, in both classes. Shorter sequences are padded to length δ.

step 3.1step 4.2
6.1

We now show MV. It suffices, by coding, to prove this for sets of ordinals. Induct on θ for Aθ in M, assuming every proper initial segment is in V. If cf(θ)δ, then a new A would be a fresh θ-sequence, contradicting step 4.1. If cf(θ)<δ, write A=A˙G and choose a sufficiently large Vζ with an elementary XVζ of size δ containing P, every element of P, and A˙. The set XOrd belongs to M by step 5.1. Hence a=AX is in M, and step 5.1 puts this size-at-most-δ set of ordinals in V. Some pG forces XA˙=aˇ. Thus X satisfies that p decides every membership question for A˙ whose index lies in X; elementarity makes the same statement true in Vζ. Therefore p decides all of A˙, so AV. The usual membership-rank coding then yields MV.

F2F3step 4.1step 5.1
7.1

The identical fresh-sequence induction, now between M and M[G], shows M=VM[G]. For a set of ordinals common to V and M[G], use step 4.1 at cofinality at least δ and step 5.1 at smaller cofinality; an arbitrary set is reduced to its index set in an M-enumeration of an ambient M-set. This is the exact target-identification needed below.

step 4.1step 5.1step 6.1
7.2

The ultrapower embedding is amenable to V[G]. We prove that jV is amenable to V. It is enough to show jθV for every ordinal θ. Induct on θ. At cofinality at least δ, a new image sequence would violate step 4.1. At smaller cofinality choose XVζ as in step 6.1. The set a=(jθ)X has size at most δ; because a is a small subset of jθ, write a=jb=j(b) for some bθ of size at most δ. Use step 4.2 to cover b by a size-δ set cMV and replace c by cθ. Then a(jc)X(jθ)X=a, while jc=j(c)MV, so aV. A condition in G decides this trace, and elementarity of X makes it decide the entire image sequence. Thus jθV. Replacement converts these image sequences to every set restriction jAV.

step 1.2F2F3step 4.1step 4.2step 6.1
8.1

In the ground model define U0={Aκ:AV and κj(A)}. Step 7.2 makes this a ground set. As in step 1.2, elementarity gives complement decision, finite-intersection closure and upward closure; no singleton belongs to U0 because j fixes all ordinals below κ. If η<κ and AξU0 for every ξ<η, then j(η)=η and κ belongs to every j(Aξ), hence to j(ξ<ηAξ). Thus U0 is a nonprincipal κ-complete ultrafilter on κ in V. By the local definition in the Statement, κ was measurable in V, as required.

F1step 1.2step 7.2

Depends on

Used by

Dependency tree · two levels

13 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