Pipeline-generated

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Choice Strength in Baire, Urysohn, Stone, and Tychonoff

1 · Prerequisites

2 · Summary

This page retrofits the choice-theoretic content of the library's catalogue remarks on the Baire category theorem, Urysohn's lemma, Stone's theorem, and the Tychonoff product theorem with proof-bearing items. It is built on the Baire-development, countability, separation-axiom, and paracompactness pages listed in its prerequisites.

The spine is as follows. Separable complete metric spaces are Baire in Zermelo-Fraenkel set theory; the complete-metric form of the Baire theorem is exactly dependent choice, and the compact-Hausdorff form is exactly dependent multiple choice. Products of compact Hausdorff spaces are Baire exactly under dependent choice. Urysohn's lemma follows from dependent multiple choice, while countable choice and the Boolean prime ideal principle are each consistent with its failure, together with the failure of bounded Tietze extension for the same continuum. Stone's theorem for metric spaces follows from the axiom of choice, fails in models of ZF plus dependent choice and of ZF plus the Boolean prime ideal principle, and the effective per-cover refinement strengthening of its hypothesis implies choice. For the product theorem, products of cofinite spaces are compact exactly under the Boolean prime ideal principle, while products of compact T1 spaces and arbitrary products of compact spaces are compact exactly under choice.

Every item states its ambient theory, and the two status remarks record the questions left open: whether Urysohn's lemma implies dependent multiple choice, and the exact strength of the ordinary Stone theorem over ZF.

3 · Logical flowchart

4 · Definitions, theorems and proofs

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

Dependent multiple choice in finite-level tree form

Definition

Work in $Z F$ (The natural numbers $N$ (von Neumann)); no choice principle is used or named in this definition beyond the one being introduced. Let $A$ be a set.

Nodes. A node over $A$ is a function $t : n \to A$ whose domain is a natural number $n$ (A function is a relation $f$ with $(a, b) \in f$ and $(a, c) \in f$ implying $b = c$ ; $f : A \to B$ , the value $f (a)$ , domain and codomain). Its length is $dom t = n$ and its entries are the values $t (0), \dots, t (n - 1)$ . The unique node of length $0$ is the empty sequence $\emptyset$ . For a node $t$ of length $n$ , a natural $m \leq n$ and $a \in A$ write

$t ↾ m : = t \cap (m \times A), t^{⌢} a : = t \cup {(n, a)},$

the initial segment of length $m$ and the node of length $n + 1$ obtained by appending $a$ . A node $u$ is an immediate successor of $t$ when $u = t^{⌢} a$ for some $a \in A$ , and a proper extension of $t$ when $t = u ↾ dom t$ and $dom u > dom t$ .

Trees. A tree of height $ω$ on $A$ is a set $T$ of nodes over $A$ such that $\emptyset \in T$ and $t ↾ m \in T$ whenever $t \in T$ and $m \leq dom t$ . Its $n$ -th level is

$T_{n} : = {t \in T : dom t = n} .$

The tree has nonempty levels when $T_{n} \neq \emptyset$ for every $n \in N$ , and finite levels when each $T_{n}$ is finite (The cardinality $∣ A ∣$ of a finite set). It is pruned, or serial, when every node has a proper extension in $T$ . A subtree of $T$ is a subset of $T$ that is itself a tree of height $ω$ on $A$ .

The $R$ -chain tree. Let $R \subseteq A \times A$ be a binary relation on $A$ and call $R$ serial on $A$ when every $x \in A$ has a successor: some $y \in A$ with $x R y$ . The $R$ -chain tree is

$T_{R} : = {t : t a node over A and t (i) R t (i + 1) for every i + 1 < dom t} .$

It is a tree of height $ω$ on $A$ . For $A \neq \emptyset$ it is pruned exactly when $R$ is serial on $A$ : a node of positive length has a proper extension precisely when its last entry $t (dom t - 1)$ has an $R$ -successor, the empty node has the one-entry node $(a)$ as an extension for every $a \in A$ , and the one-entry node $(a)$ has a proper extension exactly when $a$ has an $R$ -successor. For $A = \emptyset$ the equivalence fails: then $T_{R} = {\emptyset}$ , $R$ is vacuously serial on $A$ , and the empty node has no proper extension. If $R$ is serial on $A$ and $A \neq \emptyset$ , then every level of $T_{R}$ is nonempty, by iterating the successor condition.

Successor menus. Let $R$ again be a relation on $A$ . A successor menu sequence for $R$ is a sequence $(F_{n})_{n \in N}$ of nonempty finite subsets $F_{n} \subseteq A$ such that

$for every n and every x \in F_{n} there is y \in F_{n + 1} with x R y .$

It is coherent when in addition every $y \in F_{n + 1}$ has a predecessor in $F_{n}$ : some $x \in F_{n}$ with $x R y$ . Downward closure makes the levels of any subtree of $T_{R}$ coherent in this predecessor sense, but it does not supply the forward-successor condition: a subtree with nonempty levels may have leaves. Its levels form a successor menu sequence only after restricting to nodes that continue to later levels, as carried out in the equivalence proof.

The two forms of DMC. Dependent multiple choice in tree form is the assertion

every pruned tree of height $ω$ on every set $A$ whose levels are nonempty has a subtree with nonempty finite levels;

and dependent multiple choice in successor-menu form is the assertion

every serial relation on every nonempty set admits a successor menu sequence.

