Alphabeta Math
LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedaudited 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.

Master-condition characterizations

Statement

Let P∈M and M be as in the master-condition definition. For q∈P the following are equivalent:

  • (i) q is (M,P)-generic;
  • (ii) for every dense D∈M, q⊩G˙∩D∩M≠∅;
  • (iii) q⊩M[G˙]∩V=M;
  • (iv) q⊩M[G˙]∩Ord=M∩Ord.

Here M[G]={x˙G:x˙∈M is a P-name}. Moreover, the club-of-countable-models formulation of properness is equivalent to the all-model formulation in sufficiently large structures (Hλ,∈,<λ,P,…).

Facts & Assumptions

Given: ZFC, the displayed P,M,q, and the stronger-is-smaller forcing convention.

[F1]

(M,P)-genericity means that D∩M is predense below q for every dense D∈M. Master conditions and proper posets

[F2]

The forcing theorem supplies definability and the truth lemma for the formulas and names used below. Forcing theorem

[F3]

Forcing is persistent, every formula is densely decided, and truth on a dense set below a condition is equivalent to being forced by that condition. Monotonicity, density, and decision for forcing

[F4]

Downward Löwenheim--Skolem supplies elementary Skolem hulls containing specified parameters. Downward Löwenheim–Skolem with parameters

[A1]

AC supplies maximal antichains, well-orders of them, and the ambient well-orders/Skolem closures. The Axiom of Choice

Proof

1.1F1F2F3

Fix D∈M dense. If D∩M is predense below q, then conditions below q that extend a condition of D∩M are dense below q; F2 gives q⊩G˙∩D∩M≠∅. Conversely, if some r≤q were incompatible with every member of D∩M, then r would force that intersection empty. This proves (1) if and only if (2).

2.1F1F2F3step 1.1

Assume (1). The inclusion M⊆M[G]∩V follows from check names. For the reverse inclusion, let r≤q force that a name x˙∈M equals a ground object x. Define Dx˙ to contain (a) every s for which some ground object y satisfies s⊩x˙=yˇ, and (b) every s below which no condition has property (a). This set is dense: from any condition, either an extension has property (a), or the original condition has property (b). By definability of forcing it belongs to M. Since Dx˙∩M is predense below q, some s∈Dx˙∩M is compatible with r. It cannot have property (b), because a common extension with r would force x˙=xˇ while admitting no ground-value extension. Hence s has property (a); by elementarity its witness may be taken as some y∈M. A common extension of r and s forces both x˙=xˇ and x˙=yˇ, so x=y∈M. Thus q forces every ground member of M[G˙] to lie in M, proving (3). Statement (3) immediately implies (4), since ordinals are ground objects and check names give the opposite inclusion.

3.1F1F2A1step 2.1

Assume (4), and let A∈M be a maximal antichain. In M, use A1 to fix a bijection e:ξ→A from an ordinal ξ, and form by mixing the name β˙ for the unique index of the member of A∩G˙. Then β˙∈M and q⊩β˙∈M∩Ord by (4). Consequently q forces e(β˙)∈A∩M∩G˙, so A∩M is predense below q. Every dense D∈M contains, by elementarity and A1, such a maximal antichain A∈M; hence D∩M is predense below q and (1) follows.

4.1F1F4A1step 3.1∎

The all-model definition immediately gives the club formulation, since the countable elementary submodels of a fixed well-ordered Hμ structure form a club by F4 and A1. Conversely, suppose the good models contain a club in [Hμ]ω, where μ>2∣P∣. Represent a subclub as the models closed under a function F:Hμ<ω→Hμ. Choose λ>μ and a well-order <λ so that F may be taken as the <λ-least such witness. Every countable M≺(Hλ,∈,<λ,P,…) is then closed under F, so N=M∩Hμ is a good club model. Every subset of P, and hence every dense set or maximal antichain in M, belongs to Hμ; therefore D∩N=D∩M. An (N,P)-master below p∈P∩M is thus also an (M,P)-master. This proves the all-model formulation and completes both claimed equivalences. AC is used exactly for A1; no countable transitive model or generic filter is selected.

Depends on

Used by

Dependency tree · two levels

16 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