Alphabeta Math
LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6-sol)audited 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.

Basic bounds for p and t

Statement

In ZFC, with p and t as in The pseudointersection and tower numbers,

ℵ1≤p≤t≤c=2ℵ0,

and moreover every countable family of infinite subsets of ω with the strong finite intersection property has a pseudointersection, and every countable descending family ⟨An:n∈ω⟩ of infinite subsets of ω has a pseudointersection (Almost inclusion, pseudointersections and towers for the notions).

The countable case is the diagonal construction: the running finite intersections are infinite, and choosing the least new element of each running intersection produces an infinite set meeting every member cofinitely. That gives p≥ℵ1 and t≥ℵ1; a tower is an SFIP family with no pseudointersection, which gives p≤t; and t≤c is the normal form of a shortest tower.

Facts & Assumptions

Given: the Axiom of Choice (The Axiom of Choice).

[F1]

A pseudointersection of F⊆[ω]ω is an X∈[ω]ω with X⊆∗A for all A∈F; F has SFIP when every finite intersection of members is infinite; a tower is a decreasing family ⟨Aα:α<κ⟩ of infinite sets with no pseudointersection. (Almost inclusion, pseudointersections and towers)

[F2]

p is the least cardinality of an SFIP family with no pseudointersection, and the minimum is attained; t is the least length of a tower, the minimum is attained by a strictly decreasing tower ⟨Aα:α<t⟩, and t is a cardinal with t≤2ℵ0=c. (The pseudointersection and tower numbers)

[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))

Proof

1.1

Let ⟨Cn:n∈N⟩ be a sequence of infinite subsets of ω all of whose finite intersections are infinite, and set Bn=C0∩⋯∩Cn; then each Bn is infinite, and B0⊇B1⊇⋯.

F3F1
1.2

p≤t: by [F2] there is a strictly decreasing tower ⟨Aα:α<t⟩; its member family F has cardinality t, since α↦Aα is injective. The family has SFIP: for β0<⋯<βn<t the intersection contains Aβn minus the finitely many finite sets Aβn∖Aβi. It has no pseudointersection, because it is a tower. Hence some SFIP family without pseudointersection has size t, and p≤t.

F1F2
2.1

Recursively choose xn to be the least element of Bn∖{x0,…,xn−1}; this is legitimate because Bn is infinite and only finitely many elements have been removed, so the set is nonempty, and it has a least element by [F3]. Then xn∈Bn and the xn are pairwise distinct, since xn∉{x0,…,xn−1}.

F1F3step 1.1
3.1

X={xn:n∈N} is infinite by step 2.1, and X⊆∗Ck for every k: indeed xn∈Bn⊆Ck whenever n≥k, so X∖Ck⊆{x0,…,xk−1} is finite. Hence X is a pseudointersection of {Cn:n∈N}.

F1step 2.1
4.1

Now let F⊆[ω]ω be countable and have the strong finite intersection property. If F=∅, then ω is a pseudointersection and the claim follows. Otherwise list F as a sequence ⟨An:n∈N⟩, repeating one member if F is finite; that is possible by [F3] and [F4], and the finite intersections of the An are still infinite. Put Bn=A0∩⋯∩An; each Bn is infinite by SFIP, and the sequence ⟨Bn⟩ has all finite intersections infinite, since B0∩⋯∩Bm=Bm. By steps 1.1, 2.1 and 3.1 applied to Cn:=Bn there is X∈[ω]ω with X⊆∗Bn for every n.

F1F3F4step 3.1
4.2

Every countable descending family ⟨An:n∈N⟩ of infinite sets has a pseudointersection: reaching An from earlier members removes only finitely many points, so Bn=A0∩⋯∩An satisfies An∖Bn⊆⋃i<n(An∖Ai), a finite set, and Bn is infinite because An is; the family {Bn:n∈N} therefore consists of infinite sets with all finite intersections infinite, and steps 1.1, 2.1 and 3.1 applied to it give X∈[ω]ω with X⊆∗Bn⊆An for every n.

F1step 3.1
5.1

For each n the pseudointersection X of step 4.1 is almost contained in Bn⊆An, hence F has a pseudointersection.

F1step 4.1
5.2

t≥ℵ1: a tower of length ℵ0 would be a countable descending family of infinite sets, so by step 4.2 it would have a pseudointersection, which a tower cannot have. Since t is a cardinal, t≠ℵ0 is excluded, so t≥ℵ1.

F1F2step 4.2
6.1

ℵ1≤p: if F has size below ℵ1, then F is finite or countably infinite and, when nonempty, can be listed as a sequence with repetitions if finite; if F has SFIP then step 5.1 supplies a pseudointersection. Hence no family of size below ℵ1 has SFIP and lacks a pseudointersection, and since p is a cardinal with an attained minimum, p≥ℵ1.

F2F4step 5.1
7.1

t≤c is clause [F2]. Combining steps 6.1, 1.2, 5.2 and 7.1 gives ℵ1≤p≤t≤c=2ℵ0, and steps 5.1 and 4.2 are the two countable pseudointersection assertions. This is the statement. ∎

F2step 5.1step 4.2step 6.1step 1.2step 5.2

Depends on

Used by

Dependency tree · two levels

53 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