Alphabeta Math
Pipeline-generated
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.

Minimal Walks, Oscillation, and L- and S-Spaces

1 · Prerequisites

2 · Summary

This page develops the combinatorics behind Moore's ZFC L-space rather than recording the existence theorem as a black box. A locally finite C-sequence on ω1 produces finite minimal walks, upper and lower traces, coherent finite-to-one weights, and oscillation data. Exact club extension and block lemmas lead to a colouring that realizes finite binary patterns on functional coordinate graphs. Its clopen subbasic sets define Moore's topology and give the canonical embedding into {1,1}ω1Tω1. The same colouring proves nonseparability, the cross-injection obstruction, and hereditary Lindelöfness, yielding an L-space in ZFC.

The S-space direction is kept logically separate. Hart--Kunen ordered fundamental spaces and their compact-tail refinements produce, under CH, a strong S-space whose every positive finite power is hereditarily separable and non-Lindelöf. In the incompatible PFA branch, Abraham's dichotomy for ideals of countable sets generated modulo finite by ω1 members turns a right-separated subspace into an uncountable nonseparable witness, proving that no S-space exists.

Choice is declared at the actual ladder, model, thinning, recursion, and forcing uses. CH, V=L, and PFA are never conjoined. The final supercompact-to-no-S-space statement is only a formal relative-consistency implication, with an explicit proof-code reduction and no extraction of a transitive model from consistency.

3 · Logical flowchart

4 · Definitions, theorems and proofs

DefinitionDefinition: Literature-sourcedProof: Not applicableaudited 2026-09-14Open item page →

L-spaces, S-spaces, and strong S-spaces

Definition

A topological space is hereditarily separable when every one of its subspaces is separable, and it is hereditarily Lindelöf when every one of its subspaces is Lindelöf. Here every subset carries its subspace topology, as in Hereditary, open-hereditary and closed-hereditary properties of topological spaces; separability and Lindelöfness have the meanings in Separability: the existence of an at most countable dense subset and Countably compact, Lindel"of, sequentially compact, limit point compact and σ-compact spaces, and relatively compact subsets.

Using this library's convention that regularity does not itself include any separation axiom, a space is

  • an L-space if it is regular and Hausdorff, hereditarily Lindelöf, and nonseparable;
  • an S-space if it is regular and Hausdorff, hereditarily separable, and not Lindelöf; and
  • a strong S-space if every nonempty finite power is an S-space.

Thus a strong S-space is itself an S-space (take the first power), and every finite power of a strong S-space is hereditarily separable. Empty powers are not part of the definition: the zeroth power is a singleton, hence Lindelöf and not an S-space, so including it would make the notion impossible.

The regular-plus-Hausdorff clause implies T3 under the conventions of Regular spaces and T3 spaces, with the source disagreement over whether regularity includes T1 stated explicitly and Hausdorff space: distinct points have disjoint open neighbourhoods; every metrizable space is Hausdorff and the indiscrete topology on two points is not. It is nevertheless written in the literature's customary form so that regularity is not silently given a different meaning.

Some sources call any regular Hausdorff, hereditarily separable but not hereditarily Lindelöf space an S-space. The two conventions have the same existence content: under that broader wording, choose a subspace that is not Lindelöf; regularity, Hausdorffness, and hereditary separability pass to that subspace, which is an S-space in the definition above. Conversely, a space that is not Lindelöf is certainly not hereditarily Lindelöf. We keep the narrower definition rather than silently exchanging the two statements.

These definitions make no choice. Later assertions that construct examples simultaneously along ω1, or that use PFA or CH in ZFC, declare those axioms at the point of use.

DefinitionDefinition: Literature-sourcedProof: AI-adaptedjudge pass (gpt-5.6-terra)audited 2026-09-14Open item page →

C-sequences and the upper and lower traces of minimal walks on omega-one

Definition

Work in ZFC. A locally finite C-sequence on ω1 is a sequence Cγ:γ<ω1 such that

  • C0=;
  • if γ>0, then Cγγ is cofinal in γ;
  • Cγη is finite whenever η<γ; and
  • 0Cγ whenever γ>0.

At a successor one may and shall take Cη+1={0,η}, read as {0} when η=0. At a nonzero countable limit γ, choose a strictly increasing cofinal ω-sequence and adjoin 0. The choice, simultaneously for all limit γ<ω1, is the use of The Axiom of Choice in this definition; the definitions made from a fixed C-sequence use no further choice.

Fix such a sequence. For α<β<ω1, the minimal walk from β down to α is the finite decreasing sequence

β=β0>β1>>βn1>βn=α,

where, as long as βi>α,

βi+1=min(Cβiα)=min{ξCβi:αξ}.

The displayed set is nonempty: cofinality supplies an element at a limit stage, and the predecessor belongs to the chosen successor set. Its minimum is below βi. If the recursion never reached α, it would give an infinite strictly decreasing sequence of ordinals, contrary to the well-ordering in Ordinal (von Neumann). Thus n<ω and the walk is well defined.

Its upper trace is

Tr(α,β)={βi:i<n},

with Tr(α,α)=. For i<n put

