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
- Arithmetization, Incompleteness, and Relative Consistency
- Binary Operations, Monoids, Groups and Subgroups
- Boolean Algebras, Stone Duality, and the Prime Ideal Theorem
- Borel and Analytic Sets, Perfect Sets, and Determinacy
- Cardinal Arithmetic, Cofinality and the Alephs
- Club, Stationary Sets, and Pressing Down
- Compactness
- Compactness in Metric Spaces
- Complete Metrizability, Čech-Completeness, and Baire Category
- Completeness, Completion, and Uniform Continuity
- Condensation, GCH, and Diamond in L
- Congruences, the Integers Modulo n and the Chinese Remainder Theorem
- Construction of the Natural Numbers
- Construction of the Real Numbers via Cauchy Sequences
- Construction of the Real Numbers via Dedekind Cuts
- Countability and Uncountability
- Countability Axioms and Cardinal Functions
- Deduction, Soundness, Completeness, and Compactness
- Divisibility, Greatest Common Divisors and Bézout's Identity
- Filters and Ultrafilters
- Finite Counting, Factorials and Binomial Coefficients
- Finite-Support Iterations and Martin's Axiom
- Forcing Orders, Names, and Generic Extensions
- Formal Set-Theoretic Syntax, Structures, and Satisfaction
- Foundations of the Real Numbers for Analysis
- Hereditary and Productive Behaviour of the Separation Axioms
- Large Cardinals, Measures, and Elementary Embeddings
- Metric Spaces
- Metrization: Urysohn, Nagata–Smirnov, Bing, Smirnov
- Monotone Sequences, Bolzano-Weierstrass, and Cauchy Completeness
- Order, Zorn's Lemma, and the Axiom of Choice
- Ordinal Arithmetic and the First Uncountable Ordinal
- Ordinals, Cardinals, and Transfinite Recursion
- Preservation, Cohen Forcing, and the Continuum
- Primes, Euclid's Lemma and the Fundamental Theorem of Arithmetic
- Proper Forcing, Countable-Support Iterations, and PFA
- Reflection, Absoluteness, and Elementary Submodels
- Relations, Functions, and Quotients
- Roots, Rational Powers, and Classical Inequalities
- Separation Axioms: the Hierarchy
- Sequences and Limits
- Set-Theoretic Trees, Delta Systems, and Diamond
- Subspaces, Products, and Quotients
- Suprema and Infima
- The Arithmetical Hierarchy and Post's Theorem
- The Cantor Set, Baire Category, and Measure Zero in ℝ
- The Constructible Hierarchy and Inner Models
- The Forcing Theorem and Formal Consistency Transfer
- The ZFC Axioms and the Basic Set Constructions
- Topological Spaces and Continuity
- Topology of ℝ
- Urysohn's Lemma and the Tietze Extension Theorem
- Well-Founded Relations, Rank, and the Cumulative Hierarchy
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 -sequence on 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 . 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 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, , 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
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 under the conventions of Regular spaces and spaces, with the source disagreement over whether regularity includes 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 , or that use PFA or CH in ZFC, declare those axioms at the point of use.
C-sequences and the upper and lower traces of minimal walks on omega-one
Definition
Work in ZFC. A locally finite -sequence on is a sequence such that
- ;
- if , then is cofinal in ;
- is finite whenever ; and
- whenever .
At a successor one may and shall take , read as when . At a nonzero countable limit , choose a strictly increasing cofinal -sequence and adjoin . The choice, simultaneously for all limit , is the use of The Axiom of Choice in this definition; the definitions made from a fixed -sequence use no further choice.
Fix such a sequence. For , the minimal walk from down to is the finite decreasing sequence
where, as long as ,
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 . 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 and the walk is well defined.
Its upper trace is
with . For put
The union in the first line is a nonempty finite set: it contains , and it is a finite union of finite initial intersections. The lower trace is
listed in its inherited nondecreasing order when multiplicities along the walk matter. Equivalently, with and for ,
here an ordinal is the set of its predecessors, so subtraction discards earlier values below the new running maximum. The explicit convention avoids the undefined expression and gives for .
For finite sets of ordinals, means that every member of is below every member of . This convention will be used in the concatenation statements below; it is not the comparison of their cardinalities.
Concatenation and limit control for minimal-walk traces
Statement
Fix the locally finite -sequence of C-sequences and the upper and lower traces of minimal walks on omega-one.
- If and , then and 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.
- If is a nonzero limit ordinal, then Explicitly, for every there is such that implies .
The second assertion has the limit ordinal as the upper endpoint. It does not assert the generally false fixed- limit when .
Facts & Assumptions
Given: The fixed normalized -sequence and the trace conventions in the statement.
C-sequences and the upper and lower traces of minimal walks on omega-one defines the walk by least points of at or above the target, and defines the lower trace by the successive running maxima of the finite sets .
Proof
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 .
Let be a nonzero limit and . The first lower-trace value for the walk from to is , and all later values are running maxima containing that first intersection. Hence . The same equality is harmless at under the explicit zero convention, although limits only concern a final tail.
Every member of is below , so the separation hypothesis puts every member of below . If is a node of , the running maximum that records occurs in or is bounded by a later recorded maximum. Thus , and therefore . In particular has no point in , so .
Given , cofinality of gives with . Since is a limit, . Whenever , one has , and step 1.2 gives . This is exactly the ordinal-limit assertion in clause 2.
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.
Along the first segment, step 2.1 identifies every initial intersection and hence every running maximum with the corresponding value in . All those values are below every value of . Consequently, after the walk reaches , taking running maxima for the continued walk produces exactly the values of ; no earlier value suppresses or changes one. The lower trace is therefore the ordered union .
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.
Minimal-walk weights, labelled lower traces, and the functions e-beta
Definition
Work in ZFC and retain the fixed -sequence and traces from C-sequences and the upper and lower traces of minimal walks on omega-one. Write for Cantor space and 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 into countably many stationary sets and fix a sequence in which every member of occurs on a stationary set. Cantor's theorem Cantor's theorem: , together with AC's comparison of cardinals, gives an injection ; fix pairwise distinct . 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
For let be the least with . The labelled lower trace
is defined by . Thus the label at a repeated running maximum is the label from its first occurrence. For , its evaluated form is the integer-valued function
On the diagonal, is the empty function. In recursive language, the new minimum of the lower trace receives label , 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 ,
For , the maximal weight is
This is a natural number because the trace and every displayed intersection are finite. Equivalently, if , then
Finally define
The terms “coherent” and “finite-to-one” are conclusions of the next lemma, not assumptions smuggled into this definition.
The minimal-walk functions are coherent and finite-to-one
Statement
For every , the function is finite-to-one. If , then
is finite. Thus is coherent on the common domains of its members.
Facts & Assumptions
Given: Ordinals and the fixed minimal-walk data.
Minimal-walk weights, labelled lower traces, and the functions e-beta identifies with the maximum of the finite local weights over .
Concatenation and limit control for minimal-walk traces proves trace concatenation once the finite initial intersections above the splice have stabilized.
Proof
Fix and set . We prove that has no limit point at or below .
Let be a limit ordinal. The two traces and are finite. Local finiteness makes each finite for a trace node . Choose above every member of all these intersections, and let be the maximum of and their finitely many cardinalities. Cofinality of permits enlarging so that whenever .
For , no trace node above has a -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 , whereas the lower segment contains the weight .
Taking the maxima in [F1] therefore gives for every . Such is not in , so is not a limit point of . Zero and successor ordinals are not limit points from below, so has no limit point at or below .
If were infinite, its well-order would recursively give a strictly increasing -sequence from . Its supremum is a nonzero limit ordinal and every final segment below meets , contradicting step 3.1. Hence is finite.
The set lies in , so every fiber of is finite. Taking, for example, , the disagreement set between and also lies in and is finite.
Step 5.1 proves finite-to-one behavior and coherence simultaneously. It also covers , where the domain and disagreement set are empty, and , where disagreement is empty.
Oscillation on lower traces and Moore's modular colouring
Definition
Let be a finite set of ordinals in increasing order and let . For a nonminimum , write for its immediate predecessor in . The oscillation set of and on is
If is empty, this set is empty without evaluating ; if is a singleton, it is empty because there is no predecessor. For , define
Both restrictions are defined because , 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:
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 is excluded, so reduction modulo zero never occurs; for its contribution is zero.
Enumerate the primes increasingly as . Define by and, for ,
The minimum exists because a positive integer has only finitely many prime divisors. Put
This transform can take values larger than . The binary colouring used by the topology is defined later as ; the finite-pattern theorem controls both maps but does not conflate them.
Moore's club extension lemma
Statement
Let , and let and be uncountable pairwise-disjoint families. Regard each member as its increasing enumeration, and write for , and similarly for .
For functions with ordinal domains, put
There is a club such that, whenever , , , and , there are , , and one nonempty finite set , independent of , for which every and satisfy:
- every is below both and ;
- and ;
- for ;
- is the restriction of to ; and
- .
This formulation of clause 1 also covers , when the old lower trace is empty. Pairwise disjointness is required within each family; no disjointness between an -member and a -member is asserted.
Facts & Assumptions
Given: ZFC, the fixed minimal-walk data, positive , and families as in the statement.
The minimal-walk functions are coherent and finite-to-one says that the are finite-to-one and pairwise coherent on common domains.
Concatenation and limit control for minimal-walk traces gives lower trace concatenation under separation and makes tend to a limit .
Minimal-walk weights, labelled lower traces, and the functions e-beta defines the labelled trace , fixes the bookkeeping sequence , and proves the first-label law
Countable elementary submodels and their collapses supplies countable elementary submodels containing any specified countable parameter set; its proof uses The Axiom of Choice.
Closed unbounded subsets of ordinals gives the closed-unbounded convention.
Proof
Fix a sufficiently large regular and Skolem functions for . The ordinals obtained from countable containing 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 and put . Notice that every is below , while .
Suppose first that is equality, and fix , . By coherence in [F1], there is above every and above all disagreements below among the finitely many pairs . Hence whenever . By the limit clause of [F2], choose so that implies .
We repeatedly use the following reflection observation. If belongs to and , then is uncountable: otherwise elementarity provides in an enumeration of by , whence and , a contradiction. Thus is unbounded in . Likewise, an uncountable has unbounded in , by elementarity applied to arbitrarily large members of .
For the strict branch, let be the set of limit with the following property: for every , , , , and finite , some satisfies and for every and . This set is definable from and the fixed sequence, so .
Let consist of those for which some and simultaneously preserve each and below , agree coordinatewise on , satisfy and for , and satisfy for every . All parameters in this definition belong to . The space is countable and belongs to , so . Each and labelled trace is finite with ordinal entries below and labels in that countable space, hence is an element of . Finally the restrictions of the -functions below are finite modifications, by [F1], of restrictions coded in . Thus without using either or itself as a parameter. Taking , , and shows ; the trace and label requirements are [F2] and the first-label clause retained in [F3]. By step 2.1 choose above , with witnesses .
The cut belongs to . Indeed, for given data at , finite-to-one behavior lets us enlarge above every at which some . The restriction tuple belongs to by coherence. The definable set of ordinals for which some has these restrictions and has all values above on belongs to and contains with witness . Step 2.1 makes it unbounded, so choose such above and (with no maximum needed when is empty). Its witness proves the defining demand. Hence , and step 2.1 also makes uncountable.
Put . It is nonempty because . Its minimum exceeds , and [F2] splices it above the common old trace . Preservation below gives the two strict bounds; agreement on gives clause 3. The equality of the old labelled traces gives clause 4, and the label at the new minimum is , giving clause 5. Thus all five conclusions hold in the equality branch.
Fix and . Choose above every old trace , 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 such that the -restrictions below agree, with first label for , and .
Put and let be the maximum of the finitely many values for and . Apply the defining property of with , a bound above every old trace, , and . It gives preserving every on the old trace and satisfying on . The preservation of below , 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.
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 , so it is the required . No choice is used after selecting the Skolem functions and fixed data; those ZFC selections are precisely the declared AC dependency.
The oscillation block lemma
Statement
Let , let and be uncountable pairwise-disjoint families, and let . There is a sequence in such that, for every , some and ordinals satisfy, for all , , and :
- , meaning for every ;
- is the disjoint union
- is the restriction of to ; and
- whenever .
For 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 , uncountable pairwise-disjoint , and .
Moore's club extension lemma supplies, at every cut in one club, an equality or strict-comparison extension with exact trace and label preservation.
Oscillation on lower traces and Moore's modular colouring defines oscillations as the adjacent changes from to .
Minimal-walk weights, labelled lower traces, and the functions e-beta makes stationary and defines the labelled traces.
The minimal-walk functions are coherent and finite-to-one says that every pair of -functions has only finitely many disagreements on its common domain.
Concatenation and limit control for minimal-walk traces supplies the separated trace splice and the limit law .
Countable elementary submodels and their collapses and The Axiom of Choice supply the elementary-model selection used below.
A stationary subset of meets every club, and the intersection of finitely many clubs is club. The club filter and nonstationary ideal
Proof
Fix Skolem functions for a sufficiently large . The cuts of countable elementary Skolem hulls containing the fixed parameters form a club : larger countable ordinal parameter sets give unboundedly many cuts, and unions of increasing -chains give closure. Intersect with the club supplied by F1. By F3 and F7 this intersection meets the stationary set . Choose whose cut is such a point. This is the sole model-selection use of AC.
Choose initial and 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 . The appended nonempty block is the final part of every , and F1 makes the comparison strict on that block. Hence for all .
Suppose have been chosen, the previously marked points lie below both first-disagreement bounds to the next stage, and the last point of has for every . Apply [F1] first with equality, producing a common nonempty block on which the new -values agree, and then to that output with strict inequality, producing a common nonempty block on which the next -values exceed the next -values. Put . The two trace splices give , independently of , and both new minima have label .
On the old trace, the first-disagreement bounds preserve every comparison. At the first point of the previous comparison is strict and the new comparison is equality, so [F2] creates no downward crossing. Comparisons remain equality through that block. At , equality at its predecessor changes to strict , so exactly is added to every coordinatewise oscillation set; the comparison stays strict through , so no other new crossing appears. Label restriction in [F1] preserves all old marked labels and assigns to .
Finite induction therefore produces sequences above and increasing 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 at every marked point.
Fix . By [F4], choose above every and every disagreement below between and for . Put . For each , the restriction belongs to : the corresponding restriction of belongs to , and [F4] says that is a finite modification of it. Hence belongs to . It contains , so it is uncountable; if it were countable, an enumeration in would put every member of in .
By the limit law in [F5], choose such that implies . Since is an uncountable pairwise-disjoint family and is countable, some member of has all coordinates above ; this assertion has parameters in , so elementarity gives such an . Thus , , and the definition of gives for every . Since every lies above , one also has for all .
The inequalities in step 7.1 let [F5] splice every trace through , and [F3] gives the corresponding labelled splice . On the functions do not depend on , by the choice of ; on , 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 the same reflection chooses and all unions over marked points are empty.
Since the recursively chosen sequence is fixed before is specified, step 8.1 proves the required quantifier order. No coordinate assignment was introduced: the conclusion holds for all simultaneously.
The Moore colouring realizes finite binary patterns
Statement
Define and the binary colouring
Let , and let and be uncountable pairwise-disjoint families. For every and , some and satisfy and
for all . The same pair has ; consequently realizes every prescribed binary function on the graph .
This is a functional-coordinate pattern. It does not assert simultaneous realization of an arbitrary binary matrix on all of .
Facts & Assumptions
Given: ZFC, positive , uncountable pairwise-disjoint , and maps , .
The oscillation block lemma supplies arbitrarily long common oscillation blocks whose new points all receive one prescribed continuous label .
Oscillation on lower traces and Moore's modular colouring defines , the least-nondividing-prime transform , and the evaluated labels.
Minimal-walk weights, labelled lower traces, and the functions e-beta supplies the fixed pairwise-distinct Cantor points used to evaluate the labels.
Chinese remainder theorem for a finite pairwise-coprime list: simultaneous residues determine one class modulo the product, and the resulting bijection preserves addition and multiplication solves a finite system of congruences with pairwise-coprime positive moduli, including its empty-list convention.
The Axiom of Choice implies that a countable union of countable sets is countable and supports the uncountable thinning used below.
Proof
Choose distinct primes for . For every , the finitely many distinct Cantor points supplied by F3 have pairwise-disjoint clopen neighborhoods, so some continuous satisfies for all . There are only countably many continuous integer-valued maps on Cantor space. By F5, one value occurs for an uncountable subfamily; replace by that subfamily.
Put and . Apply [F1] with this and block length . It gives , members , and marked points such that, relative to , the evaluated label occurs exactly additional times in the oscillation set for , while every other evaluated-label count is unchanged.
For each , let and . For put , and set . The sum has finite support by F2. The primes are pairwise coprime, so F4 gives a residue modulo satisfying for every . Choose its representative and put . The right-hand side lies between and , hence is already its least nonnegative residue modulo .
Fix . The block count from step 2.1 and the definition of give an integer such that . If , this number is odd, so the least prime not dividing it is . If , it is even but is congruent to modulo , so the least prime not dividing it is . Thus [F2] gives .
The same displayed formula is odd exactly when , so . Given a desired binary pattern for , apply the proved assertion with . 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.
Positivity of 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.
Moore's clopen-generated topology
Definition
Retain the binary colouring from The Moore colouring realizes finite binary patterns. For , put
For , let be the topology on generated by declaring clopen for every . Equivalently, finite intersections of sets and , with , form a clopen base. The empty intersection is ; when is empty this gives its unique topology.
There is a useful product representation with no extra generators. Let be the unit circle and define
by
For , the inverse images of the two coordinate values are and its complement; for , the coordinate is constant. Thus the product-induced topology is exactly . If are in , then while , so the -coordinate separates their images. Hence is injective and is an embedding onto its image.
The family is point-countable and point-separating: if , then , and the countable ordinal has only countably many members. The displayed clopen base and point separation make every zero-dimensional Hausdorff, hence regular under the library convention.
Coordinates outside were deliberately padded by the constant . Allowing membership in at such a coordinate would add subbasic sets that Moore did not put into .
Every uncountable Moore subspace is nonseparable
Statement
If is uncountable, then is not separable.
Facts & Assumptions
Given: An uncountable .
Moore's clopen-generated topology says that is clopen, contains , and contains no ordinal below .
Separability: the existence of an at most countable dense subset says that a space is separable when it has a countable dense subset.
Proof
Let be countable. Its supremum is a countable ordinal, so uncountability of gives with .
By [F1], is an open neighborhood of and every one of its points is at least . Hence it is disjoint from , so is not dense.
Since every countable fails to be dense, [F2] proves that is nonseparable. The assertion deliberately excludes countable ; for or a singleton the displayed argument has no above and no nonseparability conclusion is claimed.
The Moore colouring forbids cross-injections
Statement
In ZFC, if have countable intersection, then no uncountable subspace of admits a continuous injection into .
Facts & Assumptions
Given: ZFC and with countable.
Moore's clopen-generated topology gives a clopen finite-Boolean base and iff either or and .
The Moore colouring realizes finite binary patterns realizes every binary pattern on the graph of a finite coordinate map.
Under choice, the uncountable -system lemma for finite sets gives an uncountable -subfamily of any uncountable family of finite supports.
The Axiom of Choice supports the simultaneous neighborhood choices and the finite/countable thinning steps.
Proof
Suppose is continuous and injective for an uncountable . Delete the countable sets and . After this deletion, every remaining and are distinct and lie on opposite sides of and . One of the two orientations or holds on an uncountable subfamily; retain it.
For each retained , continuity at and the neighborhood of give a basic clopen with . Encode by a finite support and its membership-bit function. Add to the support if necessary.
Apply F3 and then finite/countable pigeonhole thinning so that the form a -system with root , all petals have one size , the membership bits on the fixed root have one fixed vector, the membership bits on the increasingly enumerated petals have one fixed vector , the root lies below every retained , and the order type of each petal together with is constant. These are separate finite thinnings: agreement of the petal pattern alone would not control the root coordinates. Because is countable and the petals are disjoint, discard the countably many petals meeting . The families and are therefore uncountable, fixed-size, and pairwise disjoint.
Enumerate each member of and increasingly. The uniform order types give an insertion coordinate for in the first enumeration, a column occupied by in the second, and the other column occupied by . Define by and for . Define the desired bit at row to be , and at every other row to be the corresponding petal bit from .
By [F2], choose and with that realize these bits. Let and . At the inserted row, , and ensures ; hence .
At every petal row, the realized bit says that satisfies the corresponding petal literal in the finite Boolean condition defining . At every root row, the separately stabilized root vector has the same value for and ; since and the root lies below , F1 translates each root membership into precisely that fixed colouring bit. Thus every root and petal literal defining holds at , so .
The containment chosen in step 2.1 now gives , 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 . Hence no such continuous injection exists.
Moore's topology is hereditarily Lindelof
Statement
For every , the space is hereditarily Lindelöf.
Facts & Assumptions
Given: and the Moore topology.
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.
Moore's clopen-generated topology gives a clopen base of finite Boolean conditions in the sets .
Under choice, the uncountable -system lemma for finite sets thins an uncountable family of finite supports to an uncountable -system.
The Moore colouring realizes finite binary patterns realizes any functional binary pattern on pairwise-disjoint fixed finite families.
The Axiom of Choice supplies the transfinite cover selections and uncountable thinning.
Proof
Suppose some subspace has an open cover with no countable subcover. Recursively for , after choosing for , choose and then containing . 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 above all earlier . Thus is strictly increasing and contains no for .
By [F2], shrink each around to a finite Boolean basic set in the subspace . Intersect also with , so its finite support contains . Apply [F3] and the finite pigeonhole principle to retain an uncountable index set on which the supports form a -system with root , have fixed root and petal positions and one fixed membership-bit string, and have nonempty petals of one size . Pass to a tail so every root member is below every retained .
Let and . The family is uncountable and pairwise disjoint by the -system property; 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 . By [F4], choose a petal and a singleton with the petal below realizing all those bits.
Since belongs to its petal, the inequality from step 3.1 gives , and strict increase gives . The realized petal bits say that meets every petal condition defining . For a root coordinate , the point meets its required bit because , the root bit string is uniform, and lets [F2] read membership through . Consequently .
Step 1.1 says that contains no with , contradicting step 4.1. Therefore every subspace is Lindelöf, which is precisely hereditary Lindelöfness by [F1]. Empty and countable 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.
A ZFC L-space
Statement
ZFC proves that 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.
Moore's clopen-generated topology makes every Moore space zero-dimensional regular Hausdorff.
Moore's topology is hereditarily Lindelof proves hereditary Lindelöfness for every .
Every uncountable Moore subspace is nonseparable proves nonseparability whenever is uncountable.
L-spaces, S-spaces, and strong S-spaces defines an L-space as regular Hausdorff, hereditarily Lindelöf, and not hereditarily separable.
Proof
Take . By [F1] its Moore topology is zero-dimensional, regular, and Hausdorff; by [F2] it is hereditarily Lindelöf.
The set 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.
The four conclusions in steps 1.1 and 2.1 meet [F4] exactly, proving that 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 is uncountable.
Ordered fundamental spaces and nice refinements
Definition
A fundamental space is a Hausdorff space of cardinality that is zero-dimensional, separable, first countable, and -dense (every nonempty open set has size ), together with strictly decreasing clopen local bases
It is ordered when and is dense. The adjective does not say that : indeed .
Fix an ordered fundamental space. Suppose and . For , set
and let be the topology generated by all these ; put . A nice refinement requires:
- , and is closed while is open in ;
- for ;
- for , there are nonempty, pairwise-disjoint, compact clopen sets such that and is a clopen local base at in .
For the model-guided version, fix a continuous suitable chain of countable elementary submodels, put the global assignment in , and require the earlier -sequence and final topology below to belong to . On , choose a metric for whose ring lies at radial value from and has internal diameter at most in .
For , if is countable and , define, for ,
Here denotes the nonempty compact subsets of , with the Vietoris topology generated by the subbasic conditions and for open . Its standard basic neighbourhoods are ; in a zero-dimensional space the may be taken nonempty, pairwise-disjoint and clopen. Distances between compacta use the Hausdorff metric induced by . For the same range , the approximation condition is
The condition permits 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.
Nice refinements exist and are regular but not Lindelof
Statement
Every ordered fundamental space has a nice refinement satisfying for every . 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 and ZFC.
Ordered fundamental spaces and nice refinements gives the rings, intermediate topologies, model chain, metrics, nice-refinement clauses, the families , and .
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).
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).
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).
A space is Lindelöf when every open cover has an at most countable subcover (Countably compact, Lindel"of, sequentially compact, limit point compact and -compact spaces, and relatively compact subsets).
A clopen base gives the point--closed-set separation required for regularity (Regular spaces and spaces, with the source disagreement over whether regularity includes stated explicitly).
Countable elementary submodels and their collapses supplies a countable elementary hull containing any prescribed countable parameter set.
Transfinite recursion constructs the model chain and the later stage-by-stage refinement from their functional successor and limit clauses.
The Axiom of Choice supplies the simultaneous recursive choices of hulls, metrics, finite nets, ring points, and compact clopen enlargements.
Proof
Construct the required continuous chain explicitly. Start with an F7 hull containing the ordered fundamental space and its base assignment. At a successor, apply F7 to the countable set 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 allowed by F1 and F9. For put . Inductively suppose the and have been constructed for every , and that the resulting topology below is locally compact and zero-dimensional.
Fix . The countable model contains only countably many sets satisfying and ; list them as , repeating every such infinitely often. This collection is nonempty because it contains , and that particular makes the later star implication vacuous.
Recursively suppose is fixed for and put . This is a finite union of compact sets, hence compact. Every lies in : the first ring intersections lie in their , while all remaining points lie in the nested .
The family has a finite Hausdorff -net chosen from itself. Indeed, by [F3] choose a finite -net of the compact metric set , where . Partition the remaining tail into the outer ring and the deeper tail . Record for each which finitely many -cells meet , whether meets , and whether it meets . There are finitely many records. Two compacta with the same record are within Hausdorff distance at most : match their points in through a common recorded cell; points in are within its internal diameter ; and points in are within by the triangle inequality, since every such point has distance at most from . The two tail-incidence bits ensure that each required matching part is nonempty. Choosing one member for each realized record gives ; if , take .
Let be the union of over . It is a compact subset of the relatively clopen nonempty -th ring. Local compactness and the clopen base below cover 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 ; it contains .
For , membership in already puts its intersections with rings inside . For , the stage- definition includes in , so absorbs the -th ring intersection of . Hence .
Put . 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 and all for ; only finitely many earlier compact remain. It is therefore intermediate-closed, and [F1] makes the a clopen local base in the final refinement. The same argument for a final-open cover, now using a contained , proves that is compact in the final topology.
Whenever , steps 4.1 and 6.1 give . Every relevant occurs infinitely often, so holds.
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 .
Every is compact by step 6.2, so [F4] gives local compactness. It lies in , 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].
The set remains dense. Inductively, every nonempty relatively open meets the already dense , so every basic tail meets ; for the singleton itself lies in . Thus the refinement is separable.
Every initial segment is open: if , then each basic neighbourhood is contained in . Consequently is an open cover of . A countable subfamily has countable supremum and its union is contained in , so it misses . By [F5] the refined space is not Lindelöf.
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, has , the finite ordinals use singleton bases, and F9 records every nonempty simultaneous choice.
CH makes the nice refinement strongly hereditarily separable
Statement
Assume CH. Start with a second-countable ordered fundamental space and let be a nice refinement satisfying at every stage. Then every nonempty finite power of is hereditarily separable.
Facts & Assumptions
Given: ZFC, CH, a second-countable ordered fundamental space , and a nice refinement satisfying .
Ordered fundamental spaces and nice refinements defines the intermediate topologies , standard Vietoris neighbourhoods, the model chain, and .
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 .
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.
Second countability: an at most countable basis for the topology defines a countable basis.
Under choice, every regular second-countable space is metrizable makes the regular second-countable fundamental topology metrizable under AC.
Under choice, the uncountable -system lemma for finite sets gives an uncountable -subfamily of any uncountable family of finite sets.
L-spaces, S-spaces, and strong S-spaces defines hereditary separability and nonempty finite powers.
Closed unbounded subsets of ordinals supplies the closed-unbounded terminology used for simultaneous closure points in .
The Axiom of Choice supplies all transfinite selections, thinnings, dense-set choices, and the CH well-ordering.
Proof
A space is hereditarily separable exactly when it has no left-separated sequence , where . If a subspace is nonseparable, recursively choose outside the closure of its countable set of predecessors; otherwise those predecessors would be a countable dense subset of . Conversely, for a left-separated sequence and a countable subset of its range, choose above every index represented in ; the separating neighbourhood of misses , so is not dense in the sequence subspace.
We will use the following standard Vietoris reduction, whose proof is included. Let be compact in a zero-dimensional space, with , and let be a standard-form local base at . For put . Then iff for every with nonempty remainder. Forward, combine any standard neighbourhood of the remainder, chosen disjoint from , with the cells of to obtain a neighbourhood of . Reverse, refine any standard neighbourhood of so its cells meeting contain some , retain the cells disjoint from , and add the finitely many remainders of the former cells; the assumed closure of the remainder then supplies an element of in this refinement. For this says that, along any clopen local base at that splits , iff every lies in the closure of .
The original topology is zero-dimensional Hausdorff, hence regular and ; [F5] therefore gives a metric inducing it. Since refines , this metric topology is a coarser topology on the final space.
For each countable , is second countable: add the countably many sets with to a countable base for and close under finite intersections. Finite lists from this base form a countable standard Vietoris base for . 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.
The first closure-transfer claim is the stage case. Let , let be countable with , and suppose for the Vietoris topology. The final-open neighbourhood of leaves a compact remainder in the coarser intermediate topology; the decreasing -base and compactness give with , so every ring intersection of index at least lies in its -piece. If , each finite danger zone is clopen and misses , hence is in the intermediate closure of every . Choose infinitely large from and then close to and with . The triangle inequality makes such arbitrarily Hausdorff-close to , and the intermediate and final point-bases agree on , so is in the final closure of . If an earlier ring is bad, increase beyond it, put , and use standard neighbourhoods of the nonempty compact part , all with cells below and hence in . The family is in the model, while the tail has no danger-zone intersections; apply the argument to every such tail and then the reduction of step 1.2 to recover .
The full closure-transfer claim follows by induction on . Fix and suppose is countable in , every assigned for belongs to , and for . If , the intermediate and final bases already agree on ; if , step 2.2 applies. If and , the common bases transfer closure first to , then step 2.2 transfers it to the final topology. Otherwise, for every sufficiently small splitting , step 1.2 gives in , where . 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 topology. Step 1.2 reconstructs there, and step 2.2 finishes the transfer to .
Suppose there were a left-separated sequence of sets of one fixed finite size in and a fixed such that the were pairwise disjoint. Every has a maximum. Using step 2.1, thin so the maxima are strictly increasing; bounded maxima would put an uncountable left-separated sequence in one of the second-countable intermediate hyperspaces.
For finite target compacta, the model condition in step 3.1 can be removed. Induct on . If , the global assigned-base map and finiteness put all its -bases in the model, so step 3.1 applies. For outside the model, transfer the singleton first to its own intermediate stage, where its -base is in the model, and use step 3.1 there. Let , assume the claim below , and put . After moving to the first point of above it when necessary, either is captured by the next model or and , where and are both nonempty and smaller than . With , let consist of the -element for which in . The set belongs to , and step 2.1 gives in that model a countable dense . Every lies in the model, so step 3.1 puts in the final closure of . Meanwhile transfers to the intermediate stage because those topologies have the same point-bases on ; the induction hypothesis, applied to the smaller target , transfers it to the final topology. Given a standard neighbourhood of with one disjoint cell at each point, first choose whose points enter the -cells, then use the final closure of to choose an element of in all cells. Thus is in the final closure of .
For each , step 2.1 gives an ordinal such that is dense in the whole sequence for the Vietoris topology; choose the least such ordinal. Refinement gives when . The simultaneous closure points of and contain a club by [F9]. Choose a limit above . Then is a subset of and is dense in the whole sequence for : any basic neighbourhood mentions finitely many switched coordinates and therefore already belongs to some earlier intermediate topology.
Every hereditarily countable set is coded by a relation on a subset of , so ; the reverse inequality follows because every subset of is hereditarily countable. Thus [F3] gives . Elementarity puts a bijection from onto in , and the chain contains every countable ordinal, so . Hence choose with . Only countably many meet the countable interval , because those free parts are pairwise disjoint; choose with . The point-bases of and agree at every point of (points below use , points above use ), so their standard Vietoris local bases agree there and step 4.2 yields for . The finite-target transfer in step 4.1 gives in the final topology. But consists entirely of predecessors of , contradicting left separation.
Therefore no left-separated sequence of one fixed nonzero finite size can have pairwise-disjoint parts above one fixed countable ordinal.
Fix . If in the final Vietoris topology were not hereditarily separable, step 1.1 would give a left-separated sequence of -element sets. By [F6], thin it to a -system with finite root and put , taking when . The parts above are pairwise disjoint, contradicting step 6.1. Thus is hereditarily separable for every positive .
Fix and suppose the final product were not hereditarily separable. By step 1.1 choose a left-separated sequence of -tuples and thin so its coordinate-equality pattern is fixed. Retain one representative of each of its coordinate classes; intersecting the finitely many product coordinates belonging to one class shows that the resulting -tuple sequence is still left separated. Using the coarser metric topology from step 1.3, choose pairwise closure-disjoint basic cells around the 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 -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 , contradicting step 7.1.
Therefore every nonempty finite power is hereditarily separable, exactly as asserted. The zero power is excluded by [F8]; 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].
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.
Cantor and Baire sequence spaces and coordinate codings gives Cantor space its clopen cylinder topology; it is separable, has no isolated points, and the finite words form a countable cylinder base.
Over ZFC, The continuum hypothesis, and what this page does not prove identifies the cardinality of , and hence of its characteristic-function copy , with .
Ordered fundamental spaces and nice refinements defines ordered fundamental spaces, their strict clopen local bases, nice refinements, and the condition .
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.
Under CH, CH makes the nice refinement strongly hereditarily separable makes every nonempty finite power of such a refinement hereditarily separable.
Product projections are continuous for the product topology (The product set of functions choosing a point in each factor, the projections, the box topology, and the product topology as the initial topology of the projections; the empty product is a one-point space); products of regular spaces are regular (Arbitrary products of regular spaces are regular), and products of Hausdorff spaces are Hausdorff (Arbitrary products preserve , , and Hausdorffness).
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.
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
Let consist of the binary sequences of finite support. Sending a finite support to enumerates bijectively by , and meets every cylinder: extend the prescribed finite word by zeros. The map , where and , injects into . Inclusion gives the reverse injection, so Cantor--Bernstein and [F2] give .
Choose a bijection with : use the enumeration from step 1.1 on and a bijection on the complements. Pull the cylinder topology back along . It is Hausdorff, zero-dimensional, separable, and second countable, with dense. Every nonempty open set contains a cylinder. For a word , prefixing defines a bijection from onto its cylinder , so every nonempty open set has size .
For and , put . Then , each 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].
Apply [F4] to obtain a nice refinement satisfying every . The space is regular and Hausdorff and is not Lindelöf.
Fix . By [F5], is hereditarily separable. By [F6], is regular and Hausdorff.
The power is not Lindelöf. Otherwise let be an open cover of with no countable subcover, supplied by step 4.1. The inverse images form an open cover of . Lindelöfness would give countably many of them covering . The projection is onto: fill all coordinates other than with the fixed point . Hence the corresponding countable members of would cover , a contradiction.
Steps 5.1 and 5.2 show that every positive finite power of is regular, Hausdorff, hereditarily separable, and not Lindelöf. Thus every such power is an S-space, and [F7] says exactly that is a strong S-space. The case is included, while is deliberately excluded. The construction is nonempty because its underlying set is . Step 2.1 is the only new choice in this assembly; [F8] also propagates the ZFC choices in the two refinement suppliers.
The simple dichotomy for omega-one-generated ideals
Definition
Work in ZFC. Let be uncountable. An ideal of countable subsets of is a family that contains every finite subset of and is closed under taking subsets and finite unions. For , write when is finite.
The ideal is generated modulo finite by members if there are for such that
for every countable . This is equivalent to having an explicit family closed under finite unions: replace the displayed family by the sets for finite . The resulting family has cardinality at most in ZFC; if an -indexed family is desired, repeat members to pad the enumeration. Membership in 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 :
- is inside when ;
- is outside, or orthogonal to, when for every .
Equivalently, 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 then consists only of finite sets.
The simple dichotomy for -generated ideals is the assertion that for every such and , either some uncountable is inside , or some uncountable is outside . “Either” is inclusive: different witnesses can in principle satisfy the two clauses. One uncountable cannot satisfy both in ZFC, because AC gives a countably infinite ; inside gives , while outside says is finite. This extraction of is the only choice used in the definitional discussion. Empty and finite are allowed by the two local predicates but are not witnesses to the dichotomy.
PFA implies the simple ideal dichotomy
Statement
The Proper Forcing Axiom proves both of Abraham's forms for every ideal of countable subsets generated modulo finite by members:
- either the ground set is a countable union of sets inside , or it has an uncountable subset outside ;
- either the ground set is a countable union of sets outside , or it has an uncountable subset inside .
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 , and an ideal on generated modulo finite by .
The simple dichotomy for omega-one-generated ideals gives the ideal, generation, inside, outside, restriction, and simple-dichotomy conventions.
The Proper Forcing Axiom supplies a filter meeting any at-most family of dense subsets of a nonempty proper forcing.
Properness may be proved by adding an -master below every ; masterhood means that is predense below it for every dense (Master conditions and proper posets, Master-condition characterizations).
Suitable countable elementary submodels exist (Countable elementary submodels and their collapses).
Every ccc forcing is proper (Ccc and countably closed forcings are proper).
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 ), and by infinite-cardinal absorption (Absorption: for cardinals with infinite and , , and when ).
The Axiom of Choice supplies all model, enumeration, thinning, and witness selections below and is part of the ambient ZFC of PFA.
Proof
Put and . Generation modulo finite makes outside . AC chooses an enumeration of each countable , so injects into and [F6] gives . If is uncountable, it already supplies the outside branch of Form 1. Otherwise , and uncountability gives ; transport , and the generators along a bijection with . Thus, for the nontrivial Form-1 case, we may work on .
Assume that is not a countable union of sets inside . Define as follows. A condition has finite and a finite membership chain of countable elementary submodels of a fixed well-ordered expansion of containing and the generator map. Require that whenever are in , some satisfies and , equivalently ; this is the meaning of “the models separate distinct points of .” If lies above for , then belongs to no that is inside . A stronger enlarges all three finite coordinates and, for each , freezes .
For every , conditions putting a point above into are dense. Given , append a countable model containing and , so and . The union of the countably many inside sets belonging to cannot cover by the assumption in step 2.1. A point outside that union is outside because every singleton from is an inside set in ; append that point to . For every , the set of conditions with is dense by simply enlarging .
To prove properness, take a large countable containing and a condition . Append to the side chain. Because every finite coordinate of lies in , this is a condition . Fix and dense , and first strengthen into . The model cuts the increasing enumeration after some ; the lower part belongs to .
Let be the set of -tuples end-extending the -coordinate of that occur as the -coordinate of some condition in extending that lower part. It contains . We use the following fibre observation at each side model: if is countable, avoids every inside set in , , and contains , then is not inside ; otherwise the condition's avoidance clause would exclude . Starting at and moving down to , apply this observation to the definable successive fibres of . The intervening side model contains and all earlier coordinates but lies below the current coordinate. We obtain in nested non-inside candidate sets such that every successive choice from them completes to a tuple in .
Put . At a candidate stage, is not inside, so elementarity gives a countable with and . Since , choose ; countability of gives . Recursing through the nested fibres gives a tuple in and hence extending , with every new -point outside . The union of and is a condition: their model chains merge through ; upper points of avoid every inside generator named by ; and the replacement points of avoid every generator named by . These last two facts verify both directions of the freezing requirement. Thus is compatible with .
Step 5.1 says that is an -master, so [F3] makes proper. Apply PFA to the dense sets in step 3.1. For the resulting filter , let . It is unbounded, hence uncountable. For each generator , a condition in puts into its finite -coordinate, after which directedness and freezing show that is exactly that condition's finite intersection. By [F1], is outside . Together with the alternative excluded in step 2.1 and the reduction in step 1.1, this proves Form 1.
Now suppose there is no uncountable set inside . For every uncountable , apply Form 1 to . Its countable-union branch would make some inside piece uncountable by [F6], contrary to the supposition. Hence every uncountable contains an uncountable subset outside .
Retain and from step 1.1. The set is outside. If is countable, partition it into singletons, which are outside, and add as one more piece; this proves the countable outside decomposition. Assume henceforth that is uncountable. Then by [F6].
On define to consist of pairs with finite and finite. Put when extends both coordinates and, for every and every , Thus a recorded generator freezes every colour already present, while a new colour may be introduced once.
The forcing is ccc. Given uncountably many conditions, apply [F6] to their function domains and -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 . Their finite union is outside. For each remaining condition , the set is finite. Thin the finite 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 -set. The coordinatewise unions of their functions and side sets then satisfy both freezing clauses and form a common extension.
The following sets are dense in : conditions deciding a specified , conditions placing a specified into , and conditions whose function range contains a specified . For the first or third demand, if necessary assign a new point a colour not yet in the finite range (the specified itself when it is absent); this cannot violate a freeze, which only mentions old colours.
By steps 10.1 and [F5], is proper. PFA applied to the at-most- dense sets of step 10.2 gives a filter whose union is a total . Fix and . Directedness combines a condition recording with one already using colour ; below their common extension that intersection is frozen. Consequently is finite. Each colour class is outside by [F1], so these classes, together with , form a countable outside decomposition of . This proves Form 2 under the no-inside hypothesis; its other branch is precisely an uncountable inside set.
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 , 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].
A non-hereditarily-Lindelof regular space yields an ideal witness
Statement
Let be a regular Hausdorff space that is not hereditarily Lindelöf. Then has a right-separated subspace and open sets such that
The countable closed sets generate modulo finite an -generated ideal of countable subsets of . Every uncountable subset of inside is nonseparable, and every uncountable subset outside is discrete and hence nonseparable.
Facts & Assumptions
Given: ZFC and the space in the statement.
L-spaces, S-spaces, and strong S-spaces gives hereditary Lindelöfness and separability their all-subspaces meanings.
Regularity and Hausdorffness pass to subspaces (, , , regularity, , complete regularity, and Tychonoffness are hereditary).
In a regular space, if and is open, there is open with (A space is regular if and only if every point has a neighbourhood base of closed neighbourhoods, if and only if open gives an open with ).
The simple dichotomy for omega-one-generated ideals defines generation modulo finite and the inside and outside predicates.
The Axiom of Choice supplies the length- recursive choices, the chosen cover members, and countable enumerations. Hausdorffness supplies closed singletons, so removing finitely many points preserves openness.
Proof
By [F1], some subspace has an open cover with no countable subcover. Recursively for , the earlier chosen do not cover , so choose and then choose containing . This also makes the distinct.
Put . If , construction gives . Hence is a neighbourhood of contained in the initial segment . The union of these neighbourhoods for shows that every is open in , so is right-separated.
By [F2], is regular and Hausdorff. Apply [F3] inside to : choose open with . The set is closed in and countable because .
Let be the ideal generated modulo finite by the . Explicitly, a countable lies in exactly when for some finite . The defining family consists of countable members, and the formula is downward closed, closed under finite unions, and contains every finite set.
Let be uncountable and inside , and let be countable. By inside-ness and step 4.1, for some finite and finite . The set is countable and closed in the Hausdorff space : the are closed and the finite set is closed. Choose . Then the nonempty open subset of misses , so is not dense in . Since this holds for every countable , the space is nonseparable.
Let instead be uncountable and outside . For , outside-ness gives finite. Remove from the finite closed set . The result is an open neighbourhood in whose intersection with is exactly , so is discrete. Every dense subset of a discrete space is the whole space; because is uncountable, it is nonseparable.
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 with no earlier cover members; every and is nonempty because it contains ; finite generator lists and finite errors may be empty; and all nonempty recursive selections are the uses of AC recorded in [F5].
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 .
A non-hereditarily-Lindelof regular space yields an ideal witness turns failure of hereditary Lindelöfness into a right-separated subspace , an -generated ideal , and proves that every uncountable inside or outside witness is a nonseparable subspace.
PFA gives an uncountable inside or outside witness for every such ideal (PFA implies the simple ideal dichotomy).
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.
The Axiom of Choice is the ambient axiom used by both witness suppliers; this assembly makes no additional selection.
Proof
Assume for contradiction that is not hereditarily Lindelöf. By [F1] it has a subspace and an -generated ideal of countable subsets of with the stated witness properties.
By [F2], some uncountable is inside or outside . In either case [F1] says that , with its subspace topology, is nonseparable.
But is also a subspace of , so hereditary separability of says that is separable, contradicting step 2.1. Therefore is hereditarily Lindelöf.
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].
A supercompact gives the relative consistency of no S-spaces
Statement
For fixed effective presentations and arithmetizations,
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.
Formal consistency of PFA from a supercompact supplies, for these presentations, the formal implication without a countable-transitive- model inference.
PFA implies there are no S-spaces: ZFC+PFA proves the sentence asserting that there are no S-spaces.
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.
Primitive-recursive syntax and certified proof checking supplies verified proof parsing, concatenation, line renumbering, and malformed-input defaults.
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.
Formal consistency transfer from a verified reduction turns a verified total reduction of contradiction certificates into the corresponding formal consistency implication.
Fine measures, strong compactness and supercompactness fixes the supercompactness assertion in the source theory. No new large-cardinal property is inferred here.
Proof
Let be ZFC+PFA and let 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 -derivation of the extra axiom of . Fix its standard code . The checker from F4 accepts this particular numeral, and F5 supplies a finite PA proof of that positive closed checker instance. Thus both and PA's verification of are constructed here; neither is attributed to F2's interface.
Given a purported -refutation , use F4 to check it and to replace each use of the no-S-space axiom by a renamed copy of . Retain the ZFC axiom lines and append the same logical inferences. This yields a -refutation . The construction is a bounded syntactic substitution into the finite code , 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 is total and that .
Apply [F6] to the reduction in step 2.1. The arithmetic base proves . Compose this implication with [F1] to obtain the displayed result.
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.
L-space and S-space existence is asymmetric
Statement
The L- and S-space existence results have the following asymmetric status.
- ZFC proves that an L-space exists.
- ZFC+CH proves that a strong S-space, hence an S-space, exists; ZFC+ also proves this through .
- 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, , or PFA from another branch.
A ZFC L-space constructs an L-space in ZFC.
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.
V equals L implies diamond proves in ZF that implies on .
Diamond implies CH proves in ZFC that implies CH.
PFA implies there are no S-spaces proves in ZFC+PFA that no S-space exists.
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.
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
In the ZFC branch, apply [F1]. It gives the required L-space without CH, , PFA, or a large cardinal.
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.
In the ZFC+ branch, [F3] gives ; since this branch includes AC, [F4] gives CH; and then [F2] gives a strong S-space.
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.
For the final metatheoretic qualification, assume . Then [F6] gives . 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.
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 , [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.
5 · Examples, counterexamples and false statements
None yet.
Sources
- Moore, A solution to the L space problem, Section 7, printed p. 21
- Hart and Kunen, Ultra Strong S-Spaces, Section 1, printed p. 1
- Moore, A solution to the L space problem, Section 2, printed pp. 6--8
- Moore, A solution to the L space problem, Section 2, Facts 1--2, printed pp. 7--8
- Moore, A solution to the L space problem, Section 2, Facts 3--5 and preceding definitions, printed pp. 8--9
- Moore, A solution to the L space problem, Section 2, Fact 5 and proof, printed p. 9
- Moore, A solution to the L space problem, Sections 4--5, printed pp. 10 and 15
- Moore, A solution to the L space problem, Section 4, Lemma 4.2 and Facts 6–9, printed pp. 10–13
- Moore, A solution to the L space problem, Section 4, Lemma 4.1 and proof, printed pp. 10–14
- Moore, A solution to the L space problem, Section 5, Theorem 5.3 and proof, printed pp. 15–16
- Moore, A solution to the L space problem, Section 7, definition before Theorem 7.6, printed p. 22
- Moore, A solution to the L space problem, Section 7, printed p. 22
- Moore, A solution to the L space problem, Section 7, Theorem 7.7 and proof, printed pp. 23–24
- Moore, A solution to the L space problem, Section 7, Corollary 7.8, printed p. 24
- Moore, A solution to the L space problem, Theorem 1.3 and Section 7, printed pp. 2 and 21–24
- Hart–Kunen, Ultra Strong S-Spaces, Definitions 4.1, 4.4, 4.7, and 4.10–4.11, printed pp. 95–100
- Hart–Kunen, Ultra Strong S-Spaces, Lemmas 4.5, 4.8 and 4.12, printed pp. 96–100
- Hart–Kunen, Ultra Strong S-Spaces, Lemmas 2.7, 2.9, 2.14–2.15, 4.13–4.15 and 4.22, Theorem 4.17 and Corollary 4.18, printed pp. 91–106
- Hart–Kunen, Ultra Strong S-Spaces, Definition 4.1 discussion and Corollary 4.18, printed pp. 95 and 103
- Abraham, Three applications of ideal dichotomy, slides 2–4
- Abraham, Lecture notes on the P-ideal dichotomy, Definitions preceding Theorems 1.3–1.4
- Abraham, Lecture notes on the P-ideal dichotomy, First Form through Theorem 1.4, rendered lines 44–207
- Abraham, Three applications of ideal dichotomy, slides 1–4
- Abraham, Lecture notes on the P-ideal dichotomy, Theorem 1.5 proof, rendered lines 208–226
- Abraham, Lecture notes on the P-ideal dichotomy, Theorem 1.5 and complete proof, rendered lines 208–226
- Moore, A solution to the L space problem, Theorem 7.5, printed p. 22
- Cummings, Iterated Forcing and Elementary Embeddings, Theorem 24.11, printed pp. 99–101
- Hart–Kunen, Ultra Strong S-Spaces, Corollary 4.18, printed p. 103
- Abraham, Lecture notes on the P-ideal dichotomy, Theorem 1.5, rendered lines 208–226