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 be a forcing notion in , let be -generic, and let be an uncountable cardinal such that . If regards as measurable, then 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 , forcing , generic , and cardinal in the statement. ZFC, including Choice, is assumed in both the ground and its forcing extension.
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.
Forcing theorem supplies the definable forcing relation, truth lemma, and persistence used in the restriction argument.
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.
The trivial-forcing case is immediate, so suppose is nontrivial and replace it by an isomorphic forcing on an ordinal of size . A measure on is uniform: if in the measure had size , intersecting the complements of its singletons would both retain 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 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 . Forcing of size is -cc and preserves cardinals at and above , so is also a ground cardinal. Choose a regular ground cardinal with
We give the ultrapower facts needed later. From a nonprincipal -complete ultrafilter on , form the ultrapower using functions . Ł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 is elementary, fixes every ordinal below , and moves , so its critical point is . The derived measure is normal: for a regressive on a -large set, is fixed by , and its fibre is -large. Take the ultrapower by and again call its collapsed map . Its target is closed under -sequences from : given for , use F3 to choose the representatives and define . Normality identifies the seed with , and for every , so the entire sequence belongs to the target. Conversely, for any definable elementary 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 fixes all singleton indices below .
Thus forcing by is forcing with a gap at : the initial forcing has size below and the tail forcing is trivial, hence -strategically closed.
By step 1.2, in take a normal-measure ultrapower 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 , taking the transitive collapse implicit in this notation. Then , is -generic, and . By the ordinal presentation chosen in step 1.1, , so ; the image-filter calculation gives , and consequently . The critical-point calculation also gives agreement below , , in the two ground parts. The remaining task is to prove that and the restricted map actually belong to the ground model, not merely to the forcing extension.
First record the fresh-sequence obstruction specialized to small forcing. If , adds no sequence which is new while every proper initial segment is in . Indeed, for each the truth lemma gives a condition and a ground sequence such that . One condition occurs for an unbounded set of , because there are at most conditions and . Persistence then makes decide all of as the union of those compatible ground initial segments, contrary to newness. The same argument works over for the forcing .
We next prove the common-cover claim used by the restriction. If is a set of ordinals of extension-cardinality , there is a set of cardinality with . First, a -enumeration of is a -sequence of ordinals, so the closure from step 3.1 puts it, and hence , in . A -name for such an enumeration has at most possible ordinal values, so has a -cover of size ; the same name calculation in gives an -cover. Alternate these two operations for stages, taking increasing covers, and let be their union. The resulting sequence belongs to by its -closure. On the cofinally many stages whose values lie in , a single condition of decides unboundedly many values, because and is regular; monotonicity of the sequence makes that condition decide the union, so . Repeating this argument with an -name at the cofinally many -stages gives .
It follows that and 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 lies below . The agreement from step 3.1 puts , and hence , in both classes. Shorter sequences are padded to length .
We now show . It suffices, by coding, to prove this for sets of ordinals. Induct on for in , assuming every proper initial segment is in . If , then a new would be a fresh -sequence, contradicting step 4.1. If , write and choose a sufficiently large with an elementary of size containing , every element of , and . The set belongs to by step 5.1. Hence is in , and step 5.1 puts this size-at-most- set of ordinals in . Some forces . Thus satisfies that decides every membership question for whose index lies in ; elementarity makes the same statement true in . Therefore decides all of , so . The usual membership-rank coding then yields .
The identical fresh-sequence induction, now between and , shows For a set of ordinals common to and , 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 -enumeration of an ambient -set. This is the exact target-identification needed below.
The ultrapower embedding is amenable to . We prove that is amenable to . It is enough to show for every ordinal . Induct on . At cofinality at least , a new image sequence would violate step 4.1. At smaller cofinality choose as in step 6.1. The set has size at most ; because is a small subset of , write for some of size at most . Use step 4.2 to cover by a size- set and replace by . Then , while , so . A condition in decides this trace, and elementarity of makes it decide the entire image sequence. Thus . Replacement converts these image sequences to every set restriction .
In the ground model define . 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 because fixes all ordinals below . If and for every , then and belongs to every , hence to . Thus is a nonprincipal -complete ultrafilter on in . By the local definition in the Statement, was measurable in , as required.
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
- Joel David Hamkins, Gap Forcing, complete Gap Forcing Theorem proof and Corollaries 11–12, pp. 3–11 (standard reference, not scraped)