mi(α,β)={max ⁣(ji(Cβjα)),α>0,0,α=0.

The union in the first line is a nonempty finite set: it contains 0, and it is a finite union of finite initial intersections. The lower trace is

L(α,β)={mi(α,β):i<n},L(α,α)=,

listed in its inherited nondecreasing order when multiplicities along the walk matter. Equivalently, with β=min(Cβα) and m=max(Cβα) for α>0,

L(α,β)=(L(α,β){m})m;

here an ordinal m is the set of its predecessors, so subtraction discards earlier values below the new running maximum. The explicit α=0 convention avoids the undefined expression max and gives L(0,β)={0} for β>0.

For finite sets of ordinals, a<b means that every member of a is below every member of b. This convention will be used in the concatenation statements below; it is not the comparison of their cardinalities.

LemmaStatement: Literature-sourcedProof: AI-adaptedjudge pass (gpt-5.6-terra)audited 2026-09-14Open item page →

Concatenation and limit control for minimal-walk traces

Statement

Fix the locally finite C-sequence of C-sequences and the upper and lower traces of minimal walks on omega-one.

  1. If α<β<γ<ω1 and L(β,γ)<L(α,β), then Tr(α,γ)=Tr(β,γ)Tr(α,β) and L(α,γ)=L(β,γ)L(α,β). The unions occur in the displayed walk order: first the segment from γ to β, then the segment from β to α. The same identities hold trivially when α=β or β=γ after the corresponding empty trace is removed.
  2. If δ<ω1 is a nonzero limit ordinal, then limξδminL(ξ,δ)=δ. Explicitly, for every η<δ there is ξ0<δ such that ξ0<ξ<δ implies η<minL(ξ,δ)<δ.

The second assertion has the limit ordinal as the upper endpoint. It does not assert the generally false fixed-β limit minL(ξ,β)α when α<β.

Facts & Assumptions

Given: The fixed normalized C-sequence and the trace conventions in the statement.

[F1]

C-sequences and the upper and lower traces of minimal walks on omega-one defines the walk by least points of Cζ at or above the target, and defines the lower trace by the successive running maxima of the finite sets Cζα.

Proof

technique · direct
1.1

If α=β or β=γ, one upper and lower trace is empty by [F1], so both concatenation identities reduce to equality with the other trace. Hence suppose α<β<γ and L(β,γ)<L(α,β).

F1given
1.2

Let δ be a nonzero limit and 0<ξ<δ. The first lower-trace value for the walk from δ to ξ is max(Cδξ), and all later values are running maxima containing that first intersection. Hence minL(ξ,δ)=max(Cδξ). The same equality is harmless at ξ=0 under the explicit zero convention, although limits only concern a final tail.

F1given
2.1

Every member of L(α,β) is below α, so the separation hypothesis puts every member of L(β,γ) below α. If ζ is a node of Tr(β,γ), the running maximum that records Cζβ occurs in L(β,γ) or is bounded by a later recorded maximum. Thus Cζβα, and therefore Cζα=Cζβ. In particular Cζ has no point in [α,β), so min(Cζα)=min(Cζβ).

F1step 1.1
2.2

Given η<δ, cofinality of Cδ gives cCδ with η<c<δ. Since δ is a limit, ξ0=c+1<δ. Whenever ξ0<ξ<δ, one has cCδξ, and step 1.2 gives η<cminL(ξ,δ)<δ. This is exactly the ordinal-limit assertion in clause 2.

F1step 1.2
3.1

Step 2.1 says that the walk aimed at α makes exactly the same choices as the walk aimed at β until it reaches β. From that node onward its recursion is the walk from β to α. This proves the asserted upper-trace concatenation, with no repeated β because the first trace excludes its terminal point and the second includes its starting point.

F1step 2.1
4.1

Along the first segment, step 2.1 identifies every initial intersection and hence every running maximum with the corresponding value in L(β,γ). All those values are below every value of L(α,β). Consequently, after the walk reaches β, taking running maxima for the continued walk produces exactly the values of L(α,β); no earlier value suppresses or changes one. The lower trace is therefore the ordered union L(β,γ)L(α,β).

F1step 2.1step 3.1
5.1

Steps 3.1 and 4.1 prove the two concatenation identities, including the endpoint reductions in step 1.1, and step 2.2 proves the exact limit-target control from step 1.2.

step 1.1step 1.2step 2.2step 3.1step 4.1
DefinitionDefinition: Literature-sourcedProof: Not applicablejudge pass (gpt-5.6-terra)audited 2026-09-14Open item page →

Minimal-walk weights, labelled lower traces, and the functions e-beta

Definition

Work in ZFC and retain the fixed C-sequence and traces from C-sequences and the upper and lower traces of minimal walks on omega-one. Write 2ω for Cantor space and C(2ω,ω) for the continuous maps from Cantor space to discrete ω. Such a map has finite image by compactness and is constant on the cells of a finite clopen partition. Every clopen subset of Cantor space is a finite union of basic cylinders, so there are only countably many such maps.

Use Solovay’s stationary partition theorem to partition ω1 into countably many stationary sets and fix a sequence wξ:ξ<ω1 in which every member of C(2ω,ω) occurs on a stationary set. Cantor's theorem Cantor's theorem: AP(A), together with AC's comparison of cardinals, gives an injection ω12ω; fix pairwise distinct zα:α<ω1. These two simultaneous selections, and the stationary partition's ZFC proof, account for the The Axiom of Choice dependency.

Suppose α<β and write the walk and its running maxima as

β=β0>>βn=α,m0mn1.

For θL(α,β) let i(θ) be the least i<n with mi=θ. The labelled lower trace

μ(α,β):L(α,β)C(2ω,ω)

is defined by μ(α,β)(θ)=wβi(θ). Thus the label at a repeated running maximum is the label from its first occurrence. For ξ<ω1, its evaluated form is the integer-valued function

μ(α,β;ξ)(θ)=μ(α,β)(θ)(zξ).

On the diagonal, μ(α,α) is the empty function. In recursive language, the new minimum of the lower trace receives label wβ, and all strictly larger lower-trace points retain the labels from the next walk node. Consequently, whenever traces concatenate under the separation hypothesis, the labelled traces concatenate with the same restrictions; and for 0<ξ<δ,

μ(ξ,δ)(minL(ξ,δ))=wδ.

For αβ, the maximal weight is

ρ1(α,α)=0,ρ1(α,β)=max{Cζα:ζTr(α,β)}.

This is a natural number because the trace and every displayed intersection are finite. Equivalently, if β=min(Cβα), then

ρ1(α,β)=max(Cβα,ρ1(α,β)).

Finally define

eβ:βω,eβ(α)=ρ1(α,β).

The terms “coherent” and “finite-to-one” are conclusions of the next lemma, not assumptions smuggled into this definition.

LemmaStatement: Literature-sourcedProof: AI-adaptedjudge pass (gpt-5.6-terra)audited 2026-09-14Open item page →

The minimal-walk functions are coherent and finite-to-one

Statement

For every β<ω1, the function eβ:βω is finite-to-one. If ββ<ω1, then

{α<β:eβ(α)eβ(α)}

is finite. Thus eβ:β<ω1 is coherent on the common domains of its members.

Facts & Assumptions

Given: Ordinals ββ<ω1 and the fixed minimal-walk data.

[F1]

Minimal-walk weights, labelled lower traces, and the functions e-beta identifies eβ(α) with the maximum of the finite local weights Cζα over ζTr(α,β).

[F2]

Concatenation and limit control for minimal-walk traces proves trace concatenation once the finite initial intersections above the splice have stabilized.

Proof

technique · direct
1.1

Fix n<ω and set D={α<β:eβ(α)n or eβ(α)eβ(α)}. We prove that D has no limit point at or below β.

given
1.2

Let 0<δβ be a limit ordinal. The two traces Tr(δ,β) and Tr(δ,β) are finite. Local finiteness makes each Cζδ finite for a trace node ζ>δ. Choose δ0<δ above every member of all these intersections, and let N be the maximum of n and their finitely many cardinalities. Cofinality of Cδ permits enlarging δ0 so that Cδα>N whenever δ0<α<δ.

F1given
2.1

For δ0<α<δ, no trace node above δ has a C-point in [α,δ). Hence the walks toward α first follow the walks toward δ and then the walk from δ to α; this is the same splice calculation as [F2]. Moreover, every local weight on either upper segment is its stabilized value CζδN, whereas the lower segment contains the weight Cδα>N.

F1F2step 1.2
3.1

Taking the maxima in [F1] therefore gives eβ(α)=eδ(α)=eβ(α)>n for every δ0<α<δ. Such α is not in D, so δ is not a limit point of D. Zero and successor ordinals are not limit points from below, so D has no limit point at or below β.

F1step 2.1
4.1

If D were infinite, its well-order would recursively give a strictly increasing ω-sequence from D. Its supremum is a nonzero limit ordinal δβ and every final segment below δ meets D, contradicting step 3.1. Hence D is finite.

step 1.1step 3.1
5.1

The set {α<β:eβ(α)=n} lies in D, so every fiber of eβ is finite. Taking, for example, n=0, the disagreement set between eβ and eββ also lies in D and is finite.

step 1.1step 4.1
6.1

Step 5.1 proves finite-to-one behavior and coherence simultaneously. It also covers β=0, where the domain and disagreement set are empty, and β=β, where disagreement is empty.

step 5.1
DefinitionDefinition: Literature-sourcedProof: Not applicablejudge pass (gpt-5.6-terra)audited 2026-09-14Open item page →

Oscillation on lower traces and Moore's modular colouring

Definition

Let F be a finite set of ordinals in increasing order and let s,t:Fω. For a nonminimum ξF, write ξ for its immediate predecessor in F. The oscillation set of s and t on F is

Osc(s,t;F)={ξF{minF}:s(ξ)t(ξ) and s(ξ)>t(ξ)}.

If F is empty, this set is empty without evaluating minF; if F is a singleton, it is empty because there is no predecessor. For α<β<ω1, define

Osc(α,β)=Osc(eα,eβ;L(α,β)),osc(α,β)=Osc(α,β).

Both restrictions are defined because L(α,β)α, and they are finite by construction. Coherence from The minimal-walk functions are coherent and finite-to-one is a later structural control on these comparisons, not a prerequisite for the finite count itself.

The labelled lower trace of Minimal-walk weights, labelled lower traces, and the functions e-beta gives the stronger integer-valued colouring used here. We count labels only at oscillation points:

o(α,β)=qω{0}({ξOsc(α,β):μ(α,β;α)(ξ)=q}modq).

This oscillation-supported formula is the variant for which the block lemma's labelled new oscillations give exact changes of the summands. Moore's printed Section 5 formula takes the inverse image on the entire labelled lower trace; clauses (2)--(4) of his Lemma 4.1 do not control labels at the other newly adjoined trace points, so that stronger formula is not used here.

Only finitely many summands are nonzero because the evaluated trace has finite domain. The value q=0 is excluded, so reduction modulo zero never occurs; for q=1 its contribution is zero.

Enumerate the primes increasingly as p0=2,p1=3,. Define :ωω by (0)=0 and, for m>0,

(m)=min{n<ω:pnm}.

The minimum exists because a positive integer has only finitely many prime divisors. Put

o(α,β)=(o(α,β)).

This transform can take values larger than 1. The binary colouring used by the topology is defined later as c(α,β)=o(α,β)mod2; the finite-pattern theorem controls both maps but does not conflate them.

LemmaStatement: Literature-sourcedProof: AI-adaptedaudited 2026-09-14Open item page →

Moore's club extension lemma

Statement

Let 1k,l<ω, and let A[ω1]k and B[ω1]l be uncountable pairwise-disjoint families. Regard each member as its increasing enumeration, and write Aδ for {aA:(i<k)δa(i)}, and similarly for B.

For functions s,t with ordinal domains, put

Δ(s,t)=min({ξ<min(doms,domt):s(ξ)t(ξ)}{min(doms,domt)}).

There is a club Dω1 such that, whenever δD, aAδ, bBδ, and R{=,>}, there are a+Aδ, b+Bδ, and one nonempty finite set L+, independent of i,j, for which every i<k and j<l satisfy:

  1. every ξL(δ,b(j)) is below both Δ(ea(i),ea+(i)) and Δ(eb(j),eb+(j));
  2. L(δ,b(j))<L+ and L(δ,b+(j))=L(δ,b(j))L+;
  3. ea+(i)(ξ)Reb+(j)(ξ) for ξL+;
  4. μ(δ,b(j)) is the restriction of μ(δ,b+(j)) to L(δ,b(j)); and
  5. μ(δ,b+(j))(minL+)=wδ.

This formulation of clause 1 also covers b(j)=δ, when the old lower trace is empty. Pairwise disjointness is required within each family; no disjointness between an A-member and a B-member is asserted.

Facts & Assumptions

Given: ZFC, the fixed minimal-walk data, positive k,l, and families A,B as in the statement.

[F1]

The minimal-walk functions are coherent and finite-to-one says that the eβ are finite-to-one and pairwise coherent on common domains.

[F2]

Concatenation and limit control for minimal-walk traces gives lower trace concatenation under separation and makes minL(ξ,δ) tend to a limit δ.

[F3]

Minimal-walk weights, labelled lower traces, and the functions e-beta defines the labelled trace μ, fixes the bookkeeping sequence wξ, and proves the first-label law μ(ξ,η)(minL(ξ,η))=wη(0<ξ<η<ω1).

[F4]

Countable elementary submodels and their collapses supplies countable elementary submodels containing any specified countable parameter set; its proof uses The Axiom of Choice.

[F5]

Closed unbounded subsets of ordinals gives the closed-unbounded convention.

Proof

technique · elementary-submodel reflection, separately for $R={}$ and $R=>$. Here $R={}$ denotes equality; the extra braces only prevent the relation symbol from being read as punctuation
1.1

Fix a sufficiently large regular Θ and Skolem functions for H(Θ). The ordinals δ=Mω1 obtained from countable MH(Θ) containing A,B and all fixed walk data contain a club: Skolem hulls of successively larger countable ordinal sets give unboundedly many such cuts, while the union of an increasing ω-chain of such hulls is elementary and has cut the supremum of their cuts. This is the standard club-of-cuts refinement of [F4], and is closed and unbounded in the sense of [F5]. Fix such M and put δ=Mω1. Notice that every xMω1 is below δ, while δM.

F4F5given
1.2

Suppose first that R is equality, and fix aAδ, bBδ. By coherence in [F1], there is γ0<δ above every L(δ,b(j)) and above all disagreements below δ among the finitely many pairs ea(i),eb(j). Hence ea(i)(ξ)=eb(j)(ξ) whenever γ0<ξ<δ. By the limit clause of [F2], choose γ<δ so that γ<ξ<δ implies γ0<minL(ξ,δ).

F1F2given
2.1

We repeatedly use the following reflection observation. If Xω1 belongs to M and δX, then X is uncountable: otherwise elementarity provides in M an enumeration of X by ω, whence XM and δM, a contradiction. Thus X is unbounded in ω1. Likewise, an uncountable XM has Xδ unbounded in δ, by elementarity applied to arbitrarily large members of X.

F4step 1.1
2.2

For the strict branch, let E be the set of limit ν<ω1 with the following property: for every a0Aν, ν0<ν, ε<ω1, n<ω, and finite Kω1ν, some a1Aε satisfies ν0Δ(ea0(i),ea1(i)) and ea1(i)(ξ)>n for every i<k and ξK. This set is definable from A and the fixed sequence, so EM.

F1F4step 1.1
3.1

Let X consist of those δ+<ω1 for which some a+Aδ+ and b+Bδ+ simultaneously preserve each ea(i) and eb(j) below γ0, agree coordinatewise on (γ0,δ+), satisfy γ0<minL(ξ,δ+) and μ(ξ,δ+)(minL(ξ,δ+))=wδ+=wδ for γ<ξ<δ+, and satisfy μ(δ+,b+(j))=μ(δ,b(j)) for every j<l. All parameters in this definition belong to M. The space C(2ω,ω) is countable and belongs to M, so wδM. Each L(δ,b(j)) and labelled trace μ(δ,b(j)) is finite with ordinal entries below δ and labels in that countable space, hence is an element of M. Finally the restrictions of the e-functions below γ0 are finite modifications, by [F1], of restrictions coded in M. Thus XM without using either δ or b itself as a parameter. Taking δ+=δ, a+=a, and b+=b shows δX; the trace and label requirements are [F2] and the first-label clause retained in [F3]. By step 2.1 choose δ+X above δ, with witnesses a+,b+.

F1F2F3step 1.2step 2.1
3.2

The cut δ belongs to E. Indeed, for given data at δ, finite-to-one behavior lets us enlarge ν0<δ above every ξ<δ at which some ea0(i)(ξ)n. The restriction tuple ea0(i)ν0:i<k belongs to M by coherence. The definable set of ordinals η for which some a1Aη has these restrictions and has all values above n on (ν0,η) belongs to M and contains δ with witness a0. Step 2.1 makes it unbounded, so choose such η above ε and maxK (with no maximum needed when K is empty). Its witness a1 proves the defining demand. Hence δE, and step 2.1 also makes E uncountable.

F1step 2.1step 2.2
4.1

Put L+=L(δ,δ+). It is nonempty because δ<δ+. Its minimum exceeds γ0, and [F2] splices it above the common old trace L(δ+,b+(j))=L(δ,b(j)). Preservation below γ0 gives the two strict Δ bounds; agreement on L+ gives clause 3. The equality of the old labelled traces gives clause 4, and the label at the new minimum is wδ+=wδ, giving clause 5. Thus all five conclusions hold in the equality branch.

F2F3step 3.1
4.2

Fix aAδ and bBδ. Choose γ0Eδ above every old trace L(δ,b(j)), possible by steps 2.1 and 3.2, and then choose γ<δ by [F2] as in step 1.2. Reflecting exactly the finite restrictions, trace-tail and labelled-trace type used in step 3.1, but requiring the candidate cut to be a limit, gives a limit δ+>δ and b+Bδ+ such that the eb-restrictions below γ0 agree, γ0<minL(ξ,δ+) with first label wδ+=wδ for γ<ξ<δ+, and μ(δ+,b+(j))=μ(δ,b(j)).

F1F2F3step 2.1step 3.2
5.1

Put L+=L(δ,δ+) and let n be the maximum of the finitely many values eb+(j)(ξ) for j<l and ξL+. Apply the defining property of γ0E with a0=a, a bound ν0<γ0 above every old trace, K=L+, and ε=δ. It gives a+Aδ preserving every ea(i) on the old trace and satisfying ea+(i)(ξ)>neb+(j)(ξ) on L+. The preservation of b below γ0, the splice calculation, and the label calculation from step 4.1 now verify clauses 1, 2, 4 and 5; the displayed strict inequality verifies clause 3.

F2F3step 2.2step 4.1step 4.2
6.1

The completed equality and strict branches cover the two and only two allowed relations. The club of cuts from step 1.1 is independent of the later choices of a,b,R, so it is the required D. No choice is used after selecting the Skolem functions and fixed data; those ZFC selections are precisely the declared AC dependency.

F4F5step 1.1step 4.1step 5.1
TheoremStatement: Literature-sourcedProof: AI-adaptedaudited 2026-09-14Open item page →

The oscillation block lemma

Statement

Let 1k,l<ω, let A[ω1]k and B[ω1]l be uncountable pairwise-disjoint families, and let wC(2ω,ω). There is a sequence bm:m<ω in B such that, for every n<ω, some aA and ordinals ξ0<<ξn1 satisfy, for all mn, i<k, and j<l:

  1. a<bm, meaning a(i)<bm(j) for every i,j;
  2. Osc(a(i),bm(j)) is the disjoint union Osc(a(i),b0(j))˙{ξm:m<m};
  3. μ(a(i),b0(j)) is the restriction of μ(a(i),bm(j)) to L(a(i),b0(j)); and
  4. μ(a(i),bm(j))(ξm)=w whenever m<m.

For n=0 the ordinal list is empty and clauses 2 and 4 have their literal empty meanings. This is Moore's all-coordinate block lemma; it has no coordinate-map parameter.

Facts & Assumptions

Given: ZFC, positive k,l, uncountable pairwise-disjoint A,B, and wC(2ω,ω).

[F1]

Moore's club extension lemma supplies, at every cut in one club, an equality or strict-comparison extension with exact trace and label preservation.

[F2]

Oscillation on lower traces and Moore's modular colouring defines oscillations as the adjacent changes from eaeb to ea>eb.

[F3]

Minimal-walk weights, labelled lower traces, and the functions e-beta makes {δ:wδ=w} stationary and defines the labelled traces.

[F4]

The minimal-walk functions are coherent and finite-to-one says that every pair of e-functions has only finitely many disagreements on its common domain.

[F5]

Concatenation and limit control for minimal-walk traces supplies the separated trace splice and the limit law minL(ξ,δ)δ.

[F6]

Countable elementary submodels and their collapses and The Axiom of Choice supply the elementary-model selection used below.

[F7]

A stationary subset of ω1 meets every club, and the intersection of finitely many clubs is club. The club filter and nonstationary ideal

Proof

technique · induction, using one equality extension and one strict extension per new oscillation
1.1

Fix Skolem functions for a sufficiently large H(Θ). The cuts Mω1 of countable elementary Skolem hulls containing the fixed parameters form a club C: larger countable ordinal parameter sets give unboundedly many cuts, and unions of increasing ω-chains give closure. Intersect C with the club supplied by F1. By F3 and F7 this intersection meets the stationary set {δ:wδ=w}. Choose M whose cut δ=Mω1 is such a point. This is the sole model-selection use of AC.

F1F3F6F7given
2.1

Choose initial aA and bB with every coordinate strictly above δ; only finitely many members of either pairwise-disjoint family can contain δ. Apply the strict branch of F1 to this pair and call its outputs a0,b0. The appended nonempty block is the final part of every L(δ,b0(j)), and F1 makes the comparison strict on that block. Hence ea0(i)(maxL(δ,b0(j)))>eb0(j)(maxL(δ,b0(j))) for all i,j.

F1step 1.1base
3.1

Suppose am,bm have been chosen, the previously marked points lie below both first-disagreement bounds to the next stage, and the last point of L(δ,bm(j)) has eam(i)>ebm(j) for every i,j. Apply [F1] first with equality, producing a common nonempty block Km= on which the new e-values agree, and then to that output with strict inequality, producing a common nonempty block Km> on which the next a-values exceed the next b-values. Put ξm=minKm>. The two trace splices give L(δ,bm(j))<Km=<Km>, independently of j, and both new minima have label wδ=w.

F1step 1.1step 2.1ih
4.1

On the old trace, the first-disagreement bounds preserve every comparison. At the first point of Km= the previous comparison is strict > and the new comparison is equality, so [F2] creates no downward crossing. Comparisons remain equality through that block. At ξm, equality at its predecessor changes to strict >, so exactly ξm is added to every coordinatewise oscillation set; the comparison stays strict through Km>, so no other new crossing appears. Label restriction in [F1] preserves all old marked labels and assigns w to ξm.

F1F2step 3.1
5.1

Finite induction therefore produces sequences am,bm above δ and increasing ξm with the seven invariants used in Moore's proof: proper common trace extension, one new oscillation, preservation below the first-disagreement bounds, a terminal strict comparison, old-label restriction, and label w at every marked point.

step 2.1step 3.1step 4.1
6.1

Fix n<ω. By [F4], choose γ0<δ above every L(δ,bn(j)) and every disagreement below δ between ebm(j) and ebm(j) for m,mn. Put γ1=maxj<lL(δ,bn(j)). For each i<k, the restriction ri=ean(i)(γ1+1) belongs to M: the corresponding restriction of eγ1+1 belongs to M, and [F4] says that ri is a finite modification of it. Hence S={aA:(i<k) ea(i)(γ1+1)=ri} belongs to M. It contains anM, so it is uncountable; if it were countable, an enumeration in M would put every member of S in M.

F4F6step 1.1step 5.1
7.1

By the limit law in [F5], choose η<δ such that η<ξ<δ implies γ0<minL(ξ,δ). Since S is an uncountable pairwise-disjoint family and η is countable, some member of S has all coordinates above η; this assertion has parameters in M, so elementarity gives such an aSM. Thus a<δ, γ0<L(a(i),δ), and the definition of S gives L(δ,bn(j))<Δ(ea(i),ean(i)) for every i,j. Since every bm lies above δ, one also has a<bm for all mn.

F5F6step 6.1
8.1

The inequalities in step 7.1 let [F5] splice every trace through δ, and [F3] gives the corresponding labelled splice μ(a(i),bm(j))=μ(a(i),δ)μ(δ,bm(j)). On L(a(i),δ) the functions ebm(j) do not depend on m, by the choice of γ0; on L(δ,bm(j)), step 5.1 added exactly the marked oscillations and preserved their labels. The terminal comparison on the first piece is strict, so the splice boundary creates no further -to-> oscillation. Hence clauses 2--4 hold, while step 7.1 gives clause 1. For n=0 the same reflection chooses a and all unions over marked points are empty.

F2F3F4F5step 5.1step 7.1
9.1

Since the recursively chosen sequence bm:m<ω is fixed before n is specified, step 8.1 proves the required quantifier order. No coordinate assignment was introduced: the conclusion holds for all i<k,j<l simultaneously.

step 5.1step 8.1discharge-induction
TheoremStatement: Literature-sourcedProof: AI-adaptedaudited 2026-09-14Open item page →

The Moore colouring realizes finite binary patterns

Statement

Define o(α,β)=(o(α,β)) and the binary colouring

c(α,β)=o(α,β)mod2(α<β<ω1).

Let 1k,l<ω, and let A[ω1]k and B[ω1]l be uncountable pairwise-disjoint families. For every π:kl and χ:k2, some aA and bB satisfy a<b and

o(a(i),b(π(i)))=χ(i)

for all i<k. The same pair has c(a(i),b(π(i)))=1χ(i); consequently c realizes every prescribed binary function on the graph {(i,π(i)):i<k}.

This is a functional-coordinate pattern. It does not assert simultaneous realization of an arbitrary binary matrix on all of k×l.

Facts & Assumptions

Given: ZFC, positive k,l, uncountable pairwise-disjoint A,B, and maps π:kl, χ:k2.

[F1]

The oscillation block lemma supplies arbitrarily long common oscillation blocks whose new points all receive one prescribed continuous label w.

[F2]

Oscillation on lower traces and Moore's modular colouring defines o, the least-nondividing-prime transform , and the evaluated labels.

[F3]

Minimal-walk weights, labelled lower traces, and the functions e-beta supplies the fixed pairwise-distinct Cantor points zα:α<ω1 used to evaluate the labels.

[F5]

The Axiom of Choice implies that a countable union of countable sets is countable and supports the uncountable thinning used below.

Proof

technique · direct modular coding
1.1

Choose distinct primes qi>8 for i<k. For every aA, the finitely many distinct Cantor points za(i) supplied by F3 have pairwise-disjoint clopen neighborhoods, so some continuous wa:2ωω satisfies wa(za(i))=qi for all i<k. There are only countably many continuous integer-valued maps on Cantor space. By F5, one value w occurs for an uncountable subfamily; replace A by that subfamily.

F2F3F5given
2.1

Put Q=i<kqi and N=6Q. Apply [F1] with this w and block length N. It gives aA, members bmB, and marked points such that, relative to b0, the evaluated label qi=w(za(i)) occurs exactly m additional times in the oscillation set for (a(i),bm(π(i))), while every other evaluated-label count is unchanged.

F1step 1.1
3.1

For each i<k, let Oi=Osc(a(i),b0(π(i))) and hi={ξOi:μ(a(i),b0(π(i));a(i))(ξ)=qi}. For s0,qi put hi,s={ξOi:μ(a(i),b0(π(i));a(i))(ξ)=s}, and set ri=(s0,qi(hi,smods))mod6. The sum has finite support by F2. The primes qi are pairwise coprime, so F4 gives a residue x modulo Q satisfying x+hi6ri+2χ(i)(modqi) for every i. Choose its representative 0x<Q<N and put b=bx. The right-hand side lies between 2 and 8, hence is already its least nonnegative residue modulo qi.

F2F4step 2.1
4.1

Fix i<k. The block count from step 2.1 and the definition of ri give an integer y such that o(a(i),b(π(i)))=((x+hi)modqi)+ri+6y=2χ(i)+6(y+1). If χ(i)=0, this number is odd, so the least prime not dividing it is 2=p0. If χ(i)=1, it is even but is congruent to 2 modulo 3, so the least prime not dividing it is 3=p1. Thus [F2] gives o(a(i),b(π(i)))=χ(i).

F2step 2.1step 3.1
5.1

The same displayed formula is odd exactly when χ(i)=0, so c(a(i),b(π(i)))=1χ(i). Given a desired binary pattern ψ:k2 for c, apply the proved assertion with χ=1ψ. This proves every claimed functional pattern, including all coordinates at once, and makes no claim about two values in the same row of a nonfunctional matrix.

step 4.1
6.1

Positivity of k is part of the nonvacuous uncountable-family hypothesis; for a formal empty coordinate list F4 would supply the unique empty residue class and the conclusion would be vacuous. Finite prime choice and the least representative require no further choice; the only new AC use is the uncountable thinning in step 1.1.

F4F5step 1.1step 5.1
DefinitionDefinition: Literature-sourcedProof: AI-adaptedjudge pass (gpt-5.6-terra)audited 2026-09-14Open item page →

Moore's clopen-generated topology

Definition

Retain the binary colouring c(α,β)=o(α,β)mod2 from The Moore colouring realizes finite binary patterns. For α<ω1, put

Wα={α}{β:α<β<ω1 and c(α,β)=1}.

For Xω1, let τ[X] be the topology on X generated by declaring WξX clopen for every ξX. Equivalently, finite intersections of sets WξX and XWξ, with ξX, form a clopen base. The empty intersection is X; when X is empty this gives its unique topology.

There is a useful product representation with no extra generators. Let T be the unit circle and define

eX:X{1,1}ω1Tω1

by

eX(x)(ξ)={1,ξX and xWξ,1,otherwise.

For ξX, the inverse images of the two coordinate values are WξX and its complement; for ξX, the coordinate is constant. Thus the product-induced topology is exactly τ[X]. If x<y are in X, then xWy while yWy, so the y-coordinate separates their images. Hence eX is injective and is an embedding onto its image.

The family {WξX:ξX} is point-countable and point-separating: if xWξ, then ξx, and the countable ordinal x+1 has only countably many members. The displayed clopen base and point separation make every (X,τ[X]) zero-dimensional Hausdorff, hence regular under the library convention.

Coordinates outside X were deliberately padded by the constant 1. Allowing membership in Wξ at such a coordinate would add subbasic sets that Moore did not put into τ[X].

LemmaStatement: Literature-sourcedProof: AI-adaptedjudge pass (gpt-5.6-terra)audited 2026-09-14Open item page →

Every uncountable Moore subspace is nonseparable

Statement

If Xω1 is uncountable, then (X,τ[X]) is not separable.

Facts & Assumptions

Given: An uncountable Xω1.

[F1]

Moore's clopen-generated topology says that WβX is clopen, contains β, and contains no ordinal below β.

[F2]

Separability: the existence of an at most countable dense subset says that a space is separable when it has a countable dense subset.

Proof

technique · direct
1.1

Let DX be countable. Its supremum is a countable ordinal, so uncountability of X gives βX with supD<β.

given
2.1

By [F1], WβX is an open neighborhood of β and every one of its points is at least β. Hence it is disjoint from D, so D is not dense.

F1step 1.1
3.1

Since every countable DX fails to be dense, [F2] proves that (X,τ[X]) is nonseparable. The assertion deliberately excludes countable X; for X= or a singleton the displayed argument has no β above D and no nonseparability conclusion is claimed.

F2step 2.1
LemmaStatement: Literature-sourcedProof: AI-adaptedaudited 2026-09-14Open item page →

The Moore colouring forbids cross-injections

Statement

In ZFC, if X,Yω1 have countable intersection, then no uncountable subspace of (X,τ[X]) admits a continuous injection into (Y,τ[Y]).

Facts & Assumptions

Given: ZFC and X,Yω1 with XY countable.

[F1]

Moore's clopen-generated topology gives a clopen finite-Boolean base and xWη iff either x=η or η<x and c(η,x)=1.

[F2]

The Moore colouring realizes finite binary patterns realizes every binary pattern on the graph of a finite coordinate map.

[F3]

Under choice, the uncountable Δ-system lemma for finite sets gives an uncountable Δ-subfamily of any uncountable family of finite supports.

[F4]

The Axiom of Choice supports the simultaneous neighborhood choices and the finite/countable thinning steps.

Proof

technique · contradiction
1.1

Suppose f:X0Y is continuous and injective for an uncountable X0X. Delete the countable sets X0(XY) and f1(XY). After this deletion, every remaining α and f(α) are distinct and lie on opposite sides of XY and YX. One of the two orientations α<f(α) or f(α)<α holds on an uncountable subfamily; retain it.

F4givenassume-contra
2.1

For each retained α, continuity at α and the neighborhood Wf(α)Y of f(α) give a basic clopen Uαα with Uαf1(Wf(α)Y). Encode Uα by a finite support FαX and its membership-bit function. Add α to the support if necessary.

F1F4step 1.1
3.1

Apply F3 and then finite/countable pigeonhole thinning so that the Fα form a Δ-system with root F, all petals have one size k>0, the membership bits on the fixed root F have one fixed vector, the membership bits on the increasingly enumerated petals have one fixed vector χ0, the root lies below every retained α, and the order type of each petal together with f(α) is constant. These are separate finite thinnings: agreement of the petal pattern alone would not control the root coordinates. Because XY is countable and the petals are disjoint, discard the countably many petals meeting XY. The families A={(FαF){f(α)}:α} and B={{β,f(β)}:β} are therefore uncountable, fixed-size, and pairwise disjoint.

F3F4step 1.1step 2.1
4.1

Enumerate each member of A and B increasingly. The uniform order types give an insertion coordinate rk for f(α) in the first enumeration, a column s<2 occupied by β in the second, and the other column t<2 occupied by f(β). Define π:k+12 by π(r)=t and π(i)=s for ir. Define the desired bit at row r to be 0, and at every other row to be the corresponding petal bit from χ0.

step 3.1
5.1

By [F2], choose aA and bB with a<b that realize these bits. Let a=(FαF){f(α)} and b={β,f(β)}. At the inserted row, c(f(α),f(β))=0, and a<b ensures f(α)<f(β); hence f(β)Wf(α).

F1F2step 4.1
6.1

At every petal row, the realized bit says that β satisfies the corresponding petal literal in the finite Boolean condition defining Uα. At every root row, the separately stabilized root vector has the same value for Uα and Uβ; since βUβ and the root lies below β, F1 translates each root membership into precisely that fixed colouring bit. Thus every root and petal literal defining Uα holds at β, so βUα.

F1step 2.1step 3.1step 5.1
7.1

The containment chosen in step 2.1 now gives f(β)Wf(α), contradicting step 5.1. The construction used the orientation only to decide which column of the increasing pair is β; step 4.1 handles both orientations through s,t. Hence no such continuous injection exists.

step 2.1step 4.1step 5.1step 6.1discharge-contradiction
LemmaStatement: Literature-sourcedProof: AI-adaptedjudge pass (gpt-5.6-terra)audited 2026-09-14Open item page →

Moore's topology is hereditarily Lindelof

Statement

For every Xω1, the space (X,τ[X]) is hereditarily Lindelöf.

Facts & Assumptions

Given: Xω1 and the Moore topology.

[F1]

Countably compact, Lindel"of, sequentially compact, limit point compact and σ-compact spaces, and relatively compact subsets defines Lindelöfness by the existence of an at-most-countable subcover for every open cover, and Hereditary, open-hereditary and closed-hereditary properties of topological spaces defines hereditary Lindelöfness by requiring that property of every subspace.

[F2]

Moore's clopen-generated topology gives a clopen base of finite Boolean conditions in the sets Wξ.

[F3]

Under choice, the uncountable Δ-system lemma for finite sets thins an uncountable family of finite supports to an uncountable Δ-system.

[F4]

The Moore colouring realizes finite binary patterns realizes any functional binary pattern on pairwise-disjoint fixed finite families.

[F5]

The Axiom of Choice supplies the transfinite cover selections and uncountable thinning.

Proof

technique · contradiction
1.1

Suppose some subspace ZX has an open cover U with no countable subcover. Recursively for α<ω1, after choosing UξU for ξ<α, choose xαZξ<αUξ and then UαU containing xα. The uncovered remainder is uncountable at every stage: if it were countable, one further cover member for each remaining point, together with the previous countable family, would be a countable subcover. Hence choose xα above all earlier xξ. Thus xα is strictly increasing and Uα contains no xβ for β>α.

F1F5givenassume-contra
2.1

By [F2], shrink each Uα around xα to a finite Boolean basic set Vα in the subspace Z. Intersect also with Wxα, so its finite support FαX contains xα. Apply [F3] and the finite pigeonhole principle to retain an uncountable index set on which the supports form a Δ-system with root F, have fixed root and petal positions and one fixed membership-bit string, and have nonempty petals of one size k. Pass to a tail so every root member is below every retained xα.

F2F3F5step 1.1
3.1

Let A={FαF:α retained} and B={{xβ}:β retained}. The family A is uncountable and pairwise disjoint by the Δ-system property; B is uncountable and pairwise disjoint because the sequence is strictly increasing. Map each petal coordinate to the sole column and prescribe the corresponding fixed membership bit of Vα. By [F4], choose a petal FαF and a singleton {xβ} with the petal below xβ realizing all those bits.

F4step 2.1
4.1

Since xα belongs to its petal, the inequality from step 3.1 gives xα<xβ, and strict increase gives α<β. The realized petal bits say that xβ meets every petal condition defining Vα. For a root coordinate η, the point xβ meets its required bit because xβVβ, the root bit string is uniform, and η<xβ lets [F2] read membership through c(η,xβ). Consequently xβVαUα.

F2step 1.1step 2.1step 3.1
5.1

Step 1.1 says that Uα contains no xβ with β>α, contradicting step 4.1. Therefore every subspace Z is Lindelöf, which is precisely hereditary Lindelöfness by [F1]. Empty and countable Z cause no problem: a countable space has a countable subcover by choosing one cover member per point, and the empty space uses the empty subcover.

F1F5step 1.1step 4.1discharge-contradiction
TheoremStatement: Literature-sourcedProof: AI-adaptedjudge pass (gpt-5.6-terra)audited 2026-09-14Open item page →

A ZFC L-space

Statement

ZFC proves that (ω1,τ[ω1]) is a zero-dimensional regular Hausdorff, hereditarily Lindelöf, nonseparable space. In particular it is an L-space.

Facts & Assumptions

Given: ZFC and the fixed Moore minimal-walk construction.

[F1]

Moore's clopen-generated topology makes every Moore space zero-dimensional regular Hausdorff.

[F2]

Moore's topology is hereditarily Lindelof proves hereditary Lindelöfness for every Xω1.

[F3]

Every uncountable Moore subspace is nonseparable proves nonseparability whenever X is uncountable.

[F4]

L-spaces, S-spaces, and strong S-spaces defines an L-space as regular Hausdorff, hereditarily Lindelöf, and not hereditarily separable.

Proof

technique · direct assembly
1.1

Take X=ω1. By [F1] its Moore topology is zero-dimensional, regular, and Hausdorff; by [F2] it is hereditarily Lindelöf.

F1F2given
2.1

The set ω1 is uncountable, so [F3] says the whole space is nonseparable. A hereditarily separable space must itself be separable, since the whole underlying set is one of its subspaces. Thus this space is not hereditarily separable.

F3givenstep 1.1
3.1

The four conclusions in steps 1.1 and 2.1 meet [F4] exactly, proving that (ω1,τ[ω1]) is an L-space. No new choice is made in this assembly; every choice-dependent construction or thinning belongs to the corresponding supplier under its own stated hypotheses. The empty and singleton cases of the topology are irrelevant to the witness because ω1 is uncountable.

F1F2F3F4step 1.1step 2.1
DefinitionDefinition: Literature-sourcedProof: Not applicableaudited 2026-09-14Open item page →

Ordered fundamental spaces and nice refinements

Definition

A fundamental space is a Hausdorff space (X,T) of cardinality 1 that is zero-dimensional, separable, first countable, and 1-dense (every nonempty open set has size 1), together with strictly decreasing clopen local bases

X=W0xW1xW2x,n<ωWnx={x}.

It is ordered when X=ω1 and ω is dense. The adjective does not say that Wnαα: indeed W0α=ω1.

Fix an ordered fundamental space. Suppose VnξWnξ and Vnξ{ξ}. For αω1, set

Rnξ(α)={Vnξ,ξ<α,Wnξ,αξ,

and let T˚α be the topology generated by all these Rnξ(α); put T~=T˚ω1. A nice refinement requires:

  • maxVnα=α, and Vnα is closed while Vnαα is open in T˚α;
  • Vnα={α} for α<ω;
  • for ωα<ω1, there are nonempty, pairwise-disjoint, compact clopen sets Hαα(WαW+1α) such that Vmα={α}mHα, and {Vmα:m<ω} is a clopen local base at α in T~.

For the model-guided version, fix a continuous suitable chain Mα:α<ω1 of countable elementary submodels, put the global assignment (α,n)Wnα in M1, and require the earlier V-sequence and final topology below α to belong to Mα+1. On α+1, choose a metric dα for T˚α(α+1) whose ring (WαW+1α)(α+1) lies at radial value 2 from α and has internal diameter at most 23 in dα.

For ωα<ω1, if SMα+1 is countable and SK(α,T~α), define, for νω,

Γα(S,ν)={KS:(<ν) K(WαW+1α)Hα}.

Here K(Y) denotes the nonempty compact subsets of Y, with the Vietoris topology generated by the subbasic conditions KU and KU for open UY. Its standard basic neighbourhoods are N(U0,,Ur)={K:KirUi and KUi for every ir}; in a zero-dimensional space the Ui may be taken nonempty, pairwise-disjoint and clopen. Distances between compacta use the Hausdorff metric induced by dα. For the same range ωα<ω1, the approximation condition (α) is

S[SMα+1, S0,SK(α,T~α)ν<ω KΓα(S,ν) JΓα(S,ω) dα(K,J)2ν].

The condition permits S and either Γ-set to be empty; its implication then has the literal vacuous meaning. The model chain, compatible metrics, and recursive selections are ZFC choices and account for the declared AC dependency. They are auxiliary construction data, not part of the raw definition of a fundamental space.

LemmaStatement: Literature-sourcedProof: AI-adaptedaudited 2026-09-14Open item page →

Nice refinements exist and are regular but not Lindelof

Statement

Every ordered fundamental space has a nice refinement (ω1,T~) satisfying (α) for every ωα<ω1. The refinement is separable, locally compact, locally countable, zero-dimensional, regular, and Hausdorff, but it is not Lindelöf. Here locally countable means that every point has a countable neighbourhood.

Facts & Assumptions

Given: An ordered fundamental space (ω1,T) and ZFC.

[F1]

Ordered fundamental spaces and nice refinements gives the rings, intermediate topologies, model chain, metrics, nice-refinement clauses, the families Γα(S,ν), and (α).

[F2]

A compact topological space is one whose every open cover has a finite subcover, and a compact subset carries the intrinsic subspace topology (Open cover, subcover, and compact topological space; a compact subset is a subspace that is compact in its own right).

[F3]

A compact metric space is totally bounded: at every positive radius it has a finite net (A compact metric space is complete and totally bounded, and neither implication uses any choice principle).

[F4]

A space is locally compact when every point has a compact neighbourhood (Locally compact topological space: every point has a compact neighbourhood; and what this says in a metric space).

[F6]
[F7]

Countable elementary submodels and their collapses supplies a countable elementary hull containing any prescribed countable parameter set.

[F8]

Transfinite recursion constructs the model chain and the later stage-by-stage refinement from their functional successor and limit clauses.

[F9]

The Axiom of Choice supplies the simultaneous recursive choices of hulls, metrics, finite nets, ring points, and compact clopen enlargements.

Proof

technique · transfinite and finite recursion
1.1

Construct the required continuous chain Mα:α<ω1 explicitly. Start with an F7 hull containing the ordered fundamental space and its base assignment. At a successor, apply F7 to the countable set Mα{Mα,α} and the fixed parameters; at a countable limit take the union of the earlier increasing elementary chain, which is countable and elementary by the Tarski--Vaught test. F8 performs this recursion, and F9 makes the simultaneous hull choices. Now choose the compatible metrics dα allowed by F1 and F9. For α<ω put Vnα={α}. Inductively suppose the Vnξ and Hξ have been constructed for every ξ<α, and that the resulting topology below α is locally compact and zero-dimensional.

F1F7F8F9givenbaseih
2.1

Fix ωα<ω1. The countable model Mα+1 contains only countably many sets S satisfying S0 and SK(α,T~α); list them as Sν:ν<ω, repeating every such S infinitely often. This collection is nonempty because it contains S=, and that particular S makes the later star implication vacuous.

F1F7F9step 1.1
3.1

Recursively suppose Hα is fixed for <ν and put Aν=<νHα. This is a finite union of compact sets, hence compact. Every KΓα(Sν,ν) lies in Aν(Wναα): the first ν ring intersections lie in their Hα, while all remaining points lie in the nested Wνα.

F1F2step 1.1step 2.1ih
4.1

The family Γα(Sν,ν) has a finite Hausdorff 2ν-net Pν chosen from itself. Indeed, by [F3] choose a finite ε-net of the compact metric set Aν, where 2ε<2ν. Partition the remaining tail into the outer ring Rν=(WναWν+1α)(α+1) and the deeper tail Tν=Wν+1α(α+1). Record for each K which finitely many ε-cells meet KAν, whether K meets Rν, and whether it meets Tν. There are finitely many records. Two compacta with the same record are within Hausdorff distance at most 2ν: match their points in Aν through a common recorded cell; points in Rν are within its internal diameter 2ν3; and points in Tν are within 2ν by the triangle inequality, since every such point has distance at most 2ν1 from α. The two tail-incidence bits ensure that each required matching part is nonempty. Choosing one member for each realized record gives Pν; if Γα(Sν,ν)=, take Pν=.

F1F3F9step 3.1
5.1

Let Qν be the union of J(WναWν+1α) over JμνPμ. It is a compact subset of the relatively clopen nonempty ν-th ring. Local compactness and the clopen base below α cover Qν by finitely many compact clopen sets lying in that ring; their union is compact clopen. If this union is empty, choose a ring point and one compact clopen neighbourhood of it in the ring. Call the resulting nonempty compact clopen set Hνα; it contains Qν.

F1F2F9step 1.1step 4.1
6.1

For JPν, membership in Γα(Sν,ν) already puts its intersections with rings <ν inside Hα. For ν, the stage- definition includes Pν in μPμ, so Hα absorbs the -th ring intersection of J. Hence PνΓα(Sν,ω).

F1step 4.1step 5.1
6.2

Put Vmα={α}mHα. Its maximum is α and its part below α is open. It is compact in the intermediate topology: an intermediate-open cover has a member containing α, hence contains some WNα(α+1) and all Hα for N; only finitely many earlier compact Hα remain. It is therefore intermediate-closed, and [F1] makes the Vmα a clopen local base in the final refinement. The same argument for a final-open cover, now using a contained VNα, proves that Vmα is compact in the final topology.

F1F2step 5.1
7.1

Whenever Sν=S, steps 4.1 and 6.1 give KΓα(S,ν) JΓα(S,ω) dα(K,J)2ν. Every relevant S occurs infinitely often, so (α) holds.

F1step 2.1step 4.1step 6.1
8.1

Steps 2.1--7.1 together with step 6.2 perform the successor construction at every countable α, while limit stages take the accumulated earlier data. Transfinite induction therefore produces a nice refinement satisfying every (α).

F1step 1.1step 2.1step 3.1step 4.1step 5.1step 6.1step 6.2step 7.1discharge-induction
9.1

Every Vmα is compact by step 6.2, so [F4] gives local compactness. It lies in α+1, a countable ordinal, so it is a countable neighbourhood and the space is locally countable. The base is clopen and Hausdorff by [F1], hence zero-dimensional and regular by [F6].

F1F4F6step 6.2step 8.1
9.2

The set ω remains dense. Inductively, every nonempty relatively open Hαα meets the already dense ω, so every basic tail Vmα meets ω; for α<ω the singleton Vmα itself lies in ω. Thus the refinement is separable.

F1step 5.1step 8.1
9.3

Every initial segment α is open: if ξ<α, then each basic neighbourhood Vmξ is contained in ξ+1α. Consequently U={α:0<α<ω1} is an open cover of ω1. A countable subfamily has countable supremum δ<ω1 and its union is contained in δ, so it misses δ. By [F5] the refined space is not Lindelöf.

F1F5step 6.2step 8.1
10.1

Combining steps 7.1 and 8.1--9.3 gives all asserted properties. The empty Γ cases were handled in steps 2.1 and 4.1, ν=0 has A0=, the finite ordinals use singleton bases, and F9 records every nonempty simultaneous choice.

F8F9step 2.1step 4.1step 7.1step 8.1step 9.1step 9.2step 9.3discharge-induction
LemmaStatement: Literature-sourcedProof: AI-adaptedjudge pass (gpt-5.6-terra)audited 2026-09-14Open item page →

CH makes the nice refinement strongly hereditarily separable

Statement

Assume CH. Start with a second-countable ordered fundamental space and let (ω1,T~) be a nice refinement satisfying (α) at every stage. Then every nonempty finite power of (ω1,T~) is hereditarily separable.

Facts & Assumptions

Given: ZFC, CH, a second-countable ordered fundamental space (ω1,T), and a nice refinement satisfying ().

[F1]

Ordered fundamental spaces and nice refinements defines the intermediate topologies T˚α, standard Vietoris neighbourhoods, the model chain, and (α).

[F2]

Nice refinements exist and are regular but not Lindelof gives the zero-dimensional Hausdorff nice-refinement structure, compact clopen tails, open initial segments, and every instance of ().

[F3]

The continuum hypothesis, and what this page does not prove records CH as the assertion that no cardinality lies strictly between that of ω and that of its power set.

[F5]

Under choice, every regular T1 second-countable space is metrizable makes the regular T1 second-countable fundamental topology metrizable under AC.

[F6]

Under choice, the uncountable Δ-system lemma for finite sets gives an uncountable Δ-subfamily of any uncountable family of finite sets.

[F8]

L-spaces, S-spaces, and strong S-spaces defines hereditary separability and nonempty finite powers.

[F9]

Closed unbounded subsets of ordinals supplies the closed-unbounded terminology used for simultaneous closure points in ω1.

[F10]

The Axiom of Choice supplies all transfinite selections, thinnings, dense-set choices, and the CH well-ordering.

Proof

technique · direct, via exclusion of left-separated sequences
1.1

A space Y is hereditarily separable exactly when it has no left-separated sequence yξ:ξ<ω1, where yξ{yζ:ζ<ξ}. If a subspace A is nonseparable, recursively choose yξA outside the closure of its countable set of predecessors; otherwise those predecessors would be a countable dense subset of A. Conversely, for a left-separated sequence and a countable subset D of its range, choose ξ above every index represented in D; the separating neighbourhood of yξ misses D, so D is not dense in the sequence subspace.

F8F10given
1.2

We will use the following standard Vietoris reduction, whose proof is included. Let B,F be compact in a zero-dimensional space, with FB, and let G be a standard-form local base at F. For G=N(U0,,Ur) put SG={KG:KS, KUi (ir), KG}. Then BS iff BGSG for every GG with nonempty remainder. Forward, combine any standard neighbourhood of the remainder, chosen disjoint from G, with the cells of G to obtain a neighbourhood of B. Reverse, refine any standard neighbourhood of B so its cells meeting F contain some GG, retain the cells disjoint from F, and add the finitely many remainders of the former cells; the assumed closure of the remainder then supplies an element of S in this refinement. For F={p} this says that, along any clopen local base V at p that splits B, BS iff every BV lies in the closure of {KV:KS, V splits K}.

F1F2given
1.3

The original topology T is zero-dimensional Hausdorff, hence regular and T1; [F5] therefore gives a metric inducing it. Since T~ refines T, this metric topology is a coarser topology on the final space.

F1F5given
2.1

For each countable δ<ω1, T˚δ is second countable: add the countably many sets Vnξ with ξ<δ to a countable base for T and close under finite intersections. Finite lists from this base form a countable standard Vietoris base for K(ω1,T˚δ). Every subspace of a second-countable space is second countable and, under [F10], separable by choosing one point from every nonempty basic trace. Thus this hyperspace is hereditarily separable by step 1.1.

F1F4F10step 1.1
2.2

The first closure-transfer claim is the stage case. Let maxB=β, let SMβ+1 be countable with SK(β,T~β), and suppose BS for the T˚β Vietoris topology. The final-open neighbourhood V0β of β leaves a compact remainder BV0β in the coarser intermediate topology; the decreasing Wnβ-base and compactness give r with BWrβV0β, so every ring intersection of index at least r lies in its H-piece. If r=0, each finite danger zone is clopen and misses B, hence B is in the intermediate closure of every Γβ(S,ν). Choose infinitely large ν from (β) and then KΓβ(S,ν) close to B and JΓβ(S,ω) with dβ(K,J)2ν. The triangle inequality makes such J arbitrarily Hausdorff-close to B, and the intermediate and final point-bases agree on {β}Hβ, so B is in the final closure of S. If an earlier ring is bad, increase r beyond it, put W=Wrβ, and use standard neighbourhoods G of the nonempty compact part BW, all with cells below β and hence in Mβ+1. The family SG is in the model, while the tail BW has no danger-zone intersections; apply the r=0 argument to every such tail and then the reduction of step 1.2 to recover B.

F1F2step 1.2
3.1

The full closure-transfer claim follows by induction on maxB. Fix α and suppose SMα+1 is countable in K(α,T~α), every assigned Wnβ for βB belongs to Mα+1, and BS for T˚α. If maxB<α, the intermediate and final bases already agree on B; if maxB=α, step 2.2 applies. If β=maxB>α and B={β}, the common Wnβ bases transfer closure first to T˚β, then step 2.2 transfers it to the final topology. Otherwise, for every sufficiently small splitting Wnβ, step 1.2 gives BWnβSn in T˚α, where Sn={KWnβ:KS, Wnβ splits K}Mα+1. Its maximum is below β and it inherits the model condition, so the induction hypothesis transfers this closure to the final topology, hence to the coarser T˚β topology. Step 1.2 reconstructs BS there, and step 2.2 finishes the transfer to T~.

F1F2step 1.2step 2.2
3.2

Suppose there were a left-separated sequence Bξ:ξ<ω1 of sets of one fixed finite size 0<n<ω in K(ω1,T~) and a fixed γ<ω1 such that the Bξγ were pairwise disjoint. Every Bξ has a maximum. Using step 2.1, thin so the maxima aξ=maxBξ are strictly increasing; bounded maxima would put an uncountable left-separated sequence in one of the second-countable intermediate hyperspaces.

F2F10step 2.1
4.1

For finite target compacta, the model condition in step 3.1 can be removed. Induct on k=B. If BMα+1, the global assigned-base map and finiteness put all its W-bases in the model, so step 3.1 applies. For k=1 outside the model, transfer the singleton first to its own intermediate stage, where its W-base is in the model, and use step 3.1 there. Let k>1, assume the claim below k, and put λ=Mα+1ω1. After moving α to the first point of B above it when necessary, either B is captured by the next model or αB and B=BB+, where B=Bλ and B+=Bλ are both nonempty and smaller than B. With ζ=maxB, let E consist of the B+-element H(ζ,ω1) for which BHS in T˚α. The set E belongs to Mα+1, and step 2.1 gives in that model a countable dense FE. Every HF lies in the model, so step 3.1 puts BH in the final closure of S. Meanwhile B+F transfers to the intermediate stage β=minB+ because those topologies have the same point-bases on B+; the induction hypothesis, applied to the smaller target B+, transfers it to the final topology. Given a standard neighbourhood of BB+ with one disjoint cell at each point, first choose HF whose points enter the B+-cells, then use the final closure of BH to choose an element of S in all cells. Thus B is in the final closure of S.

F1F2F10step 2.1step 3.1
4.2

For each δ<ω1, step 2.1 gives an ordinal ρδ>δ such that {Bξ:ξ<ρδ} is dense in the whole sequence for the T˚δ Vietoris topology; choose the least such ordinal. Refinement gives ρδρϵ when δ<ϵ. The simultaneous closure points of δρδ and ξaξ contain a club C by [F9]. Choose a limit ηC above γ. Then S={Bξ:ξ<η} is a subset of K(η,T~η) and is dense in the whole sequence for T˚η: any basic neighbourhood mentions finitely many switched coordinates and therefore already belongs to some earlier intermediate topology.

F1F9F10step 2.1step 3.2
5.1

Every hereditarily countable set is coded by a relation on a subset of ω, so H(1)20; the reverse inequality follows because every subset of ω is hereditarily countable. Thus [F3] gives H(1)=1. Elementarity puts a bijection from ω1 onto H(1) in M1, and the chain contains every countable ordinal, so H(1)Mω1=α<ω1Mα. Hence choose α>η with SMα+1. Only countably many Bξγ meet the countable interval [η,α], because those free parts are pairwise disjoint; choose ξ>α+1 with Bξ[η,α]=. The point-bases of T˚η and T˚α agree at every point of Bξ (points below η use V, points above α use W), so their standard Vietoris local bases agree there and step 4.2 yields BξS for T˚α. The finite-target transfer in step 4.1 gives BξS in the final topology. But S consists entirely of predecessors of Bξ, contradicting left separation.

F1F3F10step 3.2step 4.1step 4.2contradiction
6.1

Therefore no left-separated sequence of one fixed nonzero finite size can have pairwise-disjoint parts above one fixed countable ordinal.

step 3.2step 5.1
7.1

Fix 0<n<ω. If [ω1]n in the final Vietoris topology were not hereditarily separable, step 1.1 would give a left-separated sequence of n-element sets. By [F6], thin it to a Δ-system with finite root R and put γ=sup{ρ+1:ρR}, taking γ=0 when R=. The parts above γ are pairwise disjoint, contradicting step 6.1. Thus [ω1]n is hereditarily separable for every positive n.

F6F10step 1.1step 6.1
8.1

Fix 0<n<ω and suppose the final product (ω1,T~)n were not hereditarily separable. By step 1.1 choose a left-separated sequence of n-tuples and thin so its coordinate-equality pattern is fixed. Retain one representative of each of its m coordinate classes; intersecting the finitely many product coordinates belonging to one class shows that the resulting m-tuple sequence is still left separated. Using the coarser metric topology from step 1.3, choose pairwise closure-disjoint basic cells around the m distinct coordinates and thin, by second countability, until the cells are fixed. For each tuple intersect a final-product separating neighbourhood with those cells. The corresponding standard Vietoris neighbourhood then separates its underlying m-element set from all earlier such sets: disjoint cells force membership in the Vietoris neighbourhood to match coordinatewise membership in the product neighbourhood. This produces a left-separated sequence in [ω1]m, contradicting step 7.1.

F4F7F10step 1.1step 1.3step 7.1
9.1

Therefore every nonempty finite power is hereditarily separable, exactly as asserted. The zero power is excluded by [F8]; n=1 is included; empty standard neighbourhood families and empty Δ-roots were handled in steps 1.2 and 7.1. CH is used only in step 5.1 to capture the countable dense segment in a later model, while all other selections are the ZFC uses recorded by [F10].

F8F10step 5.1step 7.1step 8.1
TheoremStatement: Literature-sourcedProof: AI-adaptedjudge pass (gpt-5.6-terra)audited 2026-09-14Open item page →

CH implies that an S-space exists

Statement

ZFC plus the continuum hypothesis proves that there is a strong S-space.

Facts & Assumptions

Given: ZFC and CH.

[F1]

Cantor and Baire sequence spaces and coordinate codings gives Cantor space C=2ω its clopen cylinder topology; it is separable, has no isolated points, and the finite words form a countable cylinder base.

[F2]

Over ZFC, The continuum hypothesis, and what this page does not prove identifies the cardinality of P(ω), and hence of its characteristic-function copy 2ω, with 1.

[F3]

Ordered fundamental spaces and nice refinements defines ordered fundamental spaces, their strict clopen local bases, nice refinements, and the condition (α).

[F4]

Nice refinements exist and are regular but not Lindelof gives every ordered fundamental space a star-satisfying nice refinement that is regular and Hausdorff but not Lindelöf.

[F5]

Under CH, CH makes the nice refinement strongly hereditarily separable makes every nonempty finite power of such a refinement hereditarily separable.

[F7]

L-spaces, S-spaces, and strong S-spaces defines an S-space and a strong S-space and excludes the zeroth power from the latter definition.

[F8]

The Axiom of Choice supplies the ZFC well-orderings and bijections in the initial reindexing and propagates all choices made in [F4] and [F5].

Proof

technique · direct construction and assembly
1.1

Let DC consist of the binary sequences of finite support. Sending a finite support a to ka2k enumerates D bijectively by ω, and D meets every cylinder: extend the prescribed finite word by zeros. The map xyx, where yx(2k)=x(k) and yx(2k+1)=1, injects C into CD. Inclusion gives the reverse injection, so Cantor--Bernstein and [F2] give CD=C=1.

F1F2
2.1

Choose a bijection b:ω1C with b[ω]=D: use the enumeration from step 1.1 on ω and a bijection ω1ωCD on the complements. Pull the cylinder topology back along b. It is Hausdorff, zero-dimensional, separable, and second countable, with ω dense. Every nonempty open set contains a cylinder. For a word s, prefixing s defines a bijection from C onto its cylinder Ns, so every nonempty open set has size 1.

F1F2F8step 1.1
3.1

For α<ω1 and n<ω, put Wnα=b1[Nb(α)n]. Then W0α=ω1, each Wnα is clopen, and these sets form a local base at α. They are strictly decreasing because the next unrestricted bit can be changed, and their intersection is {α}. Consequently step 2.1 with these bases is a second-countable ordered fundamental space in the exact sense of [F3].

F1F3step 2.1
4.1

Apply [F4] to obtain a nice refinement X=(ω1,T~) satisfying every (α). The space X is regular and Hausdorff and is not Lindelöf.

F4step 3.1
5.1

Fix 0<n<ω. By [F5], Xn is hereditarily separable. By [F6], Xn is regular and Hausdorff.

F5F6step 4.1
5.2

The power Xn is not Lindelöf. Otherwise let U be an open cover of X with no countable subcover, supplied by step 4.1. The inverse images {π01[U]:UU} form an open cover of Xn. Lindelöfness would give countably many of them covering Xn. The projection π0:XnX is onto: fill all coordinates other than 0 with the fixed point 0ω1. Hence the corresponding countable members of U would cover X, a contradiction.

F4F6step 4.1contradiction
6.1

Steps 5.1 and 5.2 show that every positive finite power of X is regular, Hausdorff, hereditarily separable, and not Lindelöf. Thus every such power is an S-space, and [F7] says exactly that X is a strong S-space. The case n=1 is included, while n=0 is deliberately excluded. The construction is nonempty because its underlying set is ω1. Step 2.1 is the only new choice in this assembly; [F8] also propagates the ZFC choices in the two refinement suppliers.

F7F8step 2.1step 5.1step 5.2
DefinitionDefinition: Literature-sourcedProof: Not applicableaudited 2026-09-14Open item page →

The simple dichotomy for omega-one-generated ideals

Definition

Work in ZFC. Let S be uncountable. An ideal of countable subsets of S is a family I[S]ω that contains every finite subset of S and is closed under taking subsets and finite unions. For a,bS, write ab when ab is finite.

The ideal I is generated modulo finite by ω1 members if there are AξI for ξ<ω1 such that

aIu[ω1]<ω  aξuAξ

for every countable aS. This is equivalent to having an explicit family closed under finite unions: replace the displayed family by the sets ξuAξ for finite uω1. The resulting family has cardinality at most ω1 in ZFC; if an ω1-indexed family is desired, repeat members to pad the enumeration. Membership in I then means almost containment in one member of that family. No increasing sequence is asserted: an ideal need not contain the union of countably many of its members.

For XS:

  • X is inside I when [X]ωI;
  • X is outside, or orthogonal to, I when Xa<ω for every aI.

Equivalently, X is outside exactly when its intersection with every chosen generator is finite: one direction uses that generators belong to the ideal; the other uses the finite-union and finite-error formula above. Also IX={aX:aI} then consists only of finite sets.

The simple dichotomy for ω1-generated ideals is the assertion that for every such S and I, either some uncountable XS is inside I, or some uncountable XS is outside I. “Either” is inclusive: different witnesses can in principle satisfy the two clauses. One uncountable X cannot satisfy both in ZFC, because AC gives a countably infinite aX; inside gives aI, while outside says Xa=a is finite. This extraction of a is the only choice used in the definitional discussion. Empty and finite X are allowed by the two local predicates but are not witnesses to the dichotomy.

TheoremStatement: Literature-sourcedProof: AI-adaptedjudge pass (gpt-5.6-terra)audited 2026-09-14Open item page →

PFA implies the simple ideal dichotomy

Statement

The Proper Forcing Axiom proves both of Abraham's forms for every ideal I of countable subsets generated modulo finite by ω1 members:

  1. either the ground set is a countable union of sets inside I, or it has an uncountable subset outside I;
  2. either the ground set is a countable union of sets outside I, or it has an uncountable subset inside I.

Consequently PFA implies the simple dichotomy for every such ideal. No P-ideal hypothesis is assumed.

Facts & Assumptions

Given: ZFC plus PFA, an uncountable set S, and an ideal I on S generated modulo finite by Aξ:ξ<ω1.

[F1]

The simple dichotomy for omega-one-generated ideals gives the ideal, generation, inside, outside, restriction, and simple-dichotomy conventions.

[F2]

The Proper Forcing Axiom supplies a filter meeting any at-most ω1 family of dense subsets of a nonempty proper forcing.

[F3]

Properness may be proved by adding an (M,P)-master below every pMP; masterhood means that DM is predense below it for every dense DM (Master conditions and proper posets, Master-condition characterizations).

[F4]

Suitable countable elementary submodels exist (Countable elementary submodels and their collapses).

[F5]

Every ccc forcing is proper (Ccc and countably closed forcings are proper).

[F6]

Under AC, every uncountable family of finite sets has an uncountable Δ-system (Under choice, the uncountable Δ-system lemma for finite sets), a countable union of countable sets is countable (Countable unions of at most countable sets, assuming ACω), and 10=1 by infinite-cardinal absorption (Absorption: for cardinals κ,λ with κ infinite and λκ, κλ=κ, and κλ=κ when λ0).

[F7]

The Axiom of Choice supplies all model, enumeration, thinning, and witness selections below and is part of the ambient ZFC of PFA.

Proof

technique · direct forcing construction
1.1

Put T=ξ<ω1Aξ and R=ST. Generation modulo finite makes R outside I. AC chooses an enumeration of each countable Aξ, so T injects into ω1×ω and [F6] gives T1. If R is uncountable, it already supplies the outside branch of Form 1. Otherwise S1, and uncountability gives S=1; transport S,I, and the generators along a bijection with ω1. Thus, for the nontrivial Form-1 case, we may work on S=ω1.

F1F6F7given
2.1

Assume that S is not a countable union of sets inside I. Define P1 as follows. A condition p=(xp,dp,Np) has finite xp,dpω1 and a finite membership chain Np of countable elementary submodels of a fixed well-ordered expansion of H(2) containing I and the generator map. Require that whenever α<β are in xp, some NNp satisfies αN and βN, equivalently α<Nω1β; this is the meaning of “the models separate distinct points of xp.” If ηxp lies above Nω1 for NNp, then η belongs to no YN that is inside I. A stronger qp enlarges all three finite coordinates and, for each ξdp, freezes xqAξ=xpAξ.

F1F4F7step 1.1
3.1

For every γ<ω1, conditions putting a point above γ into xp are dense. Given p, append a countable model N containing p and γ, so xpN and γ<Nω1. The union of the countably many inside sets belonging to N cannot cover S by the assumption in step 2.1. A point outside that union is outside Nω1 because every singleton from N is an inside set in N; append that point to xp. For every ξ<ω1, the set of conditions with ξdp is dense by simply enlarging dp.

F1F4F7step 2.1
3.2

To prove properness, take a large countable MH(κ) containing P1 and a condition p0MP1. Append N=MH(2) to the side chain. Because every finite coordinate of p0 lies in M, this is a condition pp0. Fix rp and dense DM, and first strengthen r into D. The model N cuts the increasing enumeration xr={α0<<αk} after some αi; the lower part rM belongs to M.

F3F4F7step 2.1
4.1

Let EM be the set of (k+1)-tuples end-extending the x-coordinate of rM that occur as the x-coordinate of some condition in D extending that lower part. It contains (α0,,αk). We use the following fibre observation at each side model: if N is countable, bN avoids every inside set in N, aN, and H={z<ω1:φ(z,a)}N contains b, then H is not inside I; otherwise the condition's avoidance clause would exclude b. Starting at αk and moving down to αi+1, apply this observation to the definable successive fibres of E. The intervening side model contains E and all earlier coordinates but lies below the current coordinate. We obtain in M nested non-inside candidate sets Yi+1,,Yk such that every successive choice from them completes to a tuple in E.

F1step 2.1step 3.2
5.1

Put Z=ξdrAξI. At a candidate stage, Yj is not inside, so elementarity gives a countable CjM with CjYj and CjI. Since ZI, choose ajCjZ; countability of CjM gives CjM. Recursing through the nested fibres gives a tuple in EM and hence qDM extending rM, with every new xq-point outside Z. The union of q and r is a condition: their model chains merge through N; upper points of r avoid every inside generator named by dqM; and the replacement points of q avoid every generator named by dr. These last two facts verify both directions of the freezing requirement. Thus q is compatible with r.

F1F3F7step 3.2step 4.1
6.1

Step 5.1 says that p is an (M,P1)-master, so [F3] makes P1 proper. Apply PFA to the dense sets in step 3.1. For the resulting filter G, let X=pGxp. It is unbounded, hence uncountable. For each generator Aξ, a condition in G puts ξ into its finite d-coordinate, after which directedness and freezing show that XAξ is exactly that condition's finite intersection. By [F1], X is outside I. Together with the alternative excluded in step 2.1 and the reduction in step 1.1, this proves Form 1.

F1F2F3step 1.1step 2.1step 3.1step 5.1
7.1

Now suppose there is no uncountable set inside I. For every uncountable YS, apply Form 1 to IY. Its countable-union branch would make some inside piece uncountable by [F6], contrary to the supposition. Hence every uncountable YS contains an uncountable subset outside I.

F1F6F7step 6.1
8.1

Retain T and R from step 1.1. The set R is outside. If T is countable, partition it into singletons, which are outside, and add R as one more piece; this proves the countable outside decomposition. Assume henceforth that T is uncountable. Then T=1 by [F6].

F1F6step 1.1step 7.1
9.1

On T define P2 to consist of pairs (fp,dp) with fp:Tω finite and dpω1 finite. Put qp when q extends both coordinates and, for every ξdp and every nran(fp), fq1{n}Aξ=fp1{n}Aξ. Thus a recorded generator freezes every colour already present, while a new colour may be introduced once.

F1step 7.1step 8.1
10.1

The forcing P2 is ccc. Given uncountably many conditions, apply [F6] to their function domains and d-coordinates, thin to fixed finite sizes and common roots, and make all functions agree on the domain root. Enumerate the disjoint domain petals in a fixed order. Repeatedly use step 7.1 so that, for each petal coordinate, its uncountable set of values is outside I. Their finite union O is outside. For each remaining condition pη, the set Bη=OξdpηAξ is finite. Thin the finite Bη to a Δ-system. Its root meets at most one disjoint domain petal, while its disjoint petals and the domain petals each meet only finitely many petals of the other family. Hence choose distinct η,ζ with each condition's domain petal disjoint from the other's B-set. The coordinatewise unions of their functions and side sets then satisfy both freezing clauses and form a common extension.

F1F6F7step 7.1step 9.1
10.2

The following sets are dense in P2: conditions deciding a specified tT, conditions placing a specified ξ<ω1 into dp, and conditions whose function range contains a specified n<ω. For the first or third demand, if necessary assign a new point a colour not yet in the finite range (the specified n itself when it is absent); this cannot violate a freeze, which only mentions old colours.

step 9.1
11.1

By steps 10.1 and [F5], P2 is proper. PFA applied to the at-most-ω1 dense sets of step 10.2 gives a filter whose union is a total f:Tω. Fix n and ξ. Directedness combines a condition recording ξ with one already using colour n; below their common extension that intersection is frozen. Consequently f1{n}Aξ is finite. Each colour class is outside I by [F1], so these classes, together with R, form a countable outside decomposition of S. This proves Form 2 under the no-inside hypothesis; its other branch is precisely an uncountable inside set.

F1F2F5step 8.1step 10.1step 10.2
12.1

Finally, Form 1 alone yields the simple dichotomy: its outside branch is already a witness, while in its countable-union branch [F6] makes at least one inside piece uncountable. Form 2 gives the symmetric conclusion as well. Empty finite coordinates, empty roots, a generator-free T, and new colours were handled in steps 1.1, 8.1, 9.1, and 10.2. All model, thinning, enumeration, and witness choices are the AC uses recorded by [F7].

F1F6F7step 6.1step 11.1
LemmaStatement: Literature-sourcedProof: AI-adaptedjudge pass (gpt-5.6-terra)audited 2026-09-14Open item page →

A non-hereditarily-Lindelof regular space yields an ideal witness

Statement

Let X be a regular Hausdorff space that is not hereditarily Lindelöf. Then X has a right-separated subspace S={xα:α<ω1} and open sets UαS such that

xαUαUα,S{xξ:ξα}.

The countable closed sets Cα=Uα,S generate modulo finite an ω1-generated ideal I of countable subsets of S. Every uncountable subset of S inside I is nonseparable, and every uncountable subset outside I is discrete and hence nonseparable.

Facts & Assumptions

Given: ZFC and the space X in the statement.

[F1]

L-spaces, S-spaces, and strong S-spaces gives hereditary Lindelöfness and separability their all-subspaces meanings.

[F4]

The simple dichotomy for omega-one-generated ideals defines generation modulo finite and the inside and outside predicates.

[F5]

The Axiom of Choice supplies the length-ω1 recursive choices, the chosen cover members, and countable enumerations. Hausdorffness supplies closed singletons, so removing finitely many points preserves openness.

Proof

technique · direct construction
1.1

By [F1], some subspace YX has an open cover V with no countable subcover. Recursively for α<ω1, the earlier chosen VξV do not cover Y, so choose xαYξ<αVξ and then choose VαV containing xα. This also makes the xα distinct.

F1F5given
2.1

Put S={xα:α<ω1}. If β>α, construction gives xβVα. Hence VαS is a neighbourhood of xα contained in the initial segment Sα={xξ:ξα}. The union of these neighbourhoods for ξα shows that every Sα is open in S, so S is right-separated.

step 1.1
3.1

By [F2], S is regular and Hausdorff. Apply [F3] inside S to xαSα: choose open Uα with xαUαCα=Uα,SSα. The set Cα is closed in S and countable because α<ω1.

F2F3F5step 2.1
4.1

Let I be the ideal generated modulo finite by the Cα. Explicitly, a countable aS lies in I exactly when aαuCα for some finite uω1. The defining family consists of ω1 countable members, and the formula is downward closed, closed under finite unions, and contains every finite set.

F4step 3.1
5.1

Let DS be uncountable and inside I, and let ED be countable. By inside-ness and step 4.1, EK=αuCαF for some finite u and finite FS. The set K is countable and closed in the Hausdorff space S: the Cα are closed and the finite set F is closed. Choose dDK. Then the nonempty open subset DK of D misses E, so E is not dense in D. Since this holds for every countable E, the space D is nonseparable.

F4F5step 3.1step 4.1
5.2

Let instead DS be uncountable and outside I. For xαD, outside-ness gives DCα finite. Remove from Uα the finite closed set (DCα){xα}. The result is an open neighbourhood in S whose intersection with D is exactly {xα}, so D is discrete. Every dense subset of a discrete space is the whole space; because D is uncountable, it is nonseparable.

F4F5step 3.1step 4.1
6.1

Steps 1.1–4.1 give the promised right-separated sequence, closed neighbourhoods, and generated ideal, while steps 5.1 and 5.2 prove both nonseparability conclusions. The construction starts at α=0 with no earlier cover members; every Sα and Cα is nonempty because it contains xα; finite generator lists and finite errors may be empty; and all nonempty recursive selections are the uses of AC recorded in [F5].

F5step 1.1step 2.1step 3.1step 4.1step 5.1step 5.2
TheoremStatement: Literature-sourcedProof: AI-adaptedjudge pass (gpt-5.6-terra)audited 2026-09-14Open item page →

PFA implies there are no S-spaces

Statement

Under PFA, every regular Hausdorff hereditarily separable space is hereditarily Lindelöf. Consequently no S-space exists.

Facts & Assumptions

Given: ZFC plus PFA and a regular Hausdorff hereditarily separable space X.

[F1]

A non-hereditarily-Lindelof regular space yields an ideal witness turns failure of hereditary Lindelöfness into a right-separated subspace S, an ω1-generated ideal I, and proves that every uncountable inside or outside witness is a nonseparable subspace.

[F2]

PFA gives an uncountable inside or outside witness for every such ideal (PFA implies the simple ideal dichotomy).

[F3]

L-spaces, S-spaces, and strong S-spaces defines hereditary separability and hereditary Lindelöfness over all subspaces, and defines an S-space as regular Hausdorff, hereditarily separable, and not Lindelöf.

[F4]

The Axiom of Choice is the ambient axiom used by both witness suppliers; this assembly makes no additional selection.

Proof

technique · contradiction
1.1

Assume for contradiction that X is not hereditarily Lindelöf. By [F1] it has a subspace S and an ω1-generated ideal I of countable subsets of S with the stated witness properties.

F1F3assume-contra
2.1

By [F2], some uncountable DS is inside or outside I. In either case [F1] says that D, with its subspace topology, is nonseparable.

F1F2step 1.1
3.1

But D is also a subspace of X, so hereditary separability of X says that D is separable, contradicting step 2.1. Therefore X is hereditarily Lindelöf.

F3step 2.1contradiction
4.1

If an S-space existed, [F3] would make it regular Hausdorff and hereditarily separable, so step 3.1 would make it hereditarily Lindelöf and hence Lindelöf. This contradicts the defining non-Lindelöf clause. Thus no S-space exists under PFA. No empty or singleton space can be an S-space because both are Lindelöf; the uncountable witness in step 2.1 is nonempty; and [F4] propagates the exact AC uses of [F1] and [F2].

F3F4step 3.1discharge-contradiction
CorollaryStatement: Literature-sourcedProof: AI-adaptedjudge pass (gpt-5.6-terra)audited 2026-09-14Open item page →

A supercompact gives the relative consistency of no S-spaces

Statement

For fixed effective presentations and arithmetizations,

Con(ZFC+there is a supercompact cardinal)  Con(ZFC+there are no S-spaces).

This is a formal relative-consistency implication. It neither extracts a transitive model from consistency nor asserts PFA in ZFC.

Facts & Assumptions

Given: The fixed effective theory presentations and arithmetic base used by the formal supercompact-to-PFA supplier.

[F1]

Formal consistency of PFA from a supercompact supplies, for these presentations, the formal implication Con(ZFC+a supercompact)Con(ZFC+PFA) without a countable-transitive- model inference.

[F2]

PFA implies there are no S-spaces: ZFC+PFA proves the sentence asserting that there are no S-spaces.

[F3]

Finite support, weakening, and composition of derivations: Fixed finite derivations may be concatenated after proved sentence premises are replaced by their proofs, with line references shifted accordingly.

[F4]

Primitive-recursive syntax and certified proof checking supplies verified proof parsing, concatenation, line renumbering, and malformed-input defaults.

[F5]

Primitive-recursive functions are representable in Q: Every true or false standard instance of the primitive-recursive certified-proof checker has the corresponding finite numeral proof in PA.

[F6]

Formal consistency transfer from a verified reduction turns a verified total reduction of contradiction certificates into the corresponding formal consistency implication.

[F7]

Fine measures, strong compactness and supercompactness fixes the supercompactness assertion in the source theory. No new large-cardinal property is inferred here.

Proof

technique · direct
1.1

Let TP be ZFC+PFA and let TN be ZFC plus the sentence that there are no S-spaces. Expand the fixed finite mathematical derivation underlying F2 in the chosen calculus: expand its displayed definitions and abbreviations, and replace every invoked proved premise by its fixed derivation. F3 shows that the resulting finite concatenation is a TP-derivation of the extra axiom of TN. Fix its standard code e. The checker from F4 accepts this particular numeral, and F5 supplies a finite PA proof of that positive closed checker instance. Thus both e and PA's verification of e are constructed here; neither is attributed to F2's interface.

F2F3F4F5Given
2.1

Given a purported TN-refutation p, use F4 to check it and to replace each use of the no-S-space axiom by a renamed copy of e. Retain the ZFC axiom lines and append the same logical inferences. This yields a TP-refutation r(p). The construction is a bounded syntactic substitution into the finite code p, with a fixed default on malformed inputs, so the arithmetic base combines the fixed positive checker proof from step 1.1 with induction on the decoded line list to verify that r is total and that PrfTN(p,)PrfTP(r(p),).

F4F5step 1.1
3.1

Apply [F6] to the reduction in step 2.1. The arithmetic base proves Con(TP)Con(TN). Compose this implication with [F1] to obtain the displayed result.

F1F6step 2.1
4.1

The source theory's large-cardinal clause is exactly the one fixed by [F7]. The argument only transforms finite proof codes: it does not choose a generic filter, construct a model of the whole source theory, or infer a transitive model from its consistency. Empty spaces and singleton spaces need no special consistency argument—[F2]'s no-S-space theorem already treats the complete definition—and no converse implication is asserted.

F2F7step 3.1
TheoremStatement: AI-adaptedProof: AI-adaptedjudge pass (gpt-5.6-terra)audited 2026-09-14Open item page →

L-space and S-space existence is asymmetric

Statement

The L- and S-space existence results have the following asymmetric status.

  1. ZFC proves that an L-space exists.
  2. ZFC+CH proves that a strong S-space, hence an S-space, exists; ZFC+V=L also proves this through V=LCH.
  3. ZFC+PFA proves that no S-space exists.

These are separate branches, not simultaneous conclusions. Moreover, relative to the consistency of ZFC plus a supercompact cardinal, existence of an S-space is not a theorem of ZFC. The last qualification is a relative-consistency claim, not an unqualified proof in ZFC of PFA or of its own consistency.

Facts & Assumptions

Given: The named theories are read in separate branches. ZFC includes AC; no branch inherits CH, V=L, or PFA from another branch.

[F1]

A ZFC L-space constructs an L-space in ZFC.

[F2]

CH implies that an S-space exists constructs a strong S-space in ZFC+CH, and hence an S-space by the definition it cites.

[F3]

V equals L implies diamond proves in ZF that V=L implies on ω1.

[F4]

Diamond implies CH proves in ZFC that implies CH.

[F5]

PFA implies there are no S-spaces proves in ZFC+PFA that no S-space exists.

[F6]

A supercompact gives the relative consistency of no S-spaces supplies the qualified formal consistency implication from ZFC plus a supercompact to ZFC plus no S-spaces.

[F7]

The Axiom of Choice is part of every ZFC branch and supplies the AC used by [F1], [F2], [F4], and [F5]. This assembly makes no additional choice.

Proof

technique · direct branchwise assembly
1.1

In the ZFC branch, apply [F1]. It gives the required L-space without CH, V=L, PFA, or a large cardinal.

F1Given
1.2

In the ZFC+CH branch, [F2] gives a strong S-space and therefore an S-space. This conclusion uses CH and is not transferred to the other branches.

F2Given
1.3

In the ZFC+V=L branch, [F3] gives ; since this branch includes AC, [F4] gives CH; and then [F2] gives a strong S-space.

F2F3F4F7Given
1.4

In the ZFC+PFA branch, [F5] says that no S-space exists. This is incompatible with the conclusions of steps 1.2 and 1.3, so those hypotheses are not conjoined.

F5Given
2.1

For the final metatheoretic qualification, assume Con(ZFC+a supercompact). Then [F6] gives Con(ZFC+no S-spaces). If ZFC proved that an S-space exists, appending that fixed proof to the latter theory would refute it, contrary to its consistency. Thus, under the displayed source-consistency assumption, S-space existence is not a ZFC theorem.

F6step 1.4assume-hyp
3.1

Steps 1.1--2.1 establish exactly the three branchwise assertions and the qualified asymmetry. Empty or singleton spaces do not create an exception: [F1] has underlying set ω1, [F2] likewise produces a nonempty strong S-space, and [F5] applies to the complete definition. The first power in [F2] supplies the ordinary S-space; the zeroth power is excluded by definition. All uses of AC are declared in [F7], and no converse consistency implication is claimed.

F1F2F5F7step 1.1step 1.2step 1.3step 1.4step 2.1

5 · Examples, counterexamples and false statements

None yet.

Sources