Set Theory Beyond Choice: Recorded, Not Proved Here

If ZF is consistent, then ZF + AC + GCH is consistent. Here AC is the Axiom of Choice and GCH is the generalised continuum hypothesis.

Equivalently, and this is the form the library uses: if ZF is consistent, then ZF does not refute the Axiom of Choice, and ZFC does not refute GCH.

The witness is an inner model. Gödel (1938) defines the class $L$ of constructible sets by transfinite recursion along the ordinals, $L_0 = \emptyset, \quad L_{\alpha+1} = \mathrm{Def}(L_\alpha), \quad L_\lambda = \bigcup_{\alpha < \lambda} L_\alpha \ \text{ for limit } \lambda, \quad L = \bigcup_{\alpha \in \mathrm{Ord}} L_\alpha,$ where $\mathrm{Def}(X)$ is the set of subsets of $X$ definable over $(X, \in)$ with parameters from $X$. Working inside any model of ZF, one shows that $L$ satisfies every axiom of ZF, and in addition satisfies AC and GCH. Since a model of ZF yields a model of ZF + AC + GCH, the consistency of the second follows from the consistency of the first.

The conclusion is relative: it is an implication between consistency statements, and it is not, and cannot be, a proof that ZFC is consistent. By Gödel's second incompleteness theorem the consistency of ZF is not provable in ZF, so the hypothesis of the statement cannot be discharged here or anywhere.

• Not proved in this library. Nothing about $L$ is developed here. The definition above is recorded so the statement is precise, not as a construction this library carries out.

• What would prove it. The theory of the constructible universe: the definability operator $\mathrm{Def}$, absoluteness of $\Delta_0$ formulas, the reflection and Löwenheim-Skolem arguments behind the condensation lemma, and from condensation the two consequences that $L$ has a definable global well-ordering (giving AC) and that every constructible subset of $L_{\omega_\alpha}$ appears by stage $\omega_{\alpha+1}$ (giving GCH). That is an inner-model track, and this library has not built it.

• Why it matters here. This is the half of the independence of choice that says the Axiom of Choice is safe to assume: adding it to ZF cannot introduce a contradiction that was not already there. Every result in the library proved from The Axiom of Choice ↗ leans on that reassurance, and the accounting in The choice ledger: what costs the Axiom of Choice and what does not ↗ names this result as one of the two external facts it quotes. Its partner, that ZF cannot prove the Axiom of Choice either, is Cohen 1963: ZF does not prove the Axiom of Choice ‡ and is what FALSE: Zorn's lemma is a theorem of ZF ↗ actually uses.

• Conditional discipline. The statement is never asserted unconditionally in this library. "ZF does not refute AC" is shorthand for the implication above, whose antecedent is the consistency of ZF.

If ZF is consistent, then ZF + (not AC) is consistent. Equivalently: if ZF is consistent, then ZF does not prove the Axiom of Choice.

Cohen (1963, 1964) proves this by inventing forcing. Starting from a countable transitive model $M$ of ZF, one adjoins a generic object, here a set of "Cohen reals" indexed by $\mathbb{N}$, and then passes to the symmetric submodel of the resulting extension: the sets kept are those whose names are invariant under a large group of permutations of the indices, in the sense of a fixed normal filter of subgroups. The symmetric model satisfies every axiom of ZF, and it contains the set $A$ of adjoined reals as a set with no well-ordering. In particular no choice function exists for the family of nonempty subsets of $A$, so AC fails there.

Together with Gödel 1938: ZF does not refute the Axiom of Choice ‡ this makes the Axiom of Choice independent of ZF, again relative to the consistency of ZF: neither AC nor its negation is a theorem of ZF, unless ZF is inconsistent, in which case it proves everything.

• Not proved in this library. Neither forcing nor the symmetric-model construction is developed here. The description above fixes what the statement says; it is not a proof and is not a sketch that could be completed with the material in this library.

• What would prove it. A forcing track: partial orders and dense sets, Boolean-valued models or names and the forcing relation, genericity and the truth lemma, then symmetric extensions and normal filters of subgroups. A second, older route reaches the same conclusion for ZF with atoms (Fraenkel-Mostowski permutation models) and transfers it to ZF by the Jech-Sochor embedding theorem. Neither route is in this library.

