Alphabeta MathHow 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 theorem
Statement
For every fixed membership formula , forcing is uniformly definable from P and its name parameters over a transitive ZF ground model M and satisfies the truth lemma for every M-generic G. If externally an M-generic filter through every condition is available, then
The definability assertion is a scheme indexed by fixed formulas. Existence of generics is an extra hypothesis for the displayed semantic characterization, not for the forcing predicate or truth lemma. ZF suffices.
Facts & Assumptions
Given: A transitive ZF model M, its nonempty forcing preorder P, and a fixed formula with names in M.
Atomic forcing is well-founded and definable proves atomic definability on set cones.
Forcing relation for all formulas extends definability through each fixed formula and specifies negation.
Monotonicity, density, and decision for forcing supplies density closure and persistence.
Truth lemma proves the semantic equivalence with existence of a forcing condition in a given generic.
Proof
Atomic relations are definable by F1. At conjunction and negation insert the already obtained subformula predicates into the clauses in F2; at an existential quantify over the definable class of M-names and over the set P. This gives a fixed first-order predicate for each fixed formula. Every parameter is P, its order, or one of the name arguments. F4 then supplies the truth lemma for this very internally defined predicate.
If and G is M-generic containing p, the right-to-left direction of F4 makes true in M[G]. This implication needs no assumption that any generic exists.
Suppose p does not force . By density closure F3 the conditions forcing cannot be dense below p. Hence some has no stronger condition forcing , which says by F2. The extra generic-existence hypothesis supplies an M-generic G containing q; upward closure puts p in G. F4 makes true there. Thus the asserted truth in every generic through p fails.
Steps 2.1 and 2.2 give both directions of the display. The argument selected only one generic under the stated existence hypothesis; it did not select generics simultaneously or infer their existence from definability. Formula construction used an external finite induction, so no uniform truth predicate for the universe or AC was assumed.
Depends on
Used by
- Two-step forcing iterations Definition
- Dense-equivalent forcing presentations Example
- Perfect-tree splitting of a new-real name Example
- Sealing a named maximal antichain Example
- Trivial forcing recovers the ground model Example
- A closed Easton tail adds no short sequences across its chain-condition head Lemma
- A perfect tree of mutually generic name interpretations Lemma
- A universal-meagre generic absorbs old nowhere-dense sets Lemma
- Absorption, factorization, and homogeneous truth in the Solovay collapse Lemma
- Hereditarily symmetric names have bounded layer support Lemma
- Homogeneous truth about a generic real has Borel representatives Lemma
- Master-condition characterizations Lemma
- Proper iteration master-condition lemma Lemma
- Real names are captured and coded meagre unions are absorbed Lemma
- Restriction, amalgamation, and the set-sized Prikry property Lemma
- Schema of continuity in the basic Cohen model Lemma
- Search-and-shift prime-ideal construction in the basic Cohen model Lemma
- Set-stage names and the forcing truth lemma for the Easton class product Lemma
- Small sets of ground ordinals are captured at a bounded iteration stage Lemma
- Strongly homogeneous truth has Baire representatives Lemma
- The Good-Tree-Watson symmetric model is closed under omega-sequences from the full extension Lemma
- The Lévy collapse localizes countable ordinal data Lemma
- A countably closed forcing adds a normal Suslin tree Theorem
- A supercompact cardinal can be forced to give PFA Theorem
- All sets of reals in Solovay L(R) have LM, BP, and PSP Theorem
- Cardinal effects of collapse and Lévy-collapse forcing Theorem
- Chain conditions preserve high cofinalities and ccc preserves cardinals Theorem
- Closure, distributivity, and absence of new short sequences Theorem
- Cohen coordinates are distinct and mutually generic Theorem
- Composition with universal-meagre forcing preserves sweetness Theorem
- Every prime ideal on the power set of omega is principal in the tail-flip symmetric model Theorem
- Every uncountable Solovay-model set of reals has a perfect subset Theorem
- Finite-support bookkeeping kills all named Suslin trees Theorem
- Generic extensions satisfy ZF and preserve ground-model Choice Theorem
- Generic factorization and ccc preservation for two-step iterations Theorem
- Hereditarily symmetric interpretations form a transitive ZF model Theorem
- Jech–Sochor first embedding theorem Theorem
- Prikry forcing adds no bounded subsets of kappa Theorem
- Proper forcing preserves stationary subsets of omega-one Theorem
- Relative consistency of DC with failure of Stone's theorem Theorem
…and 8 more results.
Dependency tree · two levels
10 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.