Proper forcing and the proper forcing axiom

DefinitionConditions in a model#✓fully proved

Let \(\mathbb{P}\) be a set and \(M\) a subset of the disjoint union \(\mathbb{P} \sqcup \mathcal{P}(\mathbb{P})\). The conditions in \(M\) form the set \(M_c\) of those \(p \in \mathbb{P}\) whose copy in the disjoint union belongs to \(M\); informally, \(M_c = M \cap \mathbb{P}\).

def modelConds {P : Type*} (M : Set (P ⊕ Set P)) : Set P := Sum.inl ⁻¹' M

Used by 2

Used by(M, ℙ)-generic conditions · Proper partial orders

DefinitionSets of conditions in a model#✓fully proved

Let \(\mathbb{P}\) be a set and \(M\) a subset of the disjoint union \(\mathbb{P} \sqcup \mathcal{P}(\mathbb{P})\). The sets of conditions in \(M\) form the family \(M_s\) of those \(D \subseteq \mathbb{P}\) whose copy in the disjoint union belongs to \(M\); informally, \(M_s = M \cap \mathcal{P}(\mathbb{P})\).

def modelSets {P : Type*} (M : Set (P ⊕ Set P)) : Set (Set P) := Sum.inr ⁻¹' M

Used by 1

Used by(M, ℙ)-generic conditions

DefinitionCompatible conditions#✓fully proved

Two elements \(p\) and \(q\) of a partial order \(\mathbb{P}\) are compatible if there is \(r \in \mathbb{P}\) with \(r \le p\) and \(r \le q\).

def IsCompatible {P : Type*} [PartialOrder P] (p q : P) : Prop := ∃ r : P, r ≤ p ∧ r ≤ q

Used by 1

Used byPredense below a condition

DefinitionPredense below a condition#✓fully proved

A set \(A \subseteq \mathbb{P}\) of elements of a partial order \(\mathbb{P}\) is predense below \(q \in \mathbb{P}\) if for every \(r \le q\) there is \(a \in A\) such that \(r\) and \(a\) are compatible.

def IsPredenseBelow {P : Type*} [PartialOrder P] (A : Set P) (q : P) : Prop :=
  ∀ r ≤ q, ∃ a ∈ A, IsCompatible r a

Uses 1 · Used by 1

Statement usesCompatible conditions

Used by(M, ℙ)-generic conditions

Definition(M, ℙ)-generic conditions#✓fully proved

Let \(\mathbb{P}\) be a partial order and \(M\) a subset of the disjoint union \(\mathbb{P} \sqcup \mathcal{P}(\mathbb{P})\). Write \(M_c\) for the set of \(p \in \mathbb{P}\) whose copy in the disjoint union lies in \(M\), and \(M_s\) for the set of \(D \subseteq \mathbb{P}\) whose copy lies in \(M\). A condition \(q \in \mathbb{P}\) is \((M, \mathbb{P})\)-generic if for every \(D \in M_s\) that is dense in \(\mathbb{P}\) (every element of \(\mathbb{P}\) has an element of \(D\) below it), the set \(D \cap M_c\) is predense below \(q\): for every \(r \le q\) there are \(a \in D \cap M_c\) and \(s \in \mathbb{P}\) with \(s \le r\) and \(s \le a\).

No condition is imposed on \(M\) here. In the intended application \(M\) is the trace of a countable elementary submodel of \(H(\theta)\), for a sufficiently large regular cardinal \(\theta\), that contains \(\mathbb{P}\); genericity depends only on \(M_c\) and \(M_s\), and the elementarity is supplied by the club in the definition of proper partial orders.

def IsGenericFor {P : Type*} [PartialOrder P] (M : Set (P ⊕ Set P)) (q : P) : Prop :=
  ∀ D ∈ modelSets M, IsCoinitial D → IsPredenseBelow (D ∩ modelConds M) q

Uses 3 · Used by 1

Statement usesPredense below a condition · Conditions in a model · Sets of conditions in a model

Used byProper partial orders

DefinitionProper partial orders#✓fully proved

Let \(\mathbb{P}\) be a partial order and let \(X\) be the disjoint union \(\mathbb{P} \sqcup \mathcal{P}(\mathbb{P})\); for \(M \subseteq X\) write \(M_c\) for the set of \(p \in \mathbb{P}\) whose copy in \(X\) lies in \(M\). Then \(\mathbb{P}\) is proper if there is a club \(C\) in \([X]^\omega\) such that for every \(M \in C\) and every \(p \in M_c\) there is an \((M, \mathbb{P})\)-generic condition \(q \le p\). Here a club in \([X]^\omega\) is a family of countable subsets of \(X\) such that every countable subset of \(X\) is contained in a member of the family, and the union of every increasing sequence \(M_0 \subseteq M_1 \subseteq \cdots\) of members of the family is again a member.

The usual requirement \(\mathbb{P} \in M\) is not imposed: \(\mathbb{P}\) is an element of \(X\) (as a subset of itself), and since \(C\) is cofinal it has members containing it.

def IsProperForcing (P : Type*) [PartialOrder P] : Prop :=
  ∃ C : Set (Set (P ⊕ Set P)), IsClubOmega C ∧
    ∀ M ∈ C, ∀ p ∈ modelConds M, ∃ q ≤ p, IsGenericFor M q

Uses 3 · Used by 1

Statement usesClub families of countable sets · (M, ℙ)-generic conditions · Conditions in a model

Used byProper Forcing Axiom

DefinitionProper Forcing Axiom#✓fully proved

For every proper partial order \(\mathbb{P}\), every family \(\mathcal{D}\) of at most \(\aleph_1\) dense subsets of \(\mathbb{P}\), and every condition \(p \in \mathbb{P}\), there is a filter \(G \subseteq \mathbb{P}\) with \(p \in G\) that meets every member of \(\mathcal{D}\), that is, \(G \cap D \neq \emptyset\) for every \(D \in \mathcal{D}\).

Here a set \(D \subseteq \mathbb{P}\) is dense if for every \(q \in \mathbb{P}\) there is \(d \in D\) with \(d \le q\), and a filter is a nonempty, upward closed subset \(G\) of \(\mathbb{P}\) such that any two elements of \(G\) have a common lower bound in \(G\).

def ProperForcingAxiom : Prop :=
  ∀ (P : Type*) [PartialOrder P], IsProperForcing P →
    ∀ D : Set (Set P), (∀ S ∈ D, IsCoinitial S) → Cardinal.mk D ≤ aleph 1 →
    ∀ p : P, ∃ G : Set P, Order.IsPFilter G ∧ p ∈ G ∧ ∀ S ∈ D, (G ∩ S).Nonempty

Uses 1

Statement usesProper partial orders

7 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.