ExampleConstruction: Literature-sourcedVerification: AI-adaptedPipeline-generatedprecheck passaudited 2026-09-27

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.

A diagonal pseudointersection of a countable descending family

Statement

Let $⟨ A_{n} : n \in N ⟩$ be a sequence of infinite subsets of $ω$ that is descending modulo finite sets: $A_{n + 1} \subseteq^{*} A_{n}$ for every $n$ (Almost inclusion, pseudointersections and towers). Then the following diagonal construction is legitimate: choosing

$x_{n} : = \min (⋂_{i \leq n} A_{i} ∖ {x_{0}, \dots, x_{n - 1}}) (n \in N)$

recursively produces a strictly increasing sequence of natural numbers, and $X : = {x_{n} : n \in N}$ is an infinite subset of $ω$ with $X \subseteq^{*} A_{k}$ for every $k$ , that is, $X$ is a pseudointersection of the family ${A_{k} : k \in N}$ .

Facts & Assumptions

Given: A sequence $⟨ A_{n} : n \in N ⟩$ of infinite subsets of $ω$ with $A_{n + 1} \subseteq^{*} A_{n}$ for every $n$ .

[F1]

$X \subseteq^{*} A$ means that $X ∖ A$ is finite; $\subseteq^{*}$ is reflexive and transitive on subsets of $ω$ ; a pseudointersection of a family is an infinite $X \subseteq ω$ with $X \subseteq^{*} A$ for every member $A$ ; $[ω]^{ω}$ is the family of infinite subsets of $ω$ . (Almost inclusion, pseudointersections and towers)

[F2]

Every countable descending family of infinite subsets of $ω$ has a pseudointersection, by the same diagonal construction; this is one of the two countable clauses of the basic bounds for $p$ and $t$ . (Basic bounds for p and t)

[F3]

Every nonempty subset of $N$ has a least element, and recursion on $N$ defines the unique sequence with prescribed value at $0$ and prescribed successor step. (The well-ordering principle, The recursion theorem, The natural numbers $N$ (von Neumann))

[F4]

A finite union of finite sets is finite, and a set is infinite exactly when it is not finite; $ω = N$ . (The cardinality $∣ A ∣$ of a finite set, The sum rule: a finite disjoint union is finite with $∣ A \cup B ∣ = ∣ A ∣ + ∣ B ∣$ and $∣ ⋃_{i \in I} A_{i} ∣ = \sum_{i \in I} ∣ A_{i} ∣$ , and a sum over a finite index set splits along a partition, Finite, countably infinite, countable, uncountable)

Proof

technique · construction

1.1

For all $n$ and all $i \leq n$ the difference $A_{n} ∖ A_{i}$ is finite: iterating the hypothesis and [F1] gives $A_{n} \subseteq^{*} A_{i}$ whenever $i \leq n$ .

givenF1

2.1

For every $n$ the finite intersection $B_{n} : = ⋂_{i \leq n} A_{i}$ is infinite: $A_{n} ∖ B_{n} \subseteq ⋃_{i \leq n} (A_{n} ∖ A_{i})$ is a finite union of finite sets by step 1.1, hence finite by [F4], and $A_{n} = B_{n} \cup (A_{n} ∖ B_{n})$ is infinite, so $B_{n}$ cannot be finite.

step 1.1F4

3.1

The recursion of the display is legitimate: assume $x_{0}, \dots, x_{n - 1}$ have been chosen; the set $B_{n} ∖ {x_{0}, \dots, x_{n - 1}}$ is infinite minus a finite set, hence nonempty, so it has a least element $x_{n}$ by [F3], and $x_{n} \notin {x_{0}, \dots, x_{n - 1}}$ ; recursion gives the whole sequence.

step 2.1F3F4

4.1

The sequence is strictly increasing: $B_{n + 1} \subseteq B_{n}$ , and $x_{n}$ is the least member of $B_{n}$ outside ${x_{0}, \dots, x_{n - 1}}$ . Since $x_{n + 1}$ belongs to this latter set but differs from $x_{n}$ , minimality gives $x_{n} < x_{n + 1}$ . By step 3.1 the $x_{n}$ are pairwise distinct, so $X$ is infinite; also $x_{n} \in B_{n} \subseteq A_{i}$ for every $i \leq n$ . Thus $X \in [ω]^{ω}$ by [F4].

step 3.1F1F4

5.1

For fixed $k$ , every $x_{n}$ with $n \geq k$ lies in $B_{n} \subseteq A_{k}$ by step 4.1, so $X ∖ A_{k} \subseteq {x_{0}, \dots, x_{k - 1}}$ is finite; hence $X \subseteq^{*} A_{k}$ for every $k$ , and $X$ is a pseudointersection of ${A_{k} : k \in N}$ , the countable case recorded in [F2]. ∎

step 4.1F1F2

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

45 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

J. D. Monk, Continuum cardinals, the diagonal argument preceding Proposition 34, printed p.19 (standard reference, not scraped)