Alphabeta Math
Pipeline-generated
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.

Proper Forcing, Countable-Support Iterations, and PFA

1 · Prerequisites

2 · Summary

Properness is formulated through countable elementary submodels and master conditions: every dense set in the model is required to be predense below the master, not to contain the master itself. The equivalent forcing and ground-model-capture formulations make that definition usable in proofs. Both ccc and countably closed forcing are proper, while proper forcing preserves stationary subsets of ω1 and therefore preserves ω1.

Countable-support iterations use two-step forcing at successors and inverse limits with countable nontrivial support at limits. The master-condition lemma handles a named tail condition while fixing an earlier master segment. At a countable-cofinality limit its construction unions coherent initial segments, not arbitrary descending coordinate values. Successor, countable-cofinality and bounded-model limit cases then yield the preservation theorem: a countable-support iteration whose iterands are forced proper is proper.

PFA is stated for a nonempty proper order and any family of at most ω1 dense sets. Restriction to ccc orders gives MA(ℵ1) and hence the Suslin Hypothesis. Its combinatorial consequences are developed through the P-ideal dichotomy and the inequality p>ω1. The topology argument uses both hypotheses: PID organizes the right-separated-neighborhood ideal, while the bound by p rules out the remaining obstruction. Thus regular Hausdorff hereditarily separable spaces are Lindelöf under PFA, so PFA implies that there are no S-spaces.

The consistency construction separates two uses of Laver anticipation. Laver preparation makes supercompactness indestructible under a restricted class of later forcings; the PFA construction instead uses the Laver function as bookkeeping for arbitrary proper forcing names. The length-κ countable-support iteration is proper and κ-cc, collapses precisely the ground cardinals strictly between ω1 and κ, and forces κ=ω2. When an embedding anticipates a requested proper order, the image iteration factors through that order, and elementarity reflects the required dense-set filter back to the original extension.

Finally, the semantic forcing proof is compiled into fixed finite-fragment proof transformations. Primitive-recursive syntax operations translate each certified ZFC+PFA refutation into a certified ZFC+supercompact refutation, and PA verifies the resulting consistency implication. This is a formal relative consistency result; it neither extracts a countable transitive model from bare consistency nor asserts that an outer generic filter belongs to the ground extension. Choice is declared at every elementary-model, simultaneous-choice, cardinal-arithmetic and formalization step that uses it.

3 · Logical flowchart

4 · Definitions, theorems and proofs

DefinitionDefinition: Literature-sourcedProof: Not applicablejudge pass (gpt-5.6-terra)audited 2026-09-14Open item page →

Countable-support forcing iterations

Definition

Fix an ordinal δ and set-indexed data ⟨Pα,Q˙α,1˙α:α<δ⟩. As in Finite-support forcing iterations, P0 is trivial, Pα+1 is identified with the two-step iteration Pα∗Q˙α, and 1˙α is a supplied name forced to be the largest condition of the nonempty preorder Q˙α. More precisely, for each α<δ let Rα be the set-sized second-name carrier used for that two-step iteration and require 1˙α∈Rα. At a limit γ≤δ, a condition p∈Pγ is a coherent function on γ with p(α)∈Rα such that

p↾α⊩Pαp(α)∈Q˙α

for every α<γ, and its nontrivial support

supp⁡(p)={α<γ:p↾α⊮p(α)=1˙α}

is at most countable. Coordinates outside the support are filled by the specified top names. The order is stronger-is-smaller:

p≤q⟺(∀α<γ)  p↾α⊩p(α)≤Q˙αq(α).

This recursive system is a countable-support iteration, and the limit order is its countable-support inverse limit. It differs from the direct finite-support limit precisely by allowing countably many nontrivial coordinates.

For η≤γ, the restriction map is p↦p↾η. In a Pη-generic extension, the quotient is

Pγ/Gη={p∈Pγ:p↾η∈Gη},

with the inherited order; equivalently one may use the canonical Pη-name for the tails p↾[η,γ). Thus a name for a quotient condition always comes with the requirement that its initial restriction belongs to the generic filter.

The definition itself makes no choice. Later limit arguments may take the union of a sequence of coherent initial segments, meaning qn+1↾ηn=qn for increasing ηn; this is not an assertion that arbitrary coordinatewise descending sequences in proper iterands have lower bounds. Showing that the resulting union has countable support uses the applicable countable-union principle and is kept as an explicit proof obligation there.

DefinitionDefinition: Literature-sourcedProof: Not applicablejudge pass (gpt-5.6-terra)audited 2026-09-14Open item page →

Master conditions and proper posets

Definition

Let P be a nonempty preorder, let θ be a regular cardinal with P∈Hθ, and let M be a countable elementary submodel of a structure (Hθ,∈,<θ,P,…) containing all displayed parameters, where <θ is a fixed well-order of Hθ. A condition q∈P is (M,P)-generic if, for every dense D⊆P with D∈M, the set D∩M is predense below q. Spelled out in the stronger-is-smaller convention, this means

∀r≤q  ∃s∈D∩M such that r and s are compatible in P.

For p∈P∩M, an (M,P)-master condition below p is an (M,P)-generic q satisfying q≤p. Neither genericity nor mastery requires q∈M, and genericity does not require q itself to belong to every dense set.

The preorder P is proper in the master-condition formulation if, for every sufficiently large regular θ, every such countable elementary M, and every p∈P∩M, there is an (M,P)-master condition below p. Here “sufficiently large” means that some regular θ0 works for every regular θ≥θ0. Adding the well-order makes the Skolem-closure convention explicit. The equivalent club-of-models and generic-extension formulations are assertions, not definitions, and are proved in the next item.

This item only fixes predicates and quantifiers, so it makes no selection and uses no instance of Choice. Existence of the countable elementary models and of master conditions is invoked only by later theorems under their declared axiom bases.

LemmaStatement: Literature-sourcedProof: AI-adaptedaudited 2026-09-14Open item page →

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.

TheoremStatement: Literature-sourcedProof: AI-adaptedjudge pass (gpt-5.6-terra)audited 2026-09-14Open item page →

Ccc and countably closed forcings are proper

Statement

In ZFC, every ccc forcing preorder and every countably closed forcing preorder is proper. No converse is asserted.

Facts & Assumptions

Given: A nonempty forcing preorder P and a sufficiently large well-ordered Hθ structure containing it.

[F1]

Properness may be checked by producing an (M,P)-master below each p∈P∩M. Master-condition characterizations

[F2]

Ccc means that every antichain is countable. Compatibility, ccc and Knaster for posets

[F3]

Countable closure means that every countable descending chain has a common lower bound. Closure, distributivity, and chain conditions for forcing orders

[A1]

AC supplies maximal antichains, enumerations of the countable family of dense sets in M, and the recursive choices in the closed case. The Axiom of Choice

Proof

1.1F1F2A1Given

Suppose first that P is ccc, let M be a relevant countable elementary model, and fix p∈P∩M. For each dense D∈M, elementarity and A1 give a maximal antichain A∈M with A⊆D. By F2, A is externally countable. Any externally countable set A∈M is a subset of M: elementarity supplies in M a surjection from ω onto A, and every natural number belongs to M. Hence A⊆D∩M is predense below every condition, so p itself is (M,P)-generic and is a master below p. F1 proves that P is proper.

1.2F1F3A1Given

Suppose instead that P is countably closed. Enumerate all dense subsets of P belonging to M as ⟨Dn:n<ω⟩, repeating one if the family is finite. Starting with p0=p, use elementarity and A1 to choose pn+1∈Dn∩M with pn+1≤pn; every pn stays in M. By F3 there is q≤pn for all n. For every Dn, the condition pn+1∈Dn∩M lies above q, so Dn∩M is predense below q. Thus q is an (M,P)-master below p, and F1 again makes P proper.

