Martin's axiom

DefinitionCountable chain condition#✓fully proved

A partial order \((P, \le)\) has the countable chain condition (c.c.c.) if every antichain of \(P\) is countable, where an antichain is a set of pairwise incompatible elements: no two distinct members of it have a common lower bound in \(P\).

def IsCCC (P : Type*) [PartialOrder P] : Prop :=
    ∀ A : Set P, IsAntichain (fun p q : P => ∃ r, r ≤ p ∧ r ≤ q) A → A.Countable

Used by 1

Used byMartin's axiom

Definitionσ-centered partial orders#✓fully proved

A partial order \(P\) is \(\sigma\)-centered if there is a map \(c : P \to \mathbb{N}\) such that for every \(n \in \mathbb{N}\), every finite set of elements \(p\) with \(c(p) = n\) has a common lower bound in \(P\). Thus \(P\) splits into countably many centered pieces \(c^{-1}(n)\); the empty set is among the finite sets, so \(P\) must be nonempty.

def IsSigmaCentered (P : Type*) [PartialOrder P] : Prop :=
  ∃ c : P → ℕ, ∀ (n : ℕ) (s : Finset P), (∀ p ∈ s, c p = n) → ∃ r : P, ∀ p ∈ s, r ≤ p

Used by 1

Used byMartin's axiom for σ-centered partial orders

DefinitionMartin's axiom for σ-centered partial orders#✓fully proved

For a cardinal \(\kappa\), this is the statement that for every \(\sigma\)-centered partial order \(P\), every family \(\mathcal{D}\) of at most \(\kappa\) dense subsets of \(P\) and every \(p \in P\), there is a filter \(G\) on \(P\) with \(p \in G\) that meets every member of \(\mathcal{D}\). Here \(D \subseteq P\) is dense if every element of \(P\) has an element of \(D\) below it, and a filter is a nonempty upward closed subset of \(P\) any two of whose elements have a common lower bound in it.

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

Uses 1

Statement usesσ-centered partial orders

DefinitionMartin's axiom#✓fully proved

For a cardinal \(\kappa\), \(\mathrm{MA}(\kappa)\) is the statement that for every partial order \(P\) with the countable chain condition, every family \(\mathcal{D}\) of at most \(\kappa\) dense subsets of \(P\) and every \(p \in P\), there is a filter \(G\) on \(P\) with \(p \in G\) that meets every member of \(\mathcal{D}\). Here \(D \subseteq P\) is dense if every element of \(P\) has an element of \(D\) below it, and a filter is a nonempty upward closed subset of \(P\) any two of whose elements have a common lower bound in it.

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

Uses 1

Statement usesCountable chain condition

4 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.