LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedaudited 2026-09-22

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.

Martin's axiom extends families almost disjoint from a subfamily

Statement

Assume $M A$ (Martin's Axiom at a cardinal and Martin's Axiom) and let $B \subseteq P (ω)$ be a family with $∣ a \cap b ∣ < ω for all distinct a, b \in B,$ and $∣ B ∣ < c$ . Then for every $A \subseteq B$ all of whose members are infinite there is $d \subseteq ω$ with $∣ a \cap d ∣ = ω (a \in A), ∣ b \cap d ∣ < ω (b \in B ∖ A) .$

Facts & Assumptions

Given: An almost disjoint family $B$ of subsets of $ω$ with $∣ B ∣ < c$ , a subfamily $A \subseteq B$ , and Martin's axiom.

[F1]

$M A$ is the scheme $M A (κ)$ for every infinite $κ < c$ , where $M A (κ)$ says that every nonempty ccc partial order and every family of at most $κ$ dense subsets has a filter meeting all of them (Martin's Axiom at a cardinal and Martin's Axiom).

[F2]

$∣ B ∣ < c$ and $ω < c$ give $∣ B ∣ \cdot ω < c$ , and there is a bijection $ω \times ω \to ω$ ; cardinal arithmetic is in $Z F C$ (Cardinal (initial ordinal) and cardinality, The natural numbers $N$ (von Neumann), The Axiom of Choice).

[L1]

Finite subsets of $ω$ and finite subsets of $B$ form sets, and a condition is a pair $(s, F)$ of such sets; a subset of $ω$ is a function-like set of natural numbers (A function is a relation $f$ with $(a, b) \in f$ and $(a, c) \in f$ implying $b = c$ ; $f : A \to B$ , the value $f (a)$ , domain and codomain, The cardinality $∣ A ∣$ of a finite set).

Proof

technique · direct

1.1

Let $P$ be the set of pairs $(s, F)$ with $s \subseteq ω$ finite and $F \subseteq B ∖ A$ finite, ordered by $(s, F) \leq (s^{'}, F^{'})$ if and only if $s \supseteq s^{'}$ , $F \supseteq F^{'}$ and $(s ∖ s^{'}) \cap ⋃ F^{'} = \emptyset$ . This is a partial order with greatest (weakest) element $(\emptyset, \emptyset)$ ; every condition is below it in the stronger-smaller convention.

givenL1

2.1

$P$ is ccc, indeed a countable union of centered sets: conditions with the same first coordinate $s$ are pairwise compatible, since for $(s, F_{1})$ and $(s, F_{2})$ the pair $(s, F_{1} \cup F_{2})$ is a common extension; and there are only countably many finite $s \subseteq ω$ .

step 1.1L1

2.2

For $a \in A$ and $n \in ω$ the set $D_{a, n} : = {(s, F) \in P : ∣ s \cap a ∣ \geq n}$ is dense. Given $(s^{'}, F^{'})$ , the set $a ∖ ⋃ F^{'}$ is infinite: $a$ is infinite by hypothesis, the finite family $F^{'}$ is disjoint from $A$ by step 1.1, and each $b \in F^{'}$ is distinct from $a$ and hence meets $a$ in a finite set; choose $s : = s^{'} \cup s^{''}$ where $s^{''}$ is a set of $n$ elements of $a ∖ (s^{'} \cup ⋃ F^{'})$ , and put $F : = F^{'}$ . Then $(s, F) \leq (s^{'}, F^{'})$ because $s ∖ s^{'}$ avoids $⋃ F^{'}$ , and $∣ s \cap a ∣ \geq n$ .

step 1.1L1

2.3

For $b \in B ∖ A$ the set $E_{b} : = {(s, F) \in P : b \in F}$ is dense. Given $(s^{'}, F^{'})$ , the pair $(s^{'}, F^{'} \cup {b})$ lies in $P$ by step 1.1 and extends $(s^{'}, F^{'})$ : indeed $s^{'} \supseteq s^{'}$ , $F^{'} \cup {b} \supseteq F^{'}$ and $(s^{'} ∖ s^{'}) \cap ⋃ F^{'} = \emptyset$ . Once $b$ belongs to the second coordinate of a member of the filter, no later first coordinate adds an element of $b$ , so the intersection of $d$ with $b$ is computed from a single finite $s$ .

step 1.1L1

3.1

The family of dense sets ${D_{a, n} : a \in A, n \in ω} \cup {E_{b} : b \in B ∖ A}$ has cardinality at most $∣ B ∣ \cdot ω < c$ by [F2], and $P$ is ccc by step 2.1, so $M A$ gives a filter $G \subseteq P$ meeting all of them. Put $d : = ⋃ {s : (s, F) \in G}$ .

step 2.1step 2.2step 2.3F1F2

4.1

For $b \in B ∖ A$ we have $∣ d \cap b ∣ < ω$ : by step 2.3 and step 3.1 some $(s, F) \in G$ has $b \in F$ ; for any $(s^{'}, F^{'}) \in G$ , compatibility gives $(s^{''}, F^{''}) \in G$ extending both, and then $s^{'} \cap b \subseteq s^{''} \cap b = (s \cap b) \cup ((s^{''} ∖ s) \cap b) = s \cap b$ because $(s^{''} ∖ s) \cap b = \emptyset$ . As $(s^{'}, F^{'}) \in G$ was arbitrary, $d \cap b \subseteq s \cap b$ , so $d \cap b = s \cap b$ is a finite set.

step 2.3step 3.1

4.2

For $a \in A$ we have $∣ d \cap a ∣ = ω$ : for every $n$ step 2.2 and step 3.1 give $(s, F) \in G$ with $∣ s \cap a ∣ \geq n$ , and $s \subseteq d$ .

step 2.2step 3.1

5.1

Steps 4.1 and 4.2 exhibit $d \subseteq ω$ with the two required properties for the given $A \subseteq B$ .

step 4.1step 4.2∎

Remarks

Where the hypotheses are used. Only in step 2.2, and there twice over: adding new elements of $a$ is possible because $a$ is infinite and meets the finitely many members of $F^{'}$ — which lie outside $A$ — in finite sets. The restriction of the second coordinate to $B ∖ A$ is what keeps $D_{a, n}$ extendable, since a condition carrying $a$ in its second coordinate could never add an element of $a$ again. Without infiniteness of the members of $A$ the statement is false, as $A = {\emptyset}$ shows, and the consumer Martin's axiom produces an uncountable Q-set therefore uses a base of intervals in which every real lies in infinitely many members.
The filter is supplied by MA, not by choosing conditions. The extension conditions in steps 2.2 and 2.3 are explicit constructions, so no choice beyond the given filter is used; the filter itself comes from $M A$ .

Depends on

Used by

Martin's axiom produces an uncountable Q-set Lemma

Dependency tree · two levels

33 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

Dennis K. Burke, The Normal Moore Space Problem (standard reference, not scraped)
Kenneth Kunen, Set Theory: An Introduction to Independence Proofs (standard reference, not scraped)