2.1A1step 1.1step 1.2∎

The two arguments cover the ccc and countably closed hypotheses independently and use no converse. AC is spent exactly in the maximal-antichain and enumeration/recursive-choice operations identified in steps 1.1 and 1.2. Therefore every forcing in either class is proper.

TheoremStatement: Literature-sourcedProof: AI-adaptedaudited 2026-09-14Open item page →

Proper forcing preserves stationary subsets of omega-one

Statement

In ZFC, every proper forcing preserves every ground-model stationary subset of ω1. In particular, proper forcing preserves ω1.

Facts & Assumptions

Given: A proper forcing P, a stationary S⊆ω1 in the ground model, a condition p∈P, and a name C˙ forced by p to be club in ω1.

[F1]

Master genericity is equivalent to forcing every ordinal-valued name in M to have value in M. Master-condition characterizations

[F2]

Clubs are closed and unbounded, and stationarity means meeting every club. The club filter and nonstationary ideal

[F3]

The forcing theorem supplies names, decision, and truth in the generic extension. Forcing theorem

[A1]

AC supplies ambient well-orders, Skolem functions, and the normal enumeration of a named club. The Axiom of Choice

Proof

1.1F1F2A1Given

Choose a sufficiently large well-ordered Hθ structure containing P,p,S,C˙, and fix Skolem functions for it. We first derive the elementary-model trace fact needed here. For β<ω1, let Mβ be the Skolem hull of β∪{P,p,S,C˙} and put f(β)=sup⁡(Mβ∩ω1)+1<ω1. The set E of nonzero limit ordinals δ<ω1 closed under f is club. If δ∈E, finite character of Skolem terms gives Mδ=⋃β<δMβ, so Mδ∩ω1=δ. By stationarity choose δ∈S∩E and set M=Mδ. Then M is countable elementary, contains all the required parameters, and has trace M∩ω1=δ. Properness supplies an (M,P)-master q≤p.

2.1F1F2F3A1step 1.1

In M choose a name f˙ which p forces to be the increasing continuous enumeration of C˙. For every α<δ, one has α∈M and hence the ordinal name f˙(αˇ) belongs to M. By F1, q forces its value into M∩ω1=δ. Thus q forces f˙‘‘δ⊆δ. Since an increasing enumeration satisfies f˙(α)≥α, its first δ values are cofinal in δ; closure of C˙ then gives q⊩δ∈C˙. As δ∈S is a ground ordinal, q⊩C˙∩Sˇ≠∅.

3.1F1F3A1step 2.1∎

The choices of p and the club name were arbitrary, so no condition can force a ground stationary S to become nonstationary. To see preservation of ω1 without a hidden cofinality inference, let p force that g˙:ω→ω1V is any function, choose a relevant countable model M containing p,g˙, and use properness to choose an (M,P)-master q≤p. F1 then forces each g˙(n) into the fixed countable ordinal M∩ω1, so the range is bounded and g˙ is not cofinal, hence not surjective. Therefore ω1V remains uncountable and equals the extension's ω1. AC is used exactly in A1.

LemmaStatement: Literature-sourcedProof: AI-adaptedaudited 2026-09-14Open item page →

Proper iteration master-condition lemma

Statement

Let ⟨Pξ,Q˙ξ:ξ<α⟩ be a countable-support iteration such that every preceding stage forces Q˙ξ proper. Let M≺(Hλ,∈,<) be countable and contain the iteration. Suppose γ∈M∩(α+1), q0∈Pγ is (M,Pγ)-generic, and the Pγ-name p˙ satisfies

q0⊩Pγp˙∈Pα∩M and p˙↾γ∈G˙γ.

Then there is an (M,Pα)-generic q∈Pα such that q↾γ=q0 and q⊩Pαp˙∈G˙α.

Facts & Assumptions

Given: ZFC and all iteration, model, name, and genericity hypotheses in the statement.

[F1]

Countable-support iterations use two-step successors, supplied top names, and inverse limits of countably supported coherent conditions. Countable-support forcing iterations

[F2]

A condition is model-generic exactly when it forces ordinal-name values, or equivalently generic intersections with dense sets, to remain in the model. Master-condition characterizations

[F3]

Two-step generics factor into a first-stage generic and a quotient generic, and conversely. Generic factorization and ccc preservation for two-step iterations

[F4]

The forcing theorem supplies definability of forcing and the truth lemma for all formulas and names used in the recursion. Forcing theorem

[F5]

Transfinite induction applies to the iteration length. Transfinite induction

[F6]

A countable union of countable sets is countable under countable Choice. Countable unions of at most countable sets, assuming ACω

[A1]

AC supplies well-ordered elementary structures, enumerations of dense sets and model ordinals, and the recursive name/condition choices. The Axiom of Choice

Proof

1.1F1F5GivenbaseIH

We prove the displayed extension property by transfinite induction on α. At α=γ take q=q0: the hypothesis already says q0 forces p˙∈G˙γ. Assume as induction hypothesis that the property holds at every smaller iteration length.

1.2F4A1

We record the name-selection argument used below. Suppose u forces that there is a set x satisfying a fixed formula φ(x). By the existential forcing clause, the conditions below u that force φ(x˙) for some name x˙ are dense below u. Use A1 to choose a maximal antichain A of such conditions and, for each a∈A, one witness name x˙a. The usual mixed name x˙=⋃a∈A(x˙a↾a) agrees with x˙a below a. Thus the conditions forcing φ(x˙) are dense below u, and the forcing definition gives u⊩φ(x˙). This derives the needed maximum principle from the forcing clauses and AC rather than attributing it to F4.

2.1F2F3F4A1IHstep 1.1step 1.2

Let α=β+1. Apply the induction hypothesis at β to obtain an (M,Pβ)-generic qβ extending q0 and forcing p˙↾β∈G˙β. In a Pβ-extension containing qβ, the last coordinate p(β) belongs to M[Gβ]∩Qβ. Since Qβ is proper there, choose an (M[Gβ],Qβ)-master qβ∗ below it, and apply step 1.2 to choose a name for this condition. By F3, (qβ,q˙β∗) forces p˙ into the two-step generic. It is (M,Pβ+1)-generic: for any ordinal-valued Pβ+1-name in M, the quotient master forces its value into M[Gβ], and the first-stage master then forces that ground ordinal into M; F2 applies. This gives the successor case.

2.2F1F2F4A1IHstep 1.1step 1.2

Now let α be limit. The case γ=α was settled at step 1.1, so assume γ<α and put ρ=sup⁡(M∩α). Choose an increasing sequence ⟨γn:n<ω⟩ from M∩(α+1) with γ0=γ and supremum ρ, and enumerate the dense subsets of Pα in M as ⟨Dn:n<ω⟩. Recursively construct (M,Pγn)-generic qn and Pγn-names p˙n, beginning with the given pair, so that qn+1↾γn=qn and qn forces: pn∈Pα∩M; pn≤pn−1 and pn∈Dn−1 for n>0; and pn↾γn∈Gγn. For the recursive step, work in a Pγn-generic extension containing qn and resolve pn∈Pα∩M. In the ground model define E={u∈Pγn:u⊥pn↾γn or (∃r≤pn) [r∈Dn & u≤r↾γn]}. The set E belongs to M and is dense: below a condition compatible with pn↾γn, first take a common extension, paste it to the tail of pn, and then strengthen the resulting Pα-condition into Dn. Since qn is an (M,Pγn)-master, the generic meets E∩M. Its member cannot take the incompatible alternative because pn↾γn is in the same generic. Elementarity therefore supplies pn+1∈Dn∩M below pn whose restriction lies in the generic. Apply step 1.2 to name that choice, then apply the induction hypothesis at γn+1<α to obtain qn+1.

