Alphabeta Math
TheoremStatement: Literature-sourcedProof: Literature-sourcedPipeline-generatedjudge pass (gpt-5.6-terra)audited 2026-09-14
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.

PID plus p greater than omega-one eliminates S-spaces

Statement

In ZFC plus PID and p>ω1, every regular Hausdorff hereditarily separable space is hereditarily Lindelöf. Consequently no S-space exists.

Facts & Assumptions

Given: PID, p>ω1, and a regular Hausdorff hereditarily separable space K.

[F1]

A P-ideal uses modulo-finite pseudounions; PID has the uncountable internally-small and countable orthogonal-cover alternatives; p controls pseudointersections; and S-spaces use the stated hereditary topological conventions. P-ideals, PID, the pseudointersection number, and S-spaces

[A1]

AC supplies the omega-one recursion, countable enumerations, and all simultaneous finite-modulo and topological witness choices. The Axiom of Choice

Proof

1.1

Assume for contradiction that some subspace WK is not Lindelöf. Regularity, Hausdorffness, and hereditary separability pass to subspaces, so replace K by W. Choose an open cover with no countable subcover. Recursively for α<ω1, select a cover member Uα and xαUα outside β<αUβ. Let X={xα:α<ω1} and relabel Uxα=Uα; then UxX is countable for every xX. By regularity choose open Vx with xVxVxUx. Define I={A[X]ω:(xX) AVx<ω}. It is an ideal containing all finite sets.

F1A1Givenassume-contra
2.1

We first derive the needed domination fact from p. If Fωω has size less than p, consider, on the countable set ω<ω, the sets Af={s:(i<s) f(i)s(i)} for fF and Cn={s:sn}. Every finite intersection is infinite. A pseudointersection B exists by the definition of p; thin it to distinct sn with sn>n, and put g(n)=sn(n). Since BAf, g eventually dominates every fF. Now take AnI, replace them by their increasing finite unions, and enumerate each infinite An as {an,k:k<ω}. For each x, choose fx(n) past the finite set AnVx. As X=ω1<p, choose one eventual dominator g for all fx, and set A=n{an,k:kg(n)}, ignoring finite An. Each AnA, while for fixed x all sufficiently large rows avoid Vx and the finitely many remaining rows meet it finitely. Thus AI, proving that I is a P-ideal.

F1A1step 1.1
3.1

Apply PID to I. In the first alternative take uncountable YX with [Y]ωI. For yY, the set YVy must be finite; otherwise a countably infinite subset of it would belong to I yet meet Vy infinitely. Since the space is Hausdorff and hence T1, delete the finitely many other points of YVy to obtain a relative open neighborhood isolating y. Thus Y is an uncountable discrete subspace, which is not separable, contradicting hereditary separability.

F1A1step 2.1
3.2

In PID's second alternative write X=nYn with every YnI. Some Y=Yn is uncountable, and hereditary separability gives a countable dense DY. The family {DVx:xX} has the strong finite intersection property. Indeed, if DxFVx were finite for some finite F, then YDxFVx together with finitely many points. But every VxUx and each UxX is countable, forcing Y countable, a contradiction. Since X=ω1<p, F1 gives an infinite pseudointersection aD. Then aVx is finite for every x, so aI; but aY contradicts YI. Thus the second alternative is impossible as well.

F1A1step 1.1step 2.1
4.1

Both PID alternatives contradict hereditary separability, so the assumed non-Lindelöf subspace W cannot exist. Hence every subspace of the original K is Lindelöf: K is hereditarily Lindelöf. By the S-space definition in F1, no regular Hausdorff hereditarily separable non-Lindelöf space exists. AC is used exactly as recorded in A1.

F1A1step 3.1step 3.2discharge-contradiction: step 3.1step 3.2

Depends on

Used by

Dependency tree · two levels

10 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