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 , every regular Hausdorff hereditarily separable space is hereditarily Lindelöf. Consequently no S-space exists.
Facts & Assumptions
Given: PID, , and a regular Hausdorff hereditarily separable space .
A P-ideal uses modulo-finite pseudounions; PID has the uncountable internally-small and countable orthogonal-cover alternatives; controls pseudointersections; and S-spaces use the stated hereditary topological conventions. P-ideals, PID, the pseudointersection number, and S-spaces
AC supplies the omega-one recursion, countable enumerations, and all simultaneous finite-modulo and topological witness choices. The Axiom of Choice
Proof
Assume for contradiction that some subspace is not Lindelöf. Regularity, Hausdorffness, and hereditary separability pass to subspaces, so replace by . Choose an open cover with no countable subcover. Recursively for , select a cover member and outside . Let and relabel ; then is countable for every . By regularity choose open with . Define . It is an ideal containing all finite sets.
We first derive the needed domination fact from . If has size less than , consider, on the countable set , the sets for and . Every finite intersection is infinite. A pseudointersection exists by the definition of ; thin it to distinct with , and put . Since , eventually dominates every . Now take , replace them by their increasing finite unions, and enumerate each infinite as . For each , choose past the finite set . As , choose one eventual dominator for all , and set , ignoring finite . Each , while for fixed all sufficiently large rows avoid and the finitely many remaining rows meet it finitely. Thus , proving that is a P-ideal.
Apply PID to . In the first alternative take uncountable with . For , the set must be finite; otherwise a countably infinite subset of it would belong to yet meet infinitely. Since the space is Hausdorff and hence , delete the finitely many other points of to obtain a relative open neighborhood isolating . Thus is an uncountable discrete subspace, which is not separable, contradicting hereditary separability.
In PID's second alternative write with every . Some is uncountable, and hereditary separability gives a countable dense . The family has the strong finite intersection property. Indeed, if were finite for some finite , then together with finitely many points. But every and each is countable, forcing countable, a contradiction. Since , F1 gives an infinite pseudointersection . Then is finite for every , so ; but contradicts . Thus the second alternative is impossible as well.
Both PID alternatives contradict hereditary separability, so the assumed non-Lindelöf subspace cannot exist. Hence every subspace of the original is Lindelöf: 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.
Depends on
Used by
- PFA implies that there are no S-spaces Corollary
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
- Todorcevic, Combinatorial Dichotomies in Set Theory, Theorem 23.2 and preceding argument, pp.45-46 (standard reference, not scraped)
- Todorcevic, Forcing with a coherent Souslin tree, Section 7, pp.20-22 (standard reference, not scraped)