3.1F1F4F6A1step 2.2

Define q on ρ by q=⋃nqn and fill every coordinate in [ρ,α) with its supplied top name. This is a condition: the equalities qn+1↾γn=qn make the union a coherent function, and F6 makes its support, a subset of ⋃nsupp⁡(qn), countable. This is the only fusion operation; no coordinatewise lower bound in an arbitrary proper iterand is used. To check what q forces, take any Pα-generic G containing it and resolve the names pn. For k≥n, the construction and truth lemma give pn↾γk∈Gγk. Also pn∈M, so the countable set supp⁡(pn) belongs to M and is a subset of M∩α⊆ρ; hence pn↾ρ=pn. The inverse-limit generic is determined on a condition by these cofinal projections, so pn∈Gρ⊆Gα. Thus q forces pn∈Gα for every n, in particular p0=p.

4.1F2F5F6A1step 1.1step 2.1step 3.1discharge-induction: step 1.1step 2.1step 3.1∎

Step 3.1 shows that q forces pn+1∈Dn∩M∩Gα for every n, so every Dn∩M is predense below q; F2 makes q (M,Pα)-generic. Its restriction to γ0 is q0, and step 3.1 gives q⊩p˙∈G˙α. The base, successor, and limit cases exhaust the induction, so the lemma holds for every α. AC is used exactly in A1, including the countable-support union through F6.

TheoremStatement: Literature-sourcedProof: AI-adaptedaudited 2026-09-14Open item page →

Countable-support iterations preserve properness

Statement

In ZFC, if every iterand in a countable-support iteration is forced proper by its preceding stage, then the full iteration and every initial segment are proper.

Facts & Assumptions

Given: A countable-support iteration ⟨Pξ,Q˙ξ:ξ<δ⟩ such that Pξ⊩Q˙ξ is proper for every ξ<δ.

[F1]

The proper-iteration master lemma extends a master at an earlier stage to a master at any later stage while placing a named model condition into the generic. Proper iteration master-condition lemma

[F2]

Properness means that below every p∈P∩M there is an (M,P)-master, for every relevant countable elementary model M. Master conditions and proper posets

[F3]

Properness on a club of relevant countable models is equivalent to the all-model formulation. Master-condition characterizations

[A1]

AC supplies the well-ordered elementary structures and countable models quantified over by properness. The Axiom of Choice

Proof

1.1F1F3A1Given

Fix α≤δ and a sufficiently large well-ordered Hθ containing the full iteration and α. The countable elementary submodels containing these fixed parameters form a club. Fix one such M and p∈Pα∩M; then Pα and the restricted iteration belong to M. At the trivial stage P0, its unique condition q0 is (M,P0)-generic, and the canonical P0-name pˇ is forced to belong to Pα∩M with trivial restriction in G0. Apply F1 with γ=0 to obtain an (M,Pα)-generic q such that q⊩pˇ∈G˙α. Hence q and p are compatible: otherwise directedness of a generic filter would make q force pˇ∉G˙α. Choose a common extension q′≤q,p. Predensity below q persists below the stronger condition q′, so q′ is still (M,Pα)-generic and is now literally below p.

2.1F1F2F3A1step 1.1∎

Step 1.1 proves the master condition on the club of models containing the full iteration and α; F3 converts this to the all-model formulation in F2. Thus Pα is proper. Since α≤δ was arbitrary and the hypotheses restrict to every initial segment, every Pα, including Pδ, is proper. Successor lengths, limits of countable cofinality, and limits where M∩α is bounded are already the exhaustive cases in F1; no closure of the individual iterands is assumed. AC is used only as recorded in A1 and in the supplier F1.

DefinitionDefinition: Literature-sourcedProof: Not applicablejudge pass (gpt-5.6-terra)audited 2026-09-14Open item page →

The Proper Forcing Axiom

Definition

The Proper Forcing Axiom (PFA) is the assertion that whenever P is a nonempty proper forcing partial order and D={Dξ:ξ<λ} is a family of dense subsets of P with λ≤ω1, there is a filter G⊆P such that G∩Dξ≠∅ for every ξ<λ.

The forcing order is stronger-is-smaller, so a filter is upward closed toward weaker conditions and downward directed: if p,q∈G, some r∈G satisfies r≤p,q. Replacing each dense set by its downward closure gives the equivalent dense-open formulation. Empty and finite families are included; for the empty family any singleton generated filter suffices because P is nonempty.

PFA has the fixed bound ω1. It is not being defined here as FA<2ℵ0(proper), and no value of the continuum is presupposed. The definition itself makes no selection; later uses work in ZFC plus PFA and declare their uses of Choice.

CorollaryStatement: AI-adaptedProof: AI-adaptedjudge pass (gpt-5.6-terra)audited 2026-09-14Open item page →

PFA implies MA(aleph-one) and the Suslin Hypothesis

Statement

In ZFC plus PFA, MA(ℵ1) holds and the Suslin Hypothesis holds.

Facts & Assumptions

Given: PFA.

[F1]

PFA supplies a filter meeting any family of at most ω1 dense sets in a proper forcing. The Proper Forcing Axiom

[F2]
[F3]

MA(ℵ1) rules out Suslin trees. MA(aleph-one) eliminates Suslin trees

[F4]

A Suslin line exists exactly when a Suslin tree exists; consequently SH is equivalent to nonexistence of a Suslin tree. Kurepa equivalence

[A1]

The supplier theorems work in ZFC and propagate their stated uses of AC. The Axiom of Choice

Proof

1.1F1F2A1Given

Let P be ccc and let D be a family of at most ω1 dense subsets of P. By F2, P is proper, so F1 gives a filter meeting all members of D. This is precisely MA(ℵ1).

2.1F3A1step 1.1

Applying F3 to step 1.1 shows that no Suslin tree exists.

3.1F4A1step 2.1∎

By F4, nonexistence of Suslin trees is equivalent to nonexistence of Suslin lines, which is the Suslin Hypothesis. Thus PFA implies both asserted conclusions. No value of the continuum was used.

DefinitionDefinition: Literature-sourcedProof: Not applicablejudge pass (gpt-5.6-terra)audited 2026-09-14Open item page →

P-ideals, PID, the pseudointersection number, and S-spaces

Definition

For subsets of a set A, write x⊆∗y when x∖y is finite, and write x⊥y when x∩y is finite. If F⊆P(A), then

F⊥={x⊆A:(∀y∈F) x⊥y}.

An ideal of countable subsets of A is a family I⊆[A]≤ω that contains every finite subset of A, is downward closed, and is closed under finite unions. It is a P-ideal if for every sequence ⟨an:n<ω⟩ in I there is b∈I such that an⊆∗b for every n. A set X⊆A is orthogonal to I when X∈I⊥, that is, X∩a is finite for every a∈I.

The P-ideal dichotomy (PID) says that for every such P-ideal I on every set A, at least one of the following holds:

  1. there is an uncountable B⊆A such that [B]≤ω⊆I;
  2. there are sets Xn⊆A for n<ω with A=⋃n<ωXn and each Xn⊥I.

A family A⊆[ω]ω has the strong finite intersection property if ⋂F is infinite for every finite F⊆A (including F=∅, whose intersection is ω). An infinite b⊆ω is a pseudointersection of A when b⊆∗a for every a∈A. The pseudointersection number p is the least cardinality of a strong-finite-intersection family in [ω]ω with no infinite pseudointersection. This cardinal-invariant clause is read in ZFC: AC well-orders the possible witness sizes and supplies the standard existence argument for a witnessing centered family.