The menu form is the one recorded in Multiple choice and dependent multiple choice; the tree form is the one David Fremlin writes as ${D M C}^{'}$ and attributes to Blass (1979). The next theorem proves that the two assertions are equivalent over $Z F$ .

Remarks

Pruning is a real condition. A subtree of a pruned tree need not be pruned: a node of a subtree with nonempty levels may have no extension inside the subtree. That is why the tree form above asks for the levels to be nonempty and finite but not for the subtree to be pruned, and why the proof of the equivalence has to prune the menus it obtains from the other form.
Why the empty set is excluded from the menu form. A serial relation on $A = \emptyset$ is serial vacuously, and there are no nonempty subsets of $A$ to serve as menus, so the menu form is stated for nonempty $A$ . The tree form has no such exclusion: the tree consisting of the empty sequence alone has an empty level $1$ and is not a counterexample, because it is not pruned.
The name DMC. The abbreviation is used for the principle over $Z F$ and is never asserted to be a theorem of $Z F$ ; the strictly weaker position of DMC among the choice principles is recorded separately on this page and is not part of this definition.

TheoremStatement: Literature-sourcedProof: Literature-sourcedjudge pass (gpt-5.6-terra)audited 2026-09-22Open item page →

The tree and successor-menu formulations of DMC are equivalent

Statement

Over $Z F$ the following two assertions are equivalent (Dependent multiple choice in finite-level tree form):

Tree form. Every pruned tree of height $ω$ on every set whose levels are nonempty has a subtree with nonempty finite levels.
Successor-menu form. Every serial relation on every nonempty set admits a successor menu sequence.

Assertion 2 is the principle recorded in Multiple choice and dependent multiple choice. No choice principle is used in either direction: the two assertions are equivalent over $Z F$ , and the proof constructs every object it needs from the ones already given.

Facts & Assumptions

Given: The two assertions of the statement, and their vocabulary as fixed in Dependent multiple choice in finite-level tree form.

[F1]

DMC in menu form: if $R$ is serial on a nonempty set $A$ , there is a sequence $(F_{n})_{n \in N}$ of nonempty finite subsets of $A$ with every $x \in F_{n}$ having an $R$ -successor in $F_{n + 1}$ (Multiple choice and dependent multiple choice).

[F2]

A subtree of a tree of height $ω$ over $A$ is a subset closed under initial segments containing the empty sequence, and its levels are its nodes of each length. Every immediate extension of a node $t$ has the form $t^{⌢} a$ for some $a \in A$ and there may be many such extensions; conversely, a node $u$ of positive length has the unique immediate predecessor $u ↾ (dom u - 1)$ (Dependent multiple choice in finite-level tree form).

[L1]

Functions are sets of ordered pairs and are equal exactly when they have the same domain and the same values. In particular, the restriction $u ↾ n$ of a node $u$ to the unique domain $n$ is determined by $u$ ; this makes predecessors unique, but does not make distinct immediate extensions of the same node equal (A function is a relation $f$ with $(a, b) \in f$ and $(a, c) \in f$ implying $b = c$ ; $f : A \to B$ , the value $f (a)$ , domain and codomain).

[L2]

A subset of a finite set is finite, and a finite union of finitely many finite sets is finite; a nonempty finite set has an element (The cardinality $∣ A ∣$ of a finite set, A subset of a finite set is finite, with $∣ B ∣ \leq ∣ A ∣$ , and equality holds if and only if $B = A$ , The sum rule: a finite disjoint union is finite with $∣ A \cup B ∣ = ∣ A ∣ + ∣ B ∣$ and $∣ ⋃_{i \in I} A_{i} ∣ = \sum_{i \in I} ∣ A_{i} ∣$ , and a sum over a finite index set splits along a partition).

[L3]

Every nonempty set of natural numbers has a least element, and the natural numbers satisfy induction (The natural numbers $N$ (von Neumann)).

Proof

technique · direct

1.1

Assume the tree form of the statement.

assume-hyp

1.2

Assume the successor-menu form of the statement.

assume-hyp

2.1

Under step 1.1, let $A$ be a nonempty set and let $R$ be serial on $A$ ; the $R$ -chain tree $T_{R}$ is a pruned tree of height $ω$ with nonempty levels, so by the tree form there is a subtree $T^{'}$ of $T_{R}$ whose levels $T_{n}^{'}$ are nonempty and finite.

step 1.1F2L1

2.2

Under step 1.2, let $T$ be a pruned tree of height $ω$ on a set $A$ with nonempty levels, and let $R \subseteq T \times T$ be the relation of immediate succession, $t R u$ exactly when $u = t^{⌢} a$ for some $a \in A$ .

step 1.2F2

3.1

Under step 2.1 the given subtree $T^{'}$ need not be pruned, so prune it first: put $T^{''} : = {t \in T^{'} : for every j > dom t there is v \in T_{j}^{'} with t \subseteq v}$ . Then $T^{''}$ is a subtree of $T_{R}$ contained in $T^{'}$ (it contains the empty sequence, since $T^{'}$ has nonempty levels, and it is closed under initial segments, since a shorter initial segment of $t \in T^{''}$ is extended by the same nodes that extend $t$ ), and each level $T_{n}^{''} \subseteq T_{n}^{'}$ is finite. Each level $T_{n}^{''}$ is also nonempty: otherwise every $t \in T_{n}^{'}$ would have a least level $j (t) > n$ with no extension in $T^{'}$ , and with $j^{*} : = \max {j (t) : t \in T_{n}^{'}}$ (a maximum over the finite set $T_{n}^{'}$ , whose members are naturals) no node of $T_{j^{*}}^{'}$ extends any member of $T_{n}^{'}$ , although every $v \in T_{j^{*}}^{'}$ is an extension of $v ↾ n \in T_{n}^{'}$ . Finally every node $t \in T_{n}^{''}$ has an extension in $T_{n + 1}^{''}$ . If a one-step extension in $T_{n + 1}^{'}$ already belongs to $T^{''}$ , there is nothing to prove. Otherwise suppose every one-step extension of $t$ in $T_{n + 1}^{'}$ lies outside $T^{''}$ ; their set $B$ is nonempty because $t \in T^{''}$ , and it is finite as a subset of $T_{n + 1}^{'}$ . Each $u \in B$ has a least dying level $j (u) > n + 1$ with no extension in $T^{'}$ . Put $j^{+} : = \max {j (u) : u \in B}$ . Since $t \in T^{''}$ , take $w \in T_{j^{+}}^{'}$ extending $t$ , and let $u_{0} : = w ↾ (n + 1)$ . Then $u_{0} \in B$ by the supposition, but $w$ gives an extension of $u_{0}$ through its dying level $j (u_{0}) \leq j^{+}$ , a contradiction. Now put $F_{n} : = {t (n) : t \in T_{n + 1}^{''}}$ , the set of last entries of the nodes of $T^{''}$ of length $n + 1$ : each $F_{n}$ is nonempty and finite, and if $x \in F_{n}$ is the last entry of $t \in T_{n + 1}^{''}$ then $t$ has an extension in $T_{n + 2}^{''}$ , so $x$ has an $R$ -successor in $F_{n + 1}$ , namely the last entry of that extension.

step 2.1F2L2L3

3.2

Under step 2.2: the relation $R$ is serial on $T$ , because $T$ is pruned and every proper extension of a node of length $n$ passes through an immediate successor in $T$ by [F2]; the set $T$ is nonempty, since it contains the empty sequence.

step 2.2F2

4.1

Under step 2.2, continuing: by step 3.2 and the successor-menu form there are nonempty finite sets $F_{n} \subseteq T$ with every $x \in F_{n}$ having an $R$ -successor in $F_{n + 1}$ ; define $G_{0} : = F_{0}$ and $G_{n + 1} : = {u \in F_{n + 1} : u = x^{⌢} a for some x \in G_{n} and some a}$ .

step 3.2F1L3

4.2

Under step 2.1, continuing: the sets $F_{n}$ of step 3.1 are nonempty finite subsets of $A$ ; extracting the last entry of each node uses only the defining data of the node, so no selection is made, and the successor condition verified in step 3.1 is exactly the menu condition of [F1].

step 3.1F1L1

5.1

Under step 4.1: by induction on $n$ , each $G_{n}$ is a nonempty finite subset of $F_{n}$ . The case $n = 0$ is $G_{0} = F_{0}$ . If $G_{n}$ is nonempty, choose $x \in G_{n} \subseteq F_{n}$ ; the menu property supplies an $R$ -successor $u \in F_{n + 1}$ , and the definition of $G_{n + 1}$ puts this $u$ in $G_{n + 1}$ . Finiteness follows from $G_{n + 1} \subseteq F_{n + 1}$ . Moreover every $u \in G_{n + 1}$ has a predecessor $x \in G_{n}$ by definition, and that predecessor is the canonical restriction of $u$ by [F2]; so the menus $G_{n}$ are coherent.

step 4.1F2L2L3

5.2

Under step 3.1 and step 4.2 we have produced a successor menu sequence for the arbitrary serial relation $R$ on the arbitrary nonempty set $A$ ; this is assertion 2 of the statement, so the tree form implies the successor-menu form.

step 3.1step 4.2F1

6.1

Under step 4.1 and step 5.1, put $T^{'} : = {t \in T : t \subseteq s for some s \in ⋃_{n} G_{n}}$ , the downward closure in $T$ of the coherent menus. Then $T^{'}$ is a subtree of $T$ by [F2]. Every level $T_{m}^{'}$ is nonempty: for this fixed $m$ , choose $x \in G_{0}$ and apply the successor half of coherence only $m$ times, by finite induction, to obtain $s \in G_{m}$ extending $x$ . Since each step is an immediate extension, $dom s = dom x + m \geq m$ , and $s ↾ m \in T_{m}^{'}$ . This is one finite existence argument for the arbitrary level $m$ , not a simultaneous choice of an infinite successor sequence.

step 5.1F2L3

7.1

Under step 6.1, each level $T_{m}^{'}$ is finite. Indeed let $D : = {dom s : s \in G_{0}}$ , a finite set of natural numbers by [L2]. If $t \in T^{'}$ has length $m$ and $t \subseteq s$ with $s \in G_{k}$ , then iterating the canonical predecessor restriction from [F2] and [L1] gives $s ↾ (dom s - j) \in G_{k - j}$ for every $j \leq k$ . If $m \geq dom s - k$ , set $j : = dom s - m \leq k$ and $d : = dom s - k \in D$ ; then $t = s ↾ m \in G_{k - j} = G_{m - d}$ . If instead $m < dom s - k$ , then $r : = s ↾ (dom s - k) \in G_{0}$ has length greater than $m$ and $t = r ↾ m$ . Hence $T_{m}^{'} \subseteq ⋃ {G_{m - d} : d \in D, d \leq m} \cup {r ↾ m : r \in G_{0}, dom r > m}$ , a union of finitely many finite sets, which is finite.

step 5.1step 6.1F2L1L2

8.1

Under step 6.1 and step 7.1 the subtree $T^{'}$ of the arbitrary pruned tree $T$ has nonempty finite levels; this is assertion 1 of the statement, so the successor-menu form implies the tree form.

step 6.1step 7.1

9.1

Steps 5.2 and 8.1 prove the two implications between assertions 1 and 2, so the two formulations of dependent multiple choice are equivalent over $Z F$ .

step 5.2step 8.1∎

LemmaStatement: AI-adaptedProof: AI-adaptedjudge pass (gpt-5.6-terra)audited 2026-09-22Open item page →

A nonempty countable set has a padded enumeration in ZF

Statement

In $Z F$ , every nonempty at most countable set $D$ (Finite, countably infinite, countable, uncountable) is the range of a sequence $s : N \to D$ (The natural numbers $N$ (von Neumann)). The empty set is treated separately and is not asserted to be the range of an $N$ -indexed sequence.

Conventions. $N$ contains $0$ , and a natural number $m$ is the set ${0, \dots, m - 1}$ of its predecessors. A sequence in $D$ is a function with domain $N$ and values in $D$ .

Facts & Assumptions

Given: A nonempty at most countable set $D$ .

[L1]

A nonempty set $A$ is at most countable if and only if there is a surjection $s : N \to A$ ; the forward direction is the one used here and its proof is explicit in the cited item (A nonempty set is at most countable iff it is a surjective image of $N$ , Injection, surjection, bijection).

[L2]

$D$ is at most countable exactly when $D$ is finite, that is $D \approx m$ for some $m \in N$ , or countably infinite, that is $D \approx N$ (Finite, countably infinite, countable, uncountable).

[L3]

$0 = \emptyset$ and $m \neq 0$ exactly when $0 \in m$ , for $m \in N$ (The natural numbers $N$ (von Neumann)).

Proof

technique · cases, on the two alternatives of at most countability supplied by [L2]

1.1

Assume $D$ is nonempty and at most countable; by [L1] it suffices to produce a surjection $N \to D$ explicitly from the two alternatives of [L2].

givenL1L2

1.2

Case 1: assume $D$ is countably infinite, so that there is a bijection $e : N \to D$ ; case 2: assume $D$ is finite, so that there is $m \in N$ with a bijection $e : m \to D$ .

assume-caseassume-case

2.1

In case 1, take $s : = e$ ; it is a function $N \to D$ and it is surjective, so its range is $D$ ; no choice was used, since $e$ was already given.

step 1.2L2

2.2

In case 2, since $D$ is nonempty and $e : m \to D$ is bijective, $m \neq 0$ : otherwise $D \approx m = 0 = \emptyset$ by [L3], contradicting that $D$ has an element.

step 1.2L3

3.1

In case 2, continuing, define $s : N \to D$ by the two clauses $s (n) : = e (n)$ for $n \in m$ and $s (n) : = e (0)$ for $n \in N ∖ m$ ; this is well defined because $m = {0, \dots, m - 1}$ and $0 \in m$ by step 2.2 and [L3], so $e (0) \in D$ is available as the constant value.

step 2.2L2L3

4.1

In case 2, continuing, $s$ has range $D$ : if $d \in D$ then $d = e (k)$ for some $k \in m$ because $e$ is surjective, and then $s (k) = e (k) = d$ by step 3.1; conversely every value of $s$ is a value of $e$ , hence lies in $D$ .

step 3.1L2

5.1

Every nonempty at most countable $D$ therefore falls under case 1 or case 2 and is the range of the explicitly defined sequence $s$ of step 2.1 or of step 4.1; no choice principle was used in either case.

step 1.2step 2.1step 4.1cases-exhaustive∎

Remarks

Why the statement separates the empty set. The cited equivalence of [L1] requires $A \neq \emptyset$ : there is no function from $N$ onto $\emptyset$ . The downstream Baire theorem therefore disposes of the empty ambient space before invoking this lemma, rather than manufacturing a sequence into the empty set.
The padding is what makes the finite case a sequence. A finite bijection $e : m \to D$ is not defined on the whole of $N$ ; repeating its value at $0$ is the canonical way to extend it, and it needs the one fact that $m$ is nonempty.

TheoremStatement: Literature-sourcedProof: AI-adaptedaudited 2026-09-22Open item page →

Separable complete metric spaces are Baire in ZF

Statement

In $Z F$ , every separable (Separability: the existence of an at most countable dense subset) complete (Complete metric space: every Cauchy sequence converges in the space) metric space (Metric space: $d (x, y) = 0$ iff $x = y$ , symmetry, and the triangle inequality; pseudometric and ultrametric) is a Baire space (Baire space: a topological space in which every countable intersection of dense open subsets is dense).

The form of the conclusion used below. A space $X$ is Baire exactly when $W \cap ⋂_{n} U_{n} \neq \emptyset$ for every sequence $(U_{n})$ of dense open subsets and every nonempty open $W \subseteq X$ . No choice principle is spent: separability supplies a single at most countable dense set, the padding lemma turns it into a fixed sequence, and the recursion below selects a least index-radius pair at each stage, a definable operation.

Facts & Assumptions

Given: A separable complete metric space $(X, d)$ ; a sequence $(U_{n})_{n \in N}$ of dense open subsets of $X$ ; a nonempty open $W \subseteq X$ .

[F1]

$X$ is separable when it has an at most countable dense subset; $A$ is dense in $X$ when $B (x, r) \cap A \neq \emptyset$ for every $x$ and every $r > 0$ (Separability: the existence of an at most countable dense subset, Interior, closure, boundary, limit point, isolated point and dense subset of a metric space, Open ball, closed ball and sphere in a metric space).

[F2]

$U$ is open when every $u \in U$ has $r > 0$ with $B (u, r) \subseteq U$ ; open balls are open, and open sets are closed under finite intersections and arbitrary unions (The metric topology: a set is open when every one of its points has a ball around it inside the set; closed means open complement, Arbitrary unions and finite intersections of open sets are open, open balls are open and closed balls are closed).

[F3]

Every nonempty at most countable set is the range of a sequence $N \to D$ (A nonempty countable set has a padded enumeration in ZF, Finite, countably infinite, countable, uncountable).

[L1]

Completeness of $(X, d)$ means every Cauchy sequence in $X$ converges in $X$ (Complete metric space: every Cauchy sequence converges in the space).

[L2]

Cauchy sequences and convergence are tested by arbitrarily small positive distances; real and rational epsilon tests agree (Cauchy sequence in a metric space, Convergence of a sequence in a metric space: $x_{k} \to x$ iff $d (x_{k}, x) \to 0$ in $R$ ).

[L3]

Triangle inequality, symmetry and separation are the metric axioms; nonnegativity follows from them (Metric space: $d (x, y) = 0$ iff $x = y$ , symmetry, and the triangle inequality; pseudometric and ultrametric, Nonnegativity of a metric is a consequence of the other axioms, not an axiom).

[L4]

For every positive real $ε$ there exists an integer $m \geq 1$ with $1 / m < ε$ (For every $ε > 0$ in a complete ordered field there is a natural $n \geq 1$ with $1 / n < ε$ ).

[L5]

A specified self-map of a set with an initial state defines a unique natural-number sequence by recursion (The recursion theorem).

Proof

technique · cases, on whether the ambient space is empty

1.1

Assume $(X, d)$ is separable and complete, let $(U_{n})$ be dense open subsets of $X$ , and let $W$ be a nonempty open subset of $X$ ; the task is to produce a point of $W \cap ⋂_{n} U_{n}$ .

givenF1

1.2

Case A: $X = \emptyset$ . Case B: $X \neq \emptyset$ .

assume-caseassume-case

2.1

In case A the conclusion is vacuous and no sequence is constructed: a space with empty underlying set has no nonempty open subset, so there is no $W$ to test, and in particular no sequence into $X$ is invented.

step 1.2F1

2.2

In case B, separability gives a dense at most countable $D \subseteq X$ , and $D \neq \emptyset$ because the dense set $D$ meets the nonempty open set $X$ ; by [F3] fix a sequence $s : N \to D$ whose range is $D$ .

step 1.2F1F3

3.1

In case B, continuing, for every nonempty open $G \subseteq X$ and every real $ρ > 0$ the set of pairs $(k, m) \in N \times N$ with $m \geq 1$ , $1 / m \leq ρ$ and $\overset{ˉ}{B} (s (k), 1 / m) \subseteq G$ is nonempty. Fix $y \in G$ and $r > 0$ with $B (y, r) \subseteq G$ by [F2], choose $m \geq 1$ with $1 / m < \min (r / 3, ρ)$ by [L4], and use density of $D$ to fix $k$ with $s (k) \in B (y, 1 / m)$ . If $z \in \overset{ˉ}{B} (s (k), 1 / m)$ , then $d (z, y) \leq d (z, s (k)) + d (s (k), y) < 2 / m < r,$ so $z \in B (y, r) \subseteq G$ . Thus the required closed ball, not merely its open subball, lies in $G$ .

step 2.2F1F2L3L4

3.2

In case B, continuing, put $G_{0} : = W \cap U_{0}$ ; this set is nonempty because $W$ is nonempty open and $U_{0}$ is dense, and it is open by [F2].

step 2.2F1F2

4.1

In case B, continuing, define by recursion on $n \in N$ : given the nonempty open $G_{n}$ , let $(k_{n}, m_{n})$ be the least element of the admissible set of step 3.1 for $(G_{n}, 2^{- (n + 2)})$ , put $x_{n} : = s (k_{n})$ , $r_{n} : = 1 / m_{n}$ and $G_{n + 1} : = B (x_{n}, r_{n}) \cap U_{n + 1}$ ; use lexicographic order, taking first the least admissible $k$ and then the least admissible $m$ for that $k$ , and $G_{n + 1}$ is nonempty open because the nonempty open ball $B (x_{n}, r_{n})$ meets the dense set $U_{n + 1}$ and both sets are open.

step 3.1step 3.2F1F2L5

5.1

This recursion is a set recursion: use states $(n, G)$ with $G$ a nonempty open subset of $X$ , together with one default state. The least-pair rule defines the successor on every such state, by step 3.1 and density of $U_{n + 1}$ ; let the default state map to itself. Apply [L5] with initial state $(0, G_{0})$ . Projections and the uniquely defined least-pair function give $x_{n}, r_{n}$ . This uses no choice function.

L5step 3.1step 3.2step 4.1

5.2

In case B, continuing, put $C_{n} : = \overset{ˉ}{B} (x_{n}, r_{n})$ . By the admissibility condition of step 3.1 used at stage $n$ , $C_{n} \subseteq G_{n}$ . Hence $C_{n + 1} \subseteq G_{n + 1} = B (x_{n}, r_{n}) \cap U_{n + 1} \subseteq C_{n} .$ Each $C_{n}$ contains its already defined center $x_{n}$ , and is closed by [F2]. If $a, b \in C_{n}$ , then $d (a, b) \leq 2 r_{n} \leq 2^{- (n + 1)}$ by [L3].

step 3.1step 4.1F2L3

6.1

For $j, k \geq N$ , nesting gives $x_{j}, x_{k} \in C_{N}$ , so $d (x_{j}, x_{k}) \leq 2^{- (N + 1)}$ . These bounds tend to zero: induction gives $2^{N + 1} \geq N + 1$ , and [L4] makes $1 / (N + 1)$ eventually smaller than any positive $ε$ . Thus $(x_{n})$ is Cauchy by [L2], and completeness [L1] gives a limit $p \in X$ . No points are selected from arbitrary sets; the sequence of centers was already defined in step 5.1.

step 5.1step 5.2L1L2L4

7.1

For each fixed $N$ , every $x_{j}$ with $j \geq N$ belongs to the closed set $C_{N}$ . If $p \notin C_{N}$ , its open complement contains a ball $B (p, ε)$ by [F2], but convergence [L2] puts some $x_{j}$ , $j \geq N$ , in that ball, a contradiction. Hence $p \in ⋂_{N} C_{N}$ . If $q$ is another point of the intersection, step 5.2 gives $d (p, q) \leq 2^{- (N + 1)}$ for all $N$ , whence $d (p, q) = 0$ and $p = q$ by [L3].

step 5.2step 6.1F2L2L3

8.1

In case B, continuing, $p \in C_{0} \subseteq G_{0} = W \cap U_{0}$ . For every $n$ , step 5.2 also gives $p \in C_{n + 1} \subseteq G_{n + 1} \subseteq U_{n + 1}$ . Therefore $p \in W \cap ⋂_{n} U_{n}$ .

step 3.2step 5.2step 7.1

9.1

Either the ambient space is empty, in which case step 2.1 gives the Baire condition vacuously, or it is nonempty, in which case steps 4.1 to 8.1 produce the required point of $W \cap ⋂_{n} U_{n}$ ; the two cases exhaust the possibilities, so $(X, d)$ is Baire and the only objects used were the supplied dense set, its enumeration, and least-element selections on $N \times N$ .

step 2.1step 8.1step 4.1cases-exhaustive∎

Remarks

Where the choice would have been, and why it is not spent. The classical proof of the complete-metric Baire theorem chooses a ball inside $G_{n} \cap U_{n}$ at every stage, which is dependent choice. Here the centre is forced to be the least index of a fixed enumeration of one dense set and the radius is forced to be the least admissible value, so each stage is a definable function of the previous one and no selection principle is invoked.
Completeness is used once. It supplies the limit of the explicitly constructed center sequence in step 6.1. Closedness puts that limit in every nested ball. No general intersection theorem for arbitrary nonempty sets is invoked.

DefinitionDefinition: AI-adaptedProof: Not applicablejudge pass (gpt-5.6-terra)audited 2026-09-22Open item page →

Metacompactness: every open cover has a point-finite open refinement

Definition

A topological space $X$ (Topology on a set, open and closed sets, clopen sets, the closed-set axiomatisation, and the coarser/finer comparison) is metacompact when every open cover of $X$ has a point-finite open refinement: for every open cover $U$ of $X$ there is a family $V$ of open sets such that $V$ covers $X$ , every $V \in V$ is contained in some $U \in U$ , and every point of $X$ belongs to only finitely many members of $V$ (Refinements, locally finite families, point-finite families, and star refinements).

Point-finiteness is the only new component. Refinement and covering are those of Refinements, locally finite families, point-finite families, and star refinements; metacompactness weakens paracompactness (Paracompactness: every open cover has a locally finite open refinement, with no separation axiom built into the word) by asking the refining family to be point-finite rather than locally finite. Local finiteness implies point finiteness, so every paracompact space is metacompact, and no separation axiom is built into the word.

Remarks

Why this item exists on this page. The ZF countermodel of Stone's theorem on this page produces a metrizable space with an open cover that has no point-finite open refining cover; that is the precise failure, and it is what the relative-consistency theorem and the open-status remark state. (The empty family is a point-finite refinement in the bare containment sense, but it does not cover a nonempty space.) The word metacompact is used only as an abbreviation for that covering property.
Effectivity is a separate strengthening. A refinement is called effective when it comes equipped with a refinement map $a : V \to U$ satisfying $V \subseteq a (V)$ ; the strengthening that every open cover of every discrete metric space has an effective point-finite open refinement is equivalent to the Axiom of Choice and is treated as its own theorem below, not as part of this definition.

TheoremStatement: Literature-sourcedProof: AI-adaptedaudited 2026-09-22Open item page →

DMC makes every compact Hausdorff space Baire

Statement

$Z F + D M C$ proves that every compact Hausdorff space is a Baire space (Open cover, subcover, and compact topological space; a compact subset is a subspace that is compact in its own right, Hausdorff space: distinct points have disjoint open neighbourhoods; every metrizable space is Hausdorff and the indiscrete topology on two points is not, Baire space: a topological space in which every countable intersection of dense open subsets is dense).

DMC is the principle of Dependent multiple choice in finite-level tree form, used below in its successor-menu form: every serial relation on a nonempty set admits nonempty finite successor menus.

Facts & Assumptions

Given: A compact Hausdorff space $X$ ; a sequence $(G_{n})_{n \in N}$ of dense open subsets of $X$ ; a nonempty open $W \subseteq X$ ; the principle DMC.

[F1]

A compact Hausdorff space is regular and $T_{1}$ (A compact Hausdorff space is regular and normal, hence $T_{3}$ and $T_{4}$ , Regular spaces and $T_{3}$ spaces, with the source disagreement over whether regularity includes $T_{1}$ stated explicitly, Normal spaces and $T_{4}$ spaces, with the source disagreement over whether normality includes $T_{1}$ stated explicitly).

[F2]

Regularity in the shrinking form: if $U$ is open and $x \in U$ then there is open $V$ with $x \in V \subseteq \overline{V} \subseteq U$ (A space is regular if and only if every point has a neighbourhood base of closed neighbourhoods, if and only if $x \in U$ open gives an open $V$ with $x \in V \subseteq \overline{V} \subseteq U$ ).

[F3]

A compact space is countably compact (Countably compact, Lindel"of, sequentially compact, limit point compact and $σ$ -compact spaces, and relatively compact subsets, Compact implies countably compact, Lindel"of and limit point compact; countably compact together with Lindel"of implies compact; and, at the cost of countable or dependent choice, sequentially compact implies countably compact, countably compact implies limit point compact, and the converse holds when every singleton is closed).

[F4]

DMC: if $R$ is serial on a nonempty set $P$ , there are nonempty finite $F_{n} \subseteq P$ with every $x \in F_{n}$ having an $R$ -successor in $F_{n + 1}$ (Dependent multiple choice in finite-level tree form).

[L1]

Dense means meeting every nonempty open set; an open set is a set whose every point has an open neighbourhood inside it; closures are as in Interior, closure, boundary, exterior, derived set and isolated point in a topological space, and a set is closed exactly when its complement is open (Dense, nowhere dense and codense subsets of a topological space, and the criterion by basic open sets, Topology on a set, open and closed sets, clopen sets, the closed-set axiomatisation, and the coarser/finer comparison, Interior, closure, boundary, exterior, derived set and isolated point in a topological space).

[L2]

Finite intersections of dense open sets are dense and open, by induction on the number of factors, and finite unions of closed sets are closed (Dense, nowhere dense and codense subsets of a topological space, and the criterion by basic open sets, Interior, closure, boundary, exterior, derived set and isolated point in a topological space).

[L3]

A subset of a finite set is finite (A subset of a finite set is finite, with $∣ B ∣ \leq ∣ A ∣$ , and equality holds if and only if $B = A$ ); the empty sequence is not used as a menu.

Proof

technique · direct

1.1

Assume DMC. Let $X$ be compact Hausdorff, let $(G_{n})$ be dense open, and let $W$ be nonempty open; if $X = \emptyset$ there is no such $W$ and the Baire condition is vacuous, so assume henceforth $X \neq \emptyset$ .

givenF4

2.1

If $X = \emptyset$ the conclusion of step 1.1 is vacuous: a space with empty underlying set has no nonempty open subset, so every sequence of dense open sets trivially has dense intersection.

step 1.1L1

2.2

Assume $X \neq \emptyset$ ; by [F1] and [F2] $X$ is regular, and by [F3] it is countably compact.

step 1.1F1F2F3

2.3

Put $G_{k}^{'} : = ⋂_{j < k} G_{j}$ for $k \in N$ , so that $G_{0}^{'} = X$ , each $G_{k}^{'}$ is dense and open by [L2], and $G_{k + 1}^{'} \subseteq G_{k}^{'}$ .

step 1.1L2

2.4

Let $V$ be the family of nonempty open subsets of $W$ .

step 1.1L1

3.1

Define $U ≻ V$ for $U, V \in V$ to mean that there is $k$ with $\overline{V} \subseteq U \cap G_{k}^{'}$ and $U \subseteq̸ G_{k}^{'}$ . If some $U \in V$ satisfies $U \subseteq G_{k}^{'}$ for every $k$ , then $U \subseteq W \cap ⋂_{k} G_{k} \neq \emptyset$ and the conclusion already holds; assume therefore that every $U \in V$ fails this, and note that the relation $≻$ is then serial on $V$ : given $U \in V$ , fix $x \in U$ with $x \notin G_{k}^{'}$ for some $k$ , and fix $y \in U \cap G_{k}^{'}$ , which is nonempty because $G_{k}^{'}$ is dense and $U$ is nonempty open; by step 2.2 and [F2] there is nonempty open $V$ with $V \subseteq \overline{V} \subseteq U \cap G_{k}^{'}$ , and $V \subseteq U \subseteq W$ so $V \in V$ and $U ≻ V$ .

step 2.2step 2.3step 2.4F2L1L2

4.1

Assume from now on that the first alternative of step 3.1 fails, so that $≻$ is serial on the nonempty $V$ .

step 3.1

5.1

Apply DMC of [F4] to $≻$ on $V$ : there are nonempty finite sets $V_{n} \subseteq V$ with every $U \in V_{n}$ having a $≻$ -successor in $V_{n + 1}$ .

step 4.1F4

6.1

Prune the menus: put $V_{0}^{'} : = V_{0}$ and $V_{n + 1}^{'} : = {V \in V_{n + 1} : U ≻ V for some U \in V_{n}^{'}}$ . Then each $V_{n}^{'}$ is a nonempty finite subset of $V_{n}$ : nonemptiness is by induction, since each $U \in V_{n}^{'}$ has a $≻$ -successor in $V_{n + 1}$ which then lies in $V_{n + 1}^{'}$ , and finiteness is [L3].

step 5.1L3

7.1

Induction on $n$ : every $U \in V_{n}^{'}$ satisfies $\overline{U} \subseteq G_{n}^{'}$ . For $n = 0$ this is $\overline{U} \subseteq X = G_{0}^{'}$ . For the step, let $V \in V_{n + 1}^{'}$ and fix $U \in V_{n}^{'}$ with $U ≻ V$ ; then $\overline{V} \subseteq U \cap G_{k}^{'}$ for some $k$ with $U \subseteq̸ G_{k}^{'}$ . By the induction hypothesis $U \subseteq \overline{U} \subseteq G_{n}^{'}$ , so $k > n$ : otherwise $G_{k}^{'} \supseteq G_{n}^{'} \supseteq U$ , contradicting $U \subseteq̸ G_{k}^{'}$ . Hence $\overline{V} \subseteq G_{k}^{'} \subseteq G_{n + 1}^{'}$ .

step 3.1step 6.1step 2.3

8.1

Put $W_{n} : = ⋃ V_{n}^{'}$ , a nonempty set with $W_{n} \subseteq G_{n}^{'}$ by step 6.1, and $W_{n + 1} \subseteq W_{n}$ : every $V \in V_{n + 1}^{'}$ satisfies $V \subseteq \overline{V} \subseteq U$ for some $U \in V_{n}^{'} \subseteq W_{n}$ . Put $K_{n} : = ⋃ {\overline{V} : V \in V_{n}^{'}}$ , a nonempty closed set by [L2], with $K_{n + 1} \subseteq W_{n} \subseteq K_{n}$ and $K_{n} \subseteq G_{n}^{'}$ .

step 6.1step 7.1L2

9.1

The sequence $K_{n}$ is a decreasing sequence of nonempty closed subsets of the countably compact space $X$ of step 2.2, so $⋂_{n} K_{n} \neq \emptyset$ : otherwise the open sets $X ∖ K_{n}$ would cover $X$ , and a finite subcover $X ∖ K_{n_{1}}, \dots, X ∖ K_{n_{m}}$ would give $K_{\max n_{j}} = \emptyset$ by [L2], contradicting nonemptiness.

step 2.2step 8.1F3L2

10.1

Fix $x \in ⋂_{n} K_{n}$ ; then $x \in K_{1} \subseteq W_{0} \subseteq W$ by steps 7.1 and 8.1, so $x \in W$ , and for every $n$ we have $x \in K_{n + 1} \subseteq W_{n} \subseteq G_{n}^{'} \subseteq G_{n - 1}$ for $n \geq 1$ , so $x \in ⋂_{n} G_{n}$ ; thus $W \cap ⋂_{n} G_{n} \neq \emptyset$ .

step 8.1step 9.1

11.1

Steps 2.1 and 10.1 cover the empty and nonempty cases of the ambient space, and the only choice principle used was DMC in step 5.1; hence every compact Hausdorff space is Baire.

step 2.1step 10.1F4∎

Remarks

Which hypothesis of the source is used. Fossy and Morillon state the result for countably compact regular spaces; compactness makes the space regular and countably compact in step 2.2, and countable compactness gives the common point of the decreasing closed sets in step 9.1. Hausdorffness is used only through the compact-Hausdorff regularity theorem.
Why the sets $G_{k}^{'}$ are not closed. They are finite intersections of dense open sets, hence dense and open, and they are decreasing; the closed sets whose intersection is taken in step 9.1 are the finite unions of closures of the pruned menus, which is why the pruning of step 6.1 is needed.

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

Compact Hausdorff Baire implies DMC

Statement

Over $Z F$ , if every compact Hausdorff space is a Baire space, then DMC holds (Dependent multiple choice in finite-level tree form).

The proof follows the dichotomy of Fossy and Morillon, in the form given by Fremlin: for a pruned tree $T$ one forms the product of the one-point compactifications of $T$ and considers the closed set $K$ of weakly increasing points. If $K$ is compact, Baireness of a compact Hausdorff space produces a branch of $T$ ; if $K$ is not compact, compactness failure of $K$ produces, by way of the finite-intersection property, finite levels of a subtree of $T$ .

Facts & Assumptions

Given: The hypothesis that every compact Hausdorff space is Baire; a pruned tree $T$ of height $ω$ on a set $A$ whose levels are nonempty.

[F1]

DMC in tree form is equivalent over $Z F$ to DMC in successor-menu form, so proving the tree form suffices (The tree and successor-menu formulations of DMC are equivalent, Dependent multiple choice in finite-level tree form).

[F2]

The one-point compactification $X^{*} = X \cup {\infty}$ of a space $X$ is compact and contains $X$ as an open subspace, is Hausdorff when $X$ is locally compact Hausdorff, and $X$ is dense in $X^{*}$ exactly when $X$ is not compact (The one-point (Alexandroff) compactification $X^{*} = X \cup {\infty}$ , whose open sets are the open sets of $X$ together with the complements in $X^{*}$ of the closed compact subsets of $X$ , $X^{*}$ is compact and contains $X$ as an open subspace; $X$ is dense in $X^{*}$ exactly when $X$ is not compact; and $X^{*}$ is Hausdorff exactly when $X$ is locally compact and Hausdorff).

[F3]

A discrete space is locally compact and Hausdorff, and a product of Hausdorff spaces is Hausdorff; Hausdorffness is hereditary to subspaces (The discrete, indiscrete, cofinite, cocountable, particular-point and Sierpinski topologies, Locally compact topological space: every point has a compact neighbourhood; and what this says in a metric space, Arbitrary products preserve $T_{0}$ , $T_{1}$ , and Hausdorffness, $T_{0}$ , $T_{1}$ , and Hausdorffness are hereditary, Hereditary, open-hereditary and closed-hereditary properties of topological spaces).

[F4]

A space is compact if and only if every family of closed subsets with the finite intersection property has nonempty intersection (A space is compact exactly when every family of closed subsets with the finite intersection property has nonempty intersection, Finite intersection property).

[L1]

Baireness: the intersection of every sequence of dense open sets is dense (Baire space: a topological space in which every countable intersection of dense open subsets is dense); a subset of a compact space is closed exactly when its complement is open, and closed subspaces with the subspace topology are what the hypothesis applies to (Subspace topology: the traces of the open sets, its closed sets and its bases, the continuity of the inclusion, and the characteristic property of a map into a subspace, Open cover, subcover, and compact topological space; a compact subset is a subspace that is compact in its own right).

[L2]

Nodes of $T$ are functions on a natural number, a node may have many immediate successors, but each node of length $n + 1$ has the unique length- $n$ predecessor obtained by restriction, and the levels $T_{n}$ are the nodes of length $n$ (Dependent multiple choice in finite-level tree form, The natural numbers $N$ (von Neumann)).

[F5]

Finite choices are available in ZF: fix a listing of the particular finite index set and apply Every natural-number-indexed list of nonempty sets has a choice function on its family of values; no family of such listings is selected. Subsets of finite sets are finite (A subset of a finite set is finite, with $∣ B ∣ \leq ∣ A ∣$ , and equality holds if and only if $B = A$ ).

Proof

technique · direct

1.1

Assume every compact Hausdorff space is Baire, let $T$ be a pruned tree of height $ω$ with nonempty levels on a set $A$ , and let $\infty$ be a point outside $T$ ; it suffices by [F1] to produce a subtree of $T$ with nonempty finite levels.

givenF1

2.1

Give $T$ the discrete topology and let $T^{*} : = T \cup {\infty}$ be its one-point compactification; by [F3] the discrete $T$ is locally compact Hausdorff, so $T^{*}$ is compact Hausdorff by [F2], and it is nonempty because $\infty \in T^{*}$ . In the discrete space a compact subset is finite: its singleton cover has a finite subcover. Conversely finite subsets are compact by finite choices from a cover. Thus the neighbourhoods of $\infty$ are exactly the complements of finite subsets of $T$ .

step 1.1F2F3

3.1

Let $X : = (T^{*})^{ω}$ with the product topology; by [F3] $X$ is Hausdorff, and $X$ is nonempty because the constant- $\infty$ function is a member.

step 2.1F3

4.1

Let $K \subseteq X$ be the set of those $x$ with: for all $m < n$ , either $x (m) = \infty$ , or $x (n) = \infty$ , or $x (m), x (n) \in T$ and $x (m)$ is a proper initial segment of $x (n)$ .

step 3.1L2

5.1

$K$ is closed in $X$ : its complement is the union, over $m < n$ and $s, t \in T$ for which $s$ is not a proper initial segment of $t$ , of the two-coordinate cylinders ${x : x (m) = s, x (n) = t}$ . Each such cylinder is open because every $s \in T$ is an isolated point of $T^{*}$ , so the complement of $K$ is open. Hence $K$ is a closed subspace of the Hausdorff space $X$ , and is Hausdorff by [F3]; it is nonempty because the constant sequence with value $\infty$ lies in $K$ .

step 3.1step 4.1F3L2

5.2

For $n \in N$ put $G_{n} : = {x \in K : x (i) \neq \infty for some i \geq n}$ , a subset of $K$ .

step 4.1

6.1

Each $G_{n}$ is open in $K$ : it is the union over $i \geq n$ and $t \in T$ of the sets $K \cap {x : x (i) = t}$ , and each ${x : x (i) = t}$ is a basic open set of the product because ${t}$ is open in the discrete space $T$ .

step 5.2step 2.1L2

6.2

Case B: $K$ is not compact. Choose an open cover of $K$ with no finite subcover, and refine it by taking all canonical basic product cylinders $W \subseteq X$ whose trace $K \cap W$ is contained in a member of the cover; here the coordinate restrictions in $W$ may be taken to be a singleton ${t}$ , $t \in T$ , or a cofinite neighbourhood of $\infty$ . This is still a cover of $K$ with no finite subcover. Let $E$ consist of all finite intersections of $X$ , the closed cylinder complements $X ∖ W$ , and all constraint complements $X ∖ {x : x (m) = s, x (n) = t}$ for $m < n$ and $s, t \in T$ with $s$ not a proper initial segment of $t$ . Every such generator is a closed member of the finite-coordinate cylinder algebra. Every finite intersection is nonempty: choose in $K$ a point outside the finitely many $W$ 's, which automatically satisfies every constraint complement. The intersection of all members is empty because the constraint complements cut the intersection down to $K$ and the $W$ 's cover $K$ . Thus $E$ is a downwards-directed family of nonempty closed subsets of $X$ , contains $X$ and every constraint complement, has empty intersection, and every member belongs to the finite-coordinate cylinder algebra.

step 4.1step 5.1F4

7.1

Each $G_{n}$ is dense in $K$ : let $N$ be a nonempty relatively open subset of $K$ , and choose a basic product-open $W$ with $\emptyset \neq K \cap W \subseteq N$ , restricting only the coordinates in a finite set $J$ ; choose $u \in K \cap W$ . If $u (i) \neq \infty$ for some $i \geq n$ then $u \in N \cap G_{n}$ and we are done. Otherwise every non- $\infty$ value of $u$ occurs at an index $< n$ ; let $t$ be a value of $u$ of maximal length among those, or the empty node if $u$ has no non- $\infty$ value. Choose $N_{1} \geq n$ larger than every index in $J$ and larger than $n$ , and let $s \in T$ be a proper extension of $t$ of length at least $N_{1}$ , which exists by finitely iterating pruning and restricting to the required length if needed (choose a length at least $\max (N_{1}, dom (t) + 1)$ ). Define $y$ by: $y (i) : = u (i)$ for $i \in J$ ; $y (i) : = \infty$ if $i \notin J$ and $i > N_{1}$ ; $y (N_{1}) : = s$ ; and $y (i) : = \infty$ if $i \notin J$ and $i < N_{1}$ . Then $y \in K \cap W$ , because the only non- $\infty$ values are the values of $u$ at indices in $J$ together with $s$ at $N_{1}$ , all of which are comparable by the maximality of $t$ and the choice of $s$ ; and $y (N_{1}) = s \neq \infty$ with $N_{1} \geq n$ gives $y \in G_{n}$ .

step 5.2step 6.1L2

7.2

In case B, construct families $E_{n}$ of closed subsets of $X$ by $E_{0} : = E$ and: if $\infty \in π_{n} [E]$ for every $E \in E_{n}$ , let $E_{n + 1}$ be $E_{n}$ together with $E \cap π_{n}^{- 1} [{\infty}]$ for $E \in E_{n}$ , and otherwise let $E_{n + 1} : = E_{n}$ ; here $π_{n}$ is the $n$ -th projection. The added sets are nonempty by the condition triggering the first alternative, and downward directedness follows because a lower bound $D \subseteq E \cap E^{'}$ in $E_{n}$ gives the lower bound $D \cap π_{n}^{- 1} [{\infty}]$ whenever one or both of the two sets carries the new coordinate constraint. Thus each $E_{n}$ is downwards directed, consists of nonempty closed sets, and has empty intersection because it contains $E$ . Inductively every member lies in the finite-coordinate cylinder algebra generated by the sets $π_{i}^{- 1} [{t}]$ , $i \in N$ , $t \in T$ , and $π_{i}^{- 1} [{\infty}]$ , $i < n$ . For such an $E$ , take one finite Boolean expression in the listed generators and let $H \subseteq T$ be the finite set of node labels tested at coordinate $n$ . No test $x (n) = \infty$ occurs, since all infinity tests have indices less than $n$ . If $x \in E$ and $x (n) \notin H$ , replacing only $x (n)$ by $\infty$ preserves every test and hence membership in $E$ . Therefore $\infty \notin π_{n} [E]$ implies $π_{n} [E] \subseteq H$ , so that projection is finite. This uses no compactness of an infinite or finite product.

step 2.1step 6.2F2F3

8.1

Case A: $K$ is compact. Then $K$ is a compact Hausdorff space, so by the hypothesis assumed in step 1.1 it is Baire, and by step 6.1 and step 7.1 the sets $G_{n}$ are dense open, so their intersection is dense and in particular nonempty; fix $x \in ⋂_{n} G_{n}$ . Let $D : = {i \in N : x (i) \neq \infty}$ .

step 1.1step 5.1step 6.1step 7.1L1

8.2

In case B, put $E^{*} : = ⋃_{n} E_{n}$ and $D : = {n : π_{n}^{- 1} [{\infty}] \notin E^{*}}$ . If $n \in D$ , then some $E_{0} \in E_{n}$ has $\infty \notin π_{n} [E_{0}]$ : otherwise the first alternative in step 7.2, applied also to $X \in E_{n}$ , would put $X \cap π_{n}^{- 1} [{\infty}] = π_{n}^{- 1} [{\infty}]$ in $E_{n + 1}$ , contrary to $n \in D$ . The finite-test argument in step 7.2 makes $π_{n} [E_{0}]$ finite. Put $F_{n} : = ⋂ {π_{n} [E] : E \in E^{*}}$ . Downward directedness makes the projected family finitely intersecting, so its intersection inside the finite set $π_{n} [E_{0}]$ is nonempty; hence $F_{n}$ is a nonempty finite subset of $T$ . Moreover some $E_{n}^{0} \in E^{*}$ satisfies $π_{n} [E_{n}^{0}] = F_{n}$ : using [F5] after fixing a listing of the finite set $π_{n} [E_{0}] ∖ F_{n}$ , for each such $t$ take a member whose projection omits $t$ , and take a common lower bound with $E_{0}$ . Its projection is contained in $F_{n}$ , while the definition of $F_{n}$ gives the reverse inclusion.

step 6.2step 7.2F2F5

9.1

In case A, $D$ is infinite: for each $n$ the membership $x \in G_{n}$ gives some $i \geq n$ with $x (i) \neq \infty$ , so $D$ contains arbitrarily large naturals and is therefore infinite.

step 8.1step 7.1

9.2

In case B, $D$ is infinite. Suppose instead that it is finite. Successively for $n \in D$ , one can adjoin a cylinder $π_{n}^{- 1} [{s_{n}}]$ , $s_{n} \in F_{n}$ , while preserving the finite-intersection property: at that stage include the member $E_{n}^{0}$ from step 8.2, whose $n$ -th projection is the finite set $F_{n}$ ; if no one of the finitely many cells $π_{n}^{- 1} [{s}]$ , $s \in F_{n}$ , preserved the finite-intersection property, finitely many witnessing failures, obtained using [F5], would have a common lower bound meeting $E_{n}^{0}$ but none of those cells, a contradiction. Closing under finite intersections gives a downwards-directed family $E_{1}^{*}$ of nonempty closed sets which contains $E^{*}$ and the chosen cylinders. Define $z (n) : = s_{n}$ for $n \in D$ and $z (n) : = \infty$ otherwise. Every basic neighbourhood of $z$ meets every $E \in E_{1}^{*}$ : intersect $E$ with the finitely many chosen singleton cylinders for its coordinates in $D$ and, for coordinates outside $D$ , with the cylinders $π_{n}^{- 1} [{\infty}] \in E^{*}$ . Therefore $z$ lies in the closure of every member, hence in every member because they are closed, contradicting the empty intersection of $E^{*} \subseteq E_{1}^{*}$ .

step 8.2F5

9.3

In case B, let $m < n$ lie in $D$ and $s \in F_{m}$ . Then some $t \in F_{n}$ properly extends $s$ . Otherwise every $t \in F_{n}$ gives a constraint complement $C_{t} : = X ∖ {x : x (m) = s, x (n) = t} \in E^{*}$ by step 6.2. Take $E_{n}^{0} \in E^{*}$ with $π_{n} [E_{n}^{0}] = F_{n}$ from step 8.2, and use downward directedness and the finiteness of $F_{n}$ to obtain $E^{'} \in E^{*}$ with $E^{'} \subseteq E_{n}^{0} \cap ⋂_{t \in F_{n}} C_{t}$ . Since $s \in F_{m} \subseteq π_{m} [E^{'}]$ , choose $x \in E^{'}$ with $x (m) = s$ . But $x (n) \in π_{n} [E^{'}] \subseteq F_{n}$ ; taking $t = x (n)$ contradicts $x \in C_{t}$ .

step 6.2step 8.2

10.1

In case A, the values $x (i)$ for $i \in D$ form a chain in $T$ under initial segment, strictly increasing in length, by the definition of $K$ in step 4.1 since no two of them are $\infty$ .

step 4.1step 9.1

10.2

In case B, enumerate $D$ increasingly as $m_{0} < m_{1} < \dots$ and put $F_{0}^{'} : = F_{m_{0}}$ and $F_{i + 1}^{'} : = {t \in F_{m_{i + 1}} : s is a proper initial segment of t for some s \in F_{i}^{'}}$ . By step 9.3, every $s \in F_{i}^{'}$ has an extension in $F_{i + 1}^{'}$ ; by definition every member of $F_{i + 1}^{'}$ has a predecessor in $F_{i}^{'}$ . Thus every $F_{i}^{'}$ is nonempty finite, and every one of its nodes has length at least $i$ . Let $T^{'}$ be the set of all initial segments of nodes in $⋃_{i} F_{i}^{'}$ . It is a subtree and has a node at every level $r$ , because any member of $F_{r}^{'}$ has length at least $r$ . Its level $r$ is finite: if $u \in T^{'}$ has length $r$ , choose $t \in F_{j}^{'}$ with $u$ an initial segment of $t$ . If $j < r$ , extend $t$ through the successive $F_{i}^{'}$ to a member of $F_{r}^{'}$ ; if $j > r$ , follow predecessors down to a member of $F_{r}^{'}$ . In either case, because initial segments of the same node are comparable and every member of $F_{r}^{'}$ has length at least $r$ , $u$ is the length- $r$ initial segment of some member of the finite set $F_{r}^{'}$ . Hence the level has at most $∣ F_{r}^{'} ∣$ elements.

step 9.2step 9.3L2

11.1

In case A, let $T^{'}$ be the set of all initial segments of the nodes $x (i)$ , $i \in D$ . Then $T^{'}$ is a subtree of $T$ : it is contained in $T$ because $T$ is closed under initial segments, and it is closed under initial segments by construction. Its level $m$ consists of the initial segments of length $m$ of the nodes $x (i)$ with $i \in D$ ; for $i \leq j$ in $D$ the nodes $x (i), x (j)$ are comparable and $x (i)$ is an initial segment of $x (j)$ , so all nodes $x (i)$ with length at least $m$ have the same initial segment of length $m$ , and this common node is unique; since lengths in $D$ are unbounded there is such an $i$ , so level $m$ of $T^{'}$ is a singleton. Hence $T^{'}$ has nonempty finite levels, as required.

step 10.1L2

12.1

In either case the pruned tree $T$ has a subtree with nonempty finite levels: case A by step 11.1, case B by step 10.2. This is the tree form of DMC, so by [F1] DMC in successor-menu form holds, and since $T$ was an arbitrary pruned tree with nonempty levels, the hypothesis that every compact Hausdorff space is Baire implies DMC.

step 11.1step 10.2F1∎

Remarks

What compactness of $K$ is used for, and what happens without it. In case A the hypothesis of the theorem is applied to $K$ itself, so $K$ must be compact; in case B the failure of compactness is converted into a family of closed sets with empty intersection, which is the exact form the finite-intersection characterisation of compactness provides.
The dichotomy is exhaustive and no choice is used in it. In case A, the assumed Baireness of the compact Hausdorff space $K$ supplies one point of the intersection of the dense open sets $G_{n}$ ; the recursive construction of the families $E_{n}$ in case B is a definition by recursion on $N$ and the sets $F_{i}^{'}$ are defined, not selected. Case B uses individual existential witnesses and finite choices, never countably many simultaneous selections.

TheoremStatement: Literature-sourcedProof: AI-adaptedaudited 2026-09-22Open item page →

Compact Hausdorff Baire is equivalent to DMC

Statement

Over $Z F$ , every compact Hausdorff space is a Baire space if and only if DMC holds (Dependent multiple choice in finite-level tree form, Baire space: a topological space in which every countable intersection of dense open subsets is dense, Open cover, subcover, and compact topological space; a compact subset is a subspace that is compact in its own right, Hausdorff space: distinct points have disjoint open neighbourhoods; every metrizable space is Hausdorff and the indiscrete topology on two points is not).

Both directions are the content of the two preceding theorems of this page; this item records the equivalence and the exact form of each half, without adding any hypothesis of its own.

Facts & Assumptions

Given: The two implications proved earlier on this page.

[F1]

$Z F + D M C$ proves that every compact Hausdorff space is Baire (DMC makes every compact Hausdorff space Baire).

[F2]

Over $Z F$ , if every compact Hausdorff space is Baire then DMC holds (Compact Hausdorff Baire implies DMC).

[L1]

The claim is the conjunction of the two implications of the statement, with no additional hypotheses (Baire space: a topological space in which every countable intersection of dense open subsets is dense, Dependent multiple choice in finite-level tree form).

Proof

technique · direct

1.1

Assume DMC; then by [F1] every compact Hausdorff space is Baire, which is the forward direction of the displayed equivalence.

assume-hypF1

1.2

Assume instead that every compact Hausdorff space is Baire; then by [F2] DMC holds, which is the reverse direction of the displayed equivalence.

assume-hypF2

2.1

The two implications hold unconditionally over $Z F$ , so the displayed biconditional is proved; the forward direction spends exactly DMC and the reverse direction spends only the Baireness hypothesis, as recorded by [F1] and [F2].

step 1.1step 1.2L1∎

TheoremStatement: Literature-sourcedProof: Literature-sourcedjudge pass (gpt-5.6-terra)audited 2026-09-22Open item page →

DC is equivalent to Baireness of compact-Hausdorff products

Statement

Over $Z F$ , the Axiom of Dependent Choice (The axiom of dependent choice: a relation in which every element is related to something admits an $N$ -indexed chain) is equivalent to the assertion that every product of compact Hausdorff spaces, including the empty product, is a Baire space (The product set $\prod_{i \in I} X_{i}$ 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, Open cover, subcover, and compact topological space; a compact subset is a subspace that is compact in its own right, Baire space: a topological space in which every countable intersection of dense open subsets is dense).

The equivalence is due to Herrlich and Keremedis. Their forward direction runs the pseudo-complete-space recursion, which for compact Hausdorff factors reduces to a recursion of finite-support cylinders; the reverse direction reduces the hypothesis to Baireness of the complete sequence space $A^{ω}$ of a serial relation, where the classical Blair extraction of a chain applies. No nonemptiness of an arbitrary product of nonempty compact Hausdorff spaces is claimed: that statement is strictly stronger than DC.

Facts & Assumptions

Given: The two assertions of the statement; an arbitrary family $(X_{i})_{i \in I}$ of compact Hausdorff spaces with product $X$ ; a countable family $(U_{n})_{n \in N}$ of dense open subsets of $X$ ; a nonempty open $B \subseteq X$ ; an arbitrary serial relation $R$ on a nonempty set $A$ .

[F1]

DC: for every nonempty $P$ , every relation entire on $P$ , and every $a \in P$ , there is $x : N \to P$ with $x_{0} = a$ and $x_{n} R x_{n + 1}$ (The axiom of dependent choice: a relation in which every element is related to something admits an $N$ -indexed chain).

[F2]

DC implies Countable Choice (AC implies DC implies countable choice, The Axiom of Countable Choice ( ${A C}_{ω}$ )).

[F3]

The one-point compactification of a discrete space is compact and Hausdorff, and a space is dense in its one-point compactification exactly when it is not compact (The one-point (Alexandroff) compactification $X^{*} = X \cup {\infty}$ , whose open sets are the open sets of $X$ together with the complements in $X^{*}$ of the closed compact subsets of $X$ , $X^{*}$ is compact and contains $X$ as an open subspace; $X$ is dense in $X^{*}$ exactly when $X$ is not compact; and $X^{*}$ is Hausdorff exactly when $X$ is locally compact and Hausdorff, The discrete, indiscrete, cofinite, cocountable, particular-point and Sierpinski topologies, Locally compact topological space: every point has a compact neighbourhood; and what this says in a metric space).

[F4]

The product of an arbitrary family of Hausdorff spaces is Hausdorff (Arbitrary products preserve $T_{0}$ , $T_{1}$ , and Hausdorffness, Hausdorff space: distinct points have disjoint open neighbourhoods; every metrizable space is Hausdorff and the indiscrete topology on two points is not).

[F5]

The discrete sequence space $A^{ω}$ with its reciprocal first-difference metric is nonempty and complete in $Z F$ , and its sets $U_{i} = {f : \exists j f (i) R f (j)}$ are open and dense (Discrete sequence spaces are complete in ZF, Successor-occurrence sets of a serial relation are open and dense).

[F6]

Every nonempty subset of $N$ has a least element, recursion on $N$ defines functions from a self-map and an initial value, and the prescribed-start and starting-point-free forms of DC are equivalent over $Z F$ (The well-ordering principle, The recursion theorem, Prescribed-start and starting-point-free serial choice are equivalent in ZF).

[F7]

Finite choice and finite unions: a function with finite domain all of whose values are nonempty has a choice function, a subset of a finite set is finite, and a countable union of at most countable sets is at most countable under countable choice (Every natural-number-indexed list of nonempty sets has a choice function on its family of values, A subset of a finite set is finite, with $∣ B ∣ \leq ∣ A ∣$ , and equality holds if and only if $B = A$ , Countable unions of at most countable sets, assuming ${A C}_{ω}$ , Finite, countably infinite, countable, uncountable).

[L1]

A space is Baire when the intersection of every sequence of dense open sets meets every nonempty open set; a dense subset of a space meets every nonempty open set; and a compact space is one in which every family of closed sets with the finite intersection property has nonempty intersection (Baire space: a topological space in which every countable intersection of dense open subsets is dense, Dense, nowhere dense and codense subsets of a topological space, and the criterion by basic open sets, Interior, closure, boundary, exterior, derived set and isolated point in a topological space, A space is compact exactly when every family of closed subsets with the finite intersection property has nonempty intersection, Finite intersection property, Topology on a set, open and closed sets, clopen sets, the closed-set axiomatisation, and the coarser/finer comparison).

[L2]

A compact Hausdorff space is regular and normal (A compact Hausdorff space is regular and normal, hence $T_{3}$ and $T_{4}$ ), so for every point $x$ of such a space and every open $U ∋ x$ there is an open $V$ with $x \in V \subseteq \overline{V} \subseteq U$ .

Proof

technique · direct

1.1

Assume DC and let $(X_{i})_{i \in I}$ , $(U_{n})$ and $B$ be as in the assumptions; the task is to find a point of $B \cap ⋂_{n} U_{n}$ .

assume-hypgiven

1.2

Assume instead that every product of compact Hausdorff spaces is Baire, and let $R$ be a serial relation on a nonempty set $A$ ; the task is to build an infinite $R$ -chain.

assume-hypgiven

2.1

Under step 1.1: if $X = \emptyset$ then $X$ is Baire and the empty product is the one-point space, which is Baire, so assume $X \neq \emptyset$ and fix $x \in X$ .

step 1.1L1

2.2

Under step 1.2: if $A$ is finite and nonempty, finite choice gives $f : A \to A$ with $a R f (a)$ for every $a$ , and recursion on $N$ gives the $R$ -chain $a, f (a), f (f (a)), \dots$ ; so assume $A$ is infinite.

step 1.2F6F7

3.1

Under step 1.1 and step 2.1, let $Y$ be the set of quadruples $(n, F, (B_{i})_{i \in F})$ where $n \in N$ , $F \subseteq I$ is finite, each $B_{i} \subseteq X_{i}$ is nonempty open, and $⋂_{i \in F} π_{i}^{- 1} [B_{i}] \subseteq B \cap U_{n}$ ; here $π_{i}$ is the projection. Then $Y \neq \emptyset$ : the set $B \cap U_{0}$ is nonempty open by [L1], so it contains a basic open cylinder, which is a finite intersection of coordinates.

step 2.1L1

3.2

Under step 2.2 and $A$ infinite, let $α A : = A \cup {\infty}$ be the one-point compactification of the discrete space $A$ ; by [F3] it is compact Hausdorff, and $A$ is open and dense in $α A$ because the infinite discrete space $A$ is not compact.

step 2.2F3

4.1

Under step 3.1 define $ρ$ on $Y$ by $(n, F, (B_{i})) ρ (n^{'}, F^{'}, (B_{i}^{'}))$ iff $n^{'} = n + 1$ , $F \subseteq F^{'}$ , and $\overline{B_{i}^{'}} \subseteq B_{i}$ for $i \in F$ ; the new open sets indexed by $F^{'} ∖ F$ are unrestricted beyond the membership condition of $Y$ . Then $ρ$ is entire on $Y$ : given $(n, F, (B_{i})) \in Y$ the cylinder $C : = ⋂_{i \in F} π_{i}^{- 1} [B_{i}]$ is a nonempty open subset of $B \cap U_{n}$ , so $C \cap U_{n + 1}$ is nonempty open because $U_{n + 1}$ is dense; fix a point $w$ of it. Some basic open cylinder around $w$ lies in the open set $C \cap U_{n + 1}$ ; intersecting it with $C$ and adding the coordinates of $C$ that it omits, we obtain a basic open cylinder $⋂_{i \in F^{†}} π_{i}^{- 1} [B_{i}^{†}]$ with $F \subseteq F^{†}$ , $B_{i}^{†} \subseteq B_{i}$ for $i \in F$ , and $w \in ⋂_{i \in F^{†}} π_{i}^{- 1} [B_{i}^{†}] \subseteq C \cap U_{n + 1}$ . For each $i \in F^{†}$ the point $w_{i}$ lies in $B_{i}^{†}$ , so by the regularity clause of [L2] applied in the compact Hausdorff space $X_{i}$ there is a nonempty open $B_{i}^{'}$ with $w_{i} \in B_{i}^{'} \subseteq \overline{B_{i}^{'}} \subseteq B_{i}^{†}$ ; put $F^{'} : = F^{†}$ . Then $⋂_{i \in F^{'}} π_{i}^{- 1} [B_{i}^{'}] \subseteq ⋂_{i \in F^{'}} π_{i}^{- 1} [B_{i}^{†}] \subseteq B \cap U_{n + 1}$ , so $(n + 1, F^{'}, (B_{i}^{'})) \in Y$ , and $\overline{B_{i}^{'}} \subseteq B_{i}^{†} \subseteq B_{i}$ for every $i \in F$ , so $(n, F, (B_{i})) ρ (n + 1, F^{'}, (B_{i}^{'}))$ .

step 3.1L1L2F4

4.2

Under step 3.2 let $X : = (α A)^{ω}$ ; it is a product of compact Hausdorff spaces, hence Baire by the hypothesis of step 1.2, and the sets $D_{n} : = {g \in X : g (n) \in A}$ are open and dense, so $A^{ω} = ⋂_{n} D_{n}$ is a dense $G_{δ}$ of $X$ ; a dense $G_{δ}$ subspace of a Baire space is Baire, since the traces of countably many dense open sets of the bigger space witness the subspace condition.

step 3.2L1F4

5.1

Under step 1.1 and step 4.1, DC gives a sequence $y_{n} = (n, F_{n}, (B_{i}^{n})_{i \in F_{n}})$ in $Y$ with $y_{n} ρ y_{n + 1}$ for all $n$ ; in particular $F_{n} \subseteq F_{n + 1}$ and, for every $i \in F_{n}$ , the closures nest inside the previous open sets: $\overline{B_{i}^{n + 1}} \subseteq B_{i}^{n}$ .

step 4.1F1

5.2

Under step 4.2 the subspace $A^{ω}$ is the discrete sequence space with its product topology, complete under the reciprocal first-difference metric by [F5]; so this complete metric space is Baire.

step 4.2F5

6.1

Under step 5.1 the set $F : = ⋃_{n} F_{n}$ is at most countable: it is a countable union of finite sets, and countable choice holds by [F2].

step 5.1F2F7

6.2

Under step 5.1, for each $i \in F$ let $n_{i}$ be least with $i \in F_{n_{i}}$ ; then the sets $\overline{B_{i}^{n}}$ for $n \geq n_{i}$ form a decreasing sequence of nonempty closed subsets of the compact space $X_{i}$ , so their intersection is nonempty and is contained in $⋂_{n \geq n_{i}} B_{i}^{n}$ , since $\overline{B_{i}^{n + 1}} \subseteq B_{i}^{n}$ for every $n$ .

step 5.1L1F7

6.3

Under step 5.2 the sets $V_{i} : = {f \in A^{ω} : \exists j f (i) R f (j)}$ are open and dense in $A^{ω}$ by [F5], so their intersection is dense and hence nonempty; fix $f \in ⋂_{i} V_{i}$ .

step 5.2F5L1

7.1

Under step 6.1, step 6.2 and countable choice, choose $b_{i} \in ⋂_{n \geq n_{i}} \overline{B_{i}^{n}}$ for each $i \in F$ — the set is nonempty by step 6.2, where compactness gives a point of the intersection of the nested closed sets, and step 6.2 also identifies the intersection as a subset of $⋂_{n \geq n_{i}} B_{i}^{n}$ — and define $y \in X$ by $y_{i} : = b_{i}$ for $i \in F$ and $y_{i} : = x_{i}$ for $i \notin F$ .

step 6.1step 6.2F2F7

7.2

Under step 6.3 define $q (i) : = \min {j \in N : f (i) R f (j)}$ , which exists by [F6] because $f \in V_{i}$ , and $k (0) : = 0$ , $k (n + 1) : = q (k (n))$ , a definition by recursion; then $a (n) : = f (k (n))$ satisfies $a (n) = f (k (n)) R f (q (k (n))) = f (k (n + 1)) = a (n + 1)$ for every $n$ , so $a$ is an infinite $R$ -chain.

step 6.3F6

8.1

Under step 7.1, $y \in ⋂_{i \in F_{n}} π_{i}^{- 1} [B_{i}^{n}] \subseteq B \cap U_{n}$ for every $n$ , because $b_{i} \in B_{i}^{n}$ for every $i \in F_{n}$ and the inclusion is the defining property of $Y$ ; hence $B \cap ⋂_{n} U_{n} \neq \emptyset$ , so every product of compact Hausdorff spaces is Baire under DC.

step 7.1step 3.1

8.2

Under step 2.2 and step 7.2 every serial relation on a nonempty set admits an infinite chain, which is the starting-point-free form of DC; the prescribed-start form follows by [F6], so the hypothesis of step 1.2 implies DC.

step 2.2step 7.2F6

9.1

Step 8.1 proves that DC implies Baireness of every product of compact Hausdorff spaces, and step 8.2 proves the converse; the two implications are the displayed equivalence.

step 8.1step 8.2∎

Remarks

Why the empty product is named. The product over an empty index set is the one-point space, which is trivially Baire, and a product with an empty factor is empty and hence Baire for the same reason; both cases are separated in step 2.1 and neither contributes to either implication.
What the forward direction does not claim. The quadruple recursion proves Baireness of the product; it does not prove that the product of nonempty compact Hausdorff spaces is nonempty, and the remark of Herrlich and Keremedis that this stronger statement is properly stronger than DC is not used here.

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

DMC implies Urysohn's lemma

Statement

$Z F + D M C$ proves Urysohn's lemma: in a normal space (Normal spaces and $T_{4}$ spaces, with the source disagreement over whether normality includes $T_{1}$ stated explicitly) any two disjoint closed sets $F, G$ admit a continuous $f : X \to [0, 1]$ (Continuity of a map of topological spaces at a point and globally, Intervals of $R$ : the nine order-convex forms, nondegeneracy, and length) with $F \subseteq f^{- 1} ({0})$ and $G \subseteq f^{- 1} ({1})$ .

DMC is used once, in its successor-menu form of Dependent multiple choice in finite-level tree form: it supplies the finite menus of dyadic nodes, and the finitely many open sets inside each menu are intersected coordinatewise to obtain a single dyadic scale.

Facts & Assumptions

Given: A normal space $X$ ; disjoint closed sets $F, G \subseteq X$ ; the principle DMC.

[F1]

Normality via shrinking: if $A$ is closed, $U$ is open and $A \subseteq U$ , then there is open $V$ with $A \subseteq V \subseteq \overline{V} \subseteq U$ (A space is normal if and only if every closed $A$ inside an open $U$ admits an open $V$ with $A \subseteq V \subseteq \overline{V} \subseteq U$ ).

[F2]

The dyadic rationals $D \subseteq [0, 1]$ are an increasing union of finite levels $D_{n}$ , the level $D_{n + 1}$ inserts one new point strictly between each pair of $D_{n}$ -consecutive elements, every two elements of $D$ lie in a common $D_{n}$ , and the positive dyadics have infimum zero (the displayed dyadic growth bound gives $2^{- n} \to 0$ ) (The dyadic rationals of $[0, 1]$ , their finite levels $D_{n}$ , and their density in $[0, 1]$ ).

[F3]

Dyadic scale lemma: if $(U_{r})_{r \in D}$ are open subsets of $X$ with $\overline{U_{r}} \subseteq U_{s}$ whenever $r < s$ and $U_{1} = X$ , then $f (x) : = \inf ({r \in D : x \in U_{r}} \cup {1})$ is a continuous map $X \to [0, 1]$ (If $(U_{r})_{r \in D}$ are open with $\overline{U_{r}} \subseteq U_{s}$ whenever $r < s$ and $U_{1} = X$ , then $x \mapsto \inf {r \in D : x \in U_{r}}$ is a continuous map $X \to [0, 1]$ , and no choice principle is used).

[F4]

Finite choice: a finite list indexed by a natural number, all of whose entries are nonempty sets admits a choice function for its family of values (Every natural-number-indexed list of nonempty sets has a choice function on its family of values).

[F5]

DMC: every serial relation on a nonempty set admits nonempty finite successor menus (Dependent multiple choice in finite-level tree form).

[L1]

Closure and union: the closure of a finite union is the union of the closures, a finite intersection of open sets is open, and $\overline{A}$ is the smallest closed superset of $A$ ; closed sets are complements of open sets (Interior, closure, boundary, exterior, derived set and isolated point in a topological space, Interior commutes with finite intersections and closure with finite unions, while the two reverse combinations are inclusions only and both fail for infinite families; the space is the disjoint union of interior, boundary and exterior, Topology on a set, open and closed sets, clopen sets, the closed-set axiomatisation, and the coarser/finer comparison).

[L2]

A nonempty subset of $N$ has a least element, and a specified set self-map with an initial state admits recursion on $N$ (The well-ordering principle, The recursion theorem).

Proof

technique · direct

1.1

Assume DMC, let $X$ be normal and let $F, G$ be disjoint closed subsets of $X$ .

givenF5

2.1

Under step 1.1, $X ∖ G$ is open and $F \subseteq X ∖ G$ ; by [F1] fix open $V_{0}$ with $F \subseteq V_{0} \subseteq \overline{V_{0}} \subseteq X ∖ G$ , and put $V_{1} : = X ∖ G$ .

step 1.1F1L1

3.1

Under step 1.1, define a node of level $n$ to be a tuple $⟨ U_{1}, \dots, U_{2^{n}} ⟩$ of open subsets of $X$ such that $\overline{U_{i}} \subseteq U_{i + 1}$ for $1 \leq i < 2^{n}$ , $F \subseteq U_{1}$ , and $U_{2^{n}} = X ∖ G$ . Let $T$ be the set of such nodes over all $n \in N$ , and let the relation $S$ on $T$ be: $a S b$ when $b$ is a node of level $n + 1$ whose even entries are the entries of $a$ , that is $b_{2 i} = a_{i}$ for $1 \leq i \leq 2^{n}$ .

step 2.1L1

4.1

Under step 3.1, $⟨ V_{1} ⟩ = ⟨ X ∖ G ⟩$ is a node of level $0$ in $T$ : it has the single required entry, $F \subseteq X ∖ G$ and its last entry is $X ∖ G$ , so $T \neq \emptyset$ . And $S$ is serial on $T$ : given a node $a = ⟨ U_{1}, \dots, U_{2^{n}} ⟩$ , apply [F1] to the closed set $F$ inside the open set $U_{1}$ to obtain an open $W_{0}$ with $F \subseteq W_{0} \subseteq \overline{W_{0}} \subseteq U_{1}$ , for each $1 \leq i < 2^{n}$ apply [F1] to the closed set $\overline{U_{i}}$ inside the open set $U_{i + 1}$ to obtain an open $W_{i}$ with $\overline{U_{i}} \subseteq W_{i} \subseteq \overline{W_{i}} \subseteq U_{i + 1}$ , and use [F4] to choose all of $W_{0}, \dots, W_{2^{n} - 1}$ at once (when $n = 0$ one may take $W_{0}$ to be the $V_{0}$ of step 2.1, which has exactly the required inclusions); then $b : = ⟨ W_{0}, U_{1}, W_{1}, U_{2}, \dots, W_{2^{n} - 1}, U_{2^{n}} ⟩$ has $2^{n + 1}$ entries, its even entries are $b_{2 i} = U_{i}$ for $1 \leq i \leq 2^{n}$ , and $F \subseteq b_{1}$ , $\overline{b_{j}} \subseteq b_{j + 1}$ for $1 \leq j < 2^{n + 1}$ , $b_{2^{n + 1}} = X ∖ G$ by step 3.1, so $b$ is a node of level $n + 1$ with $a S b$ .

step 2.1step 3.1F1F4L1

5.1

Under step 4.1, apply [F5] to obtain finite nonempty menus $F_{n} \subseteq T$ . They need not be level-aligned. Let $k$ be the least level represented in $F_{0}$ by [L2] and let $H_{0}$ consist of its level- $k$ members. Define $H_{n + 1} = {b \in F_{n + 1} : (\exists a \in H_{n}) a S b}$ . This is a definable recursion (encode the index and subset in a set state, with a default for other states), licensed by [L2]. Induction shows that $H_{n}$ is nonempty finite, every member has level $k + n$ , and the $H_{n}$ have both successor and predecessor properties: each retained $a$ has a successor in the original next menu and that successor is retained. To recover levels below $k$ , for a level- $k$ node $a$ and $0 \leq m \leq k$ put $π_{m} (a)_{i} = a_{i 2^{k - m}}$ for $1 \leq i \leq 2^{m}$ . Each projection is a level- $m$ node: all entries contain $F$ , the last is $X ∖ G$ , and the closure inclusions follow by skipping along the original chain. Moreover $π_{m + 1} (a)_{2 i} = π_{m} (a)_{i}$ and $π_{k} (a) = a$ . Now put $F_{m}^{'} = {π_{m} (a) : a \in H_{0}}$ for $m < k$ , and $F_{m}^{'} = H_{m - k}$ for $m \geq k$ . These are nonempty finite menus of exactly level $m$ , with both predecessor and successor properties, including the transition into level $k$ . In particular $F_{0}^{'} = {⟨ X ∖ G ⟩}$ . No enumeration of infinitely many finite menus or branch choice is made.

step 3.1step 4.1F5L1L2

6.1

Under step 5.1, for $n \in N$ and $1 \leq i \leq 2^{n}$ put $U_{n, i} : = ⋂ {a_{i} : a \in F_{n}^{'}}$ , the intersection of the $i$ -th entries of the finitely many menu elements; each $U_{n, i}$ is open, $F \subseteq U_{n, 1}$ , $U_{n, 2^{n}} = X ∖ G$ , and $\overline{U_{n, i}} \subseteq U_{n, i + 1}$ , because the intersection is contained in every entry, its closure is contained in every entry closure by monotonicity, and each such closure is contained in the corresponding next entry. Monotonicity follows directly from the smallest-closed-superset characterization in [L1].

step 5.1L1

7.1

Under step 6.1, $U_{n + 1, 2 i} = U_{n, i}$ for all $n$ and $1 \leq i \leq 2^{n}$ : every $b \in F_{n + 1}^{'}$ has $b_{2 i} = a_{i}$ for the predecessor $a \in F_{n}^{'}$ with $a S b$ , and every $a \in F_{n}^{'}$ occurs as the predecessor of some $b \in F_{n + 1}^{'}$ by the successor property, so the two intersections have the same entries.

step 5.1step 6.1

8.1

Under step 7.1 define a family on all dyadics by $U_{0} : = \emptyset$ , $U_{1} : = X$ , and, for $0 < r < 1$ , $U_{r} : = U_{n, i}$ whenever $r = i / 2^{n}$ with $1 \leq i < 2^{n}$ . This is well defined by step 7.1 and [F2]. If $0 < r < s < 1$ , choose $N$ with $r = i / 2^{N}$ , $s = j / 2^{N}$ and $i < j$ by [F2]; then $U_{r} = U_{N, i}$ , $U_{s} = U_{N, j}$ , and $\overline{U_{r}} \subseteq U_{s}$ by step 6.1. The same inclusion is automatic when $r = 0$ or $s = 1$ . Thus $(U_{r})_{r \in D}$ satisfies the hypotheses of [F3] literally.

step 6.1step 7.1F2F3

9.1

Under step 8.1, [F3] applies to the scale and gives the continuous $f (x) = \inf ({r \in D : x \in U_{r}} \cup {1}) : X \to [0, 1]$ .

step 8.1F3

10.1

Under step 9.1, $F \subseteq f^{- 1} ({0})$ : if $a \in F$ and $0 < r = i / 2^{n} < 1$ , then $a \in F \subseteq U_{n, 1} \subseteq U_{n, i} = U_{r}$ , and also $a \in U_{1} = X$ . Hence ${r \in D : a \in U_{r}} = D ∖ {0}$ , whose infimum is $0$ , so $f (a) = 0$ .

step 6.1step 8.1step 9.1F2

10.2

Under step 9.1, $G \subseteq f^{- 1} ({1})$ : for $b \in G$ , first $b \notin U_{0} = \emptyset$ . For $r = i / 2^{n} \in D$ with $0 < r < 1$ we have $i \geq 1$ , $i < 2^{n}$ and $U_{n, i} \subseteq U_{n, 2^{n}} = X ∖ G$ , so $b \notin U_{r}$ ; also $b \in X = U_{1}$ ; hence ${r \in D : b \in U_{r}} \cup {1} = {1}$ and $f (b) = 1$ .

step 6.1step 8.1step 9.1

11.1

Under steps 9.1, 10.1 and 10.2 the map $f$ is continuous with $F \subseteq f^{- 1} ({0})$ and $G \subseteq f^{- 1} ({1})$ , which is Urysohn's lemma for the arbitrary normal space $X$ and disjoint closed sets $F, G$ ; the only choice principle used was DMC.

step 9.1step 10.1step 10.2F5∎

Remarks

Comparison with the dependent-choice proof. The published Urysohn's lemma, under the axiom of dependent choice: in a normal space two disjoint closed sets are separated by a continuous function into $[0, 1]$ , and conversely such a space is normal runs the same dyadic construction under DC, choosing one new open set at a time by dependent choice. Here the menus are finite, so a whole level of the scale is obtained at once, and the only price is DMC, without inferring a single branch from the menus.
Where the finite intersections enter. Passing from the finite menus to the single scale values $U_{n, i}$ is the step that makes the construction a proof in $Z F$ : a finite intersection of open sets is open, its closure is contained in the intersection of the closures, and the coherence verified in step 7.1 makes the resulting values nest along the dyadic refinement.

RemarkRemark: Literature-sourcedProof: Not applicableaudited 2026-09-22Open item page →

DMC versus DC over ZF remains open

Statement

Over $Z F$ : DC implies DMC. Strictness is known in $Z F A$ , but whether DMC implies DC in $Z F$ is open; no strictness over $Z F$ is asserted.

Remarks

The implication. DC implies DMC over $Z F$ by DC and finite multiple selections, which records the equivalence $D C \leftrightarrow (D M C \land {A C}_{ω, f i n})$ and hence gives the direction used here. The principles are those of The axiom of dependent choice: a relation in which every element is related to something admits an $N$ -indexed chain and Dependent multiple choice in finite-level tree form; the finite-selection form is the one in which the implication is stated, so no conversion between the tree and menu presentations is needed.
The $Z F A$ strictness. Dodu and Morillon record that Fraenkel's second model of $Z F A$ satisfies DMC but does not satisfy DC. Thus the model has a DMC menu system for every serial relation while some serial relation has no infinite dependent-choice chain. This is the direction needed to show that DMC does not imply DC in $Z F A$ . It is not a statement about $Z F$ , and no such statement is made here.
The open question. Morillon poses the reversal over $Z F$ as an open question in the same section that records the tree form of DMC. This item reports that status and nothing more: absence of a published proof of $D M C \Rightarrow D C$ in $Z F$ is not converted into a nonimplication theorem, and the separately proved independence results of this page, which refute Urysohn's lemma under principles that do not imply DMC, do not decide the reversal either.
Why the qualification matters for consumers. The published Baire-category ledger on the deferred catalogue asserts strictness of DMC below DC and below multiple choice in $Z F$ and $Z F A$ alike. That stronger wording is not a theorem here: the results proved on this page give the implication and the $Z F A$ separation, and consumers of this item must keep the two theories apart.

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

Brunner's ordered Läuchli permutation models

Definition

Work internally in a model $M$ of $Z F A + A C$ (ZFA universes, atoms, pure sets, and the kernel, The Axiom of Choice). No external well-foundedness or transitivity of $M$ is assumed. All order types, compact supports and support ideals in the following construction are computed in $M$ , and the associated permutation model is the hereditarily symmetric submodel as computed there. When a concrete transitive ground is available, this internal presentation agrees with the usual external one. AC is a ground-model assumption, not an assertion about the resulting permutation model.

The permutation system. Let $A$ be the set of atoms, carrying a linear order $\leq$ . Let $G$ be the group of all increasing bijections of $A$ . A support ideal $I$ is a family of subsets of $A$ that contains every singleton, is closed under subsets and finite unions, and is $G$ -invariant: $e \in I$ implies $g [e] \in I$ for every $g \in G$ . The filter it generates consists of the subgroups of $G$ that contain the pointwise stabiliser $fix (e)$ of some $e \in I$ . It is a normal filter: finite intersections use $fix (e \cup f) \subseteq fix (e) \cap fix (f)$ , conjugation uses $g fix (e) g^{- 1} = fix (g [e])$ , and the singleton clause supplies every atom stabiliser. The associated ordered permutation model $P (A, G, I)$ is the hereditarily symmetric interpretation of Symmetric and hereditarily symmetric sets for that filter (Permutation groups, stabilizers, supports, and normal filters). For a transitive ground this is precisely the construction in Fraenkel–Mostowski permutation-model theorem. For the internal convention here, its axiom argument is interpreted inside $M$ , as follows. The action and hereditary-symmetry predicate are definable by the rank recursion of $M$ . Conjugation makes that predicate invariant. Atoms and pure sets are hereditarily symmetric; membership closure gives inherited Extensionality and Foundation. Intersections of finitely many stabilisers support pairing, union, and a subset defined by any fixed formula with hereditarily symmetric parameters, all quantifiers of that formula being restricted to hereditary symmetry. The internal power set of $x$ is the set of hereditarily symmetric members of $P^{M} (x)$ ; every permutation fixing $x$ preserves this set. For Replacement, apply $M$ -Replacement to the relativised formula: uniqueness makes its image invariant under every permutation fixing the domain and parameters, and every value is hereditarily symmetric. Thus the image is hereditarily symmetric too. Infinity is witnessed by the pure $ω^{M}$ . These arguments verify each instance of Separation and Replacement and the remaining ZFA axioms in the interpreted substructure; they use internal rank induction, not external well-foundedness of $M$ .

The two instances. Two choices are used below and they are not interchangeable.

Real-ordered, countable compact supports. $(A, <)$ is order-isomorphic to $(R, <)$ in the ground model. The ideal consists of all subsets of countable compact subsets of $A$ , where compactness uses the order topology and the intrinsic subspace convention of Open cover, subcover, and compact topological space; a compact subset is a subspace that is compact in its own right and Subspace topology: the traces of the open sets, its closed sets and its bases, the continuity of the inclusion, and the characteristic property of a map into a subspace. Equivalently it is the ideal generated by countable compact subsets. Finite unions of such compact sets are compact and countable, and increasing bijections preserve this property: they and their inverses preserve order intervals and hence are continuous. Thus this ideal has the required closure and invariance properties.
Rational-ordered, finite supports. $(A, <)$ is order-isomorphic to $(Q, <)$ in the ground model, and $I$ consists of all finite subsets of $A$ . This ideal also contains singletons and is invariant under $G$ .

The interval and the terminology. Fix atoms $a < b$ and put $L = [a, b]_{A} = {c \in A : a \leq c \leq b} .$ Equip $L$ with its order topology as computed inside $P (A, G, I)$ (The order topology of a linearly ordered set, with the open rays as a subbasis; order-convex sets, order-density, the least upper bound property, and linear continua). This is an actual object of that model: $L$ and its restricted order have support ${a, b}$ , and atoms and finite tuples of atoms are hereditarily symmetric. The topology is then formed internally from the interval basis. Its open sets and its open covers are internal sets; ambient subsets of $L$ need not be in the model. The distinct endpoints are the atoms $a, b$ . Their singletons are closed, since their complements are order rays.

A space is strongly connected in Brunner's terminology if every continuous function from it to $R$ is constant (Continuity of a map of topological spaces at a point and globally). An ordered Läuchli continuum means a linearly ordered space with its order topology that is compact, Hausdorff, connected and strongly connected (Open cover, subcover, and compact topological space; a compact subset is a subspace that is compact in its own right, Hausdorff space: distinct points have disjoint open neighbourhoods; every metrizable space is Hausdorff and the indiscrete topology on two points is not, Separation of a topological space, connected and disconnected spaces, clopen sets, and connected subsets). All these quantifiers, including the quantifier over continuous functions, are interpreted in the symmetric model when applied to $L$ .

Remarks

Brunner §1.2(c) uses the closed atom interval in the rational finite-support model; §3.4(b) specifies the real-ordered model and its countable compact supports. The Läuchli and choice properties of these constructions are results to be justified in the subsequent items, not extra axioms in this definition. In particular countable choice (The Axiom of Countable Choice ( ${A C}_{ω}$ )) is not inferred from the closure of the support ideal under finite unions.

There is no assertion that the ambient Dedekind completion of $A$ belongs to the symmetric model. In the rational case an ambient irrational cut has no finite support: for any finite $e \subseteq A$ , that cut lies in a component of $A ∖ e$ , and an increasing automorphism fixing $e$ can move the cut inside that component. Such a cut is not symmetric. Internal order completeness, when established for $L$ , concerns only internal bounded sets.

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

Brunner's models satisfy the required choice and Urysohn obstructions

Statement

The real-ordered countable-compact-support Läuchli model of Brunner's ordered Läuchli permutation models satisfies the Axiom of Countable Choice (The Axiom of Countable Choice ( ${A C}_{ω}$ )), and both that model and the rational-ordered finite-support model contain a nondegenerate compact linearly ordered normal space $L$ (Open cover, subcover, and compact topological space; a compact subset is a subspace that is compact in its own right, Normal spaces and $T_{4}$ spaces, with the source disagreement over whether normality includes $T_{1}$ stated explicitly) on which every continuous real-valued function is constant (Continuity of a map of topological spaces at a point and globally); hence Urysohn's lemma fails in both models.

Facts & Assumptions

Given: The two models of Brunner's ordered Läuchli permutation models, formed internally in a ground model $M$ of ZFA+AC. All constructions and arguments below, including ranks, real coordinates, compactness and sequences, are interpreted inside $M$ ; no external well-foundedness or transitivity of $M$ is required. Write $N$ for either symmetric model and $L = [a, b]_{A}$ for the closed atom interval, with $a < b$ . Ground order coordinates identify $A$ with $R$ or $Q$ in $M$ , outside $N$ ; no such enumeration is asserted to belong to $N$ .

[F1]

Internally in $M$ , the permutation model is membership-closed with the same pure kernel; its objects are hereditarily symmetric, not merely symmetric. Pure reals and natural numbers are fixed by every atom permutation. Conjugation transports supports, and a symmetric set of hereditarily symmetric members is hereditarily symmetric (Brunner's ordered Läuchli permutation models, Permutation groups, stabilizers, supports, and normal filters, Symmetric and hereditarily symmetric sets).

[F2]

The real model's support ideal consists of subsets of countable compact ground sets; the rational model's supports are finite. The group is all increasing atom bijections. The interval and its internal order topology are objects of the model (Brunner's ordered Läuchli permutation models, The order topology of a linearly ordered set, with the open rays as a subbasis; order-convex sets, order-density, the least upper bound property, and linear continua, Subspace topology: the traces of the open sets, its closed sets and its bases, the continuity of the inclusion, and the characteristic property of a map into a subspace).

[F3]

Ground AC permits simultaneous witness choices and countable unions of countable sets are countable there (The Axiom of Choice, Countable unions of at most countable sets, assuming ${A C}_{ω}$ ). A compact real set is closed and bounded, and conversely (A subset of $R$ is compact if and only if it is closed and bounded). Every nondegenerate real interval is uncountable (Every nondegenerate interval of $R$ is uncountable); the rationals are dense and countable (Both $Q$ and $R ∖ Q$ are dense in $R$ , and every nonempty open subset of $R$ is uncountable, $Q$ is countably infinite).

[F4]

A continuous real function on a closed real interval has the intermediate-value property (Intermediate value theorem, by bisection with a canonical left-half rule: a continuous function on $[a, b]$ takes every value between $f (a)$ and $f (b)$ ). Continuity and the order topology have their ordinary preimage-of-open-set meaning (Continuity of a map of topological spaces at a point and globally, The order topology of a linearly ordered set, with the open rays as a subbasis; order-convex sets, order-density, the least upper bound property, and linear continua).

[F5]

A compact Hausdorff space is normal, without an additional choice hypothesis (A compact Hausdorff space is regular and normal, hence $T_{3}$ and $T_{4}$ , Open cover, subcover, and compact topological space; a compact subset is a subspace that is compact in its own right, Hausdorff space: distinct points have disjoint open neighbourhoods; every metrizable space is Hausdorff and the indiscrete topology on two points is not, Normal spaces and $T_{4}$ spaces, with the source disagreement over whether normality includes $T_{1}$ stated explicitly).

Proof

technique · direct

1.1

All constructions involving order coordinates in the following support argument take place in $M$ . Given a sequence $(F_{n})$ of nonempty sets in the real model, enlarge a support for the sequence to a nonempty countable compact set $e$ . Ground AC chooses $x_{n} \in F_{n}$ and countable compact supports $e_{n}$ for them. Each $x_{n}$ is hereditarily symmetric by membership closure. The sequence support fixes each $F_{n}$ , since the index $n$ is pure.

givenF1F2F3

1.2

In the real model the internal interval $L$ is compact: each internal open cover is, in ground real coordinates, an open cover of the real closed bounded interval, hence has a finite subcover by [F3]. Every member of this subcover is already hereditarily symmetric, and a finite set of such objects is hereditarily symmetric by combining their finitely many supports. Thus that finite subcover belongs to $N$ . The internal order topology is Hausdorff in either model: between two distinct points choose two intervening points and use the disjoint order rays. This is a finite existence argument in the dense atom order.

givenF1F2F3

1.3

In the rational model, every nonempty internal subset $S \subseteq L$ has a supremum in $L$ . Enlarge a finite support for $S$ by $a, b$ , and call it $e$ . In the ground real completion of the rational order let $r = \sup S$ . If $r \notin e$ , it lies in a complementary interval of the finite set $e$ . Choose rational points $u < r < v$ inside that interval and an increasing rational order automorphism fixing $e$ whose extension to real cuts moves $r$ : for instance choose rational breakpoints around $r$ and a piecewise-affine map with positive rational slopes, identity outside the component, which moves the whole small interval containing $r$ to its right. Such a map preserves the rational order and fixes $e$ , hence preserves $S$ , contradicting uniqueness of its real supremum. Therefore $r \in e \cap L$ , so it is an atom and is the supremum internally too. This concerns internal sets only; no ambient irrational cut is added to $N$ .

givenF1F2F3

1.4

Let $g : L \to R$ be an internal continuous map. Enlarge a support of $g$ to include $a, b$ , using a countable compact support in the real model and a finite support in the rational model. An automorphism fixing this support fixes every pure real value, hence $g (p x) = g (x)$ . On each complementary interval of the support in $L$ , increasing automorphisms fixing the support act transitively: a piecewise-affine increasing map sends any prescribed interior point to another and fixes the boundary, and in the rational case its pieces can have rational coefficients. Hence $g$ is constant on each such interval. No assertion is made that supported points move.

givenF1F2F4

2.1

Put $ε_{n} = 1 / (n + 1)$ . There is an increasing bijection $p_{n}$ of the real order fixing $e$ and sending every point of $e_{n}$ within distance $ε_{n}$ of $e$ . Here is the component construction. On a bounded complementary interval $(c, d)$ of $e$ , choose $c < u < v < d$ with $[u, v] \cap e_{n} = \emptyset$ : the closed countable set $e_{n}$ cannot contain an interval by [F3]. Choose $0 < δ < \min (ε_{n}, (d - c) / 3)$ . Map $[c, u]$ affinely to $[c, c + δ]$ , $[u, v]$ affinely to $[c + δ, d - δ]$ , and $[v, d]$ affinely to $[d - δ, d]$ . The pieces agree, are strictly increasing and send the portion of $e_{n}$ into the two boundary strips. On a right unbounded component $(c, \infty)$ , choose $R > c$ above all of $e_{n}$ , map $[c, R]$ affinely onto $[c, c + ε_{n} / 2]$ , and continue by a positive-slope affine bijection onto $[c + ε_{n} / 2, \infty)$ ; treat the left ray by reflection. Fix $e$ pointwise. The component maps and this fixed part form a global increasing bijection, since each component maps onto itself with its endpoints fixed. AC in $M$ permits these choices for all components and $n$ .

step 1.1F2F3

2.2

Order completeness from step 1.3 implies compactness of the rational-model interval without choice. Given an internal open cover, internally form $C = {x \in L : [a, x] has a finite subcover}$ . It contains $a$ and has a supremum $c$ . A cover member containing $c$ contains an interval neighbourhood of $c$ . If $c > a$ , choose $x \in C$ in the left part of that neighbourhood using the supremum property; its finite subcover together with this member covers $[a, c]$ . If $c = a$ , that member alone covers $[a, c]$ . Thus $c \in C$ . If $c < b$ , the same neighbourhood extends to a point to the right of $c$ and would put that point in $C$ , a contradiction. Hence $c = b$ , and the cover has a finite subcover. This whole argument is internal to $N$ . Combined with step 1.2, both intervals are compact Hausdorff and therefore normal by [F5].

step 1.2step 1.3F2F5

2.3

In the rational model there are only finitely many support points and complementary intervals. Continuity at each interior support point makes the constants on its two adjacent intervals equal to its value: if a constant differed, disjoint real neighbourhoods of the two values would contradict continuity along that adjacent interval. The same one-sided argument applies at $a, b$ . Moving across the finite ordered list of support points proves that $g$ is constant on $L$ .

step 1.4F4

2.4

In the real model the complementary intervals are countable in $M$ : enumerate the ground rationals and assign to each interval the least rational index inside it; disjoint intervals get different indices. Together with the countable support and step 1.4 this makes $g [L]$ at most countable in $M$ , by [F3]. But $g$ , viewed in ground real coordinates, is continuous: the preimage of every ground open real set is internally open (the pure kernel is unchanged), and internally open subsets of $L$ are ground open subsets. If two values differed, the intermediate-value theorem on the real subinterval between their arguments would put a nondegenerate real interval in $g [L]$ , contrary to [F3]. Thus $g$ is constant here as well.

step 1.4F1F3F4

3.1

Let $K = e \cup ⋃_{n} p_{n} [e_{n}]$ . It is countable by [F3] and bounded, since every new point is within $1$ of the bounded nonempty set $e$ . It is closed: if $z \notin e$ , some neighbourhood of $z$ has positive distance from $e$ , so it misses $p_{n} [e_{n}]$ for all sufficiently large $n$ . The remaining finitely many sets $p_{n} [e_{n}]$ , and $e$ , are closed, since increasing real bijections are homeomorphisms (they map order intervals to order intervals). Thus a point outside $K$ has an open neighbourhood missing $K$ . By [F3], $K$ is compact and is an allowed support.

step 2.1F3

4.1

Set $y_{n} = p_{n} (x_{n})$ . Since $p_{n}$ fixes $e$ , $y_{n} \in F_{n}$ ; conjugation makes $p_{n} [e_{n}]$ a support for $y_{n}$ . Hence $K$ supports the graph ${(n, y_{n}) : n \in N}$ . Its members and all their membership descendants are hereditarily symmetric by [F1], so this graph belongs to $N$ . It is a choice function for the given sequence. This proves Countable Choice in the real model; AC was used only in $M$ to obtain the supported graph.

step 1.1step 2.1step 3.1F1F3

5.1

The endpoint atoms $a, b$ are distinct closed singleton subsets of the normal space $L$ . A Urysohn separator would take values $0$ and $1$ at these endpoints and would be a nonconstant internal continuous real-valued function, contradicting steps 2.3 and 2.4. Hence Urysohn's lemma fails in both models, while step 4.1 establishes Countable Choice in the real model.

step 4.1step 2.2step 2.3step 2.4F2F5∎

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

Extreme amenability yields BPI in finite-support permutation models

Statement

Work internally in an arbitrary model $M$ of ZFA+AC (ZFA universes, atoms, pure sets, and the kernel, The Axiom of Choice); no external well-foundedness or transitivity of $M$ is assumed. Let $M$ see a group $G$ acting on a set of atoms $A$ , and let its associated hereditarily symmetric interpretation be built from the finite-support filter (Permutation groups, stabilizers, supports, and normal filters, Symmetric and hereditarily symmetric sets). Suppose that for every finite $E \subseteq A$ , $M$ satisfies that the pointwise stabiliser $fix (E)$ is extremely amenable in the topology of pointwise convergence: every internally continuous action on an internally nonempty compact Hausdorff space has a fixed point. Then the hereditarily symmetric interpretation satisfies BPI (The Boolean prime ideal principle).

Facts & Assumptions

Given: Inside $M$ , a finite-support permutation system, the stated extreme-amenability hypothesis, an internally nontrivial Boolean algebra $B$ of the hereditarily symmetric interpretation, and a finite support $E$ of its entire algebra structure (underlying set, operations and distinguished constants). Every compactness, topology and fixed-point assertion below is interpreted in $M$ .

[F1]

The internal rank recursion defining hereditary symmetry and the standard normal-filter closure argument give a ZFA interpretation in any model of ZFA+AC: the action and hereditary-symmetry predicate are defined by the rank recursion of $M$ ; normality gives invariance; the power set is the set of hereditarily symmetric members of the ambient power set; and Separation and Replacement are the relativised instances in $M$ . An object belongs to that interpretation exactly when it is hereditarily symmetric. Admitting a finite support proves symmetry of the object itself, but membership additionally requires hereditary symmetry of every membership descendant (Symmetric and hereditarily symmetric sets, Permutation groups, stabilizers, supports, and normal filters).

[F2]

Internally in $M$ , AC implies BPI (The Axiom of Choice, AC implies BPI) and hence the set ultrafilter lemma (BPI and the set ultrafilter lemma are equivalent). Under that lemma a product of compact Hausdorff spaces is compact (Assuming the ultrafilter lemma, an arbitrary product of compact Hausdorff spaces is compact), and a closed subspace of a compact space is compact (A closed subspace of a compact space is compact, and a finite union of compact subspaces is compact). These are theorem instances evaluated by $M$ , not external compactness claims about an ill-founded presentation of $M$ .

[F4]

Prime ideals contain $0$ , exclude $1$ , are downward closed and closed under joins, and satisfy the meet-primality condition (Boolean ideals, filters, prime ideals and ultrafilters). BPI asserts existence for every nontrivial Boolean algebra (The Boolean prime ideal principle).

[F3]

Extreme amenability of $H = fix (E)$ : every continuous action of $H$ on a nonempty compact Hausdorff space has a fixed point. [given]

[L1]

Basic product neighbourhoods in $2^{B}$ restrict finitely many coordinates; subspace neighbourhoods are their traces (The product set $\prod_{i \in I} X_{i}$ 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, Subspace topology: the traces of the open sets, its closed sets and its bases, the continuity of the inclusion, and the characteristic property of a map into a subspace). Continuity is tested by open neighbourhoods (Continuity of a map of topological spaces at a point and globally, Topology on a set, open and closed sets, clopen sets, the closed-set axiomatisation, and the coarser/finer comparison). The finite discrete space $2$ is compact and Hausdorff (Open cover, subcover, and compact topological space; a compact subset is a subspace that is compact in its own right, Hausdorff space: distinct points have disjoint open neighbourhoods; every metrizable space is Hausdorff and the indiscrete topology on two points is not).

Proof

technique · direct

1.1

Carry out the argument in $M$ . Let $B$ be an internally nontrivial Boolean algebra of the hereditarily symmetric interpretation, and choose a finite support $E$ for its entire structure; put $H = fix (E)$ . The induced action of $H$ on its underlying set preserves every algebra operation and constant, so acts by Boolean automorphisms. Each $b \in B$ is hereditarily symmetric and has a finite support of its own.

givenF1

2.1

In $M$ let $S (B)$ be the set of prime ideals, represented by their characteristic functions in $2^{B}$ . It is internally nonempty by [F2]. It is internally closed: failure of any condition in [F4] is witnessed by finitely many coordinates ( $0$ , $1$ , a pair $a \leq b$ , a join or a meet), so every nonideal or nonprime subset has a basic product neighbourhood disjoint from $S (B)$ . Internally, $2^{B}$ is compact by [F2] and [L1], and $S (B)$ is therefore compact with its subspace topology. Distinct subsets differ at a coordinate, whose two complementary cylinders separate them, so $S (B)$ is Hausdorff. AC is used in $M$ for BPI and the resulting product compactness; it is not assumed in the hereditarily symmetric interpretation.

step 1.1F2F4L1

2.2

For $h \in H$ and $P \in S (B)$ put $h P = {h b : b \in P}$ . Boolean automorphisms preserve the prime-ideal conditions, so this defines an action on $S (B)$ . To prove joint continuity, fix $(h_{0}, P_{0})$ and a basic neighbourhood of $h_{0} P_{0}$ specifying membership on a finite set $C \subseteq B$ . For each $b \in C$ , take a finite support of $h_{0}^{- 1} b$ , and let $D$ be their finite union. Then $K = H \cap fix (D)$ is open in $H$ for the pointwise-convergence topology on atoms. The coset $h_{0} K$ is open: its defining restrictions are $h (a) = h_{0} (a)$ for $a \in D$ , within $H$ . Let $V$ consist of prime ideals agreeing with $P_{0}$ on $h_{0}^{- 1} C$ . For $h = h_{0} k \in h_{0} K$ and $P \in V$ , one has $h^{- 1} b = k^{- 1} h_{0}^{- 1} b = h_{0}^{- 1} b$ for $b \in C$ , so $b \in h P$ exactly when $b \in h_{0} P_{0}$ . Thus $(h_{0} K) \times V$ maps into the prescribed neighbourhood. This proves joint continuity; it does not assert openness of a prime ideal's point stabilizer.

step 1.1F1F4L1

3.1

Inside $M$ , apply the Given extreme amenability of $H$ to the internally nonempty compact Hausdorff space of step 2.1 and the continuous action of step 2.2. Obtain a prime ideal $P$ fixed by every member of $H$ .

step 2.1step 2.2F3

4.1

The finite set $E$ supports $P$ . Moreover every member of $P$ belongs to $B$ and hence is hereditarily symmetric. Thus $P$ is hereditarily symmetric by [F1], so belongs to the interpretation. The prime-ideal conditions are bounded formulas about $P$ , $B$ , their operations and their members. Relativising those bounded quantifiers to the hereditarily symmetric interpretation changes no witness: all elements of $B$ already lie there, and the operations are the same supported objects. Therefore the interpretation itself satisfies that $P$ is a prime ideal of $B$ . No appeal to external transitivity is made.

step 1.1step 3.1F1F4

5.1

The reasoning in steps 1.1--4.1 is an argument formalised inside the arbitrary model $M$ . Since $B$ was an arbitrary internally nontrivial Boolean algebra of its hereditarily symmetric interpretation, the internal prime ideal furnished in step 4.1 establishes BPI there. The trivial algebra requires no prime ideal. This conclusion therefore applies equally to externally ill-founded models used in relative-consistency arguments.

step 4.1F4∎

Remarks

What the extreme-amenability hypothesis is used for. It replaces the missing choice inside the symmetric interpretation by a fixed-point statement in $M$ : the prime-ideal space is internally nonempty and compact there, and one stabiliser of the algebra's finite support has a fixed point, which is then supported by that same finite set.
Why finite supports. The argument needs the stabiliser of the algebra to be one of the groups assumed extremely amenable, and in a finite-support model the stabiliser of any set with finite support has finite support; no claim is made for infinite supports.

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

Finite stabilizers in Aut(Q,<) are extremely amenable

Statement

$Aut (Q, <)$ , with the topology of pointwise convergence, is extremely amenable, and so is the pointwise stabiliser of every finite subset of $Q$ : every continuous action of such a group on a nonempty compact Hausdorff space has a fixed point.

Facts & Assumptions

Given: A finite subset $E \subseteq Q$ and a continuous action of $fix (E)$ on a nonempty compact Hausdorff space.

[F1]

Finite Ramsey for colourings of $k$ -element subsets: for all positive $k, c, r$ there is $N$ with $N \to (r)_{c}^{k}$ (For positive $k, c, r$ there is an $N$ such that every $c$ -colouring of $[N]^{k}$ has a monochromatic $r$ -element set, Finite colourings of $k$ -element subsets, monochromatic sets, and the arrow notations $N \to (s, t)^{2}$ and $N \to (r)_{c}^{k}$ , The natural numbers $N$ (von Neumann)).

[F2]

The KPT correspondence: for a Fraïssé structure with rigid finite substructures and the Ramsey property, the automorphism group is extremely amenable. This is Kechris--Pestov--Todorcevic, Theorem 4.7; its finite-linear- order instance is the one used here. The Ramsey hypothesis for that instance, but not the KPT fixed-point conclusion itself, is supplied by For positive $k, c, r$ there is an $N$ such that every $c$ -colouring of $[N]^{k}$ has a monochromatic $r$ -element set.

[L1]

A finite point stabiliser of $Aut (Q, <)$ is the direct product of the automorphism groups of the finitely many open intervals cut out by the support, each of which is order-isomorphic to $Q$ ; a finite product of extremely amenable groups is extremely amenable, because fixed points can be taken one factor at a time: an action of $G_{1} \times G_{2}$ on a compact space has a fixed point for $G_{1}$ by extreme amenability of $G_{1}$ , the fixed-point set is compact and invariant under $G_{2}$ , and extreme amenability of $G_{2}$ supplies a point fixed by both. [given]

Proof

technique · direct

1.1

The age of $(Q, <)$ consists of the finite linear orders, each of which is rigid, and the Ramsey property required by the KPT correspondence is precisely finite Ramsey for colourings of $k$ -element subsets, since a colouring of embeddings of the $a$ -element order into an $N$ -element order is a colouring of $a$ -element subsets of $N$ and a homogeneous $b$ -element subset is a monochromatic copy.

1.2

For the stabiliser of a finite $E$ : the points of $E$ cut $Q$ into finitely many open intervals, each order-isomorphic to $Q$ , and $fix (E)$ is the direct product of the automorphism groups of those intervals.

givenL1

2.1

By [F2] applied to the age of $(Q, <)$ described in step 1.1, $Aut (Q, <)$ is extremely amenable.

step 1.1F2

3.1

By step 2.1 and [L1], applied factor by factor to the finitely many interval automorphism groups of step 1.2, $fix (E)$ is extremely amenable: the fixed-point set of an action is computed one factor at a time, and each factor contributes a fixed point because it is an automorphism group of a copy of $Q$ and hence extremely amenable by step 2.1.

step 2.1step 1.2L1

4.1

Thus $Aut (Q, <)$ and each of its finite point stabilisers is extremely amenable, which is the assertion of the statement; the argument used the ZF theorem of [F1] and the fixed-point criterion of [F2] only.

step 2.1step 3.1F1F2∎

Remarks

Why the finite-linear-order instance suffices here. The permutation model of this pair uses only the rational-ordered atom set of Brunner's ordered Läuchli permutation models, whose automorphism group is $Aut (Q, <)$ ; the finite stabiliser form of the statement is what the BPI theorem consumes.
The product argument is where "finite" is used. A finite product of extremely amenable groups is extremely amenable by the one-factor-at-a-time argument; an infinite product need not be, and no such claim is made.

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

The Läuchli Urysohn obstruction is injectively boundable

Statement

Let $T$ be the sentence asserting that there are a topological space $(X, τ)$ and disjoint closed sets $E_{0}, E_{1} \subseteq X$ such that $X$ is normal and no continuous $f : X \to R$ satisfies $f [E_{0}] \subseteq {0}$ and $f [E_{1}] \subseteq {1}$ . The sentence $T$ is boundable, hence injectively boundable, and it admits an atom-blind typed transfer certificate in the sense of Boundable sentences over an atom set. A fixed absolute bound below $ω + ω$ captures all subsets of $X$ , members of $τ$ , and candidate real-valued function graphs. Brunner's ordered continuum is a witness to $T$ in each of the two permutation models.

Facts & Assumptions

Given: The ordered Läuchli continuum $L$ of Brunner's ordered Läuchli permutation models, its two endpoint closed sets, and the failure of Urysohn's lemma in the two models of Brunner's models satisfy the required choice and Urysohn obstructions.

[F1]

Boundable sentences over an atom set: a formula is boundable only when it is provably equivalent, uniformly in ZFA, to its relativisation to $V_{α} (⋃ \vec{x})$ for a fixed absolutely defined ordinal $α$ ; a syntactic restriction alone is insufficient (Boundable sentences over an atom set).

[F2]

The space $L$ is a compact linearly ordered normal space with two distinct closed endpoint singletons, and every continuous real-valued function on it is constant (Brunner's models satisfy the required choice and Urysohn obstructions, Normal spaces and $T_{4}$ spaces, with the source disagreement over whether normality includes $T_{1}$ stated explicitly, Continuity of a map of topological spaces at a point and globally).

[F3]

Every boundable statement is, up to equivalence, injectively boundable (Pincus's Fact 5.4 as reproduced in the cited Tachtsis paper).

[L1]

For the parameter tuple $(X, τ, E_{0}, E_{1})$ put $B = X \cup τ \cup E_{0} \cup E_{1}$ . Then $X, τ, E_{0}, E_{1}$ and every subset of $X$ lie in $V_{1} (B)$ . The canonical pure codes for $R$ , its topology, $0$ and $1$ , and every graph $f \subseteq X \times R$ lie in $V_{ω + n} (B)$ for one fixed finite $n$ : ordered-pair and graph coding adds only finitely many power-set iterations. Hence all of them lie below $V_{ω + ω} (B)$ (Boundable sentences over an atom set).

Proof

technique · direct

1.1

Let $Φ (X, τ, E_{0}, E_{1})$ be the following fixed membership-language formula: $τ \subseteq P (X)$ is a topology; $E_{0}, E_{1} \subseteq X$ are disjoint, nonempty and closed; every two disjoint closed subsets $C, D \subseteq X$ are contained in disjoint members of $τ$ ; and there is no function graph $f \subseteq X \times R$ whose inverse image of every open subset of $R$ belongs to $τ$ and which takes the constant values $0$ on $E_{0}$ and $1$ on $E_{1}$ . This says exactly that $(X, τ)$ is normal and the specified closed pair has no Urysohn separator.

2.1

To establish boundability it suffices to prove the uniform ZFA equivalence between $Φ$ and its relativisation to the fixed segment $V_{ω + ω} (B)$ .

step 1.1F1suffices: uniform relativisation

2.2

Expand the abbreviations in step 1.1. The topology axioms quantify over members and subfamilies of $τ$ ; closedness and normality quantify over subsets of $X$ and members of $τ$ ; the function condition quantifies over ordered-pair graph entries; and continuity quantifies over the fixed pure real topology and subsets of $X$ obtained as graph preimages. Every one of these domains is contained in the relative segment of [L1]. Consequently ZFA proves $Φ (X, τ, E_{0}, E_{1}) ⟷ Φ^{V_{ω + ω} (B)} (X, τ, E_{0}, E_{1}) .$ For the forward implication, every quantified object in the expanded formula is present in the segment by step 1.1 and [L1], so restricting the quantifiers loses no candidate closed set, normality witness, real open set, or function graph. For the reverse implication the same domain equalities show that each restricted universal quantifier ranges over the entire bounded sort named in the unrestricted formula, and each restricted existential witness is an actual member of that sort. Thus the two formulas have identical bounded domains, uniformly in every ZFA universe.

step 1.1step 2.1L1F1

3.1

The relativised formula is atom-blind: its only atomic tests are equality and membership among the carried sorts and the fixed pure real codebook. Points of $X$ are treated opaquely; the formula never asks whether a point is an atom or examines any members it may have outside the carried incidence structure. Therefore the same typed formula describes a normal space and a failed separator after an atom-to-set embedding.

step 1.1step 2.2L1F1

4.1

By step 2.2 and [F1], the existential closure of $Φ$ is boundable with the fixed absolute bound $ω + ω$ ; by [F3] it is injectively boundable, and step 3.1 supplies the atom-blind typed certificate. In each Läuchli model, take $X = L$ , $τ$ its order topology and $E_{0} = {a}$ , $E_{1} = {b}$ . They satisfy $Φ$ by [F2], because a separator would be a nonconstant continuous real-valued map.

step 1.1step 2.2step 3.1F1F2F3discharge-construct∎

Remarks

Why a certificate is needed at all. The transfer theorem used below accepts a sentence together with an absolute bound and a typed incidence structure; without the certificate the transfer step would have to be taken on trust. The certificate produced here is the one the Pincus and Jech–Sochor interfaces consume.
What the certificate does not say. It speaks only of the carried continuum and its separating functions; it asserts nothing about the rest of the permutation model, and in particular it does not certify countable choice or BPI, which are transferred through the separate exceptional clauses.

TheoremStatement: Literature-sourcedProof: AI-adaptedaudited 2026-09-22Open item page →

Pincus transfer for BPI and injectively boundable conjunctions

Statement

Let a ZFA permutation model be given, and let $T_{1}, \dots, T_{k}$ be finitely many certified atom-blind boundable sentences. Then the conjunction $T_{1} \land \dots \land T_{k}$ transfers to a model of $Z F$ . Moreover, if the permutation model satisfies BPI (The Boolean prime ideal principle), BPI may be conjoined with the certified sentences and transferred with them. If the model satisfies both BPI and Countable Choice (The Axiom of Countable Choice ( ${A C}_{ω}$ )), the simultaneous conjunction $B P I \land {A C}_{ω}$ may be transferred with the certified sentences. This item does not assert an ${A C}_{ω}$ -only exceptional clause. No arbitrary ZFA truth, no full Choice, and no uncertified sentence is transferred.

Facts & Assumptions

Given: A permutation model of ZFA with atom set $A$ ; finitely many certified atom-blind boundable sentences with their absolute rank bounds.

[F1]

A boundable statement is injectively boundable (Pincus, cited in Tachtsis as Fact 5.4). Thus an atom-blind boundable statement carrying the typed certificate of Jech–Sochor transfer for certified atom-blind boundable sentences has the preservation data needed by the Pincus theorem (Boundable sentences over an atom set).

[F2]

Pincus's transfer theorem admits BPI as a named exceptional conjunct alongside a finite conjunction of injectively boundable statements. Tachtsis Theorem 5.5 records the stronger simultaneous $B P I \land {A C}_{ω}$ form. It does not state an ${A C}_{ω}$ -only exceptional clause, so none is used here. This is direct source input, not an inference from the orientation-only remark Pincus transfer interfaces and preservation limits (The Boolean prime ideal principle, The Axiom of Countable Choice ( ${A C}_{ω}$ )).

Proof

technique · direct

1.1

Fix the finite list $T_{1}, \dots, T_{k}$ of certified sentences. By [F1], each $T_{j}$ is injectively boundable; the finite conjunction retains the finitely many certificates and absolute bounds.

givenF1

2.1

Let $Ω$ be the conjunction of the $T_{j}$ , together with BPI when that exceptional clause is to be used, and together with both BPI and ${A C}_{ω}$ when the simultaneous exceptional clause is to be used. No other truth of the permutation model is included in $Ω$ , and ${A C}_{ω}$ is never adjoined here without BPI.

step 1.1givenF2

3.1

Apply the corresponding Pincus theorem in [F2] to $Ω$ . It produces an atom-free model of ZF satisfying every injectively boundable conjunct and the named exceptional principle or principles. In particular, omitting the exceptional clauses transfers the finite conjunction alone, adjoining BPI transfers BPI with it, and adjoining the simultaneous $B P I \land {A C}_{ω}$ clause transfers both principles with it.

step 1.1step 2.1F2

4.1

Step 3.1 is exactly the transfer asserted in the Statement. BPI and the simultaneous $B P I \land {A C}_{ω}$ conjunction enter only through [F2]'s exceptional clauses and are not relabelled as injectively boundable; the typed certificates restrict all other transferred content to the named $T_{j}$ .

step 2.1step 3.1F1F2∎

Remarks

What is exceptional about BPI and countable choice. BPI is transferable alongside an injectively boundable conjunction, and the cited stronger theorem transfers BPI and countable choice together. Neither principle is relabelled as injectively boundable here, and this interface supplies no countable-choice-only transfer.
What the statement does not do. It does not transfer the truth of the permutation model wholesale, and in particular it does not transfer the failure of well-orderability of the atom set or the countable-choice structure of the model; only the named principles and the certified sentences cross.

TheoremStatement: Literature-sourcedProof: Literature-sourcedaudited 2026-09-22Open item page →

Relative consistency of Countable Choice without Urysohn's lemma

Statement

If $Z F$ is consistent, then $Z F + {A C}_{ω} + failure of Urysohn’s lemma$ is consistent: there is a model of $Z F$ with countable choice (The Axiom of Countable Choice ( ${A C}_{ω}$ )) in which some normal space has two disjoint closed sets admitting no continuous separation (Normal spaces and $T_{4}$ spaces, with the source disagreement over whether normality includes $T_{1}$ stated explicitly).

Facts & Assumptions

Given: The assumed consistency of $Z F$ .

[F1]

Tachtsis's cited theorem, read together with its published erratum, proves the exact external implication $Con (Z F) ⟹ Con (Z F + {A C}_{ω} + \neg U R Y) .$ Here $U R Y$ is the usual Urysohn separation assertion for disjoint closed subsets of a normal space. This item records that published relative-consistency theorem; it does not reconstruct the permutation-model and transfer argument.

[F2]

By definition, $\neg U R Y$ supplies a normal space $X$ and disjoint closed subsets $A, B \subseteq X$ for which there is no continuous $f : X \to [0, 1]$ satisfying $A \subseteq f^{- 1} ({0}) and B \subseteq f^{- 1} ({1}) .$ Equivalently, such an $f$ would have $f (a) = 0$ for every $a \in A$ and $f (b) = 1$ for every $b \in B$ (Normal spaces and $T_{4}$ spaces, with the source disagreement over whether normality includes $T_{1}$ stated explicitly). Equality of the images with the endpoint singletons is not the definition: it is too strong when either closed set is empty.

Proof technique: direct.

Proof

1.1

Assume $Con (Z F)$ . The published relative-consistency theorem [F1], with its erratum included in the cited interface, yields a model of $Z F + {A C}_{ω} + \neg U R Y$ .

givenF1

2.1

In that model ${A C}_{ω}$ is precisely countable choice (The Axiom of Countable Choice ( ${A C}_{ω}$ )), while [F2] expands $\neg U R Y$ as a normal space with two disjoint closed sets admitting no continuous Urysohn separator. Thus the model has exactly the two properties asserted in the Statement.

step 1.1F2

3.1

Therefore $Con (Z F) ⟹ Con (Z F + {A C}_{ω} + failure of Urysohn’s lemma)$ , as claimed. This proof depends on the corrected published theorem itself and makes no unsupported Pincus transfer of countable choice alone.

step 2.1F1∎

TheoremStatement: Literature-sourcedProof: AI-adaptedaudited 2026-09-22Open item page →

Relative consistency of BPI without Urysohn's lemma

Statement

If $Z F$ is consistent, then $Z F + B P I + failure of Urysohn’s lemma$ is consistent: there is a model of $Z F$ in which the Boolean prime ideal principle holds (The Boolean prime ideal principle) and some normal space has two disjoint closed sets admitting no continuous separation (Normal spaces and $T_{4}$ spaces, with the source disagreement over whether normality includes $T_{1}$ stated explicitly).

Facts & Assumptions

Given: The rational-ordered finite-support Läuchli model, its continuum, and the assumed consistency of $Z F$ .

[F1]

In the rational-ordered finite-support model the stabilisers of finite atom sets are extremely amenable, because they are finite products of copies of $Aut (Q, <)$ (Finite stabilizers in Aut(Q,<) are extremely amenable, Brunner's ordered Läuchli permutation models).

[F2]

Extreme amenability of the finite stabilisers yields BPI in the finite-support permutation model (Extreme amenability yields BPI in finite-support permutation models).

[F3]

The same model contains the ordered continuum with every continuous real-valued function constant, hence a normal space violating Urysohn's lemma (Brunner's models satisfy the required choice and Urysohn obstructions), and that failure is certified with an absolute bound (The Läuchli Urysohn obstruction is injectively boundable).

[F4]

Pincus transfer with the exceptional clauses permits BPI to be conjoined with the certified sentence (Pincus transfer for BPI and injectively boundable conjunctions). The verified constructible-universe reduction gives $Con (Z F) \Rightarrow Con (Z F C + G C H)$ (Formal consistency of ZFC plus GCH relative to ZF), and countable first-order completeness supplies a model of that theory without any transitivity or well-foundedness conclusion (Completeness for explicitly countable set languages).

Proof

technique · direct

1.1

Assume $Con (Z F)$ . By [F4] obtain a possibly externally ill-founded model $M$ of $Z F C + G C H$ . All constructions in the next steps are interpreted internally in $M$ .

givenF4

2.1

Inside $M$ , let $A = {⟨ 0, q ⟩ : q \in Q^{M}}$ , ordered by the rational order of $M$ , and represent sets by tagged objects $⟨ 1, S ⟩$ . Define the tagged ZFA hierarchy by $X_{0} = A$ , $X_{α + 1} = A \cup {⟨ 1, S ⟩ : S \subseteq X_{α}}$ and unions at limits, and put $u \in_{*} ⟨ 1, S ⟩$ exactly when $u \in S$ . Interpreted inside $M$ , this is a model of ZFA+AC: the usual tagged constructions give Extensionality, Pairing, Union and Power Set; translated Separation and Replacement are instances in $M$ (Collection bounds the construction ranks of Replacement images); minimal construction rank gives Foundation; the tagged copy of $ω^{M}$ gives Infinity; and an $M$ -well-order of every underlying member set gives the tagged choice function. This internal tagged construction does not require $M$ to be externally transitive.

step 1.1

3.1

In this ZFA+AC interpretation form the rational-ordered finite-support Läuchli model of [F1]. The automorphism group and all finite stabilisers are the objects computed internally by $M$ . Thus [F1] gives their internal extreme amenability, and the arbitrary-ground formulation [F2] gives BPI in the hereditarily symmetric interpretation.

step 2.1F1F2

4.1

By [F3] the same interpretation contains the certified Urysohn obstruction, so BPI and that certified sentence hold together there.

step 3.1F3

5.1

By [F4], the conjunction of BPI with the certified sentence transfers to an atom-free model of $Z F$ . Therefore $Con (Z F) \Rightarrow Con (Z F + B P I + \neg U R Y) .$ This is an external relative-consistency construction. The model supplied by completeness need not be transitive; the internal tagged interpretation and the arbitrary-ground BPI theorem are precisely what makes the construction apply. No unprovided uniform proof-code reduction for the subsequent permutation and Pincus constructions is asserted.

step 1.1step 2.1step 3.1step 4.1F4∎

CorollaryStatement: AI-adaptedProof: AI-generatedaudited 2026-09-22Open item page →

Brunner's endpoint obstruction also refutes bounded Tietze extension

Statement

Let $L$ be the compact normal ordered continuum of Brunner's models satisfy the required choice and Urysohn obstructions with its two distinct endpoint closed sets $A$ and $B$ . The continuous map $g : A \cup B \to [0, 1]$ that is $0$ on $A$ and $1$ on $B$ has no continuous extension to $L$ . Consequently $Con (Z F)$ implies both $Con (Z F + {A C}_{ω} + failure of bounded Tietze extension)$ and $Con (Z F + B P I + failure of bounded Tietze extension)$ .

Facts & Assumptions

Given: The continuum $L$ , its two endpoint closed sets $A, B$ , and the function $g$ that is $0$ on $A$ and $1$ on $B$ .

[F1]

In $L$ every continuous real-valued function is constant, and $L$ is a compact Hausdorff, hence normal, space (Brunner's models satisfy the required choice and Urysohn obstructions, Normal spaces and $T_{4}$ spaces, with the source disagreement over whether normality includes $T_{1}$ stated explicitly, Continuity of a map of topological spaces at a point and globally).

[F2]

The subspace $A \cup B$ carries the subspace topology, in which a subset is open exactly when it is the trace of an open set of $L$ (Subspace topology: the traces of the open sets, its closed sets and its bases, the continuity of the inclusion, and the characteristic property of a map into a subspace).

[F3]

Conditional on $Con (Z F)$ , the relative-consistency theorems of this page give, respectively, a model of $Z F + {A C}_{ω}$ and a model of $Z F + B P I$ in which some normal space has two disjoint closed sets admitting no continuous separation (Relative consistency of Countable Choice without Urysohn's lemma, Relative consistency of BPI without Urysohn's lemma).

[L1]

The interval $[0, 1]$ is a closed bounded interval of $R$ (Intervals of $R$ : the nine order-convex forms, nondegeneracy, and length).

Proof

technique · direct

1.1

The sets $A$ and $B$ are complementary closed subsets of the subspace $A \cup B$ , so each is clopen in that subspace by [F2] and [L1].

givenF2L1

2.1

By step 1.1, the map $g$ that is $0$ on the clopen set $A$ and $1$ on the clopen set $B$ is continuous on $A \cup B$ : the preimage of any subset of $[0, 1]$ is a union of some of $A$ , $B$ , both of which are open in the subspace.

step 1.1F2

3.1

Suppose $G : L \to [0, 1]$ were a continuous extension of $g$ . Then $G$ is a continuous real-valued function on $L$ , hence constant by [F1]; but $G$ equals $0$ on $A$ and $1$ on $B$ , and $A, B$ are nonempty, so no constant function can agree with $g$ .

step 2.1F1

4.1

Therefore no continuous extension of $g$ exists, which is the failure of bounded Tietze extension for the closed subspace $A \cup B$ of $L$ . For either model supplied by [F3], let $X$ be its normal-space witness and let $C, D$ be the disjoint closed sets admitting no continuous separation. The map on $C \cup D$ with values $0$ on $C$ and $1$ on $D$ is continuous by the same clopen-subspace argument as steps 1.1--2.1; any continuous extension to $X$ would separate $C$ and $D$ , contrary to their defining property. Thus each model supplied by [F3] also witnesses failure of bounded Tietze extension, giving the two displayed consistency statements.

step 1.1step 2.1step 3.1F3∎

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

The Good-Tree-Watson symmetric Stone model

Definition

Work in a transitive ZFC ground model $M$ with GCH (The Axiom of Choice), and fix a regular uncountable cardinal $λ$ . Put $P : = Fn (λ \times R \times λ \times λ, 2, λ),$ the set of partial functions with domain a subset of $λ \times R \times λ \times λ$ of size below $λ$ and values in $2$ , ordered by reverse inclusion: $q \leq p$ means $p \subseteq q$ (Forcing preorders, compatibility and filters).

Fix an $M$ -generic filter $H \subseteq P$ in an ambient universe. Let $B : = RO (P)$ be the regular-open completion (Completeness, regular opens, and order continuity, Choice-free regular open completion of forcing preorders).

The group. Put $J = λ \times R \times λ$ . Use all permutations $π$ of $J$ of the form $π (ξ, r, α) = (ξ, ρ_{ξ} (r), σ_{ξ, r} (α)), ρ_{ξ} (r) = ε_{ξ} r + t_{ξ},$ where $ε_{ξ} \in {- 1, 1}$ , $t_{ξ} \in R$ , and each $σ_{ξ, r}$ is a permutation of $λ$ . All these data belong to $M$ . The real isometries are allowed independently for different $ξ$ . Composition replaces two real maps by $r \mapsto ε^{'} ε r + ε^{'} t + t^{'}$ in each component; inverses have the same form. The fibre permutations compose with the corresponding reindexing of $r$ , and their inverses are permutations too. Thus these maps form a group, containing translations as well as reflections.

The induced action on conditions fixes the last coordinate: $(π p) (π (ξ, r, α), δ) = p (ξ, r, α, δ) .$ It preserves domain cardinalities and reverse inclusion and has the stated inverse, hence acts by forcing automorphisms. It also acts on $B$ by taking images of regular open sets: an order automorphism is a homeomorphism for the downward-open topology and commutes with interior and closure. Write $G$ for this group of induced automorphisms. Its action on $P$ -names is the recursion of Automorphisms acting on forcing names.

The filter and interpretation. For $e \subseteq J$ of ground-model size less than $λ$ , put $fix (e) = {π \in G : π ∣_{e} = i d}$ . Let $F$ consist of the subgroups containing some such stabilizer. It is upward closed, contains $G = fix (\emptyset)$ , and $fix (e \cup f) = fix (e) \cap fix (f)$ . Also $π fix (e) π^{- 1} = fix (π [e])$ and $∣ π [e] ∣ = ∣ e ∣$ , proving normality. For fewer than $λ$ subgroups in $F$ , ground-model AC chooses their support witnesses; regularity of $λ$ makes their union have size less than $λ$ , and its stabilizer is contained in their intersection. Thus $F$ is $< λ$ -complete in $M$ .

Define $N = {H S}_{F}^{H}$ using the symmetric system $(P, G, F)$ (Symmetric forcing systems, supports, and hereditarily symmetric names). It is a transitive ZF model with $M \subseteq N \subseteq M [H]$ (Hereditarily symmetric interpretations form a transitive ZF model).

The canonical families. For $ξ < λ$ , $r \in R$ and $α < λ$ let $x_{ξ r α} : = {δ < λ : (\exists p \in H) p (ξ, r, α, δ) = 1} .$ Thus $x_{ξ r α}$ is a generic subset of $λ$ , not in general a real. Let $X_{ξ r} : = {x_{ξ r α} : α < λ}$ , let $R_{ξ} : = {X_{ξ r} : r \in R}$ , and let $R : = {R_{ξ} : ξ < λ}$ , keeping $M$ for the ground model. For two distinct triples and any condition, choose a last coordinate $δ < λ$ unused at both triples and extend the condition by opposite values there. This is possible because fewer than $λ$ coordinates have been used. These extensions are dense, so genericity makes all the canonical subsets for distinct triples distinct. In particular the nonempty families $X_{ξ r}$ for distinct $(ξ, r)$ are disjoint. Consequently the rule $d_{ξ} (X_{ξ r}, X_{ξ s}) : = \frac{∣ r - s ∣}{1 + ∣ r - s ∣}$ is a well-defined metric on $R_{ξ}$ , transported from the displayed bounded metric on $R$ ; no metric is induced from the sets $x_{ξ r α} \subseteq λ$ themselves.

The name for $x_{ξ r α}$ is fixed by $fix ({(ξ, r, α)})$ , the name for $X_{ξ r}$ is fixed by $fix ({(ξ, r, α_{0})})$ for any fixed $α_{0} < λ$ , and the names for $R_{ξ}$ and $R$ are fixed by the whole group. Their members are hereditarily symmetric by induction, so all four kinds of canonical object lie in $N$ . The component family has the full index set $λ$ ; this does not assert that the real-label enumeration of each component is in $N$ . The canonical name for $d_{ξ}$ is fixed by the whole group since $∣ ρ_{ξ} (r) - ρ_{ξ} (s) ∣ = ∣ r - s ∣$ ; its subnames are hereditarily symmetric by the same calculation, so $d_{ξ} \in N$ . The metric triangle inequality follows from the real triangle inequality and, for $a, b \geq 0$ , $\frac{a + b}{1 + a + b} \leq \frac{a}{1 + a} + \frac{b}{1 + b}$ ; the function $t \mapsto t / (1 + t)$ is increasing for $t \geq 0$ . Separation and symmetry follow directly from the distinct real labels. Thus the metric assertion is justified internally as well as in the full extension.

The case $λ = ω_{1}$ is the case used for the dependent-choice model below; the same definition with larger $λ$ is the one whose $< λ$ -sequence closure is proved in the next item.

Remarks

Why the presentation is indexed by $λ$ and not by $ω$ . The paper's Theorems 1–3 use the countable index set and finite supports, and the paragraph after Theorem 3 states the regular- $λ$ replacement with supports of size below $λ$ . The dependent-choice model needs the replacement with supports of size $< λ$ . Closure under sequences is not inferred here from the finite-support presentation; it is a separate proof obligation for the regular- $λ$ construction.
What is not claimed here. The definition does not assert dependent choice, the failure of Stone's theorem, or the existence of the metric sum of the components; those are separate items of this page.
Source convention repaired. The source's Theorem 1 proof describes the real actions as identity or reflection, a class not closed under composition: two distinct reflections compose to a nonzero translation. Its Claim 1.3 also uses a reflection on just one component. The componentwise affine isometry group above makes closure and this independence explicit, preserves the displayed metric, and retains all the canonical support calculations.

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

The Good-Tree-Watson symmetric model is closed under omega-sequences from the full extension

Statement

In the regular- $λ$ Good-Tree-Watson construction of The Good-Tree-Watson symmetric Stone model, if $β < λ$ and $g \in M [H]$ is a function with domain $β$ all of whose values lie in the symmetric model $N$ , then $g \in N$ . In particular, for $λ = ω_{1}$ the conclusion holds for $ω$ -sequences: $N$ is closed under $ω$ -sequences from the full generic extension.

Facts & Assumptions

Given: The regular- $λ$ construction, an ordinal $β < λ$ , and a function $g : β \to N$ in $M [H]$ .

[F1]

The forcing $P$ is $< λ$ -closed: the union of a descending chain of conditions of length below $λ$ is a condition, because the union of fewer than $λ$ sets each of size below $λ$ has size below $λ$ by regularity of $λ$ (Forcing preorders, compatibility and filters, The Good-Tree-Watson symmetric Stone model).

[F2]

The forcing theorem identifies the values of names in the generic extension, and the symmetry lemma transports forcing statements along automorphisms of the group; hereditarily symmetric names have hereditarily symmetric images (Forcing theorem, Symmetry lemma for forcing automorphisms, Automorphisms acting on forcing names).

[F3]

The symmetric model is $N = {τ_{H} : τ \in {H S}^{M}}$ . A coordinate set $e$ of ground size below $λ$ supports a name $τ$ when $fix (e)$ fixes that name. This proves symmetry only; hereditary symmetry also requires every subname recursively to be hereditarily symmetric. Every HS name has such a small support by the definition of the generated filter (The Good-Tree-Watson symmetric Stone model, Symmetric forcing systems, supports, and hereditarily symmetric names, Hereditarily symmetric interpretations form a transitive ZF model).

[F4]

AC holds in $M$ (The Axiom of Choice) and well-orders the set $P$ (The well-ordering theorem). A specified class-function rule on a well-order admits transfinite recursion (Transfinite recursion).

[F5]

Forcing persists under strengthening; an $M$ -generic filter containing $p$ meets every ground set dense below $p$ (Monotonicity, density, and decision for forcing, Dense open sets and generic filters over a model). Two members of a forcing filter have a common stronger member (Forcing preorders, compatibility and filters).

[F6]

The all-conditions set-name operation $S (T) = T \times P$ and the Kuratowski pair-name construction give a graph name for any ground family $(τ_{ξ})$ ; its value is $ξ \mapsto (τ_{ξ})_{H}$ (Names for pairs, functions and ordinals). Automorphisms fix check names and permute all of $P$ , so these constructions commute with the name action (Automorphisms acting on forcing names).

Proof

technique · direct

1.1

Choose in $M$ a name $\dot{g}$ for $g$ . By the truth lemma choose $p \in H$ forcing that $\dot{g}$ is a function on $\overset{ˇ}{β}$ . For each $ξ < β$ , define in $M$ the downward-closed set $D_{ξ} = {q \leq p : for some τ \in {H S}^{M}, q ⊩ \dot{g} (\overset{ˇ}{ξ}) = τ} .$ These are sets by Separation: HS is a definable ground class and forcing is definable for this fixed formula. They are downward closed by [F5]. Each $H \cap D_{ξ}$ is nonempty: $g (ξ) \in N$ has an HS name, the truth lemma gives a member of $H$ forcing the equality, and directedness combines it with $p$ . This does not yet choose a simultaneous sequence of names or conditions.

givenF2F3F5

2.1

Put $E_{ξ} = D_{ξ} \cup {q \leq p : no r \leq q belongs to D_{ξ}} .$ Each $E_{ξ}$ is downward closed and dense below $p$ : either a stronger member of $D_{ξ}$ exists or the condition is already in the second part. Their intersection is dense below $p$ . Indeed, from any $r \leq p$ run a recursion of length $β$ : at stage $ξ$ choose the least extension in $E_{ξ}$ in a fixed ground well-order of $P$ ; at limit stages take the union of the preceding partial functions. The final union at $β$ is a condition by [F1], is stronger than $r$ , and remains in every earlier $E_{ξ}$ by downward closure. For $β = 0$ retain $r$ . This is one ground recursion licensed by [F4]; it spends ground AC in the well-order of $P$ .

step 1.1F1F4

3.1

By genericity [F5], fix $q \in H \cap ⋂_{ξ < β} E_{ξ}$ with $q \leq p$ . In fact $q \in D_{ξ}$ for every $ξ$ : step 1.1 supplies some $r_{ξ} \in H \cap D_{ξ}$ , and directedness gives a common stronger member of $H$ below $q, r_{ξ}$ , lying in $D_{ξ}$ . Thus $q$ cannot be in the part of $E_{ξ}$ that forbids all stronger $D_{ξ}$ conditions. All coordinates can now be represented below the same actual generic condition $q$ .

step 1.1step 2.1F5

4.1

Work in $M$ with this condition $q$ . For each $ξ < β$ choose a pair $(τ_{ξ}, e_{ξ})$ such that $τ_{ξ}$ is HS, $∣ e_{ξ} ∣^{M} < λ$ , $e_{ξ}$ supports $τ_{ξ}$ , and $q ⊩ \dot{g} (\overset{ˇ}{ξ}) = τ_{ξ}$ . Such witnesses exist by step 3.1 and [F3]. This is set-sized choice: Collection first bounds witnesses for the set of indices in one ground set, and ground AC chooses from its nonempty witness subsets. Hence the sequences of names and supports belong to $M$ without selecting from a proper class. Put $e = ⋃_{ξ < β} e_{ξ}$ . Ground regularity of $λ$ and ground AC imply $∣ e ∣^{M} < λ$ .

step 3.1F1F3F4

5.1

Use [F6] to form in $M$ the graph name $\dot{k}$ from the names $\overset{ˇ}{ξ}, τ_{ξ}$ . Each automorphism in $fix (e)$ fixes every $τ_{ξ}$ and check name, and therefore fixes $\dot{k}$ . The pair and set-name constructions use only HS constituent names, all of $P$ and finite set operations; their subnames are HS recursively. Thus $\dot{k}$ is hereditarily symmetric, not just supported. The empty graph is covered by the same construction.

step 4.1F3F6

6.1

Since $q \in H$ , every forced equality of step 4.1 holds after evaluation. Consequently $(\dot{k})_{H} = {⟨ ξ, g (ξ) ⟩ : ξ < β} = g$ . By step 5.1 and [F3], $g \in N$ . This proves the assertion for all ground ordinals $β < λ$ , including $ω$ when $λ = ω_{1}^{M}$ . Forcing does not add ordinals, so these are exactly the ordinals below the fixed ordinal $λ$ in the extension; no assumption that an extension sequence of ground names is already available was needed.

step 3.1step 4.1step 5.1F2F3F6∎

LemmaStatement: Literature-sourcedProof: Literature-sourcedaudited 2026-09-22Open item page →

The symmetric Stone model has no componentwise proper selector

Statement

No function in the symmetric model $N$ of The Good-Tree-Watson symmetric Stone model assigns to every distinguished metric component $R_{ξ}$ a nonempty proper subset of that component.

Facts & Assumptions

Given: A function $f \in N$ with domain $M = {R_{ξ} : ξ < λ}$ and $f (R_{ξ})$ a proper nonempty subset of $R_{ξ}$ for every $ξ$ .

[F1]

Membership in $N$ is hereditary symmetry: $f$ has a support $fix (e)$ in the normal filter, with $e \subseteq λ \times R \times λ$ of size below $λ$ (The Good-Tree-Watson symmetric Stone model, Symmetric forcing systems, supports, and hereditarily symmetric names).

[F2]

In Claim 1.3 of the source, the reflection/identity choice is made separately at each first coordinate. Explicitly, if $ξ < λ$ , $ρ$ is a reflection of $R$ , and $τ$ is a permutation of $λ$ , the coordinate map which is the identity off the $ξ$ -block and sends $(ξ, t, α)$ to $(ξ, ρ (t), τ (α))$ is an allowed automorphism. It fixes $R_{ξ}$ and sends $X_{ξ t}$ to $X_{ξ, ρ (t)}$ . [given, source, Automorphisms acting on forcing names]

[F3]

The symmetry lemma sends a forced statement to its image under a forcing automorphism; if two conditions are compatible, their common extension cannot force contradictory statements (Symmetry lemma for forcing automorphisms, Forcing preorders, compatibility and filters).

Proof

technique · contradiction

1.1

Suppose $f \in N$ is such a selector. Choose a hereditarily symmetric name $\dot{f}$ , a condition $p_{0}$ forcing that $\dot{f}$ has the stated selector property, and a support $e \subseteq λ \times R \times λ$ of size below $λ$ such that every member of $fix (e)$ fixes $\dot{f}$ .

assume-contraF1

2.1

The projection of $e$ to the first coordinate has size below $λ$ , so choose $ξ < λ$ outside it. Strengthen $p_{0}$ to a condition $p$ and choose distinct ground-model reals $r, s$ so that $p$ forces $X_{ξ r} \in \dot{f} (R_{ξ})$ and $X_{ξ s} \notin \dot{f} (R_{ξ})$ .

step 1.1F1

3.1

Let $C$ be the set of third coordinates $α$ occurring in $dom (p)$ at first coordinate $ξ$ . Then $∣ C ∣ < λ$ . Choose a disjoint $C^{'} \subseteq λ$ of the same cardinality and a permutation $τ$ of $λ$ interchanging $C$ and $C^{'}$ and fixing the complement. Let $ρ$ be reflection about $(r + s) / 2$ , and let $π$ be the coordinate-local automorphism from [F2] using $ρ$ and $τ$ at $ξ$ and the identity elsewhere.

step 2.1F2

4.1

The automorphism $π$ lies in $fix (e)$ because it is the identity outside the $ξ$ -block, so $π \dot{f} = \dot{f}$ . It fixes $R_{ξ}$ and swaps $X_{ξ r}$ with $X_{ξ s}$ . By [F3], $π p$ therefore forces $X_{ξ s} \in \dot{f} (R_{ξ})$ and $X_{ξ r} \notin \dot{f} (R_{ξ})$ .

step 1.1step 2.1step 3.1F2F3

4.2

The conditions $p$ and $π p$ are compatible. On every coordinate whose first index is not $ξ$ , $π$ is the identity, so the two conditions agree on their common domain. At first index $ξ$ , every third coordinate used by $p$ lies in $C$ , whereas every third coordinate used by $π p$ lies in the disjoint set $C^{'}$ , so their domains are disjoint there. Hence $p \cup π p$ is a common extension.

step 3.1F3

5.1

The common extension $p \cup π p$ inherits from $p$ the assertion $X_{ξ s} \notin \dot{f} (R_{ξ})$ and from $π p$ the assertion $X_{ξ s} \in \dot{f} (R_{ξ})$ , a contradiction. Therefore no componentwise nonempty proper selector belongs to $N$ .

step 2.1step 4.1step 4.2discharge-contradiction∎

TheoremStatement: Literature-sourcedProof: AI-adaptedaudited 2026-09-22Open item page →

Relative consistency of DC with failure of Stone's theorem

Statement

If $Z F$ is consistent, then $Z F + D C$ is consistent with the failure of Stone's theorem: there is a model of $Z F + D C$ (The axiom of dependent choice: a relation in which every element is related to something admits an $N$ -indexed chain) containing a metric space that is not paracompact (Paracompactness: every open cover has a locally finite open refinement, with no separation axiom built into the word, Refinements, locally finite families, point-finite families, and star refinements). The witness space of this separation is not zero-dimensional: it is the metric sum of the nondegenerate connected components of fact [F4], so no base of clopen sets can exist. (The source's zero-dimensional witness is a different space, the rational-parameter subset $⋃_{n} Q_{n}$ , whose nonparacompactness is proved there in $Z F$ without DC.)

Facts & Assumptions

Given: The regular- $λ$ symmetric model of The Good-Tree-Watson symmetric Stone model with $λ = ω_{1}$ , its components $R_{ξ}$ , and the assumed consistency of $Z F$ .

[F1]

In the transitive-ground presentation of the construction, the model $N$ is a transitive model of ZF between the ground model and the full extension, and it is closed under $ω$ -sequences from the full extension (Hereditarily symmetric interpretations form a transitive ZF model, The Good-Tree-Watson symmetric model is closed under omega-sequences from the full extension, Forcing theorem).

[F2]

Dependent choice holds in $N$ : given a relation $R$ on a set of $N$ that is entire there, for each prescribed starting point $a$ in the set, DC in the full extension supplies an $ω$ -sequence of $R$ -related points starting at $a$ , and by [F1] that sequence lies in $N$ . (The axiom of dependent choice: a relation in which every element is related to something admits an $N$ -indexed chain)

[F3]

No function of $N$ chooses a nonempty proper subset of every component $R_{ξ}$ (The symmetric Stone model has no componentwise proper selector).

[F4]

The metric sum $⨆_{ξ < λ} R_{ξ}$ carries the metric that agrees with the metric of each component and puts distance $1$ between different components; its topology is the topological sum of the components, each $R_{ξ}$ is a clopen connected subspace with more than one point, and the whole space is metrizable (Metric space: $d (x, y) = 0$ iff $x = y$ , symmetry, and the triangle inequality; pseudometric and ultrametric, Open ball, closed ball and sphere in a metric space, The metric topology: a set is open when every one of its points has a ball around it inside the set; closed means open complement, Arbitrary unions and finite intersections of open sets are open, open balls are open and closed balls are closed, Topology on a set, open and closed sets, clopen sets, the closed-set axiomatisation, and the coarser/finer comparison). Because a clopen connected set with more than one point has no proper nonempty clopen subset, the space has no base of clopen sets and is therefore not zero-dimensional.

[F5]

Good--Tree--Watson's Theorem 2 explicitly states, relative to ZF, the consistency of a model with a metrizable nonparacompact space, and their Theorem 3 explicitly states that Stone's theorem is not provable in ZF+DC. In the generalization immediately following Theorem 3 they replace the finite-support construction by the regular- $λ$ construction, take $λ = ω_{1}$ , and use closure under countable sequences to obtain DC. Thus the relative-consistency bridge used here is the published theorem itself, not an inference from the existence of a transitive ground model. [source]

Proof technique: direct.

Proof

1.1

Invoke the external relative-consistency construction of [F5], in its regular- $λ$ form with $λ = ω_{1}$ , and write $N$ for its symmetric model. The invocation is exactly the source's relative-consistency theorem; it does not infer a transitive ground model from $Con (Z F)$ .

givenF5

2.1

The model satisfies DC by [F2], because every $ω$ -sequence in the full extension with values in $N$ is already in $N$ by [F1].

step 1.1F1F2

2.2

In $N$ form the metric sum $X : = ⨆_{ξ < λ} R_{ξ}$ with the metric of [F4]; it is a metrizable space whose components $R_{ξ}$ are clopen and connected.

step 1.1F4

3.1

Let $U = {B_{X} (x, 1 / 3) : x \in X}$ . This is an open cover. Every member lies in one component, since distinct components have distance $1$ , and is a proper subset of that component: under $d (r, s) = ∣ r - s ∣ / (1 + ∣ r - s ∣)$ , a radius- $1 / 3$ ball corresponds to a bounded ordinary interval.

step 2.2F4

4.1

Suppose that $U$ has a locally finite open refining cover $V$ , and define $S = X ∖ ⋃_{V \in V} (\overline{V} ∖ V), S_{ξ} = S \cap R_{ξ} .$ Each $S_{ξ}$ is nonempty. Indeed, a point of $R_{ξ}$ has a nonempty open neighbourhood $W \subseteq R_{ξ}$ meeting only finitely many refinement members $V_{0}, \dots, V_{k}$ . Starting with $W_{0} = W$ , recursively choose the nonempty open set $W_{i + 1} = W_{i} \cap V_{i}$ if that intersection is nonempty, and otherwise choose $W_{i + 1} = W_{i} ∖ \overline{V_{i}}$ . The latter is nonempty: an open $W_{i}$ disjoint from the open set $V_{i}$ cannot be contained in $\overline{V_{i}}$ . Thus every point of $W_{k + 1}$ avoids the boundaries of the $V_{i}$ , and it avoids the boundary of every other refinement member because that member misses $W$ . Hence $W_{k + 1} \subseteq S_{ξ}$ . The set $S_{ξ}$ is also proper. Choose a nonempty $V \in V$ meeting $R_{ξ}$ . Such a member exists because $V$ covers $R_{ξ}$ . By refinement and step 3.1, $V$ lies in $R_{ξ}$ and is contained in a proper ball there. It is therefore a nonempty proper open subset of the connected space $R_{ξ}$ , so $\overline{V} ∖ V$ is nonempty and disjoint from $S_{ξ}$ . Consequently $ξ \mapsto S_{ξ}$ is a function assigning a nonempty proper subset to every component.

step 3.1F4

5.1

By [F3] no such function exists in $N$ ; hence $U$ has no locally finite open refining cover, and $X$ is not paracompact.

step 4.1F3

6.1

Steps 2.1 and 5.1 identify the DC and nonparacompactness conclusions inside the published model. By [F5], that construction has exactly the asserted consistency strength relative to ZF. The argument uses the regular- $λ$ presentation and not the finite-support $ω$ -indexed one.

step 1.1step 2.1step 5.1F5∎

DefinitionDefinition: AI-adaptedProof: Not applicableaudited 2026-09-22Open item page →

Corson's ordered-rational permutation model

Definition

Work internally in a model $M$ of $Z F A + A C$ with an internally countably infinite set $A$ of all its atoms (ZFA universes, atoms, pure sets, and the kernel, The Axiom of Choice); no external well-foundedness or transitivity of $M$ is assumed. Every structure, group, support and hereditarily symmetric set below is computed in $M$ . Equip $A$ , using an internal enumeration, with a copy of the rational ordered Urysohn metric space $U_{Q}^{<}$ : the countable metric space with rational distances which is universal and homogeneous for finite ordered rational metric spaces, and let $G : = Aut (U_{Q}^{<})$ be the group of its order-and-metric automorphisms. The finite-support filter is generated by the pointwise stabilisers $fix (e)$ of finite $e \subseteq A$ (Permutation groups, stabilizers, supports, and normal filters), and Corson's permutation model is the hereditarily symmetric interpretation of Symmetric and hereditarily symmetric sets for that filter; it is a ZFA model with the same atoms and kernel by the internal argument below. The transitive-ground special case is Fraenkel–Mostowski permutation-model theorem. Ambient AC licenses the usual countable construction of the universal homogeneous structure; AC is not asserted in the symmetric interpretation.

The atom space itself, with its metric, belongs to the model: the whole structure has empty support, each coded metric or order tuple is supported by its finitely many atom coordinates, and pure rational values and their membership descendants are fixed. Thus the structure is hereditarily symmetric, not merely symmetric. Its metric satisfies the metric axioms in the model (Metric space: $d (x, y) = 0$ iff $x = y$ , symmetry, and the triangle inequality; pseudometric and ultrametric, The Axiom of Choice). The ordering is a distinguished dense rational order used to rigidify the finite metric structures; no equality or compatibility between its order topology and the metric topology is part of the construction.

For completeness, the model assertion is an internal axiom verification, as in Kleppmann §2.1, rather than an appeal to external well-foundedness. Finite supports form a normal system: intersections are handled by unions of supports, and $g fix (e) g^{- 1} = fix (g [e])$ . Rank recursion inside $M$ defines the action and the HS predicate; internal induction proves that HS is closed under membership and invariant under $G$ . Every atom has singleton support, $A$ has empty support, and all pure sets are HS. Empty Set, Infinity, Extensionality and Foundation therefore restrict to HS. Pairing and Union preserve HS, using finite unions of supports. For $x \in H S$ , Separation in $M$ forms ${y \in P^{M} (x) : y \in H S}$ ; invariance gives it any support of $x$ , and its members are HS. This is the power set in the interpretation. For each fixed formula with HS parameters, relativize its quantifiers to HS. The action preserves the relativized formula. Consequently Separation on an HS set produces an HS subset, supported by the union of the supports of the set and parameters. If the formula defines a unique HS value for each member of an HS set, Replacement in $M$ produces its range; uniqueness and formula invariance give that range the same finite support, and all its members are HS. This verifies every instance of Separation and Replacement. The atom predicate and set of all atoms are inherited, completing ZFA. Purity is unchanged: internal membership closure places every descendant of an HS object in HS, so the pure kernel is exactly that of $M$ . All recursions and inductions here are in $M$ ; no external induction on its possibly ill-founded membership relation is used.

Remarks

Why this group and not $Aut (Q, <)$ . The atoms carry both a rational metric and a distinguished order, and the automorphisms preserve both structures without any claim that their induced topologies coincide. The ordered-metric analogue of the finite-stabiliser extreme-amenability criterion is supplied separately in the next items, through Nešetřil's Ramsey theorem for finite ordered rational metric spaces and the KPT correspondence.

LemmaStatement: Literature-sourcedProof: Literature-sourcedaudited 2026-09-22Open item page →

Corson's rational metric space is not metacompact

Statement

In Corson's permutation model of Corson's ordered-rational permutation model, the rational Urysohn metric space has an open cover with no point-finite refinement; in particular it is not metacompact (Metacompactness: every open cover has a point-finite open refinement, Paracompactness: every open cover has a locally finite open refinement, with no separation axiom built into the word, Refinements, locally finite families, point-finite families, and star refinements).

Facts & Assumptions

Given: The atom space $U_{Q}^{<}$ in its model, the open cover $U = {B (c, 1 / 2) : c \in A}$ , and a supposed point-finite open refining cover.

[F1]

The model is a ZFA model in which every set has a finite support; an element of the model has a finite support $E \subseteq A$ fixed by the automorphisms used below (Corson's ordered-rational permutation model, Permutation groups, stabilizers, supports, and normal filters).

[F2]

$U_{Q}^{<}$ is universal and ultrahomogeneous for finite ordered rational metric spaces: every finite such space embeds in it, and every finite partial isometry preserving the order extends to an automorphism of the whole space. [given, source]

[L1]

Every member of a refinement of $U$ has diameter at most $1$ : if $V \subseteq B (c, 1 / 2)$ and $x, y \in V$ , then $d (x, y) < 1$ by the triangle inequality. The radius- $1 / 2$ balls form an open cover (Open ball, closed ball and sphere in a metric space, The metric topology: a set is open when every one of its points has a ball around it inside the set; closed means open complement, Metric space: $d (x, y) = 0$ iff $x = y$ , symmetry, and the triangle inequality; pseudometric and ultrametric).

[L2]

If $V$ is open and $a \in V$ , then some positive-radius metric ball about $a$ is contained in $V$ ; shrinking the radius to $1 / m$ for a sufficiently large integer $m \geq 1$ preserves the inclusion (The metric topology: a set is open when every one of its points has a ball around it inside the set; closed means open complement).

Proof

technique · contradiction

1.1

Suppose $U$ has a point-finite open refining cover $V$ . Since $V$ is a set of the model, fix a finite support $E \subseteq A$ of $V$ by [F1]. Enlarge $E$ by one atom if necessary, so that $E$ is nonempty, without destroying the support property. Let $D$ be the diameter of $E$ .

assume-contraL1F1

2.1

By universality in [F2], choose $a \in A ∖ E$ such that $e < a$ and $d (a, e) = D + 4$ for every $e \in E$ . Fix an arbitrary integer $n \geq 1$ . Since $V$ covers $A$ , choose $V \in V$ with $a \in V$ ; by [L2], choose an integer $m \geq 1$ with $B (a, 1 / m) \subseteq V$ , and put $K : = n m$ .

step 1.1F2L2

3.1

Extend $E \cup {a}$ , using [F2], by points $a_{0} < \dots < a_{3 K} = a$ such that $d (a_{i}, e) = D + 4$ for $e \in E$ and $d (a_{i}, a_{j}) = ∣ i - j ∣ / K$ for $0 \leq i, j \leq 3 K$ . These prescriptions form a finite ordered rational metric space: the old-to-new distances are constant and exceed the diameter of both $E$ and the new chain. Ultrahomogeneity then extends the partial isometry fixing $E$ and sending $a_{i}$ to $a_{i + 1}$ for $0 \leq i < 3 K$ to an automorphism $φ$ . Since $E$ supports $V$ , every $φ^{j} (V)$ belongs to $V$ .

step 2.1F2F1

4.1

The points $a_{3 K - n + 1}, \dots, a_{3 K}$ lie in $B (a, 1 / m) \subseteq V$ , because their distances from $a = a_{3 K}$ are all strictly less than $n / K = 1 / m$ . Hence $a \in φ^{j} (V)$ for every $0 \leq j < n$ .

step 2.1step 3.1

5.1

By [L1], $V$ has diameter at most $1$ . Consequently, if $a_{i} \in V$ , then $i \geq 2 K$ . Let $L$ be the least index with $a_{L} \in V$ . Step 4.1 gives $2 K \leq L \leq 3 K - n + 1$ . For $0 \leq j < n$ , one has $a_{L + j} \in φ^{j} (V)$ . Moreover, if $K \leq i < L + j$ , then $a_{i} \notin φ^{j} (V)$ : otherwise $a_{i - j} = φ^{- j} (a_{i})$ would lie in $V$ , while $0 \leq i - j < L$ , contradicting the minimality of $L$ .

L1step 3.1step 4.1

6.1

The members $φ^{j} (V)$ for $0 \leq j < n$ are pairwise distinct. Indeed, for $j < j^{'} < n$ , the point $a_{L + j}$ belongs to $φ^{j} (V)$ , whereas step 5.1, applied with $i = L + j < L + j^{'}$ , shows that it does not belong to $φ^{j^{'}} (V)$ . Thus, for every $n \geq 1$ , the map $j \mapsto φ^{j} (V)$ injects $n$ into ${W \in V : a \in W}$ . The set on the right is therefore not finite, contradicting point-finiteness at $a$ . Hence $U$ has no point-finite open refining cover, so the space is not metacompact and, a fortiori, not paracompact.

step 4.1step 5.1discharge-contradiction∎

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

Aut(U_Q^<) is extremely amenable

Statement

Assume the Axiom of Choice (The Axiom of Choice). The group $Aut (U_{Q}^{<})$ of order-and-metric automorphisms of the rational ordered Urysohn metric space, with the topology of pointwise convergence on the underlying countable set given the discrete topology, is extremely amenable, and so is every finite point stabiliser required by the finite-support permutation model of Corson's ordered-rational permutation model.

Facts & Assumptions

Given: The age of $U_{Q}^{<}$ , namely the finite ordered rational metric spaces, and a finite support $E$ .

[A1]

The Axiom of Choice is assumed (The Axiom of Choice).

[F1]

Nešetřil's Ramsey theorem says that the class $K$ of finite ordered rational metric spaces is a Ramsey class: for all $A, B \in K$ and every positive integer $k$ , there is $C \in K$ such that $C ⟶ (B)_{k}^{A} .$ Thus every $k$ -colouring of the copies of $A$ in this extension $C$ has a copy $B^{'} ≅ B$ whose copies of $A$ are monochromatic (Finite colourings of $k$ -element subsets, monochromatic sets, and the arrow notations $N \to (s, t)^{2}$ and $N \to (r)_{c}^{k}$ ). No self-arrow $B \to (B)_{k}^{A}$ is asserted.

[F2]

The KPT correspondence: the automorphism group of a Fraïssé structure whose finite substructures are rigid and whose age is Ramsey is extremely amenable (Kechris--Pestov--Todorcevic, Theorem 4.7; Theorem 6.16 gives this ordered-rational-Urysohn instance). This is the external KPT theorem, not a conclusion of the BPI criterion. Its use is the literature prerequisite specified by this item’s manifest; it is verified against the source cited above.

[F3]

Under AC, an arbitrary product of compact spaces is compact (Tychonoff's theorem: an arbitrary product of compact spaces is compact in the product topology, assuming the Axiom of Choice), and a closed subspace of a compact space is compact (A closed subspace of a compact space is compact, and a finite union of compact subspaces is compact). Products and their coordinate topology are as in The product set $\prod_{i \in I} X_{i}$ 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.

[L2]

For continuous maps into a Hausdorff space, the agreement set is closed (For continuous $f, g : Z \to Y$ with $Y$ Hausdorff the agreement set ${z \in Z : f (z) = g (z)}$ is closed in $Z$ , Hausdorff space: distinct points have disjoint open neighbourhoods; every metrizable space is Hausdorff and the indiscrete topology on two points is not).

[L3]

A basic neighbourhood in a product topology restricts only finitely many coordinates (The product set $\prod_{i \in I} X_{i}$ 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).

[L1]

A finite ordered rational metric space is rigid: an isomorphism onto itself preserving the order and all distances is the identity, because the least point must be fixed, then the least remaining point, and so on through the finite order. The order alone suffices; the metric has the meaning of Metric space: $d (x, y) = 0$ iff $x = y$ , symmetry, and the triangle inequality; pseudometric and ultrametric.

Proof

technique · direct

1.1

The age of $U_{Q}^{<}$ is the class of finite ordered rational metric spaces, and $U_{Q}^{<}$ is its Fraïssé limit, since it is countable, universal and homogeneous for that class by Corson's ordered-rational permutation model. Encode rational distances by a binary relation for each rational value, together with the order relation; this is a countable relational language. Its automorphism group is closed in the permutation group of the underlying countable set: failure to preserve a relation is witnessed by a finite tuple and remains a failure on a basic neighbourhood.

given

2.1

Every finite ordered rational metric space is rigid by [L1], and the age is a Ramsey class by [F1]; hence the hypotheses of the KPT criterion [F2] hold for the Fraïssé limit $U_{Q}^{<}$ , and $Aut (U_{Q}^{<})$ is extremely amenable.

step 1.1F1F2L1

3.1

Put $G : = Aut (U_{Q}^{<})$ and $H : = fix (E)$ . In the pointwise-convergence topology $H$ is an open subgroup of $G$ , since fixing the finitely many points of $E$ is a basic identity neighbourhood.

givenstep 2.1

4.1

Let $X$ be a nonempty compact Hausdorff $H$ -flow. Inside the product $X^{G}$ , define the coinduced space $Y : = {Φ : G \to X : Φ (h g) = h \cdot Φ (g) for all h \in H, g \in G} .$ It is nonempty: AC chooses one representative of every left $H$ -orbit in $G$ ; fix one $x_{0} \in X$ , assign that same value at every representative, and then the displayed rule extends it uniquely to that orbit.

givenA1step 3.1construct

5.1

The space $Y$ is closed in $X^{G}$ : for fixed $h, g$ , the equation $Φ (h g) = h \cdot Φ (g)$ is an equaliser of two continuous coordinate maps and is closed because $X$ is Hausdorff. Arbitrary intersections of these closed equalisers are closed. Hence [F3] makes $Y$ compact with its subspace topology. It is Hausdorff: two distinct functions differ at some coordinate, where disjoint open neighbourhoods in $X$ pull back to disjoint cylinder neighbourhoods in $Y$ .

step 4.1F3L2

5.2

Define a $G$ -action on $Y$ by $(a \cdot Φ) (g) : = Φ (g a) .$ The defining equivariance of $Y$ is preserved, since $Φ (h g a) = h \cdot Φ (g a)$ . It is a left action: $a \cdot (b \cdot Φ)$ evaluated at $g$ is $Φ ((g a) b) = Φ (g (a b))$ , and the identity acts trivially. This action is continuous. Indeed, at $a_{0} \in G$ and for each of finitely many output coordinates $g_{i}$ , openness of $H$ gives a neighbourhood on which $h_{i} (a) : = g_{i} a a_{0}^{- 1} g_{i}^{- 1} \in H$ ; then $g_{i} a = h_{i} (a) g_{i} a_{0}$ and $Φ (g_{i} a) = h_{i} (a) \cdot Φ (g_{i} a_{0})$ . Continuity of $h_{i}$ , of the $H$ -action, and the product topology at the finitely many fixed coordinates $g_{i} a_{0}$ therefore give joint continuity.

step 3.1step 4.1L3

6.1

Extreme amenability of $G$ from [step 2.1] gives a $G$ -fixed $Φ \in Y$ . The right-translation action then makes $Φ$ constant, since $Φ (a) = (a \cdot Φ) (1) = Φ (1)$ for every $a \in G$ . For $h \in H$ , the defining equation for $Y$ gives $h \cdot Φ (1) = Φ (h) = Φ (1)$ , so $Φ (1)$ is an $H$ -fixed point of $X$ .

step 2.1step 4.1step 5.1step 5.2

7.1

Thus every nonempty compact Hausdorff $H$ -flow has a fixed point, so $H = fix (E)$ is extremely amenable. Since $E$ was arbitrary and $E = \emptyset$ gives the whole group, the stated group and all required finite point stabilisers are extremely amenable.

step 3.1step 6.1∎

Remarks

The stabiliser conclusion supplies the hypothesis of Extreme amenability yields BPI in finite-support permutation models. That consumer proves BPI from extreme amenability and is not a source for the KPT correspondence.

LemmaStatement: Literature-sourcedProof: Literature-sourcedaudited 2026-09-22Open item page →

Corson's Stone obstruction is ordinal boundable

Statement

The sentence asserting that there is a rational-valued metric space with an open cover having no point-finite open refining cover is an atom-blind boundable sentence in the sense of Boundable sentences over an atom set, with the explicit absolute bound $ω + 41$ of the source's Lemma 5.

Facts & Assumptions

Given: Corson's model and the covering failure certified in Corson's rational metric space is not metacompact.

[F1]

A formula $φ (\vec{x})$ is boundable when a fixed absolutely defined ordinal $α$ makes ZFA prove $φ (\vec{x}) \leftrightarrow φ^{V_{α} (⋃ \vec{x})} (\vec{x})$ ; its existential closure is then a boundable sentence (Boundable sentences over an atom set).

[F2]

The metric space is the ordered rational Urysohn space of Corson's ordered-rational permutation model, its metric is rational-valued, and its open cover has no point-finite refinement (Corson's rational metric space is not metacompact, Metric space: $d (x, y) = 0$ iff $x = y$ , symmetry, and the triangle inequality; pseudometric and ultrametric, Metacompactness: every open cover has a point-finite open refinement).

[L1]

With the standard set encodings, $ω \in V_{ω + 1} (\emptyset)$ , and successively constructing $(ω, +)$ , $Z$ , $(Z, +)$ , $Q$ , and $(Q, +)$ puts $(Q, +)$ in $V_{ω + 30} (\emptyset)$ . [source, Corson Lemma 5]

[L2]

With Kuratowski ordered pairs, each $(x, y)$ for $x, y \in X$ lies in $V_{2} (X)$ , so the set $X \times X$ of all those pairs lies in $V_{3} (X)$ , not necessarily in $V_{2} (X)$ . The larger stated bounds remain valid: the pure rational codebook from [L1] dominates this one-level correction, so a function $d : X \times X \to Q$ lies in $V_{ω + 33} (X)$ ; a family of subsets of $X$ lies in $V_{2} (X)$ ; an ordered triple $(X, d, U)$ lies in $V_{ω + 37} (X)$ ; and a function from a natural number into an open cover of $X$ lies in $V_{ω + 41} (X)$ . [L1, source, Corson Lemma 5]

Proof

technique · direct

1.1

Let $Cov (X, d, U)$ say that $d$ is a rational-valued metric on $X$ and $U$ is an open cover in its metric topology. Let $Ref (X, d, U, V)$ say that both $U$ and $V$ satisfy $Cov$ and that $V$ refines $U$ . Let $Inj (f, Y, Z)$ say that $f$ is an injection from $Y$ into $Z$ . These are formulas built only from equality, membership, the carried sets, and the fixed pure rational codebook.

givenF1F2

2.1

Define $Φ (X, d, U)$ to be $Cov (X, d, U)$ together with the assertion that for every $V \in P (P (X))$ , if $Ref (X, d, U, V)$ , then some $x \in X$ has the following property: for every $n \in ω$ there is $f \subseteq n \times V$ such that $Inj (f, n, V)$ and $x \in f (m)$ for every $m < n$ . Thus $Φ$ says exactly that $U$ has no point-finite open refining cover.

step 1.1

3.1

The bounds [L1]-[L2] contain every object quantified in step 2.1: candidate covers and refinements lie in the second relative level over $X$ , while every finite injection witnessing arbitrarily many members through $x$ lies below level $ω + 41$ . Expanding the displayed definitions therefore gives the ZFA theorem $Φ (X, d, U) \leftrightarrow Φ^{V_{ω + 41} (X \cup d \cup U)} (X, d, U)$ .

step 2.1L1L2

3.2

The formula is atom-blind: its base sort $X$ is used only opaquely through the carried metric, subsets, covers, and finite function graphs; its atomic tests are equality and membership together with the fixed pure rational parameter, and it never tests whether an element of $X$ is an atom or inspects its internal membership structure.

step 1.1step 2.1

4.1

By [F1] and step 3.1, the existential closure $\exists X \exists d \exists U Φ (X, d, U)$ is boundable with the fixed absolute bound $ω + 41$ ; step 3.2 supplies the atom-blind typed certificate, and [F2] supplies a witness in Corson's model.

step 3.1step 3.2F1F2∎

TheoremStatement: Literature-sourcedProof: AI-adaptedaudited 2026-09-22Open item page →

Relative consistency of BPI with failure of Stone's theorem

Statement

If $Z F$ is consistent, then $Z F + B P I$ with a metrizable nonmetacompact space is consistent; a fortiori $Z F + B P I$ does not prove that every metrizable space is paracompact (The Boolean prime ideal principle, Metacompactness: every open cover has a point-finite open refinement, Paracompactness: every open cover has a locally finite open refinement, with no separation axiom built into the word).

Facts & Assumptions

Given: Corson's permutation model, its rational metric space, and the assumed consistency of $Z F$ .

[F1]

The finite point stabilisers of the model are extremely amenable, so the model satisfies BPI (Aut(U_Q^<) is extremely amenable, Extreme amenability yields BPI in finite-support permutation models, Corson's ordered-rational permutation model).

[F2]

The model contains the rational metric space with an open cover having no point-finite open refinement (Corson's rational metric space is not metacompact), and that failure is certified as an atom-blind boundable sentence with the bound $ω + 41$ (Corson's Stone obstruction is ordinal boundable).

[F3]

Pincus transfer with the exceptional clauses transfers BPI together with the certified sentence (Pincus transfer for BPI and injectively boundable conjunctions). Corson's Proposition 6 states this exact transfer for the conjunction of BPI and the ordinal-boundable Stone obstruction. [source]

[F4]

The verified constructible-universe reduction gives $Con (Z F) \Rightarrow Con (Z F C + G C H)$ (Formal consistency of ZFC plus GCH relative to ZF), and countable first-order completeness supplies a model of the latter theory without a transitivity or well-foundedness conclusion (Completeness for explicitly countable set languages).

Proof

technique · direct

1.1

Assume $Con (Z F)$ . By [F4] obtain a possibly externally ill-founded model $M$ of $Z F C + G C H$ . All following constructions are interpreted internally in $M$ .

givenF4

2.1

In $M$ choose its countable rational ordered Urysohn metric structure $U_{Q}^{<}$ and let $A = {⟨ 0, u ⟩ : u \in U_{Q}^{<}}$ , carrying the transported order and metric. Represent sets by tagged objects $⟨ 1, S ⟩$ and form the class hierarchy $X_{0} = A$ , $X_{α + 1} = A \cup {⟨ 1, S ⟩ : S \subseteq X_{α}}$ , with unions at limits and membership in a tag given by membership in its second coordinate. Internally this satisfies ZFA+AC: tagged set operations give the elementary axioms and Power Set; translated Separation and Replacement follow in $M$ , with Collection bounding construction ranks; minimal construction rank gives Foundation; and $M$ 's well-orders give tagged choice functions. No external well-foundedness of $M$ is used.

step 1.1

3.1

Form Corson's ordered-rational finite-support permutation model inside this ZFA+AC interpretation. The group, topology, finite stabilisers and their extreme amenability are all computed internally. Hence [F1], using the arbitrary-ground form of the fixed-point theorem, gives BPI in the hereditarily symmetric interpretation. By [F2] that interpretation also contains the certified rational metric space and its open cover with no point-finite open refinement.

step 2.1F1F2

4.1

By [F3], the conjunction of BPI with the certified sentence transfers from this permutation model to an atom-free model of $Z F$ . Consequently $Con (Z F) \Rightarrow Con (Z F + B P I + there is a metrizable nonmetacompact space) .$ This is Corson's external relative-consistency construction. Completeness did not supply a transitive model; the internal tagged interpretation and the arbitrary-ground BPI theorem provide the required bridge. No application of the formal proof-reduction interface, and hence no unprovided uniform code map, is asserted.

step 1.1step 2.1step 3.1F3

5.1

A space that is not metacompact has an open cover with no point-finite open refinement. Every locally finite open refinement is point-finite, so that cover has no locally finite open refinement either. The space is therefore not paracompact, and Stone's theorem fails in the transferred model.

step 4.1F2∎

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

Effective metacompactness for discrete metric spaces implies AC

Statement

Over $Z F$ : suppose that for every discrete metrizable space $X$ and every open cover $U$ of $X$ there exist a point-finite open refinement $V$ which covers $X$ , and a map $a : V \to U$ with $V \subseteq a (V)$ for every $V \in V$ . Then the Axiom of Choice holds (The Axiom of Choice, Metacompactness: every open cover has a point-finite open refinement, Refinements, locally finite families, point-finite families, and star refinements).

Facts & Assumptions

Given: The effective-metacompactness hypothesis, including that each supplied refining family covers the space; an arbitrary family $F$ of nonempty sets.

[F1]

Multiple choice and its equivalence with AC: in ZF, MC is equivalent to AC, and MC asserts that every family of nonempty sets admits a function assigning to each member a nonempty finite subset (Multiple choice and dependent multiple choice, Multiple choice is equivalent to AC in ZF).

[F2]

On the discrete metric space $X : = (F \times {0}) \cup (⋃ F \times {1})$ with the discrete metric, every subset is open, and the family $U : = {{(x, 1), (F, 0)} : x \in F \in F}$ is an open cover of $X$ : a point $(F, 0)$ with $F \in F$ lies in ${(x, 1), (F, 0)}$ for each $x \in F$ , and a point $(x, 1)$ with $x \in F \in F$ lies in ${(x, 1), (F, 0)}$ (Metric space: $d (x, y) = 0$ iff $x = y$ , symmetry, and the triangle inequality; pseudometric and ultrametric, The metric topology: a set is open when every one of its points has a ball around it inside the set; closed means open complement, Arbitrary unions and finite intersections of open sets are open, open balls are open and closed balls are closed).

[L1]

A point-finite family is one every point of which belongs to only finitely many members; a refinement map is a function on the refining family whose value at each member contains it (Refinements, locally finite families, point-finite families, and star refinements, Choice function).

Proof

technique · direct

1.1

Let $F$ be an arbitrary family of nonempty sets and let $X : = (F \times {0}) \cup (⋃ F \times {1})$ carry the discrete metric; the two tags keep the family and its members apart, so that the zero-tagged family member is uniquely recovered from each cover pair. Explicitly, $d (u, v) = 0$ if $u = v$ and $1$ otherwise satisfies separation and symmetry; if $u \neq w$ , at least one of $u \neq v$ or $v \neq w$ holds, proving the triangle inequality. Each radius- $1 / 2$ ball is a singleton, so every subset is open. No disjointness of the members of $F$ is used.

givenF2

2.1

The family $U$ of [F2] is an open cover of $X$ by [F2], so by the hypothesis applied once to this cover there are a point-finite open refinement $V$ which covers $X$ and a map $a : V \to U$ with $V \subseteq a (V)$ for all $V \in V$ ; no global refinement operator is assumed, only this one per-cover existential pair.

step 1.1F2L1

3.1

For each $F \in F$ let $C (F) : = {V \in V : (F, 0) \in V}$ , the set of refinement members through the point $(F, 0)$ of the space; $C (F)$ is nonempty because $V$ covers $X$ , and finite because $V$ is point-finite at $(F, 0)$ .

step 2.1L1

4.1

Define $f (F) : = {x \in F : a (V) = {(x, 1), (F, 0)} for some V \in C (F)}$ ; then each $V \in C (F)$ determines a unique $x$ by its image pair (the one-tagged point); thus $f (F)$ is the image of the finite set $C (F)$ under a uniquely defined function. It is a finite subset of $F$ , and it is nonempty because for $V \in C (F)$ one has $(F, 0) \in V \subseteq a (V)$ and $a (V) \in U$ , so $a (V) = {(x, 1), (F^{'}, 0)}$ with $x \in F^{'} \in F$ ; now $(F, 0) \in a (V)$ forces $(F, 0) = (F^{'}, 0)$ , that is $F^{'} = F$ , because the alternative $(F, 0) = (x, 1)$ would give $0 = 1$ . Hence $a (V) = {(x, 1), (F, 0)}$ with $x \in F$ , as required.

step 2.1step 3.1L1

5.1

The assignment $F \mapsto f (F)$ is therefore a function on the family $F$ of nonempty sets whose values are nonempty finite subsets, which is Multiple Choice for $F$ , including the empty family via the empty function. For any indexed family $(X_{i})_{i \in I}$ apply this construction to its set of values $F = {X_{i} : i \in I}$ and compose to get $i \mapsto f (X_{i})$ ; repeated values cause no difficulty. Since the original family was arbitrary, MC holds, and by [F1] the Axiom of Choice holds.

step 4.1F1∎

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

Products of cofinite spaces are compact exactly under BPI

Statement

Over $Z F$ , BPI (The Boolean prime ideal principle) is equivalent to the compactness in the product topology (The product set $\prod_{i \in I} X_{i}$ 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, Open cover, subcover, and compact topological space; a compact subset is a subspace that is compact in its own right) of every product of spaces each carrying the cofinite topology (The discrete, indiscrete, cofinite, cocountable, particular-point and Sierpinski topologies).

Facts & Assumptions

Given: A family ${(X_{i}, T_{i})}_{i \in I}$ of spaces with $T_{i}$ the cofinite topology on $X_{i}$ , and its product $X$ with projections $π_{i}$ .

[F1]

The closed sets of the cofinite topology on a set are the set itself and its finite subsets; the cofinite space is $T_{1}$ (The discrete, indiscrete, cofinite, cocountable, particular-point and Sierpinski topologies, $T_{0}$ (Kolmogorov) and $T_{1}$ (Frechet) spaces).

[F2]

A space is compact if and only if every family of closed sets with the finite intersection property has nonempty intersection (A space is compact exactly when every family of closed subsets with the finite intersection property has nonempty intersection, Finite intersection property).

[F3]

The set ultrafilter lemma is equivalent over ZF to BPI: every proper filter on a set extends to an ultrafilter, and an ultrafilter contains exactly one of a subset and its complement (BPI and the set ultrafilter lemma are equivalent, Ultrafilter, Characterisation of ultrafilters: every set or its complement, The Boolean prime ideal principle).

[F4]

Under BPI, every product of compact Hausdorff spaces is compact, and the two-point discrete space is compact Hausdorff (Compact Hausdorff Tychonoff is equivalent to BPI, The discrete, indiscrete, cofinite, cocountable, particular-point and Sierpinski topologies).

[L1]

The complements of basic product-open sets form the following closed basis: $C (X) = {⋃_{q \in Q} π_{q}^{- 1} [C_{q}] : Q \subseteq I finite and every C_{q} \subseteq X_{q} is closed} .$ Consequently $X$ is compact if every subfamily of $C (X)$ with the finite intersection property has nonempty intersection: the complementary basic open sets then satisfy the finite-subcover test (The product set $\prod_{i \in I} X_{i}$ 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, Open cover, subcover, and compact topological space; a compact subset is a subspace that is compact in its own right, Finite intersection property).

[L2]

Every cofinite space is compact in ZF. Indeed, a family of its closed sets with the finite intersection property either contains only the whole space, or contains a finite member $C$ ; in the latter case the intersections with $C$ have nonempty total intersection, since otherwise finitely many of them already exclude the finitely many points of $C$ (A space is compact exactly when every family of closed subsets with the finite intersection property has nonempty intersection, The natural numbers $N$ (von Neumann)).

Proof

technique · direct

1.1

Assume BPI for the forward direction. If $X = \emptyset$ for any reason, it is compact; this includes an empty factor and does not assert that nonempty factors have nonempty product. If $I = \emptyset$ , the product is a singleton and compact. In the remaining case $X \neq \emptyset$ , fix one $\overset{ˉ}{x} \in X$ .

givenF2

2.1

By [L1], it is enough to let $H \subseteq C (X)$ have the finite intersection property. By [F3], extend the filter generated by $H$ to an ultrafilter $F$ of subsets of $X$ .

step 1.1F3L1

3.1

For each $i \in I$ , push $F$ forward through the projection by putting $G_{i} : = {B \subseteq X_{i} : π_{i}^{- 1} [B] \in F} .$ Preimages preserve complements and finite intersections, so $G_{i}$ is an ultrafilter on $X_{i}$ . Its closed members have the finite intersection property. By compactness of the cofinite factor [L2], their intersection $A_{i} : = ⋂ {C \in G_{i} : C is closed in X_{i}}$ is nonempty.

step 2.1F2F3L2

4.1

By [F1], each $A_{i}$ , being an intersection of closed sets, is either all of $X_{i}$ or finite. If it is finite, $G_{i}$ contains a finite set: this is $X_{i}$ itself when $X_{i}$ is finite, while if $X_{i}$ is infinite and $A_{i} \neq X_{i}$ , some closed member occurring in the intersection defining $A_{i}$ is proper and hence finite. An ultrafilter containing a nonempty finite set contains exactly one of its singleton subsets. If that singleton is ${a_{i}}$ , then every member of $G_{i}$ contains $a_{i}$ , and ${a_{i}}$ is itself a closed member, so $A_{i} = {a_{i}}$ . Define $x_{i}$ to be the unique point of $A_{i}$ whenever $A_{i}$ is a singleton, and otherwise put $x_{i} : = {\overset{ˉ}{x}}_{i}$ ; in this latter case $A_{i} = X_{i}$ . This defines $x = (x_{i})_{i \in I} \in X$ without making a new choice.

step 1.1step 3.1F1F3

5.1

Fix $H \in H$ . By [L1], write $H = ⋃_{q \in Q} π_{q}^{- 1} [C_{q}]$ with $Q$ finite and each $C_{q}$ closed. Since $H \in F$ , finite primeness of the ultrafilter gives some $q \in Q$ with $π_{q}^{- 1} [C_{q}] \in F$ . Thus $C_{q} \in G_{q}$ , so $x_{q} \in A_{q} \subseteq C_{q}$ by step 4.1. Hence $x \in H$ . Therefore $x \in ⋂ H$ , and [L1] proves that $X$ is compact.

step 2.1step 3.1step 4.1F3L1

6.1

The forward implication is established in step 5.1. For the converse, assume every product of cofinite spaces is compact. Let $S$ be any set carrying a proper filter $D$ , and put $Y = 2^{P (S)}$ . The two-point cofinite topology is discrete, so the hypothesis makes $Y$ compact. The constant-zero function shows $Y$ is nonempty in ZF. The finite discrete factor is also the one described in [F4]; no converse for arbitrary compact Hausdorff products is inferred from that fact.

step 5.1F4L1

7.1

On a point $v : P (S) \to 2$ impose the constraints $v (S) = 1$ , $v (\emptyset) = 0$ , $v (S ∖ A) = 1 - v (A)$ and $v (A \cap B) = v (A) v (B)$ for every $A, B \subseteq S$ , and $v (D) = 1$ for every $D \in D$ . Each constraint defines a clopen subset of $Y$ : it is a finite union of patterns in its finitely many involved coordinates, and both each pattern and its complement are unions of basic discrete-coordinate cylinders. This family has FIP. For any finite list of constraints, only finitely many filter-members $D_{1}, \dots, D_{k}$ occur. Their intersection is nonempty by properness of the filter, with the empty intersection equal to $S$ , also nonempty. Fix $s$ in that intersection and set $v_{s} (A) = 1$ exactly when $s \in A$ . This valuation satisfies all Boolean equations, including the listed filter constraints. Thus [F2] and compactness give a single $v$ satisfying every constraint.

step 6.1F2F3L1

8.1

Put $U = {A \subseteq S : v (A) = 1}$ . The constraints include $S$ and exclude $\emptyset$ , close $U$ under intersections, and make it upward closed: if $A \subseteq B$ and $v (A) = 1$ , then $1 = v (A \cap B) = v (A) v (B)$ forces $v (B) = 1$ . They also decide exactly one of $A$ and its complement, so [F3] makes $U$ an ultrafilter extending $D$ . Every proper filter has therefore been extended; if $S$ is empty there is no proper filter and the assertion is vacuous. By the UFL-to-BPI direction of [F3], BPI holds. Combined with step 5.1, this proves the equivalence.

step 5.1step 7.1F3∎

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

The isolated-point repair of Kelley's choice space

Statement

Let $A$ be a set and let $A_{c}$ be $A$ with the cofinite topology (The discrete, indiscrete, cofinite, cocountable, particular-point and Sierpinski topologies). Then the topological sum $X_{A} : = A_{c} ⊔ {\infty}$ of $A_{c}$ with a one-point space (The disjoint union (coproduct) $⨆_{i} X_{i}$ with the final topology of the canonical injections: a set is open exactly when each of its traces is) is compact (Open cover, subcover, and compact topological space; a compact subset is a subspace that is compact in its own right) and $T_{1}$ ( $T_{0}$ (Kolmogorov) and $T_{1}$ (Frechet) spaces), and $A$ is a closed subspace of $X_{A}$ (Subspace topology: the traces of the open sets, its closed sets and its bases, the continuity of the inclusion, and the characteristic property of a map into a subspace). This is the repaired coordinate of the product-compactness argument. We identify each summand with its tagged copy in the disjoint union, so the added point is distinct from every point of $A$ . This is in contrast with the cofinite topology on $A \cup {\infty}$ itself.

Facts & Assumptions

Given: A set $A$ ; the cofinite space $A_{c}$ ; the sum $X_{A} = A_{c} ⊔ {\infty}$ .

[F1]

In the cofinite topology the open sets are $\emptyset$ and the sets with finite complement, and the closed sets are the whole space and the finite sets; the cofinite space is $T_{1}$ (The discrete, indiscrete, cofinite, cocountable, particular-point and Sierpinski topologies, $T_{0}$ (Kolmogorov) and $T_{1}$ (Frechet) spaces).

[F2]

In the topological sum a subset $U \subseteq X_{A}$ is open exactly when its trace $U \cap A$ is open in $A_{c}$ ; independently, its trace on the singleton summand may be either $\emptyset$ or ${\infty}$ , both of which are open. Thus $\emptyset$ and ${\infty}$ are open, and the summand $A$ is clopen (The disjoint union (coproduct) $⨆_{i} X_{i}$ with the final topology of the canonical injections: a set is open exactly when each of its traces is, A map out of a disjoint union is continuous iff each of its restrictions is; the canonical injections are open and closed embeddings; and each summand is clopen in the union).

[F3]

A space is compact when every open cover has a finite subcover; in particular, the empty space and a one-point space are compact directly from this definition (Open cover, subcover, and compact topological space; a compact subset is a subspace that is compact in its own right).

[F4]

For a function $F$ with domain a natural number $n$ , if each $F (j)$ is nonempty then its family of values $F [n]$ has a choice function (Every natural-number-indexed list of nonempty sets has a choice function on its family of values). A finite set admits a bijection from some natural number; fixing one such enumeration for one finite set is a single existential instantiation (Finite, countably infinite, countable, uncountable).

Proof

technique · direct

1.1

Assume $X_{A}$ is nonempty, which it is because $\infty$ is one of its points.

given

2.1

The cofinite space $A_{c}$ is compact. Given an open cover $U$ , if $A = \emptyset$ the empty subfamily covers it. Otherwise fix $a \in A$ and $U_{0} \in U$ containing $a$ . By [F1] the complement $C = A ∖ U_{0}$ is finite. Fix a natural number $n$ and a bijection $e : n \to C$ by [F4], including the empty enumeration when $C = \emptyset$ . Define $F (j) = {U \in U : e (j) \in U}$ for $j < n$ . Every value is nonempty because $U$ covers $A$ . Apply [F4] to this function and let $c$ choose from its family of values. Then $U_{0}$ together with the list $c (F (j))$ , $j < n$ , is a finite subcover. No simultaneous choice of enumerations for an infinite family is involved.

step 1.1F1F3F4

2.2

$X_{A}$ is $T_{1}$ : for distinct points $x, y$ of $X_{A}$ , the set $X_{A} ∖ {y}$ is open — if $y = \infty$ it is $A$ , which is cofinite in $A$ and open in the sum by [F2]; if $y \in A$ it is $(A ∖ {y}) \cup {\infty}$ , whose trace on $A$ is cofinite, hence open in the sum by [F2] — and symmetrically for $X_{A} ∖ {x}$ .

step 1.1F1F2

3.1

Let $V$ be an open cover of $X_{A}$ . By [F2], ${V \cap A : V \in V}$ is an open cover of $A_{c}$ . Step 2.1 and [F3] give either the empty subcover or a finite list of traces $W_{j}$ , $j < m$ , covering $A$ . Define $G (j) = {V \in V : V \cap A = W_{j}}$ for $j < m$ . Each value is nonempty by the definition of the trace family. Apply [F4] to $G$ and choose $d$ on its family of values; the list $d (G (j))$ , $j < m$ , covers $A$ . Fix one $V_{\infty} \in V$ containing $\infty$ , which exists since $V$ covers $X_{A}$ . Adjoining it to this finite list covers $X_{A}$ , proving compactness. When $A$ is empty take $m = 0$ , so $V_{\infty}$ alone suffices.

step 2.1F2F3F4

4.1

$A$ is closed in $X_{A}$ : its complement ${\infty}$ is open in the sum by [F2], and the subspace topology that $A$ inherits is the cofinite topology of $A_{c}$ ; hence $A$ is a closed subspace of $X_{A}$ in the sense of Subspace topology: the traces of the open sets, its closed sets and its bases, the continuity of the inclusion, and the characteristic property of a map into a subspace.

step 2.2F1F2∎

Remarks

Why the naive coordinate fails. If instead $A \cup {\infty}$ carries the cofinite topology, then for infinite $A$ the set $A$ is not closed: its complement ${\infty}$ is finite and hence closed, while a proper closed set in a cofinite space must itself be finite. Thus $A$ is open but not closed. That failure is the content of the companion counterexample.
What compactness costs. Compactness of $A_{c}$ uses finite choice only, and the sum with a point adds no further cost, so the repaired coordinate is available in ZF; this is what makes it usable in the product argument below.

TheoremStatement: Literature-sourcedProof: AI-adaptedaudited 2026-09-22Open item page →

The compact T1 product theorem is equivalent to AC

Statement

Over $Z F$ , the Axiom of Choice (The Axiom of Choice) is equivalent to the assertion that every product of compact $T_{1}$ spaces ( $T_{0}$ (Kolmogorov) and $T_{1}$ (Frechet) spaces, Open cover, subcover, and compact topological space; a compact subset is a subspace that is compact in its own right, The product set $\prod_{i \in I} X_{i}$ 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) is compact.

Facts & Assumptions

Given: A family $(A_{i})_{i \in I}$ of nonempty sets; the repaired coordinates $X_{A_{i}}$ of The isolated-point repair of Kelley's choice space; the product $X : = \prod_{i} X_{A_{i}}$ with projections $π_{i}$ .

[F1]

Each $X_{A_{i}}$ is compact and $T_{1}$ , and $A_{i}$ is a closed subspace of it (The isolated-point repair of Kelley's choice space, Subspace topology: the traces of the open sets, its closed sets and its bases, the continuity of the inclusion, and the characteristic property of a map into a subspace).

[F2]

Under AC, Tychonoff's theorem gives compactness of arbitrary products of compact spaces (Tychonoff's theorem: an arbitrary product of compact spaces is compact in the product topology, assuming the Axiom of Choice, The Axiom of Choice).

[F3]

[F4]

If $n \in N$ and $F : n \to V$ is a natural-number-indexed list of nonempty sets, then the family of values $F [n]$ has a choice function (Every natural-number-indexed list of nonempty sets has a choice function on its family of values).

[L1]

A cylinder $π_{i}^{- 1} [A_{i}]$ is closed in $X$ when $A_{i}$ is closed in $X_{A_{i}}$ , being the preimage of a closed set under a continuous projection (The product set $\prod_{i \in I} X_{i}$ 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, For $A \subseteq S \subseteq X$ the closure of $A$ in $S$ is ${\overline{A}}^{X} \cap S$ , while the interior only contains ${int}^{X} (A) \cap S$ , with equality when $S$ is open; and a dense subset of $X$ traces to a dense subset of every open $S$ ).

Proof

technique · direct

1.1

Under AC every product of compact spaces is compact by [F2], so every product of compact $T_{1}$ spaces is compact; this is the forward direction.

assume-hypF2

1.2

Conversely, assume every product of compact $T_{1}$ spaces is compact, and let $(A_{i})_{i \in I}$ be a family of nonempty sets; if $I = \emptyset$ the product over the empty index set is a one-point space and the unique element is a choice function, and if $I \neq \emptyset$ we build one below.

assume-hypgiven

2.1

Form $X : = \prod_{i \in I} X_{A_{i}}$ where $X_{A_{i}}$ is the repaired coordinate of [F1]; each factor is compact $T_{1}$ , so $X$ is compact by the hypothesis.

step 1.2F1

3.1

For each $i$ the cylinder $C_{i} : = π_{i}^{- 1} [A_{i}]$ is closed in $X$ by [L1] and [F1]. To verify the finite intersection property in its finite-list form, let $n \in N$ and let $s : n \to {C_{i} : i \in I}$ be arbitrary. For each $k < n$ , choose the unique $i_{k} \in I$ with $s (k) = C_{i_{k}}$ (the cylinder determines its coordinate), and define $F (k) : = A_{i_{k}}$ . By [F4] the family $F [n]$ has a choice function $h$ . Define $x \in X$ by $x (i) : = h (A_{i})$ when $i = i_{k}$ for some $k < n$ , and by the distinguished point $\infty \in X_{A_{i}}$ otherwise. If the same coordinate occurs more than once this gives the same value, and $h (A_{i}) \in A_{i}$ ; hence $x \in C_{i_{k}} = s (k)$ for every $k < n$ . Thus every finite list from ${C_{i} : i \in I}$ has nonempty intersection.

step 2.1F1F4L1

4.1

By compactness of $X$ and [F3] the intersection $⋂_{i} C_{i}$ is nonempty; any point $x$ of it has $x_{i} \in A_{i}$ for every $i$ , so $i \mapsto x_{i}$ is a choice function for the family $(A_{i})_{i \in I}$ .

step 2.1step 3.1F3

5.1

The family of nonempty sets was arbitrary, so AC holds; together with step 1.1 this proves the displayed equivalence.

step 1.1step 4.1∎

TheoremStatement: Literature-sourcedProof: Literature-sourcedaudited 2026-09-22Open item page →

The arbitrary compact product theorem is equivalent to AC

Statement

Over $Z F$ , AC (The Axiom of Choice) is equivalent to the assertion that every product of arbitrary compact spaces (Open cover, subcover, and compact topological space; a compact subset is a subspace that is compact in its own right, The product set $\prod_{i \in I} X_{i}$ 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) is compact. The empty product is a one-point space and is included.

Facts & Assumptions

Given: AC and, in the reverse direction, the hypothesis that every product of compact spaces is compact.

[F1]

Under AC, Tychonoff's theorem gives compactness of every product of compact spaces, the empty product being the one-point space (Tychonoff's theorem: an arbitrary product of compact spaces is compact in the product topology, assuming the Axiom of Choice, The product set $\prod_{i \in I} X_{i}$ 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).

[F2]

Over ZF, AC is equivalent to compactness of every product of compact $T_{1}$ spaces (The compact T1 product theorem is equivalent to AC, $T_{0}$ (Kolmogorov) and $T_{1}$ (Frechet) spaces).

[F3]

Over ZF, BPI is equivalent to compactness of every product of compact Hausdorff spaces (Compact Hausdorff Tychonoff is equivalent to BPI).

Proof

technique · direct

1.1

Under AC every product of compact spaces is compact by [F1], and the empty product is the one-point space; this is one direction.

assume-hypF1

2.1

Conversely, if every product of compact spaces is compact then in particular every product of compact $T_{1}$ spaces is compact, since compact $T_{1}$ spaces are compact spaces; by [F2] this gives AC.

step 1.1F2

3.1

The two directions give the displayed equivalence; in particular the compact-Hausdorff case is a different statement, whose strength is BPI by [F3] and which is not identified with the arbitrary compact case here.

step 1.1step 2.1F2F3∎

Remarks

Why the two strengths differ. Products of compact $T_{1}$ spaces and products of compact Hausdorff spaces are not the same assertion: the first is equivalent to AC by [F2] and the second to BPI by [F3]. The empty product is compact in both cases and therefore separates nothing.

CorollaryStatement: AI-adaptedProof: AI-adaptedaudited 2026-09-22Open item page →

BPI does not imply DMC

Statement

Relative to $Con (Z F)$ , BPI (The Boolean prime ideal principle) does not imply DMC (Dependent multiple choice in finite-level tree form) over $Z F$ : there is a model of $Z F + B P I$ in which DMC fails.

Facts & Assumptions

Given: The assumed consistency of $Z F$ .

[F1]

Relative to $Con (Z F)$ , the theory $Z F + B P I + \neg U R Y$ is consistent, where $\neg U R Y$ asserts the existence of a normal space with two disjoint closed sets that admit no continuous separation (Relative consistency of BPI without Urysohn's lemma, Normal spaces and $T_{4}$ spaces, with the source disagreement over whether normality includes $T_{1}$ stated explicitly).

[F2]

Over $Z F$ , DMC implies Urysohn's lemma: in every normal space any two disjoint closed sets are separated by a continuous function (DMC implies Urysohn's lemma, Dependent multiple choice in finite-level tree form).

Proof

technique · contradiction

1.1

Assume $Con (Z F)$ and suppose, for the sake of contradiction, that $Z F + B P I$ proves DMC.

assume-contragiven

2.1

By [F2] the theory $Z F + B P I + \neg U R Y$ then proves DMC and hence proves $U R Y$ , since DMC implies Urysohn's lemma in ZF; but it also proves $\neg U R Y$ by its own axiom, so it is inconsistent.

step 1.1F2

3.1

This contradicts the consistency of $Z F + B P I + \neg U R Y$ given by [F1] under the assumption $Con (Z F)$ ; hence BPI does not imply DMC over $Z F$ , conditionally on the consistency of $Z F$ .

step 2.1F1discharge-contradiction∎

CorollaryStatement: AI-adaptedProof: AI-adaptedaudited 2026-09-22Open item page →

If ZF is consistent, DMC is not provable in ZF

Statement

If $Z F$ is consistent, then $Z F$ does not prove DMC (Dependent multiple choice in finite-level tree form); indeed there is a model of $Z F$ with countable choice (The Axiom of Countable Choice ( ${A C}_{ω}$ )) in which DMC fails.

Facts & Assumptions

Given: The assumed consistency of $Z F$ .

[F1]

Relative to $Con (Z F)$ , the theory $Z F + {A C}_{ω} + \neg U R Y$ is consistent (Relative consistency of Countable Choice without Urysohn's lemma).

[F2]

DMC implies Urysohn's lemma over $Z F$ (DMC implies Urysohn's lemma).

Proof

technique · contradiction

1.1

Assume $Con (Z F)$ and suppose $Z F$ proves DMC.

assume-contragiven

2.1

Then $Z F + {A C}_{ω}$ proves DMC, hence by [F2] proves $U R Y$ ; but by [F1] the theory $Z F + {A C}_{ω} + \neg U R Y$ is consistent, and it would prove both $U R Y$ and its negation, hence be inconsistent.

step 1.1F1F2

3.1

This contradiction shows that $Z F$ does not prove DMC, conditionally on $Con (Z F)$ ; the witness model supplied by [F1] has countable choice, while Urysohn's lemma fails there and therefore DMC fails.

step 2.1F1F2discharge-contradiction∎

RemarkRemark: Literature-sourcedProof: Not applicableaudited 2026-09-22Open item page →

The exact choice strength of Stone's theorem remains open

Statement

As of 15 September 2026: AC proves Stone's theorem, while, assuming the consistency of ZF, neither DC nor BPI proves it; the stronger assertion that every open cover of every discrete metrizable space has a point-finite refinement equipped with a refinement map implies AC; the exact strength of the ordinary existential Stone theorem over $Z F$ is not identified here and remains open in the cited line of work.

Remarks

The ZFC positive theorem. Stone's theorem, under choice: every metric space is paracompact proves that under AC every metric space is paracompact, and it is the positive half of the ledger.
The two countermodels. Conditional on $Con (Z F)$ , Relative consistency of DC with failure of Stone's theorem gives a model of $Z F + D C$ with a metrizable nonparacompact space, and Relative consistency of BPI with failure of Stone's theorem gives a model of $Z F + B P I$ with a metrizable nonmetacompact space (Metacompactness: every open cover has a point-finite open refinement); hence, under that same consistency hypothesis, neither DC nor BPI proves Stone's theorem.
The stronger assertion. Effective metacompactness for discrete metric spaces implies AC proves that if every open cover of every discrete metrizable space has a point-finite refinement together with a refinement map, then the Axiom of Choice holds (The Axiom of Choice). The refinement map is part of the hypothesis: the statement is about a per-cover existential pair, not about a global class operator, and it is not identified with the ordinary Stone theorem.
What remains open. The gap between the ordinary existential Stone theorem and the effective strengthening is not closed here: no model of $Z F$ is known to the cited authors in which Stone's theorem holds while the effective refinement assertion fails, and no proof of the ordinary theorem from a principle weaker than AC is known. The status is dated for that reason.

RemarkRemark: Literature-sourcedProof: Not applicableaudited 2026-09-22Open item page →

DMC, Multiple Choice, and AC qualifications

Statement

DC implies DMC. DMC together with finite-selection countable choice implies DC. In $Z F$ , Multiple Choice is equivalent to AC, but that equivalence must not be imported into $Z F A$ ; the cited permutation-model strictness results are $Z F A$ qualifications only. No strict DMC-versus-DC claim is made over $Z F$ .

Remarks

The implication and the equivalence. DC and finite multiple selections proves over $Z F$ that $D C \leftrightarrow (D M C \land {A C}_{ω, f i n})$ , which gives both the implication DC to DMC and the converse implication from DMC plus finite-selection countable choice; the principles are those of The axiom of dependent choice: a relation in which every element is related to something admits an $N$ -indexed chain and Dependent multiple choice in finite-level tree form.
Multiple choice in ZF. Multiple choice is equivalent to AC in ZF proves $M C \leftrightarrow A C$ in $Z F$ (Multiple choice and dependent multiple choice, The Axiom of Choice). That is a theorem about $Z F$ ; it says nothing about $Z F A$ , where the same sentence is not available at this point in the library.
The ZFA qualification. The separations known for DMC are obtained in permutation models with atoms; they are therefore theorems about $Z F A$ and are not transferred to $Z F$ by this item. In particular the strictness of DMC below DC over $Z F$ is not asserted, and the only ZF-side nonprovability recorded here is If ZF is consistent, DMC is not provable in ZF, conditional on $Con (Z F)$ .
Consumers. Any use of "DMC is weaker than DC" must name the theory: the $Z F A$ model supplies the separation there, while over $Z F$ the question is open, as recorded by the dated status item of this page.

CorollaryStatement: AI-adaptedProof: AI-adaptedaudited 2026-09-22Open item page →

If ZF is consistent, ZF does not prove Urysohn's lemma

Statement

If $Z F$ is consistent then $Z F$ does not prove Urysohn's lemma: there is a model of $Z F$ in which some normal space has two disjoint closed sets that admit no continuous separation (Normal spaces and $T_{4}$ spaces, with the source disagreement over whether normality includes $T_{1}$ stated explicitly).

The statement is conditional on $Con (Z F)$ and is stated in the metatheory; no model of $Z F$ is exhibited in the library and no unconditional nonprovability is asserted.

Facts & Assumptions

Given: A proof of Urysohn's lemma in $Z F$ and the consistency of $Z F$ .

[F1]

Relative to $Con (Z F)$ , the theory $Z F + {A C}_{ω} + \neg U R Y$ is consistent (Relative consistency of Countable Choice without Urysohn's lemma, The Axiom of Countable Choice ( ${A C}_{ω}$ )).

[L1]

If $T^{'} \supseteq T$ and $T$ proves a sentence $σ$ , then $T^{'}$ also proves $σ$ ; consequently $T^{'} + \neg σ$ is inconsistent. Equivalently, if $T^{'} + \neg σ$ is consistent, then $T$ does not prove $σ$ . In particular, if $Z F$ proves $σ$ , then so does $Z F + {A C}_{ω}$ (elementary consequences of the definition of derivability).

Proof

technique · contradiction

1.1

Assume, for the sake of contradiction, that $Z F$ proves Urysohn's lemma, and assume $Con (Z F)$ .

assume-contra

2.1

Then $Z F + {A C}_{ω}$ proves Urysohn's lemma, since it extends $Z F$ ; but Urysohn's lemma is the sentence $U R Y$ whose negation is consistent with $Z F + {A C}_{ω}$ by [F1].

step 1.1F1L1

3.1

The theory $Z F + {A C}_{ω} + \neg U R Y$ is therefore inconsistent, contradicting its consistency given by [F1] under the assumption $Con (Z F)$ ; hence $Z F$ does not prove Urysohn's lemma.

step 2.1F1discharge-contradiction∎

Remarks

Why the conditional is not weakened to a ZF theorem. The nonprovability is relative to the consistency of $Z F$ ; this library proves no independence result unconditionally, and the cited relative-consistency theorem carries the same qualification.
The stronger statements this corollary is drawn from. The cited theorem gives a model of $Z F$ with countable choice in which Urysohn's lemma fails; the same failure occurs in the BPI model of this page, and either witness would serve. The corollary records the catalogue clause that Urysohn's lemma is not a theorem of $Z F$ alone, using the countable-choice witness, and it is generated directly from the published relative-consistency statement.

RemarkRemark: Literature-sourcedProof: Not applicableaudited 2026-09-22Open item page →

The converse from Urysohn's lemma to DMC is open

Statement

As of 15 September 2026, $Z F$ proves that DMC implies Urysohn's lemma, while whether Urysohn's lemma implies DMC remains open. The countable-choice and BPI countermodels refute both Urysohn's lemma and the bounded Tietze extension conclusion; by contraposition of the proved DMC-to-Urysohn implication, they also fail DMC. Thus they realise $\neg U R Y \land \neg D M C$ , which does not decide the converse $U R Y \Rightarrow D M C$ .

Remarks

The positive implication. DMC implies Urysohn's lemma proves that DMC yields a continuous separation of any two disjoint closed sets of a normal space, using only finite menus of dyadic nodes. That theorem is the source of every "DMC suffices" clause on this page.
The two countermodels. Relative consistency of Countable Choice without Urysohn's lemma and Relative consistency of BPI without Urysohn's lemma give, relative to $Con (Z F)$ , models with countable choice, respectively BPI, in which Urysohn's lemma fails; the same models refute bounded Tietze extension for the same space by Brunner's endpoint obstruction also refutes bounded Tietze extension. The corresponding nonprovability conclusion for ZF is recorded as If ZF is consistent, ZF does not prove Urysohn's lemma, conditional on $Con (Z F)$ .
Why these do not settle the converse. Each countermodel fails Urysohn's lemma, so DMC implies Urysohn's lemma directly gives failure of DMC in that same model by contraposition. These are therefore models of $\neg U R Y \land \neg D M C$ , not models of the conjunction needed to refute the converse. A model of $Z F + U R Y + \neg D M C$ would settle the converse negatively, and no such model is known to the cited line of work.
Dating. The status is dated because it is a report about the present state of the subject rather than a mathematical theorem; if the question is answered, this item must be replaced by the corresponding theorem and its proof, not reworded.

RemarkRemark: AI-adaptedProof: Not applicableaudited 2026-09-22Open item page →

Choice ledger for Baire, Urysohn, Stone, and Tychonoff

Statement

Ledger: separable complete metric Baire is a theorem of $Z F$ ; complete metric Baire is DC; compact-Hausdorff Baire is exactly DMC; Baireness of products of compact Hausdorff spaces is DC; DMC implies Urysohn's lemma, while, relative to the consistency of ZF, countable choice and BPI are each consistent with the failure of Urysohn's lemma and of bounded Tietze extension; Stone follows from AC, while relative to the consistency of ZF both DC and BPI are separately consistent with a metrizable space having an open cover with no locally finite open refinement; the stronger per-cover effective refinement assertion for discrete metrizable spaces implies AC; compact Hausdorff products and cofinite products have the strength of BPI; compact $T_{1}$ and arbitrary compact products have the strength of AC. DC implies DMC; if ZF is consistent, ZF does not prove DMC; and DMC-to-DC over $Z F$ remains open.

Remarks

Baire rows. Separable complete metric spaces are Baire in ZF is ZF, whereas Dependent Choice is equivalent to the complete-metric Baire principle over ZF proves over ZF that the unrestricted complete-metric Baire principle is equivalent to DC; DMC makes every compact Hausdorff space Baire gives DMC implies compact-Hausdorff Baire, Compact Hausdorff Baire implies DMC gives the converse and Compact Hausdorff Baire is equivalent to DMC packages the equivalence; DC is equivalent to Baireness of compact-Hausdorff products is the product row, which is DC and not merely DMC.
Urysohn rows. DMC implies Urysohn's lemma is the positive row; Relative consistency of Countable Choice without Urysohn's lemma and Relative consistency of BPI without Urysohn's lemma are the two separations, and Brunner's endpoint obstruction also refutes bounded Tietze extension records the bounded-Tietze consequence. The status of the converse is The converse from Urysohn's lemma to DMC is open.
Stone rows. Stone's theorem, under choice: every metric space is paracompact is the AC row; Relative consistency of DC with failure of Stone's theorem and Relative consistency of BPI with failure of Stone's theorem are relative-consistency separations from DC and BPI, respectively. In the BPI model the sharper obstruction is a metrizable space with an open cover having no point-finite open refinement, hence no locally finite open refinement; Effective metacompactness for discrete metric spaces implies AC is the effective strengthening, and the exact strength of the ordinary theorem is recorded as open in The exact choice strength of Stone's theorem remains open.
Tychonoff rows. Cofinite products and compact Hausdorff products have the strength of BPI (Products of cofinite spaces are compact exactly under BPI, and the compact Hausdorff equivalence cited there); compact $T_{1}$ products and arbitrary compact products have the strength of AC (The compact T1 product theorem is equivalent to AC, The arbitrary compact product theorem is equivalent to AC).
Principle rows. DC implies DMC and, assuming the consistency of ZF, DMC is not a ZF theorem (If ZF is consistent, DMC is not provable in ZF); BPI does not imply DMC (BPI does not imply DMC); the qualifications over $Z F A$ and the openness of the reversal are in DMC, Multiple Choice, and AC qualifications and DMC versus DC over ZF remains open. No strict DMC-versus-DC claim over $Z F$ is made anywhere in this ledger.

5 · Examples, counterexamples and false statements

None yet.