• Why it matters here. This is the result that FALSE: Zorn's lemma is a theorem of ZF ↗ and FALSE: the well-ordering theorem is a theorem of ZF ↗ quote when they refuse to accept Zorn's lemma or the well-ordering theorem as theorems of ZF: both are equivalent to the Axiom of Choice over ZF (The Axiom of Choice and Zorn's lemma are equivalent ↗), so a ZF proof of either would be a ZF proof of The Axiom of Choice ↗. It is also one of the two external facts recorded in The choice ledger: what costs the Axiom of Choice and what does not ↗.

• Conditional discipline. "ZF does not prove AC" always abbreviates the implication above. Nothing in this library asserts the unconditional form, which is not available: by Gödel's second incompleteness theorem the consistency of ZF cannot be proved in ZF.

Write CH for the continuum hypothesis, the assertion that no set $A$ satisfies $\mathbb{N} \prec A \prec \mathcal{P}(\mathbb{N})$, where $X \prec Y$ means that $X$ injects into $Y$ but $Y$ does not inject into $X$. Write GCH for the generalised continuum hypothesis, the assertion that for no infinite $A$ is there a $B$ with $A \prec B \prec \mathcal{P}(A)$.

If ZFC is consistent, then all four of ZFC + CH, ZFC + (not CH), ZFC + GCH and ZFC + (not GCH) are consistent. In particular neither CH nor GCH is decided by ZFC, unless ZFC is inconsistent.

The two halves come from the two constructions already recorded here. The constructible universe of Gödel 1938: ZF does not refute the Axiom of Choice ‡ satisfies GCH, and hence CH, which rules out a ZFC refutation of either. Cohen's forcing, the method of Cohen 1963: ZF does not prove the Axiom of Choice ‡, adjoins $\aleph_2$ many generic subsets of $\mathbb{N}$ to a model of ZFC + GCH while preserving cardinals, producing a model of ZFC in which CH, and therefore GCH, fails.

In cardinal notation, using the alephs and beths of the aleph and beth hierarchies developed later in the library, GCH is the statement $2^{\aleph_\alpha} = \aleph_{\alpha+1}$ for every ordinal $\alpha$, and CH is its instance $\alpha = 0$.

• Not proved in this library. Neither half is proved here. The cardinal arithmetic in which the statement is phrased above is now fully available — Cardinal (initial ordinal) and cardinality ↗, cardinal exponentiation and the aleph and beth hierarchies are all developed on a later page — what is absent is the forcing and inner-model machinery that would prove the independence statement itself.

• What would prove it. For consistency of CH, the inner model $L$ together with its condensation lemma. For consistency of the negation, the forcing $\mathrm{Fn}(\aleph_2 \times \omega, 2)$ of finite partial functions, plus the countable chain condition and the $\Delta$-system lemma, which are what show that this forcing collapses no cardinal. Both belong to a forcing and inner-model track that this library does not contain.

• Why it matters here. The continuum hypothesis, and what this page does not prove ↗ states CH immediately after Cantor's theorem: $A \prec \mathcal{P}(A)$ ↗ establishes the gap $\mathbb{N} \prec \mathcal{P}(\mathbb{N})$, and has to record that the obvious next question is not answerable. This item is the result it quotes. Note the gap that The continuum hypothesis, and what this page does not prove ↗ itself points out: the form of CH about $\mathbb{R}$ rather than about $\mathcal{P}(\mathbb{N})$ needs $\mathbb{R} \approx \mathcal{P}(\mathbb{N})$, which the library now proves in ZF, on a later page, so the two forms are interchangeable after all — the gap The continuum hypothesis, and what this page does not prove ↗ records was closed by a later page, not a standing limitation of this remark's own claim.

• Conditional discipline. Every clause above is relative to the consistency of ZFC. "CH is independent of ZFC" is shorthand and is never used here as a standalone assertion.

Over ZF, the generalised continuum hypothesis implies the Axiom of Choice.

Precisely: assume ZF, and assume GCH in the choice-free form "for every infinite set $A$ there is no set $B$ with $A \prec B \prec \mathcal{P}(A)$", where $X \prec Y$ means $X$ injects into $Y$ but not conversely. Then every set can be well-ordered, and so the Axiom of Choice holds.

The argument (Lindenbaum and Tarski announced it in 1926; Sierpiński gave the published proof in 1947) runs through Hartogs numbers. For a set $A$ let $\aleph(A)$ be the least ordinal not injecting into $A$, which exists in ZF. One shows in ZF that $\aleph(A) \preceq \mathcal{P}(\mathcal{P}(\mathcal{P}(A)))$, and then uses GCH three times, on $A$, on $\mathcal{P}(A)$ and on $\mathcal{P}(\mathcal{P}(A))$, to force $A$ into bijection with an ordinal.

• Not proved in this library. Choice-free cardinal arithmetic is now developed elsewhere in the library — A set equinumerous with some ordinal has a least such ordinal, that ordinal is a cardinal, and equinumerous sets get the same one; no choice principle is used ↗, Hessenberg's theorem and the successor-cardinal lemma between them give $A + A$ and the successor-cardinal step for a well-orderable $A$ — but that is not enough by itself: the argument here needs the comparison of $\aleph(A)$ against iterated power sets of an arbitrary, not-yet-well-ordered $A$, which is a genuinely different and harder computation, and remains undeveloped.

• What would prove it. The choice-free cardinal arithmetic the library now has, on top of the Hartogs construction, gets partway there. The ingredients the library already has are Hartogs: an ordinal that does not inject into a given set ↗ (for every set there is a least ordinal that does not inject into it, proved with no choice at all) and, since this build, A set equinumerous with some ordinal has a least such ordinal, that ordinal is a cardinal, and equinumerous sets get the same one; no choice principle is used ↗, Hessenberg's theorem and the successor-cardinal lemma. What is still missing is the comparison of $\aleph(A)$ with $\mathcal{P}(\mathcal{P}(A))$ and $\mathcal{P}(\mathcal{P}(\mathcal{P}(A)))$ for an arbitrary infinite $A$, which is not in this library.

• Why it matters here. It settles the status of GCH as a hypothesis: GCH is not a harmless size assumption to be added to ZF, it is at least as strong as the Axiom of Choice (The Axiom of Choice ↗). This is why The continuum hypothesis and its generalisation are independent of ZFC ‡ is stated over ZFC rather than ZF, and why The continuum hypothesis, and what this page does not prove ↗ records that GCH implies CH and reaches far beyond it. What carries the argument is the generalised form: the proof applies the hypothesis to $A$, to $\mathcal{P}(A)$ and to $\mathcal{P}(\mathcal{P}(A))$ for an arbitrary infinite $A$, and the single instance $A = \mathbb{N}$ that is CH gives none of that. This library records no result at all about whether CH alone implies the Axiom of Choice, in either direction, and no page here may assert one.

• Conditional discipline. This one statement is not an independence result and needs no consistency hypothesis: it is an ordinary implication provable in ZF. It appears on this page only because its proof, not its status, is beyond the library's current machinery.

If ZF is consistent, then ZF is consistent with the existence of a set $A \subseteq \mathbb{R}$ that is infinite and Dedekind-finite: $A$ is not equinumerous with any natural number, yet $A$ has no countably infinite subset, equivalently $A$ is not equinumerous with any proper subset of itself.

This is the model Cohen produced first, in 1963. Adjoin a countable family $(a_n)_{n \in \mathbb{N}}$ of mutually generic Cohen reals to a countable transitive model of ZFC, and pass to the symmetric submodel determined by finite supports and the full permutation group of the indices. In that submodel the set $A = \{a_n : n \in \mathbb{N}\}$ exists, but the sequence $n \mapsto a_n$ does not: a hereditarily symmetric name for an injection $\mathbb{N} \to A$ has a finite support $E$, and a permutation of the indices fixing $E$ but moving some index outside $E$ then fixes the injection while moving one of its values, which is impossible. So $A$ is infinite and has no countably infinite subset in the model.

• Not proved in this library. The symmetric-extension construction is not developed here; the description above is a statement of what is built, not a construction carried out.

• What would prove it. Forcing with finite partial functions $\mathrm{Fn}(\mathbb{N} \times \mathbb{N}, 2)$, the automorphism action on names, and the finite-support symmetric submodel, together with the standard genericity argument showing that no name for an injection $\mathbb{N} \to A$ is hereditarily symmetric. That is the same forcing track named in Cohen 1963: ZF does not prove the Axiom of Choice ‡.

• Why it matters here. It is the external fact that FALSE: every infinite set has a countably infinite subset, in ZF ↗ quotes. Without it, the natural argument "$A$ is infinite, so pick $a_0$, then $a_1$, and so on" looks like a ZF proof, and the failure is invisible: what the argument uses is a choice principle (The Axiom of Countable Choice ($\mathrm{AC}_\omega$) ↗), and this model is the witness that it cannot be removed. It is also the reason this library defines finiteness by equinumerosity with a natural number rather than by the Dedekind condition (Finite, countably infinite, countable, uncountable ↗): the two definitions part company in ZF.

• Conditional discipline. As always, the statement is an implication between consistency statements. This library never asserts that an infinite Dedekind-finite set exists, only that ZF cannot rule one out unless ZF is inconsistent.

If ZF is consistent, then ZF does not prove that every countable family of two element sets has a choice function. Equivalently: if ZF is consistent, then so is ZF together with the existence of a countable family of two element sets admitting no choice function.

This is the statement behind Russell's socks. Fraenkel gave the first model, the one Jech presents as the second Fraenkel model: work in ZFA, Zermelo-Fraenkel set theory with atoms (urelements), take a countable set of atoms divided into pairs $P_n = \{a_n, b_n\}$, and pass to the permutation model determined by the group of permutations of the atoms that fix each $P_n$ setwise, with finite supports. Every axiom of ZFA holds there, the sequence $\langle P_n : n \in \mathbb{N} \rangle$ is in the model, so $\{P_n : n \in \mathbb{N}\}$ is countable there, and no choice function for it exists: a choice function would have a finite support, and a permutation swapping $a_n$ with $b_n$ for some $n$ outside that support would fix the function while moving one of its values, which is impossible.

On the date: the permutation-model method is Fraenkel's, introduced in his papers from 1922 onwards and put into its precise support form by Mostowski at the end of the 1930s; Jech records both this model and the basic one as Fraenkel's, and dates the method to the range 1922-1937 rather than to a single paper. This library therefore attributes the model to Fraenkel and does not pin it to one year.

A permutation model is not a model of ZF, because ZF has no atoms. The conclusion is carried over to ZF proper by the Jech-Sochor embedding theorem (the First Embedding Theorem), which produces from a permutation model a symmetric extension of a model of ZF in which a prescribed initial segment $\mathcal{P}^\alpha$ of the permutation model reappears, so any statement bounded in that segment is preserved. The same conclusion is also reached directly, without atoms, by Cohen's symmetric submodels of a forcing extension: Jech's second Cohen model is exactly the atom-free analogue of the model above, with the pairs realised as pairs of sets of generic reals rather than pairs of atoms. That is the machinery of Cohen 1963: ZF does not prove the Axiom of Choice ‡.

• Not proved in this library. Neither permutation models, nor the Jech-Sochor embedding theorem, nor forcing is developed here. The description above fixes what the statement says and names the constructions; it is not a proof, and it is not a sketch that could be completed with the material in this library.

• What would prove it. Either of two tracks. First: ZFA, the cumulative hierarchy over a set of atoms, normal filters of subgroups of the symmetry group, the permutation model and its support lemma, then the Jech-Sochor embedding theorem to remove the atoms. Second: the forcing track named in Cohen 1963: ZF does not prove the Axiom of Choice ‡, with the pairs realised as pairs of sets of mutually generic reals rather than atoms.

• What fails here is far less than the full axiom. The Axiom of Choice (The Axiom of Choice ↗) implies that every countable family of pairs has a choice function (Choice function ↗), so any ZF proof of the Axiom of Choice would in particular yield a ZF proof of that much weaker principle. The statement above says ZF has no proof of the weaker principle, so it already gives the conclusion of Cohen 1963: ZF does not prove the Axiom of Choice ‡, that ZF does not prove the Axiom of Choice. The reverse reading is what a reader is most likely to supply and is not what is recorded: the family here is countable and its members have two elements each, and even that much choice is unavailable.

• Why it matters here. Russell's shoes and socks ↗ proves the shoe half of Russell's illustration in ZF outright and quotes this item for the sock half. Without it the sock half would be only the observation that no rule has been found, and no search establishes an impossibility. It also fixes the lower end of the scale in The choice ledger: what costs the Axiom of Choice and what does not ↗: even choice for countably many pairs is not free.

• Conditional discipline. As everywhere in this library, the statement is an implication between consistency statements. Nothing here asserts that a countable family of pairs without a choice function exists, only that ZF cannot rule one out unless ZF is inconsistent.

If ZF is consistent, then ZF is consistent with all of the following holding simultaneously:

• $\mathbb{R}$ is a countable union of countable sets;
• the first uncountable ordinal $\omega_1$ is singular, indeed $\mathrm{cf}(\omega_1) = \omega$;
• consequently "a countable union of countable sets is countable" fails, and $\omega_1$ is not regular.

Feferman and Levy (1963) obtain this by collapsing: starting from a model of ZFC, force with the finite-support product that makes each $\aleph_n$ of the ground model countable, for $n \in \mathbb{N}$, and take the symmetric submodel with finite supports. The ground model's $\aleph_\omega$ becomes the new $\omega_1$, and it is the supremum of the countably many ordinals $\aleph_n$, each now countable, so its cofinality is $\omega$. The reals of the extension are the union over $n$ of the reals added at stage $n$, and each of those layers is countable in the extension.

Note what does not fail: $\omega_1$ still exists, and $\mathbb{R}$ is still uncountable. A countable union of countable sets is being exhibited whose union is uncountable, which is possible exactly because no enumeration of the layers can be chosen uniformly.

• Not proved in this library. The Levy collapse and the symmetric submodel are not developed here.

• What would prove it. The forcing track of Cohen 1963: ZF does not prove the Axiom of Choice ‡, specialised to the Levy collapse $\mathrm{Coll}(\omega, {<}\aleph_\omega)$ with finite supports, plus the cofinality computation in the symmetric model. Ordinal and cardinal arithmetic beyond Cardinal (initial ordinal) and cardinality ↗ is also needed to state the cofinality claim properly.

• Why it matters here. Two library results lean on it directly. It is the external fact behind FALSE: countable unions of countable sets are countable is a theorem of ZF ↗: the countable union theorem Countable unions of at most countable sets, assuming $\mathrm{AC}_\omega$ ↗ is proved here from The Axiom of Countable Choice ($\mathrm{AC}_\omega$) ↗, and this model shows the hypothesis cannot be dropped. It is also the standing warning attached to $\omega_1$: any counterexample built on the ordinal space $[0, \omega_1)$ and its sequential compactness is silently spending a choice principle, because in this model $\omega_1$ has countable cofinality and those arguments collapse. Note also that $\mathbb{R}$ is uncountable (Cantor's nested intervals, 1874) ↗ survives untouched: it is a theorem of ZF, and it is not in tension with $\mathbb{R}$ being a countable union of countable sets.

• Conditional discipline. Everything above is relative to the consistency of ZF, and this library never asserts that the reals are a countable union of countable sets, only that ZF alone cannot refute it.

If ZF is consistent, then ZF does not prove that there is a free (that is, non-principal) ultrafilter on $\mathbb{N}$.

Feferman (1965), using Cohen's forcing, produces a model of ZF in which every ultrafilter on $\mathbb{N}$ is principal. The forcing adjoins countably many Cohen reals $x_n \subseteq \mathbb{N}$ by finite partial functions $\mathbb{N} \times \mathbb{N} \to \{0,1\}$, but the symmetry group is not a group of permutations of the indices: it is the group of automorphisms obtained by flipping the generic bits on an arbitrary set of coordinates, with supports the finite subsets of $\mathbb{N}$. A hereditarily symmetric name for an ultrafilter on $\mathbb{N}$ has such a finite support, and for any index $n$ outside that support there is a flip that fixes the name while replacing $x_n$ by a set differing from it on a cofinite set. The purported ultrafilter would then have to contain both, which forces it to be principal.

Consequence, and this is the form the library needs. The ultrafilter lemma (UL), that every filter on a set extends to an ultrafilter, produces a free ultrafilter on $\mathbb{N}$ from the filter of cofinite sets. So, if ZF is consistent, UL is not a theorem of ZF, and neither is its equivalent, the Boolean prime ideal theorem.

• This is not the basic Cohen model. The distinction is load-bearing. The basic Cohen model uses the same forcing but the group of permutations of the indices, and by Halpern and Lévy 1971: the Boolean prime ideal theorem does not imply the Axiom of Choice ‡ the Boolean prime ideal theorem, hence the ultrafilter lemma, holds there, so the basic Cohen model does contain free ultrafilters on $\mathbb{N}$. Only the flip-symmetric model above kills them. Reading Feferman's model as "the Cohen model" would put two items on this page in direct contradiction.

• Not proved in this library. Forcing and symmetric models are not developed here.

• What would prove it. The forcing track named in Cohen 1963: ZF does not prove the Axiom of Choice ‡, plus the symmetry argument above: no hereditarily symmetric name can decide the membership of every subset of $\mathbb{N}$ in a purported ultrafilter.

• Why it matters here. What the ultrafilter lemma costs: a choice principle strictly weaker than AC ↗ cites exactly this result for its first bullet, "UL is not a theorem of ZF", which is one of the two poles that locate UL strictly between ZF and the Axiom of Choice; the other pole is Halpern and Lévy 1971: the Boolean prime ideal theorem does not imply the Axiom of Choice ‡. It is also what makes FALSE, once the ultrafilter lemma is available: every ultrafilter is principal ↗ an unusual item: that statement is false in ZFC, since The ultrafilter lemma, from the Axiom of Choice: every filter extends to an ultrafilter ↗ refutes it, and yet it is consistent with ZF, so the refutation genuinely consumes a choice principle and cannot be made choice-free. The strengthening from $\mathbb{N}$ to arbitrary sets is Blass 1977: a model of ZF with no free ultrafilter on any set ‡.

• Conditional discipline. The statement is relative to the consistency of ZF. This library never says "free ultrafilters do not exist"; it says that ZF alone cannot produce one, and that Ultrafilter ↗ is satisfied non-principally only once a choice principle is available.

If ZF is consistent, then ZF is consistent with the statement that every ultrafilter on every set is principal. Equivalently: there is a model of ZF containing no free ultrafilter at all, on any set whatsoever.

This is Blass (1977). As a statement it strengthens Feferman 1965: ZF does not prove that a free ultrafilter on the naturals exists ‡, where the conclusion was obtained only for $\mathbb{N}$: "every ultrafilter on every set is principal" implies "every ultrafilter on $\mathbb{N}$ is principal", so the consistency of the first is the stronger result. The model is again obtained by forcing and symmetry, but the construction is not reproduced here: the published note is a summary (see the citation remark below), and this library has not read a full account of it, so it records the conclusion and not the method.

• Not proved in this library. No forcing or symmetric-model machinery is developed here.

• What would prove it. The forcing and symmetric-model machinery named in Cohen 1963: ZF does not prove the Axiom of Choice ‡, with the additional uniformity argument that handles arbitrary sets rather than a single fixed set.

• Why it matters here. FALSE, once the ultrafilter lemma is available: every ultrafilter is principal ↗ refutes the claim that every ultrafilter is principal, and does so only after invoking The ultrafilter lemma, from the Axiom of Choice: every filter extends to an ultrafilter ↗, which costs a choice principle. This item is the sharp statement of why that cost is unavoidable in the strongest possible sense: it is not that the refutation happens to use choice for the particular filter of tails on $\mathbb{N}$, it is that in ZF alone one cannot get a single non-principal instance of Ultrafilter ↗ anywhere.

• On the citation. The primary source is a short note in the Bulletin de l'Académie Polonaise des Sciences (volume 25, number 4, pages 329-331), which has no open electronic edition and which the reviewing literature describes as a summary rather than a full account. The reference url above therefore points at the standard survey statement of the fact, "ZF alone does not even imply that there exists a non-principal ultrafilter on some set", rather than at the note itself; the note's full bibliographic details are given in the reference title. The survey page states the fact but does not name Blass, so the attribution rests on the bibliographic record, not on that page.

• Conditional discipline. Relative to the consistency of ZF, as always. The claim is that ZF cannot refute "every ultrafilter is principal", not that the statement is true.

Write BPI for the Boolean prime ideal theorem, that every nontrivial Boolean algebra has a prime ideal; over ZF this is equivalent to the ultrafilter lemma (UL), that every filter on a set extends to an ultrafilter.

If ZF is consistent, then ZF + BPI + (not AC) is consistent. So BPI does not imply the Axiom of Choice over ZF.

Halpern and Lévy (1971) prove this in the basic Cohen model, the first symmetric model Cohen built: adjoin countably many mutually generic Cohen reals and take the symmetric submodel with finite supports and the group of all permutations of the index set. The Axiom of Choice fails there, because the set of adjoined reals cannot be well-ordered. That BPI nevertheless holds is the difficult half, and it rests on the Halpern-Läuchli partition theorem for products of finitely many trees.

Combined with Feferman 1965: ZF does not prove that a free ultrafilter on the naturals exists ‡ this places UL strictly between ZF and AC, relative to the consistency of ZF: UL is not provable in ZF, and UL does not recover AC.

• Which Cohen model this is. The model is the one recorded in Cohen's first model: an infinite Dedekind-finite set of reals ‡, Jech's basic Cohen model. Jech's second Cohen model is a different construction, the atom-free analogue of Fraenkel's socks (Fraenkel's socks: ZF does not prove choice for countably many pairs ‡), and is not the model used here. The distinction matters: BPI holds in the basic Cohen model, so free ultrafilters on $\mathbb{N}$ exist there, which is why Feferman 1965: ZF does not prove that a free ultrafilter on the naturals exists ‡ must use a different symmetric model altogether.

• Not proved in this library. Neither the symmetric model nor the Halpern-Läuchli partition theorem is developed here.

• What would prove it. The forcing track of Cohen 1963: ZF does not prove the Axiom of Choice ‡, plus a Ramsey-theoretic component: the Halpern-Läuchli theorem, and the deduction of BPI in the symmetric model from it. The partition theorem is genuinely combinatorial and is not implied by the forcing machinery alone.

• Why it matters here. What the ultrafilter lemma costs: a choice principle strictly weaker than AC ↗ and The choice ledger: what costs the Axiom of Choice and what does not ↗ both quote this result, and it is what licenses the library's habit of naming The ultrafilter lemma, from the Axiom of Choice: every filter extends to an ultrafilter ↗ as a separate statement instead of inlining it into its applications. A theorem proved from UL costs strictly less than The Axiom of Choice ↗, and "strictly" is exactly this item.

• Conditional discipline. Relative to the consistency of ZF. Note also the direction that is not claimed: the library proves AC implies UL, and cites this result for the failure of the converse; it proves neither the converse nor its failure.

If ZFC together with "there exists an inaccessible cardinal" is consistent, then so is the theory

ZF + DC + "every set of reals is Lebesgue measurable" + "every set of reals has the Baire property" + "every uncountable set of reals contains a perfect set",

where DC is the axiom of dependent choice.

Solovay (1970) builds the model by Levy-collapsing an inaccessible cardinal $\kappa$ to $\omega_1$ and then passing to an inner model of the extension. His own model is the class of sets hereditarily definable from a countable sequence of ordinals; the inner model $L(\mathbb{R})$ of the same extension is the other standard choice and satisfies the same conclusions. The two are not being claimed here to be the same class. Every set of reals in the model is definable from a real and an ordinal, and each such set is shown to be measurable by a homogeneity argument about the collapse.

What this rules out. Every classical pathology of the real line that is proved by well-ordering $\mathbb{R}$ is therefore not available from ZF + DC alone, relative to the stated large-cardinal hypothesis: a Vitali set, a Bernstein set, a Hamel basis for $\mathbb{R}$ over $\mathbb{Q}$ and with it a discontinuous additive solution of Cauchy's functional equation, and the Banach-Tarski decomposition.

• Not proved in this library. Neither the Levy collapse nor the measurability argument is developed here, and no measure theory is developed here either, so even the statement "Lebesgue measurable" is being borrowed.

• What would prove it. Three tracks at once: forcing (the Levy collapse and its homogeneity), large cardinals (the inaccessible, which Shelah 1984: the inaccessible is needed for measurability, not for the Baire property ‡ shows is genuinely required for the measurability clause), and Lebesgue measure theory. None of the three exists in this library.

• Why it matters here. It is the sharpest available answer to "how much choice does the pathology of $\mathbb{R}$ actually cost". DC is enough for essentially all of classical analysis of sequences and limits, and this model says that DC alone still produces none of the non-measurable objects. So whenever a later page produces such an object through Zorn's lemma ↗ or a well-ordering, the use of full The Axiom of Choice ↗ is not laziness: the ledger in The choice ledger: what costs the Axiom of Choice and what does not ↗ can record it as irreducible.

• Conditional discipline. The hypothesis here is stronger than mere consistency of ZF: it is the consistency of ZFC plus an inaccessible cardinal, which is strictly stronger and is not provable from Con(ZFC). That extra hypothesis is needed for the measurability clause and, by Shelah, not for the Baire-property clause.

Shelah (1984) settles which half of Solovay's model: ZF + DC with every set of reals measurable ‡ really needs a large cardinal.

If ZF is consistent, then so is ZF + DC + "every set of reals has the Baire property". No inaccessible cardinal is required for this half.

The measurability half is different. If ZF + DC + "every set of reals is Lebesgue measurable" is consistent, then so is ZFC + "there exists an inaccessible cardinal". So the large-cardinal hypothesis in Solovay's theorem is not an artefact of the proof: the two theories are equiconsistent, and the inaccessible cannot be removed.

• Not proved in this library. Neither direction is proved here. The second direction in particular is a reverse-mathematical calculation about consistency strength, of a kind this library has no machinery for.

• What would prove it. For the first direction, an amalgamated Souslin forcing replacing the Levy collapse. For the second, the observation that if every set of reals is measurable then $\omega_1$ is inaccessible in $L[r]$ for every real $r$, which needs the fine structure of the constructible universe relativised to a real. Both belong to a forcing and inner-model track that this library does not contain.

• Why it matters here. It sharpens the reading of Solovay's model: ZF + DC with every set of reals measurable ‡ in a way that matters for how the library reports costs. "Every set of reals has the Baire property" is consistent with ZF + DC at no extra consistency cost at all, so any Baire-category pathology on $\mathbb{R}$ that this library later produces must be using more than DC. Measurability pathologies sit strictly higher. When The choice ledger: what costs the Axiom of Choice and what does not ↗ records what a theorem costs, this is the result that keeps the two cases apart.

• Conditional discipline. The first clause is relative to Con(ZF); the second is an implication between consistency statements and is not an assertion that an inaccessible cardinal exists.

If ZFC together with "there is a proper class of strongly compact cardinals" is consistent, then so is ZF + "every uncountable cardinal is singular".

That is: relative to that large-cardinal hypothesis, there is a model of ZF in which no uncountable cardinal is regular at all, so $\aleph_1$, $\aleph_2$ and every other uncountable aleph has cofinality $\omega$. Gitik (1980) obtains it by an iterated Prikry-style forcing over a model with a proper class of strongly compact cardinals, followed by a symmetric submodel.

• Not proved in this library. No forcing, no large cardinals, and no symmetric submodels: that part of the machinery is entirely outside the library's stack. The cofinality function $\operatorname{cf}(\alpha)$ and the words regular and singular are themselves defined here (Cofinality $\operatorname{cf}(\alpha)$, and regular and singular cardinals ↗), and the library proves one regularity fact under choice ($\aleph_0$ is regular in ZF; assuming the Axiom of Choice every successor aleph $\aleph_{\alpha+1}$ is regular; $\operatorname{cf}(\aleph_\omega) = \aleph_0$, so $\aleph_\omega$ is singular, and under choice it is the least singular infinite cardinal ↗) — but that is choice-theoretic ground truth, the opposite of what Gitik's result denies, and nothing here touches the choice-free question this remark records.

• What would prove it. Large-cardinal theory (strongly compact cardinals and their embeddings), Prikry forcing and its iterations, and symmetric extensions. This is the deepest result recorded on this page and is far outside the library's stack.

• Why it matters here. It is the extreme point of the phenomenon that The Feferman-Levy model: the reals as a countable union of countable sets ‡ introduces. That model makes $\omega_1$ singular; Gitik's makes every uncountable cardinal singular. The practical reading for this library is that regularity of an uncountable cardinal is never a free structural fact about Cardinal (initial ordinal) and cardinality ↗: it is a consequence of choice, and without choice it can fail everywhere at once. What survives in ZF is the much weaker existence statement Hartogs: an ordinal that does not inject into a given set ↗, which is why the library leans on Hartogs numbers, and why the one regularity statement it does prove — that no at most countable subset of $\omega_1$ is cofinal in it — carries the Axiom of Countable Choice as an explicit standing hypothesis rather than reading it off the structure. The choice ledger: what costs the Axiom of Choice and what does not ↗ records that distinction.

• Conditional discipline. The hypothesis is a large-cardinal consistency assumption strictly stronger than Con(ZFC), and the conclusion is a relative consistency statement. Nothing here asserts that strongly compact cardinals exist.

Over ZF, "the Baire category theorem" is not one statement. Naming the versions by the class of spaces they quantify over:

(BCT-metric) In a complete metric space, a countable intersection of dense open sets is dense. Over ZF this is equivalent to the axiom of dependent choice (DC). The implication from DC is the usual proof, in which each nested ball is chosen in terms of the previous one; the converse is Blair (1977).

(BCT-separable) The same statement restricted to separable complete metric spaces is a theorem of ZF, with no choice principle at all: a fixed countable dense set removes every choice from the construction.

(BCT-compact-Hausdorff) Every compact Hausdorff space is a Baire space. Over ZF this is equivalent to the principle "every tree has a subtree all of whose levels are finite", introduced by Blass (1979) and known as dependent multiple choice (DMC). The equivalence is Fossy and Morillon (1998).

Separating them. DMC is strictly weaker than each of DC and the axiom of multiple choice, in ZF and in ZFA alike, so BCT-metric and BCT-compact-Hausdorff are genuinely different assumptions. The Boolean prime ideal theorem does not imply DMC either, and so does not give BCT-compact-Hausdorff. The ground for that last point is recorded elsewhere on this page: DMC implies Urysohn's lemma (Blass 1979) while BPI does not (Brunner 1983, in the Mostowski linearly ordered model). The same pair shows DMC is not itself a theorem of ZF, since Urysohn's lemma is not.

If ZF is consistent, none of these principles is a theorem of ZF except BCT-separable, and the non-implications listed are witnessed by models.

• Where the DMC separations are recorded. The two facts about DMC used in "Separating them" are the ones stated in Urysohn's lemma is not a theorem of ZF, nor of ZF plus countable choice ‡: Blass's implication from DMC to Urysohn's lemma, and Brunner's model in which BPI holds and Urysohn's lemma fails.

• Not proved in this library. No direction of any of these equivalences is proved here, and the models witnessing the non-implications are symmetric extensions and permutation models that this library does not build.

• What would prove it. For the equivalences: a careful ZF development of metric and compact Hausdorff spaces together with the combinatorics of trees. For the separations: permutation models with the Jech-Sochor or Pincus transfer theorems, that is, the same track as Cohen 1963: ZF does not prove the Axiom of Choice ‡.

• Why it matters here. Every use of the Baire category theorem in this library must name its version and pay for it. It is easy to write "by Baire" and quietly consume DC where the separable case would have been free, and easy to claim the locally compact or compact Hausdorff case is choice-free when it is not. The accounting pages The choice ledger: what costs the Axiom of Choice and what does not ↗ and What the ultrafilter lemma costs: a choice principle strictly weaker than AC ↗ record principles by name for exactly this reason, and The Axiom of Countable Choice ($\mathrm{AC}_\omega$) ↗ is where the weakest of the relevant principles is defined. What is not affected is availability: nothing about the Baire category theorem needs measure theory or functional analysis, so the theorem is in scope; only its cost is recorded here.

• A variant not asserted here. The locally compact regular form of the theorem is sometimes attributed to Bacsich (1972) with the same equivalence. That attribution was not confirmed against a primary source, so this item does not state it.

• Conditional discipline. The unprovability and non-implication clauses are relative to the consistency of ZF. The two equivalences are ordinary ZF theorems and need no consistency hypothesis; they are on this page because their proofs, not their status, are out of reach here.

Urysohn's lemma (UL). If $X$ is a $T_4$ space and $A, B \subseteq X$ are disjoint closed sets, there is a continuous $f : X \to [0,1]$ with $A \subseteq f^{-1}(\{0\})$ and $B \subseteq f^{-1}(\{1\})$.

The following are all relative to the consistency of ZF.

(a) UL is not a theorem of ZF. Läuchli (1962/63) builds a permutation model of ZF with atoms in which the set of atoms is densely linearly ordered, of the order type of the rationals of the ground model, and in which that set with its order topology is a $T_4$ space on which every continuous real-valued function is constant; UL fails there. Since the negation of UL is a boundable statement, the Jech-Sochor first embedding theorem transfers the failure to ZF proper.

(b) UL is not a theorem of ZF + countable choice. Tachtsis (2019) produces a model of ZF in which $\mathrm{AC}_\omega$ holds and UL fails, and hence in which the Tietze extension theorem fails as well.

(c) What does suffice. Dependent choice implies UL by the usual dyadic construction. Blass (1979) proves the stronger statement that dependent multiple choice implies UL. Whether UL implies DMC is open.

(d) The Boolean prime ideal theorem does not suffice. Brunner (1983) shows UL fails in the Mostowski linearly ordered model, where BPI holds; Pincus's transfer theorems carry this to ZF.

• Not proved in this library. None of (a) to (d) is proved here. Even the positive direction, that DC implies UL, is not proved here, because the library has no topology track yet at the point where this page sits.

• What would prove it. For (a), (b) and (d): permutation models of ZF with atoms, plus the Jech-Sochor and Pincus transfer theorems, that is, the same track named in Cohen 1963: ZF does not prove the Axiom of Choice ‡. For (c): the tree combinatorics behind DMC, the same principle that appears in The Baire category theorem is four inequivalent statements over ZF ‡.

• Why it matters here. Urysohn's lemma is the workhorse of every separation and metrisation argument, and it looks like pure point-set topology. It is not: the usual proof indexes a family of open sets by the dyadic rationals and chooses one at each stage in terms of the previous stage, which is dependent choice. Any page in this library that proves Urysohn's lemma, Tietze extension, or a metrisation theorem must therefore record a choice principle in The choice ledger: what costs the Axiom of Choice and what does not ↗, and must not claim the argument is free merely because it never mentions a well-ordering. Note that the weakest standard principle, The Axiom of Countable Choice ($\mathrm{AC}_\omega$) ↗, is provably not enough, by (b).

• Conditional discipline. Clauses (a), (b) and (d) are relative to the consistency of ZF; clause (c) is an ordinary implication over ZF. Nothing here asserts that Urysohn's lemma is false.

Stone's theorem. Every metric space is paracompact.

The following are relative to the consistency of ZF.

(a) Not provable in ZF + DC. Good, Tree and Watson (1998) show that Stone's theorem does not follow from ZF together with the axiom of dependent choice.

(b) Not implied by BPI. Corson (2020) gives a permutation model in which the Boolean prime ideal theorem holds and Stone's theorem fails; the offending metric space takes only rational distances and is not even metacompact. Transfer theorems carry the independence to ZF. This answers a question left open by Good, Tree and Watson.

(c) What is not known. Stone's theorem is not known to be equivalent to the Axiom of Choice, and no published result places it strictly below AC. What Good, Tree and Watson do record on the upper side is that every proof of Stone's theorem known to them in fact proves a stronger statement that implies AC: their Proposition 5 shows that "every discrete metric space is effectively metacompact", where a refinement is effective when a function chooses a member of the cover containing each refining set, already yields the axiom of multiple choice for disjoint families, and the axiom of multiple choice implies the Axiom of Choice over ZF. Note that the last step is a ZF fact, not a weakening: over ZF multiple choice and the Axiom of Choice are equivalent, so "the axiom of multiple choice" is not an upper bound below AC here. It is only over ZFA that the two come apart, which is why the models in (a) and (b) are permutation models needing a transfer theorem.

• Not proved in this library. No part of the independence analysis is proved here. Paracompactness and the choice-based proof of Stone's theorem are unavailable at this point in the reading order; they are developed later in Stone's theorem, under choice: every metric space is paracompact ↗.

• What would prove it. Permutation models with Pincus-style transfer, the same track named in Cohen 1963: ZF does not prove the Axiom of Choice ‡, together with a ZF development of metric spaces, refinements and local finiteness.

• Why it matters here. Paracompactness of metric spaces is used silently wherever partitions of unity, metrisation theorems or Stone-type refinements appear, and it is the sort of statement that reads as pure point-set topology. The later proof records its costs in Choice and convention ledger for paracompactness, Stone's theorem, and partitions of unity ↗; its exact strength relative to The Axiom of Choice ↗ remains open.

• Conditional discipline. Clauses (a) and (b) are relative to the consistency of ZF. Clause (c) mixes two things and they are kept apart: "not known to be equivalent to AC" is a statement about the current state of knowledge and not a mathematical claim, recorded so that no later page over-reports the result as "equivalent to AC"; the facts about effective metacompactness and about multiple choice are ordinary ZF theorems and need no consistency hypothesis.

Kelley (1950) derived the Axiom of Choice from Tychonoff's theorem as follows. Given nonempty sets $X_a$ for $a \in I$, adjoin a point $\infty$ to each and topologise $X_a \cup \{\infty\}$ by the cofinite topology; each such space is compact, the sets $X_a$ are claimed to be closed, and the finite intersection property of the family $\{\pi_a^{-1}(X_a)\}$ then yields a point of the product, that is, a choice function.

Schechter (2006): that argument does not prove the Axiom of Choice. In the cofinite topology on $X_a \cup \{\infty\}$ the set $X_a$ is not closed when $X_a$ is infinite, since every nonempty open set is cofinite and therefore meets $X_a$. What Kelley's specialisation actually proves, and is equivalent to over ZF, is the Boolean prime ideal theorem.

The repair. Make the adjoined point isolated: topologise $X_a \cup \{\infty\}$ as the disjoint sum of $X_a$ with its cofinite topology and the one-point space $\{\infty\}$, so that the open sets are the unions of a cofinite subset of $X_a$ (or $\emptyset$) with a subset of $\{\infty\}$. This space is compact and $T_1$, and now $X_a$ genuinely is closed, its complement $\{\infty\}$ being open. With the repair the classical conclusion survives in the form: "every product of compact $T_1$ spaces is compact" is equivalent to the Axiom of Choice over ZF, while "every product of compact Hausdorff spaces is compact" is equivalent to BPI.

• Not proved in this library. Neither Tychonoff's theorem nor either equivalence is proved here.

• What would prove it. A ZF development of product topologies and compactness, plus the filter arguments of the ultrafilter lemma. Only the independence half, that BPI does not imply the Axiom of Choice, needs forcing; that half is Halpern and Lévy 1971: the Boolean prime ideal theorem does not imply the Axiom of Choice ‡. The rest is elementary once topology exists, which is why this item records a correction rather than a deep theorem.

• Why it matters here. The claim "Tychonoff implies AC" is standard, and the standard proof of it is the one Kelley gave. A library that repeats it verbatim would be asserting an equivalence with The Axiom of Choice ↗ on the strength of a false lemma, and would also be mis-pricing the Hausdorff case, which costs only The ultrafilter lemma, from the Axiom of Choice: every filter extends to an ultrafilter ↗. When the topology track reaches Tychonoff, this correction is what keeps the two statements and their two prices apart in The choice ledger: what costs the Axiom of Choice and what does not ↗.

• Conditional discipline. This item states an error and its repair, plus two ZF equivalences; only the accompanying strictness claim, that BPI is genuinely weaker, is an independence result and it is recorded conditionally in Halpern and Lévy 1971: the Boolean prime ideal theorem does not imply the Axiom of Choice ‡.

A partial order $P$ has the countable chain condition (ccc) when every family of pairwise incompatible elements of $P$ is countable. For a cardinal $\kappa$, $\mathrm{MA}(\kappa)$ asserts:

for every ccc partial order $P$ and every family $\mathcal{D}$ of at most $\kappa$ dense subsets of $P$, there is a filter on $P$ meeting every member of $\mathcal{D}$.

Martin's Axiom (MA) is the assertion that $\mathrm{MA}(\kappa)$ holds for every $\kappa < 2^{\aleph_0}$.

Three facts fix its status.

(a) $\mathrm{MA}(\aleph_0)$ is a theorem of ZFC (the Rasiowa-Sikorski lemma), so MA is not vacuous but its content is entirely in the uncountable cases.

(b) CH implies MA, trivially, since under CH there is no $\kappa$ with $\aleph_0 < \kappa < 2^{\aleph_0}$. So MA alone decides nothing that CH does not.

(c) If ZFC is consistent, then so is ZFC + MA + (not CH). This is Solovay and Tennenbaum (1971), and it is where finite-support iterated ccc forcing was invented: one iterates ccc posets $\aleph_2$ times, catching every ccc poset of size less than the continuum along the way, and the iteration is itself ccc so no cardinal is collapsed.

What MA + (not CH) buys. Every set of reals of cardinality less than $2^{\aleph_0}$ is Lebesgue null and meagre; the union of fewer than $2^{\aleph_0}$ meagre sets is meagre; $2^{\kappa} = 2^{\aleph_0}$ for every infinite $\kappa < 2^{\aleph_0}$; and the product of two ccc spaces is ccc, so ccc is productive.

• Not proved in this library. Neither the consistency result nor any of the consequences is proved here.

• What would prove it. Iterated forcing with finite support, the ccc preservation theorem for such iterations, and a bookkeeping argument for the $\aleph_2$-length iteration. This is the forcing track named in Cohen 1963: ZF does not prove the Axiom of Choice ‡, one level beyond a single-step extension.

• Why it matters here. MA is the standard hypothesis under which the continuum behaves as if it were $\aleph_1$ for the purposes of category and measure while nevertheless being large. It is the axiom that makes the two sides of The Suslin hypothesis is independent of ZFC, in both directions ‡ and of The normal Moore space conjecture is independent, and its consistency needs a large cardinal ‡ possible, and it is the reason a topology page cannot state "ccc is productive" as a theorem: that statement is a consequence of MA + (not CH) and is refuted by a Suslin line. Notice also what MA is not: it is not a choice principle and not a size axiom about Cardinal (initial ordinal) and cardinality ↗; it is a genericity assumption, and its interaction with CH is recorded in The continuum hypothesis, and what this page does not prove ↗.

• Conditional discipline. Clause (c) is relative to the consistency of ZFC. Clauses (a) and (b) are ZFC theorems. Nothing here asserts MA.

• On the citation. The Solovay-Tennenbaum paper is behind a paywall that refuses automated access, so the reference url points at the survey account of the result; the full bibliographic details are in the reference title.

A Suslin line is a dense complete linear order without endpoints that satisfies the countable chain condition (every family of pairwise disjoint nonempty open intervals is countable) but is not separable. The Suslin hypothesis (SH) says that no Suslin line exists; equivalently, that every such order satisfying the ccc is order-isomorphic to $\mathbb{R}$.

Kurepa (1935): three equivalent forms. Over ZFC, a Suslin line exists if and only if a Suslin tree exists (a tree of height $\omega_1$ with no uncountable chain and no uncountable antichain), if and only if a Suslin algebra exists (a Boolean algebra that is complete, atomless, countably distributive and satisfies the countable chain condition).

The following are relative to the consistency of ZFC.

(a) Con(ZFC + SH). Solovay and Tennenbaum (1971) force SH by iterating ccc forcings that kill Suslin trees. The clean statement of what they proved is: MA + (not CH) implies SH, together with the consistency of MA + (not CH) recorded in Martin's Axiom ‡.

(b) Con(ZFC + not SH). Jech (1967) and Tennenbaum (1968) force a Suslin tree into existence. Jensen (1972) then proved the sharper result that the diamond principle implies a Suslin tree exists, and diamond holds in the constructible universe, so a Suslin line exists in $L$.

(c) The consequence for the ccc. If a Suslin line exists then the countable chain condition is not productive: there is a ccc partial order whose square is not ccc. So "a product of ccc spaces is ccc" is not a ZFC theorem, while under MA + (not CH) it is.

• Not proved in this library. None of (a), (b), (c) is proved here, and neither trees of height $\omega_1$ nor the diamond principle is defined here.

• What would prove it. For (a), iterated ccc forcing as in Martin's Axiom ‡. For (b), the fine structure of $L$ far enough to derive diamond, plus the tree construction from diamond. For (c), the combinatorics of Suslin trees. All lie in a forcing and inner-model track this library does not contain.

• Why it matters here. Suslin's 1920 question is the natural sequel to the order-theoretic characterisation of $\mathbb{R}$: the classical theorem says a dense complete separable linear order without endpoints is order-isomorphic to $\mathbb{R}$, and the question is whether "separable" can be weakened to "ccc". The answer is that ZFC does not decide it, so the characterisation of the real line cannot be improved in that direction by any argument in this library. It is also the reason the library must not use "ccc implies separable" as a step anywhere. The ZFC-provable substitute is available and needs no independence at all: the Cantor cube $\{0,1\}^{\kappa}$ for $\kappa$ larger than the continuum is ccc and not separable, which settles the question for topological spaces even though it says nothing about linear orders (Well-order and well-ordered set ↗, Cardinal (initial ordinal) and cardinality ↗, $\mathbb{R}$ is uncountable (Cantor's nested intervals, 1874) ↗).

• Conditional discipline. (a) and (b) are relative consistency statements; the implications inside them, MA + (not CH) implies SH, and diamond implies not SH, are ordinary ZFC theorems. Nothing here asserts that a Suslin line exists or that one does not.

A Moore space is a regular space carrying a development: a sequence $(\mathcal{G}_n)_{n \in \mathbb{N}}$ of open covers such that for each point $x$ the collection of stars $\mathrm{St}(x, \mathcal{G}_n)$ is a neighbourhood base at $x$. The normal Moore space conjecture (NMSC) asserts that every normal Moore space is metrisable.

NMSC is not decided by ZFC, and its two sides have very different costs.

(a) It fails under CH. Fleissner (1982) constructs a normal nonmetrisable Moore space from the continuum hypothesis. Since CH holds in the constructible universe, NMSC fails in $L$. Non-metrisable normal Moore spaces also exist under MA + (not CH), so both of the standard opposing hypotheses of Martin's Axiom ‡ refute it.

(b) It holds under PMEA. Nyikos (1980) proves that the product measure extension axiom, that the usual product measure on $\{0,1\}^{\kappa}$ extends to a measure on all subsets, implies every normal Moore space is metrisable. PMEA is consistent relative to the existence of a strongly compact cardinal.

(c) A large cardinal is necessary, not just convenient. Fleissner (1982) proves that if every normal Moore space is metrisable then there is an inner model with a measurable cardinal. So the consistency of NMSC is not provable from the consistency of ZFC alone.

• Not proved in this library. None of (a), (b), or (c) is proved here. The library now has a metrisation track and the standard metrisation theorems, but not the large-cardinal, forcing, measure-theoretic or inner-model machinery needed for these independence statements.

• What would prove it. For (a), a CH construction plus the standard metrisation theorems. For (b), large-cardinal theory (strongly compact cardinals) and the forcing that produces PMEA, plus measure theory. For (c), inner-model theory and the covering lemma. Two deferred tracks meet here, set theory beyond choice and measure theory.

• Why it matters here. It is the cleanest example in general topology of a natural question whose answer is not merely independent but genuinely expensive: unlike CH (The continuum hypothesis, and what this page does not prove ↗), one side of it cannot be obtained from Con(ZFC) at all. Any metrisation page in this library must therefore state Bing's and Nagata-Smirnov's theorems and stop; the tempting further step, dropping collectionwise normality to plain normality, is not available and cannot be made available by working harder.

• Conditional discipline. (a) and (b) are implications from stated hypotheses; the consistency of PMEA is relative to a large-cardinal hypothesis strictly stronger than Con(ZFC), and (c) is an implication between consistency strengths. Nothing here asserts that measurable or strongly compact cardinals exist.

A regular space is an S-space if it is hereditarily separable but not Lindelöf, and an L-space if it is hereditarily Lindelöf but not separable. Since separability and the Lindelöf property are dual in most elementary respects, the historical expectation was that the two existence questions would have the same answer. They do not.

(a) An L-space exists in ZFC. Justin Moore (announced 2005, published 2006) constructs one outright, with no extra axiom. The space is a topology $\tau[X]$ on an uncountable set $X \subseteq \omega_1$ of countable ordinals, built from a colouring obtained by analysing oscillations of a coherent sequence $\langle e_\alpha : \alpha < \omega_1 \rangle$ of finite-to-one functions, along the lower trace of Todorcevic's minimal walks on countable ordinals.

(b) It is consistent that no S-space exists. Todorcevic proved that the proper forcing axiom implies there are no S-spaces. Since PFA is consistent relative to a supercompact cardinal, "there are no S-spaces" is consistent relative to that large-cardinal hypothesis.

(c) S-spaces do exist under other hypotheses, for instance under CH, so (b) is a genuine independence and not a theorem.

• Not proved in this library. Neither construction is carried out here. The library now develops separability, the Lindelöf property and their hereditary forms, but it does not develop the minimal-walk and oscillation machinery for the ZFC L-space or the forcing machinery for the S-space consistency result.

• What would prove it. For (a), the combinatorics of minimal walks on countable ordinals and oscillation theory, which is ordinary ZFC but rests on the ordinal machinery and on a substantial theory of colourings. For (b), the proper forcing axiom, hence proper forcing, iteration with countable support, and a supercompact cardinal for its consistency.

• Why it matters here. It is the standard warning against arguing by duality in general topology. "Hereditarily separable" and "hereditarily Lindelöf" look like mirror images, and the corresponding existence questions are not mirror images at all: one is settled outright in ZFC and the other is independent. Any page in this library that states such a duality must therefore state it for the specific properties proved, and never as a general principle. Note that the countability notions the library does have (Finite, countably infinite, countable, uncountable ↗, $\mathbb{R}$ is uncountable (Cantor's nested intervals, 1874) ↗) are untouched by this: nothing here is a statement about $\mathbb{R}$, whose separability and Lindelöf property are both elementary.

• Conditional discipline. (a) is a ZFC theorem, cited and not proved. (b) is a relative consistency statement whose hypothesis is strictly stronger than Con(ZFC). Nothing here asserts PFA or the existence of a supercompact cardinal.

Dowker's theorem (1951) characterises the normal spaces whose product with the unit interval is again normal: for a normal $X$, the product $X \times [0,1]$ is normal if and only if $X$ is countably paracompact. A Dowker space is a normal space that is not countably paracompact, that is, a witness that the hypothesis cannot be dropped.

(a) Dowker spaces exist in ZFC. M. E. Rudin (1971) gives one, a subspace of a product of ordinal spaces; its cardinality is $\aleph_\omega^{\aleph_0}$.

(b) Smaller ZFC examples. Balogh (1996) constructs a Dowker space of cardinality the continuum. Kojman and Shelah (1998) construct one of cardinality $\aleph_{\omega+1}$, using pcf theory.

(c) The $\aleph_1$ case is open. Whether ZFC alone proves the existence of a Dowker space of cardinality $\aleph_1$ is not known. Such spaces are known to exist under extra hypotheses, the standard ones being the continuum hypothesis and the diamond principle.

• Not proved in this library. The library now has a substantial general- topology track, including separation, compactness and paracompactness, but it does not construct a Dowker space or develop the specialised countable-paracompactness and set-theoretic machinery used by the cited constructions.

• What would prove it. All three constructions are ZFC arguments, so no forcing is needed for (a) and (b), but they need ordinal and cardinal arithmetic well past Cardinal (initial ordinal) and cardinality ↗, the ordinal spaces, and in the Kojman-Shelah case Shelah's pcf theory. Clause (c) is an open problem and no track would discharge it.

• Why it matters here. Dowker's theorem is the reason "normal" is not a well-behaved property under products, and a theorem with a hypothesis and no witness is a theorem no reader can calibrate. Recording the ZFC examples is what lets a later separation or product page state Dowker's theorem honestly: the countable paracompactness hypothesis is not removable, and the smallest known ZFC witness is large. Recording (c) is what stops that page from claiming a small witness exists.

• Conditional discipline. (a) and (b) are ZFC theorems, cited and not proved. (c) is a statement about the current state of knowledge, not a mathematical claim, and is recorded so no later page asserts more than is known.