A topological space is hereditarily separable (respectively, hereditarily Lindelöf) if every one of its subspaces is separable (respectively, Lindelöf). An S-space is a regular Hausdorff, hereditarily separable, non-Lindelöf space. Here regularity and Hausdorffness are both stated because this library's word “regular” does not by itself carry a separation axiom. The empty and singleton spaces are Lindelöf, so neither is an S-space. These are predicates and cardinal definitions only; no individual witness is selected in this item, but the existence and well-defined cardinal value of p use ambient AC as just stated.

TheoremStatement: Literature-sourcedProof: Literature-sourcedaudited 2026-09-14Open item page →

PFA implies the P-ideal dichotomy

Statement

In ZFC, PFA implies PID: every P-ideal of countable subsets of an arbitrary set satisfies one of the two alternatives in the P-ideal dichotomy.

Facts & Assumptions

Given: PFA and a P-ideal I⊆[S]≤ω.

[F1]

PFA supplies a filter meeting at most ω1 dense sets in every proper forcing. The Proper Forcing Axiom

[F2]

The P-ideal property supplies modulo-finite pseudounions, and PID's two conclusions are an uncountable Z with all countable subsets in I or a countable cover by sets orthogonal to I. P-ideals, PID, the pseudointersection number, and S-spaces

[F3]

A model-generic condition forces the model-generic intersection and the ground/ordinal trace properties used below. Master-condition characterizations

[A1]

AC supplies simultaneous P-ideal bounds, well-ordered elementary models, finite-chain choices, names, and the omega-one recursions. The Axiom of Choice

Proof

1.1F2A1Given

Fix a large regular θ. For every countable X⊆I, use F2 and A1 to fix IX∈I with a⊆∗IX for all a∈X, and put IN=IN∩I for a countable N≺Hθ. Define QI as follows. A condition p=(Zp,Np) has finite Zp⊆S and a finite membership-chain Np of countable elementary submodels containing I; distinct points of Zp are separated by some N∈Np; and if N∈Np and X∈N∩I⊥, then X∩Zp⊆N. Put p≤q when Zq⊆Zp, Nq⊆Np, and (Zp∖Zq)∩N⊆IN for every N∈Nq. These clauses are preserved by extension and make the empty pair a greatest condition.

2.1F2F3A1step 1.1

We verify properness, including the combinatorial compatibility step. Let M be suitable, p0∈QI∩M, and add N=M∩Hθ to its side chain; the result q is a condition below p0. Fix once and for all the well-order of Hθ carried by the elementary structure. For a condition u and a model K∈Nu, define the condition trace u↾K=(Zu∩K,Nu∩K), and enumerate the finite set Zu∖K in the fixed well-order, writing tu,K∈S∣Zu∖K∣ for the resulting tuple. It suffices by F3 to take r≤q and dense D∈M, first strengthen r into D, and then find a member of D∩M compatible with this strengthening; rename the strengthened condition r. Put r0=r↾N and n=∣Zr∖N∣. By elementarity, restrict D to the conditions s carrying a distinguished Ns∈Ns such that s↾Ns=r0 and ∣Zs∖Ns∣=n; the witnesses for r are Nr=N and tr,N. Let T={ts,Ns:s∈D}⊆Sn and let J be the sigma-ideal generated by I⊥. For U⊆Sn, let ∂U retain the tuples u for which, at every coordinate k<n, the fibre of possible kth entries above u↾k is J-positive. The derivative claim in Moore's cited tutorial says that T′=∂nT is a nonempty J+-splitting member of M and contains the external tuple tr,N. Its finite induction uses the membership chain and clause 4 of the forcing: if tr,N first disappeared, the least bad fibre's countable I⊥ decomposition, coded in the relevant side model, would put one of the corresponding outside points of Zr in a member of I⊥ from that model, contrary to clause 4. In particular, this claim does not assume that tr,N itself belongs to M. Starting with the empty tuple, choose successively in M an initial segment extendible in T′. Its next-coordinate set C∈M is not in J, hence is not orthogonal to I; elementarity gives an infinite H∈I∩M with H⊆C. For every one of the finitely many outer models P∈Nr∖M, membership-chain coherence gives H∈P∩I, so H⊆∗IP. Choose the next coordinate in H∩⋂P∈Nr∖MIP. After n choices, elementarity supplies s∈D∩M whose tuple ts,Ns is the chosen one, and hence Zs∖Ns is contained in every IP. Then (Zs∪Zr,Ns∪Nr) is a common extension. Thus q is an (M,QI)-master and QI is proper.

3.1F2F3A1step 2.1

If S is a countable union of members of I⊥, PID's second alternative holds. Otherwise choose a suitable countable M and x∈S∖⋃(M∩I⊥). Then q=({x},{M∩Hθ}) is a condition and, by step 2.1, an M-master. For a QI-generic G containing q, set Z˙=⋃p∈G˙Zp and N˙=⋃p∈G˙Np. The master condition forces Z˙ uncountable: if an M-name enumerated it countably, F3 would put all of its ground points in M, contrary to x∈Z˙∖M. Properness gives the ground-model countable-covering property by the same master-name argument, so every countable subset of Z˙ is contained in some side model N∈N˙. The order clause gives N∩Z˙⊆∗IN, and therefore N∩Z˙∈I. Hence q forces every countable subset of Z˙ to lie in I.

4.1F1F2A1step 3.1∎

Work in the proper cone QI↾q. Choose names f˙:ω1→Z˙ and g˙:ω1→I such that q forces f˙ injective and f˙‘‘ξ⊆g˙(ξ) for every ξ<ω1; step 3.1 supplies them. For each ξ, the set Dξ of conditions deciding both values is dense. By F1 there is a filter meeting all Dξ. Compatibility within the filter makes the decided values coherent, producing in the ground universe an injection f:ω1→S and g:ω1→I with f‘‘ξ⊆g(ξ). Put Z=f‘‘ω1. If a⊆Z is countable, the set of its f-indices is bounded by some ξ<ω1, so a⊆f‘‘ξ⊆g(ξ)∈I and downward closure gives a∈I. Thus Z witnesses PID's first alternative. Together with the first sentence of step 3.1, this proves PID. AC is used exactly through A1 and the stated ZFC suppliers.

LemmaStatement: Literature-sourcedProof: AI-adaptedjudge pass (gpt-5.6-terra)audited 2026-09-14Open item page →

PFA implies the pseudointersection number exceeds omega-one

Statement

In ZFC plus PFA, p>ω1: every family of at most ω1 infinite subsets of ω with the strong finite intersection property has an infinite pseudointersection.

Facts & Assumptions

Given: PFA and a family A⊆[ω]ω of cardinality at most ω1 with the strong finite intersection property.

[F1]

The definitions of strong finite intersection, pseudointersection, and p use modulo-finite containment and require the witness to be infinite. P-ideals, PID, the pseudointersection number, and S-spaces

[F2]
[F3]

MA(ℵ1) applies to ccc partial orders and at most ω1 dense sets with the stronger-is-smaller filter convention. Martin's Axiom at a cardinal and Martin's Axiom

[A1]

AC supplies an omega-one indexing when needed and is the ambient choice principle in the stated ZFC result. The Axiom of Choice

Proof

1.1F1A1Given

Let P consist of pairs (s,F) with s∈[ω]<ω and F∈[A]<ω. Put (t,G)≤(s,F) exactly when s⊆t, F⊆G, and t∖s⊆⋂F, taking ⋂∅=ω. For a fixed finite stem s, every finite collection of conditions with that stem has the common extension whose side set is the union of their side sets. Since there are countably many finite subsets of ω, P is sigma-centered and therefore ccc.

2.1F1A1step 1.1

For each a∈A, the set Ea={(s,F):a∈F} is dense, because adding a to F changes no stem. For each n<ω, let Dn={(s,F):(∃k∈s) k≥n}. Given (s,F) outside Dn, the strong finite intersection property makes ⋂F infinite, so choose k∈⋂F with k≥n and extend the stem by k; hence Dn is dense. The family of all Ea and Dn has cardinality at most ω1.

3.1F1F2F3A1step 2.1

By F2 and F3, choose a filter G⊆P meeting every set from step 2.1, and put b=⋃{s:(s,F)∈G}. Meeting all Dn makes b unbounded in ω, hence infinite. Fix a∈A and choose (s,F)∈G∩Ea. For any (t,H)∈G, directedness gives (u,K)∈G below both; the order relative to (s,F) gives u∖s⊆⋂F⊆a, and t⊆u. Thus t∖a⊆s, and after taking the union, b∖a⊆s is finite. Therefore b⊆∗a for every a∈A, so b is an infinite pseudointersection.

4.1F1step 3.1∎

Since every at-most-ω1 strong-finite-intersection family has such a pseudointersection, no family witnessing the definition of p has cardinality at most ω1. By F1, p>ω1. Empty and finite A are included: the same forcing works, and for A=∅ the constructed b is simply infinite.

TheoremStatement: Literature-sourcedProof: Literature-sourcedjudge pass (gpt-5.6-terra)audited 2026-09-14Open item page →

PID plus p greater than omega-one eliminates S-spaces

Statement

In ZFC plus PID and p>ω1, every regular Hausdorff hereditarily separable space is hereditarily Lindelöf. Consequently no S-space exists.

Facts & Assumptions

Given: PID, p>ω1, and a regular Hausdorff hereditarily separable space K.

[F1]

A P-ideal uses modulo-finite pseudounions; PID has the uncountable internally-small and countable orthogonal-cover alternatives; p controls pseudointersections; and S-spaces use the stated hereditary topological conventions. P-ideals, PID, the pseudointersection number, and S-spaces

[A1]

AC supplies the omega-one recursion, countable enumerations, and all simultaneous finite-modulo and topological witness choices. The Axiom of Choice

Proof

1.1F1A1Givenassume-contra

Assume for contradiction that some subspace W⊆K is not Lindelöf. Regularity, Hausdorffness, and hereditary separability pass to subspaces, so replace K by W. Choose an open cover with no countable subcover. Recursively for α<ω1, select a cover member Uα and xα∈Uα outside ⋃β<αUβ. Let X={xα:α<ω1} and relabel Uxα=Uα; then Ux∩X is countable for every x∈X. By regularity choose open Vx with x∈Vx⊆Vx‾⊆Ux. Define I={A∈[X]≤ω:(∀x∈X) ∣A∩Vx‾∣<ω}. It is an ideal containing all finite sets.

2.1F1A1step 1.1

We first derive the needed domination fact from p. If F⊆ωω has size less than p, consider, on the countable set ω<ω, the sets Af={s:(∀i<∣s∣) f(i)≤s(i)} for f∈F and Cn={s:∣s∣≥n}. Every finite intersection is infinite. A pseudointersection B exists by the definition of p; thin it to distinct sn with ∣sn∣>n, and put g(n)=sn(n). Since B⊆∗Af, g eventually dominates every f∈F. Now take An∈I, replace them by their increasing finite unions, and enumerate each infinite An as {an,k:k<ω}. For each x, choose fx(n) past the finite set An∩Vx‾. As ∣X∣=ω1<p, choose one eventual dominator g for all fx, and set A=⋃n{an,k:k≥g(n)}, ignoring finite An. Each An⊆∗A, while for fixed x all sufficiently large rows avoid Vx‾ and the finitely many remaining rows meet it finitely. Thus A∈I, proving that I is a P-ideal.

3.1F1A1step 2.1

Apply PID to I. In the first alternative take uncountable Y⊆X with [Y]≤ω⊆I. For y∈Y, the set Y∩Vy must be finite; otherwise a countably infinite subset of it would belong to I yet meet Vy‾ infinitely. Since the space is Hausdorff and hence T1, delete the finitely many other points of Y∩Vy to obtain a relative open neighborhood isolating y. Thus Y is an uncountable discrete subspace, which is not separable, contradicting hereditary separability.

3.2F1A1step 1.1step 2.1

In PID's second alternative write X=⋃nYn with every Yn⊥I. Some Y=Yn is uncountable, and hereditary separability gives a countable dense D⊆Y. The family {D∖Vx‾:x∈X} has the strong finite intersection property. Indeed, if D∖⋃x∈FVx‾ were finite for some finite F, then Y⊆D‾⊆⋃x∈FVx‾ together with finitely many points. But every Vx‾⊆Ux and each Ux∩X is countable, forcing Y countable, a contradiction. Since ∣X∣=ω1<p, F1 gives an infinite pseudointersection a⊆D. Then a∩Vx‾ is finite for every x, so a∈I; but a⊆Y contradicts Y⊥I. Thus the second alternative is impossible as well.

4.1F1A1step 3.1step 3.2discharge-contradiction: step 3.1step 3.2∎

Both PID alternatives contradict hereditary separability, so the assumed non-Lindelöf subspace W cannot exist. Hence every subspace of the original K is Lindelöf: K is hereditarily Lindelöf. By the S-space definition in F1, no regular Hausdorff hereditarily separable non-Lindelöf space exists. AC is used exactly as recorded in A1.

CorollaryStatement: Literature-sourcedProof: AI-adaptedjudge pass (gpt-5.6-terra)audited 2026-09-14Open item page →

PFA implies that there are no S-spaces

Statement

In ZFC plus PFA, no regular Hausdorff hereditarily separable non-Lindelöf space exists; equivalently, there are no S-spaces.

Facts & Assumptions

Given: PFA.

[F3]

PID together with p>ω1 makes every regular Hausdorff hereditarily separable space hereditarily Lindelöf, excluding S-spaces. PID plus p greater than omega-one eliminates S-spaces

Proof

1.1F1F2Given

By F1 and F2, the PFA universe satisfies both PID and p>ω1.

2.1F3step 1.1∎

Apply F3. Every regular Hausdorff hereditarily separable space is hereditarily Lindelöf and therefore Lindelöf itself, so none meets the non-Lindelöf clause in the definition of an S-space.

RemarkRemark: AI-adaptedProof: Not applicablejudge pass (gpt-5.6-terra)audited 2026-09-14Open item page →

Laver preparation versus PFA bookkeeping

Laver preparation and the standard forcing of PFA share one input but have different jobs. A Laver anticipation function ℓ:κ→Vκ can make a chosen set appear as j(ℓ)(κ) for a suitable supercompactness embedding. Its existence from a supercompact cardinal is the content of Existence of a Laver function at a supercompact, with the exact anticipation convention in Laver anticipation functions.

The Laver preparation uses that function in an iteration designed to make κ indestructibly supercompact under subsequent <κ-directed-closed set forcing, exactly within the class stated by Supercompact preparation interface. Its conclusion does not cover arbitrary proper forcing.

The PFA bookkeeping iteration instead uses ℓ to anticipate names for proper partial orders and places each valid guess into a countable-support iteration. The anticipated posets need not be directed closed. The final embedding argument uses j(ℓ)(κ) to expose the requested proper forcing as the next factor of j(Pκ); it does not appeal to prior indestructibility. Indeed, the PFA iteration deliberately collapses cardinals so that the former supercompact κ becomes ω2, and therefore does not preserve its supercompactness.

Thus the preparation theorem is comparison material, not a load-bearing premise of the PFA proof. No implication saying that proper forcing preserves a supercompact cardinal is asserted. All existence statements above retain their ZFC and supercompact hypotheses; ambient AC is supplied by The Axiom of Choice, and this comparison makes no fresh selection.

DefinitionDefinition: Literature-sourcedProof: Not applicableaudited 2026-09-14Open item page →

Laver-guided proper bookkeeping iteration

Definition

Let κ be supercompact and let ℓ:κ→Vκ be a Laver anticipation function. The Laver-guided proper bookkeeping iteration is the countable-support iteration

⟨Pα,Q˙α:α<κ⟩

defined recursively as follows. Start with the trivial P0. Once Pα has been defined, inspect ℓ(α). If it is a Pα-name and

Pα⊩“the interpretation of ℓ(α) is a nonempty proper partial order,”

put Q˙α=Top⁡(ℓ(α)), where Top⁡ is the canonical name normalization that leaves a partial order with a greatest condition unchanged and otherwise adjoins one new greatest condition. Otherwise put Q˙α=1ˇ, the canonical name for the one-condition forcing. Successors use the usual two-step iteration and limits use the countable-support inverse limit. Thus every iterand is forced proper, including every fallback, and all coordinate top names required by the iteration interface are supplied. Adjoining a greatest condition preserves properness and gives a dense copy of the original order below the new top, so this normalization changes no generic extension.

The test is internal to the preceding forcing extension: “is a name” is a syntactic property and the assertion of properness is evaluated by the forcing relation for Pα. No guess that fails either test is used. The construction therefore never assumes that an arbitrary element of Vκ denotes a forcing.

For each ω1≤α<κ, the collapse Col⁡(ω1,α) as computed after stage α is countably closed and hence proper. The Laver reflection argument in the next lemma shows that names for these collapses occur at unboundedly many valid guessing stages; this is a theorem about the defined iteration, not an extra clause silently built into a malformed guess. The same factor mechanism says that whenever an embedding is chosen with j(ℓ)(κ)=Q˙ and Pκ forces Q˙ nonempty and proper, stage κ of j(Pκ) is Top⁡(Q˙). Hence the image iteration factors, up to the canonical forcing equivalence, through Q˙ itself; if Q˙ already has a greatest condition, the stage is literally Q˙.

The recursive construction from the supplied κ and ℓ is definition-level data and makes no fresh choice. Existence of ℓ retains the ZFC plus supercompact hypothesis of Existence of a Laver function at a supercompact; no Laver preparation or indestructibility assumption is part of this definition.

LemmaStatement: Literature-sourcedProof: AI-adaptedjudge pass (gpt-5.6-terra)audited 2026-09-14Open item page →

Size, collapse, and factorization for the PFA iteration

Statement

Let κ be supercompact and let Pκ be the Laver-guided countable-support iteration. Then Pκ is proper, has cardinality κ, is κ-cc, preserves ω1, collapses every ground cardinal strictly between ω1 and κ, and forces κ=ω2. If a sufficiently closed supercompactness embedding j:V→M anticipates a Pκ-name Q˙ for a proper forcing, then

j(Pκ)≃Pκ∗Q˙∗R˙

for the tail iteration R˙ in M.

Facts & Assumptions

Given: ZFC, a supercompact κ, a Laver function ℓ, and the iteration from the statement.

[F1]

The bookkeeping construction uses countable support, only forced-proper iterands, a trivial fallback, and identifies an anticipated proper name as stage κ of the image iteration. Laver-guided proper bookkeeping iteration

[F2]

Countable-support iterations of forced-proper iterands are proper. Countable-support iterations preserve properness

[F3]
[F4]

Supercompactness supplies sufficiently closed embeddings with critical point κ. Supercompactness and closed elementary embeddings

[F5]

Below an inaccessible cardinal all required rank and exponentiation bounds are below κ. Size and rank bounds below an inaccessible

[F6]

Families of small supports admit large delta subsystems under the stated inaccessible arithmetic. Generalized delta systems for small supports

[F7]

A κ-cc forcing preserves the regular cardinal κ and all larger cardinals and cofinalities. Chain conditions preserve high cofinalities and ccc preserves cardinals

[F8]

Every supercompact cardinal is inaccessible. Large-cardinal implication and consistency ledger

[A1]

AC supplies thinning, well-orders, simultaneous names, and the selected supercompactness embeddings. The Axiom of Choice

Proof

1.1F1F2F3Given

By F1 every stage forces its iterand proper, so F2 makes every Pα, including Pκ, proper. F3 therefore preserves ω1.

1.2F1F4A1Given

Let S be the set of α∈[ω1,κ) for which ℓ(α) is a valid Pα-name for Col⁡(ω1,α)VPα. We verify the required reflection instead of assuming it. Let C˙ be the canonical Pκ-name for Col⁡(ω1,κ)VPκ. The Laver anticipation property gives a sufficiently closed supercompactness embedding j:V→M with j(ℓ)(κ)=C˙. By elementarity and the recursive definition in F1, the first κ stages of j(Pκ) are exactly Pκ, so M recognizes C˙ as the required proper collapse name at stage κ. Hence κ∈j(S). If S were bounded below some η<κ, then j(S)=S⊆η, contradicting κ∈j(S). Thus S is unbounded.

2.1F1F5F6F8A1step 1.1

By F8, κ is inaccessible. Inductively, Pα and every iterand name for α<κ have hereditary size below κ: F1 places the guesses in Vκ, while F5 bounds the number of countable supports and the countable products of earlier hereditary presentations. At every limit of uncountable cofinality, countable support is bounded, so the inverse-limit carrier equals the direct limit; such limits form a stationary subset of inaccessible κ. For a κ-sized family of conditions, F6 thins their countable supports to a delta system. The root is bounded below some β<κ; since ∣Pβ∣<κ, regularity thins again so all root restrictions agree. The union of any two remaining conditions is a condition: below β they agree, and beyond the root their supports are disjoint, so at each coordinate monotonicity of the earlier forcing relation preserves the unique tail requirement. Hence the family has two compatible members and Pκ is κ-Knaster, in particular κ-cc. Every countable support is bounded in κ, so Pκ=⋃α<κPα and ∣Pκ∣≤κ.

3.1F1F5F7A1step 1.1step 1.2step 2.1

For α∈S the collapse is countably closed and hence proper, so F1 uses it rather than the fallback. Consequently, for every ground cardinal μ with ω1<μ<κ, a stage α∈S above μ makes ∣μ∣≤ω1. Moreover Pα+1 has at least ∣α∣ conditions: the one-point functions in Col⁡(ω1,α) give that many distinct last-coordinate conditions. Since S is unbounded, ∣Pκ∣≥κ, so equality holds in step 2.1. By F7, κ itself remains a cardinal, while step 1.1 preserves ω1; therefore the final model has no cardinal strictly between them and forces κ=ω2.

4.1F1F4A1step 2.1∎

Let j:V→M be supplied by F4 with enough closure to contain the relevant Pκ-name Q˙, and suppose j(ℓ)(κ)=Q˙ and Pκ forces Q˙ proper. Since crit⁡(j)=κ, elementarity applied to the recursive definition in F1 makes the first κ stages of j(Pκ) exactly Pκ. The closure agreement makes M recognize the same forced-properness assertion, so stage κ is Q˙, not the fallback. Splitting the remaining image iteration after that coordinate gives a tail name R˙ and the canonical dense isomorphism j(Pκ)≃Pκ∗Q˙∗R˙. This proves every clause, with Choice used exactly through A1 and the declared suppliers.

TheoremStatement: Literature-sourcedProof: AI-adaptedjudge pass (gpt-5.6-terra)audited 2026-09-14Open item page →

A supercompact cardinal can be forced to give PFA

Statement

If κ is supercompact, the Laver-guided countable-support iteration Pκ forces PFA and κ=ω2, while preserving ω1 and ZFC.

Facts & Assumptions

Given: A ZFC ground universe V with a supercompact cardinal κ. Generic filters used in the semantic proof are supplied in common outer universes; none is asserted to exist inside its ground model.

[F1]

PFA asks for a filter meeting every family of at most ω1 dense subsets of each nonempty proper partial order. The Proper Forcing Axiom

[F2]

A supercompact cardinal has a Laver anticipation function. Existence of a Laver function at a supercompact

[F3]

The Laver-guided iteration is proper, preserves ω1, forces κ=ω2, and an embedding anticipating a forced-proper name factors its image as Pκ∗Q˙∗R˙. Size, collapse, and factorization for the PFA iteration

[F4]

Set-forcing extensions of ZFC models satisfy ZFC. Generic extensions satisfy ZF and preserve ground-model Choice

[F5]

Forcing is definable formula by formula and satisfies the truth lemma and, when the stated outer generics are available, its semantic characterization. Forcing theorem

[F6]

The bookkeeping iteration uses the anticipated name exactly when the preceding stage forces that it is a nonempty proper order with a greatest condition. Laver-guided proper bookkeeping iteration

[A1]

AC supplies the ground well-orders and the set-sized selections of names, bounds, and embeddings used below. The Axiom of Choice

Proof

1.1F2F3F4F6Given

By F2 fix a Laver function and form Pκ as in F6. By F3 this forcing is proper, preserves ω1, and forces κ=ω2. Let G⊆Pκ be arbitrary V-generic. F4 gives V[G]⊨ZFC. It remains to prove PFA in this arbitrary extension.

2.1F1F5A1step 1.1

Work in V[G]. Fix a nonempty proper partial order Q and a family ⟨Dξ:ξ<λ⟩ of dense subsets, where λ≤ω1. If λ=0, any q∈Q generates a filter and there is nothing to meet. Suppose 0<λ≤ω1 and repeat D0 to regard the family as an ω1-sequence. Choose ground names Q˙,D⃗˙ for these objects. By F5 there is p∈G forcing that Q˙ is proper and that D⃗˙ is an ω1-sequence of dense subsets of it. Restrict every coefficient of Q˙ below p and adjoin a new greatest condition, obtaining a name Q˙∗. In a generic containing p its value is Q with that new top; in a generic on the incompatible side its value is the one-condition order. Adding a top preserves properness: an old condition uses a Q-master, while below the new top a countable model containing the nonempty Q contains an old condition and a Q-master below it. The set of conditions below p or incompatible with p is dense, so F5 shows that 1Pκ forces Q˙∗ to be nonempty, proper, and to have a greatest condition. In the actual extension every Dξ⊆Q remains dense in Q∗.

3.1F2F3F6A1step 2.1

Choose a cardinal large enough for the names in step 2.1 and all restrictions of the desired embedding to them. Laver anticipation and supercompactness give a correspondingly closed j:V→M with critical point κ and j(ℓ)(κ)=Q˙∗. By step 2.1 and F6 the image iteration uses Q˙∗ at stage κ, and F3 gives in M a tail name R˙ and a canonical dense factorization j(Pκ)≃Pκ∗Q˙∗∗R˙.

4.1F3F5Givenstep 3.1

By the outer-universe convention in Given, take g⊆Q∗ generic over V[G], followed by an M[G∗g]-generic H⊆R, all in a common outer universe. Under the factorization let K=G∗g∗H. Every condition of G has countable, hence bounded, support in κ; the canonical first factor therefore sends it into K, so j‘‘G⊆K. Define jG(val⁡G(τ))=val⁡K(j(τ)). If two Pκ-names have the same G-value, F5 gives a condition of G forcing their equality; its image belongs to K, so F5 in M makes the displayed definition independent of the name. The same argument, applied to a formula or its negation, proves formula-by-formula that jG:V[G]→M[K] is elementary and extends j.

5.1F1F5A1step 2.1step 3.1step 4.1

Enumerate in V the transitive closure of the name Q˙∗ below the closure bound chosen in step 3.1. Closure puts the pointwise image of that enumeration in M, and evaluating it with G and K constructs the set restriction jG↾Q∗ in M[K]. There form the upward-closed filter F generated by jG‘‘g. It is directed because g is directed and jG preserves the order. Since crit⁡(jG)=κ>ω1, jG(⟨Dξ:ξ<ω1⟩)=⟨jG(Dξ):ξ<ω1⟩. For every ξ<ω1, genericity gives qξ∈g∩Dξ, and jG(qξ)∈F∩jG(Dξ). Thus M[K] satisfies that a filter on jG(Q∗) meets every member of the image sequence. Elementarity of jG reflects the existential assertion to a filter f on Q∗ in V[G] meeting every Dξ. Because the sequence is nonempty and every Dξ lies in Q, f∩Q is nonempty; it is upward closed in Q, and any common extension in f of two of its members lies in Q, not at the newly adjoined greatest condition. Hence f∩Q is the required filter on Q.

6.1F1F3F4F5A1step 1.1step 5.1∎

The choice of Q and its dense family in V[G] was arbitrary, including the empty-family case, so F1 and step 5.1 give V[G]⊨PFA. Since G was an arbitrary generic, F5 yields Pκ⊩PFA. Step 1.1 and F3 give preservation of ω1 and Pκ⊩κ=ω2, while F4 gives preservation of ZFC. All uses of Choice are those declared in A1; the outer generics facilitate the semantic argument and are not claimed to be elements of V[G].

LemmaStatement: AI-adaptedProof: AI-adaptedaudited 2026-09-14Open item page →

Finite-fragment compiler for the PFA iteration

Statement

Fix certified presentations of the source theory S=ZFC+“there is a supercompact cardinal” and the target T=ZFC+PFA, together with certified formal versions of the preceding Laver-guided forcing proof. Require these fixed data to include checker-certified, formula-parametric proof templates for the forcing translations of Separation and Replacement, the nonschematic ZFC axioms and logical rules, together with their PA correctness derivations, as well as the one fixed PFA forcing block. PA then verifies total primitive-recursive constructors which take every certified finite target fragment to source proofs of the finite ground and forcing facts needed for that fragment, and which take every certified T-refutation to a certified S-refutation. No countable transitive model of either full theory is inferred from consistency.

Facts & Assumptions

Given: The fixed certified calculi, code-parametric templates, PA correctness derivations, and formal proof blocks in the statement. A certificate for a Separation or Replacement axiom includes its defining formula, and the PFA axiom has one fixed tag. All malformed codes use the stipulated zero or empty-list defaults. The uniform templates are explicit input data here; they are not inferred from F2's externally indexed assertion.

[F1]

The semantic Laver-guided construction proves in ZFC plus a supercompact that its nonempty iteration forces PFA and preserves ZFC. A supercompact cardinal can be forced to give PFA

[F2]

For each externally fixed finite target fragment whose formal forcing verification is supplied, the verification expands to finitely many formula-specific truth, valuation, Separation, Replacement, parameter, and preorder proofs; this interface asserts no uniform arithmetic constructor. Forcing transfer for finite ZFC fragments

[F3]

A formal forcing transfer requires verified total support extraction, proof construction, composition, and soundness operations; semantic correctness alone is insufficient. Formal consistency transfer by forcing

[F4]

Formula recognition, free-variable and free-for tests, capture-free substitution, numeral formation, negation, and certified derivation checking are primitive recursive, with defaults on malformed inputs. Primitive-recursive syntax and certified proof checking

[F5]

Validity, length, coordinates, append, concatenation, fixed-register iteration, and finite-history recursion for the certified sentinel list coding are primitive recursive. Primitive-recursive sentinel coding for certified syntax

[F6]

Primitive-recursive functions have representations whose totality and uniqueness PA proves. Primitive-recursive functions are representable in Q

Proof

1.1F1F4F5Given

Fix the source and target proof predicates. Let Good⁡(P) be the fixed source formula saying that some supercompact κ and Laver function ℓ witness that P is the recursively defined Laver-guided iteration. The stored formalization of F1 proves ∃P Good⁡(P) and proves from Good⁡(P) the nonemptiness and forcing conclusions of F1. Define by recursion on a parsed membership formula φ the code Forc⁡P(φ) of “1P forces φ,” leaving P as the one displayed free parameter. Atomic clauses insert the two fixed forcing-relation formulas; Boolean connectives and quantifiers insert the corresponding fixed clauses with fresh variables. F4 supplies parsing and capture-free substitution; fresh indices are obtained by a bounded scan above the largest parsed index, and F5 supplies the bounded syntax-tree traversal and output-list recursion. Alongside the formula code, the recursion emits the fixed logical derivations showing that forcing respects each logical axiom and inference rule. Invalid formula codes return the fixed tautology proof.

2.1F1F4F5step 1.1Given

Define the target-axiom constructor A from the certified templates in Given. For each of the finitely many nonschematic ZFC axioms it returns the corresponding stored forcing proof. On a certified Separation instance for φ, it substitutes Forc⁡P(ρ∈σ∧φ) into the supplied name-and-Separation template; on a Replacement instance it substitutes into the supplied least-witness-rank template and its bounding name. The Power Set branch inserts the stored subname construction, and the Choice branch inserts the stored ground-well-order and least-fibre construction. The PFA tag returns the one stored formalization of F1, including the forced-proper name normalization, image factor, lifted-embedding formula, image-generated filter, and elementarity reflection. Each branch is weakened by the antecedent Good⁡(P) and finishes with the supplied checker-certified derivation of Good⁡(P)→Forc⁡P(δ) for its input axiom δ. F4 verifies the displayed substitutions and certificate tags, while F5 supplies the finite template and list assembly. No truth evaluator, proof search, or uniformity inference from F2 occurs.

3.1F1F2F4F5step 2.1Given

Traverse a certified finite fragment Δ, apply A to each entry, rename bound and proof-line variables above the current maxima, concatenate the blocks, and collect the nonlogical source-axiom certificates actually appearing. The resulting finite list Γ(Δ) contains the supercompact axiom because this compiler uniformly uses the PFA iteration, and it contains exactly the finitely many ZFC schema instances used by the emitted derivations. It also contains the parameter, preorder, forcing-recursion, proper-iteration, factorization, master-condition, and forcing-truth instances occurring in that fixed block, together with the fixed proof of ∃P Good⁡(P). Thus the output proves every finite ground fact and every conditional Good⁡(P)→Forc⁡P(δ) for δ∈Δ, not merely a citation to the semantic theorem. For each particular output fragment, F2 identifies these finite proof roles; it does not construct the traversal.

4.1F3F4F5F6step 1.1step 2.1step 3.1

Every loop in steps 1.1–3.1 is bounded by a decoded formula, proof, or fragment length; every update is one of F4's primitive-recursive syntax operations or F5's primitive-recursive list recursions. Hence their composition is primitive recursive. PA proves the following simultaneous invariant by induction first on formula-tree size and then on the fragment position: every returned line reference is earlier than its use, every substitution passes the free-for test, each source axiom line carries its supplied certificate, and the last line of the block is the advertised forcing formula. Constant branches reduce to checking fixed finite numerals; the two schematic branches use the constructor tags and annotations that F4's checker recomputes. F6 supplies PA-provably total single-valued graphs for the composite functions. This verifies totality and checker acceptance rather than inferring either from F1 or F2.

5.1F1F4F5step 1.1step 2.1step 4.1

Now define R on a proposed target proof p. If F4 rejects p or its conclusion is not the fixed contradiction, put R(p)=0. Otherwise scan its lines. For a target-axiom line append the block supplied by A. For a logical-axiom line append the corresponding forcing-logic block from step 1.1, weakened by Good⁡(P). For modus ponens, generalization, or existential elimination, append the fixed block deriving Good⁡(P)→Forc⁡P(φ) for the conclusion φ from the already emitted conditional translations of the cited earlier lines, after renumbering its references. Maintain the table sending each input line to its output concluding line. The final target contradiction therefore yields Good⁡(P)→1P⊩⊥. Append the fixed derivation that nonemptiness of P implies 1P⊮⊥; since Good⁡(P) includes nonemptiness, obtain ∀P ¬Good⁡(P). Combining this with F1's stored source proof of ∃P Good⁡(P) gives an S-refutation without adding a witness constant to the source language.

6.1F3F4F5F6step 4.1step 5.1

PA induction on the decoded line number proves the precise loop invariant if the first i target lines check, the output prefix checks and ends each line block with its forcing translation. The axiom, logical, and inference cases are exactly the branches in step 5.1, and malformed references take only the rejected-input branch. F4 checks the input and every emitted annotation; F5 supplies the bounded output-list and table recursions, and F6 proves the composite functions total. PA therefore verifies ∀p(Prf⁡T(p,⌜⊥⌝)⟶Prf⁡S(R(p),⌜⊥⌝)). This supplies all constructor verifications demanded by F3, including the zero-occurrence case in which no PFA block is emitted.

7.1F1F2F3Givenstep 3.1step 4.1step 6.1∎

Steps 1.1–4.1 give the promised compiler on every finite target fragment, and steps 5.1–6.1 give its verified refutation-reduction form. The construction manipulates finite codes only. F2 is used only after an output is fixed, to identify the finite semantic proof roles that output must realize; the uniform templates and their PA correctness derivations are the explicit certified data in Given. F1 supplies the one fixed object-theoretic PFA block. No step asserts that consistency creates a generic extension or a countable transitive model of full S or full T.

CorollaryStatement: AI-adaptedProof: AI-adaptedjudge pass (gpt-5.6-terra)audited 2026-09-14Open item page →

Formal consistency of PFA from a supercompact

Statement

For the fixed certified arithmetizations of S=ZFC+“there is a supercompact cardinal” and T=ZFC+PFA,

PA⊢Con⁡(S)⟶Con⁡(T).

This is a formal proof-code reduction. It does not extract a transitive model of either full theory from consistency.

Facts & Assumptions

Given: The proof predicates, contradiction sentence, and PA representations fixed by the two suppliers.

[F1]

PA verifies a total map R taking every certified T-refutation to a certified S-refutation. Finite-fragment compiler for the PFA iteration

[F2]

A base-verified total refutation reduction from U to T0 yields in that base Con⁡(T0)→Con⁡(U). Formal consistency transfer from a verified reduction

Proof

1.1F1F2Given

Apply F2 with arithmetic base PA, source theory T0=S, target theory U=T, and reduction R from F1. Its verified premise has the required orientation: a proof of contradiction in ZFC+PFA is sent to a proof of contradiction in ZFC plus a supercompact. Therefore PA proves Con⁡(S)⟶Con⁡(T).

2.1F1step 1.1

Equivalently, inside PA assume Con⁡(S) and let p be arbitrary. If p were a certified T-refutation, F1 would make R(p) a certified S-refutation, contradicting the assumption. Universal generalization over p gives Con⁡(T). This spells out both quantifiers and confirms that no converse implication is being used.

3.1F1F2step 2.1∎

On standard natural numbers the formal implication gives the corresponding external relative-consistency consequence. F1 constructs only finite proof codes, and F2 explicitly requires no model extraction. Hence neither step produces a generic extension or a countable transitive model from the bare consistency hypothesis.

5 · Examples, counterexamples and false statements

None yet.

Sources