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 compares locally proved forms of the Baire category theorem, Urysohn separation, metric paracompactness and compact-product principles. Separable complete metric spaces are Baire in ZF. The unrestricted complete-metric form is equivalent to dependent choice, and the compact Hausdorff form is equivalent to dependent multiple choice. Products of compact Hausdorff spaces are Baire exactly under dependent choice.

Dependent multiple choice implies Urysohn separation. A given failure of Urysohn separation yields a failure of bounded Tietze extension and of dependent multiple choice. The nonprovability corollaries explicitly assume consistency of an extending theory containing a counterexample; no countable-choice or Boolean-prime-ideal countermodel is constructed here. The Brunner and Corson local constructions in ZFA remain available with their stated ambient theory.

Stone's theorem follows from AC; its effective per-cover strengthening implies AC. The separately constructed dependent-choice countermodel retains its own contract. Products of cofinite spaces are compact exactly under BPI, while the compact T1 and unrestricted compact-product principles are equivalent to AC. The final ledger distinguishes these positive implications and exact ambient theories from conditional metatheorems. Questions about converses are presented as questions without a claim about current research status.

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.1assume-hyp

Assume the tree form of the statement.

1.2assume-hyp

Assume the successor-menu form of the statement.

2.1step 1.1F2L1

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.

2.2step 1.2F2

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$ .

3.1step 2.1F2L2L3

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.

3.2step 2.2F2

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.

4.1step 3.2F1L3

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}$ .

4.2step 3.1F1L1

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].

5.1step 4.1F2L2L3

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.

5.2step 3.1step 4.2F1

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.

6.1step 5.1F2L3

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.

7.1step 5.1step 6.1F2L1L2

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.

8.1step 6.1step 7.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.

9.1step 5.2step 8.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$ .

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.1givenL1L2

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].

1.2assume-caseassume-case

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$ .

2.1step 1.2L2

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.

2.2step 1.2L3

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.

3.1step 2.2L2L3

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.

4.1step 3.1L2

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$ .

5.1step 1.2step 2.1step 4.1cases-exhaustive∎

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.

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.1givenF1

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}$ .

1.2assume-caseassume-case

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

2.1step 1.2F1

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.

2.2step 1.2F1F3

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$ .

3.1step 2.2F1F2L3L4

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$ .

3.2step 2.2F1F2

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].

4.1step 3.1step 3.2F1F2L5

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.

5.1L5step 3.1step 3.2step 4.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.

5.2step 3.1step 4.1F2L3

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].

6.1step 5.1step 5.2L1L2L4

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.

7.1step 5.2step 6.1F2L2L3

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].

8.1step 3.2step 5.2step 7.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}$ .

9.1step 2.1step 8.1step 4.1cases-exhaustive∎

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$ .

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.1givenF4

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$ .

2.1step 1.1L1

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.

2.2step 1.1F1F2F3

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

2.3step 1.1L2

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}^{'}$ .

2.4step 1.1L1

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

3.1step 2.2step 2.3step 2.4F2L1L2

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$ .

4.1step 3.1

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

5.1step 4.1F4

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}$ .

6.1step 5.1L3

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].

7.1step 3.1step 6.1step 2.3

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}^{'}$ .

8.1step 6.1step 7.1L2

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}^{'}$ .

9.1step 2.2step 8.1F3L2

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.

10.1step 8.1step 9.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$ .

11.1step 2.1step 10.1F4∎

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.

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.1givenF1

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.

2.1step 1.1F2F3

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$ .

3.1step 2.1F3

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

4.1step 3.1L2

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)$ .

5.1step 3.1step 4.1F3L2

$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$ .

5.2step 4.1

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

6.1step 5.2step 2.1L2

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$ .

6.2step 4.1step 5.1F4

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.

7.1step 5.2step 6.1L2

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}$ .

7.2step 2.1step 6.2F2F3

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.

8.1step 1.1step 5.1step 6.1step 7.1L1

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}$ .

8.2step 6.2step 7.2F2F5

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.

9.1step 8.1step 7.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.

9.2step 8.2F5

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}^{*}$ .

9.3step 6.2step 8.2

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}$ .

10.1step 4.1step 9.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$ .

10.2step 9.2step 9.3L2

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.

11.1step 10.1L2

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.

12.1step 11.1step 10.2F1∎

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.

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.1assume-hypF1

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

1.2assume-hypF2

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

2.1step 1.1step 1.2L1∎

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].

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.1assume-hypgiven

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}$ .

1.2assume-hypgiven

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.

2.1step 1.1L1

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$ .

2.2step 1.2F6F7

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.

3.1step 2.1L1

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.

3.2step 2.2F3

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.

4.1step 3.1L1L2F4

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}^{'}))$ .

4.2step 3.2L1F4

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.

5.1step 4.1F1

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}$ .

5.2step 4.2F5

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.

6.1step 5.1F2F7

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].

6.2step 5.1L1F7

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$ .

6.3step 5.2F5L1

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}$ .

7.1step 6.1step 6.2F2F7

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$ .

7.2step 6.3F6

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.

8.1step 7.1step 3.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.

8.2step 2.2step 7.2F6

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.

9.1step 8.1step 8.2∎

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.

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.1givenF5

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

2.1step 1.1F1L1

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$ .

3.1step 2.1L1

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}$ .

4.1step 2.1step 3.1F1F4L1

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$ .

5.1step 3.1step 4.1F5L1L2

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.

6.1step 5.1L1

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].

7.1step 5.1step 6.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.

8.1step 6.1step 7.1F2F3

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.

9.1step 8.1F3

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]$ .

10.1step 6.1step 8.1step 9.1F2

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$ .

10.2step 6.1step 8.1step 9.1

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$ .

11.1step 9.1step 10.1step 10.2F5∎

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.

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.1givenF1F2F3

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.

1.2givenF1F2F3

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.

1.3givenF1F2F3

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$ .

1.4givenF1F2F4

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.

2.1step 1.1F2F3

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$ .

2.2step 1.2step 1.3F2F5

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].

2.3step 1.4F4

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$ .

2.4step 1.4F1F3F4

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.

3.1step 2.1F3

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.

4.1step 1.1step 2.1step 3.1F1F3

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.

5.1step 4.1step 2.2step 2.3step 2.4F2F5∎

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.

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.1givenF1

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.

2.1step 1.1F2F4L1

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.

2.2step 1.1F1F4L1

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.

3.1step 2.1step 2.2F3

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$ .

4.1step 1.1step 3.1F1F4

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.

5.1step 4.1F4∎

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.

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.1F1

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.2givenL1

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.

2.1step 1.1F2

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

3.1step 2.1step 1.2L1

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.

4.1step 2.1step 3.1F1F2∎

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.

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.1F2

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.1step 1.1F1

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

3.1step 1.1step 2.1L1F1

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.

4.1step 1.1step 3.1L1F1

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.

5.1step 1.1step 3.1step 4.1F1F2F3∎

By step 3.1 and [F1], the existential closure of $Φ$ is boundable with the fixed absolute bound $ω + ω$ ; by [F3] it is injectively boundable, and step 4.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.

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.

CorollaryStatement: AI-adaptedProof: AI-generatedOpen item page →

A Urysohn separation obstruction also obstructs bounded Tietze extension

Statement

Let $X$ be a normal space (Normal spaces and $T_{4}$ spaces, with the source disagreement over whether normality includes $T_{1}$ stated explicitly) and let $A, B$ be disjoint closed subsets admitting no continuous map $X \to [0, 1]$ that is zero on $A$ and one on $B$ . Then the map $g : A \cup B \to [0, 1]$ equal to zero on $A$ and one on $B$ is continuous and has no continuous extension to $X$ .

Consequently, over ZF, failure of Urysohn's lemma implies failure of bounded Tietze extension. This is an implication between existence assertions; it constructs neither a counterexample space nor a model of ZF.

Facts & Assumptions

Given: The normal space $X$ and disjoint closed $A, B$ with the stated separation obstruction.

[F1]

Closed sets in a subspace are traces of ambient closed sets (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]

Continuity means that preimages of open sets are open (Continuity of a map of topological spaces at a point and globally); the target is $[0, 1]$ (Intervals of $R$ : the nine order-convex forms, nondegeneracy, and length).

Proof

1.1givenF1F2construct

In the subspace $A \cup B$ , the sets $A$ and $B$ are closed by F1 and are each other's complements. Thus both are open. Define $g = 0$ on $A$ and $g = 1$ on $B$ , well-defined since the sets are disjoint. The preimage under $g$ of any open subset of $[0, 1]$ is one of $\emptyset, A, B, A \cup B$ , all open in the subspace. Hence $g$ is continuous by F2.

2.1givenstep 1.1∎

A continuous extension $G : X \to [0, 1]$ of $g$ would vanish on $A$ and be one on $B$ , contradicting the given obstruction. Therefore no such extension exists. Since $A \cup B$ is closed in $X$ , this is exactly a failure of bounded Tietze extension. Applying this construction to any normal-space witness of $\neg U R Y$ proves the final implication.

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.1givenF2F3F5

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.

2.1step 1.1F1F4

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$ .

3.1step 1.1step 2.1F5

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$ .

4.1step 3.1F1F3F4

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} < λ$ .

5.1step 4.1F3F6

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.

6.1step 3.1step 4.1step 5.1F2F3F6∎

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.

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.1assume-contraF1

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}$ .

2.1step 1.1F1

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_{ξ})$ .

3.1step 2.1F2

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.

4.1step 1.1step 2.1step 3.1F2F3

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_{ξ})$ .

4.2step 3.1F3

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.

5.1step 2.1step 4.1step 4.2discharge-contradiction∎

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$ .

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.1givenF5

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)$ .

2.1step 1.1F1F2

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

2.2step 1.1F4

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.

3.1step 2.2F4

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.

4.1step 3.1F4

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.

5.1step 4.1F3

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

6.1step 1.1step 2.1step 5.1F5∎

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.

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.1assume-contraL1F1

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$ .

2.1step 1.1F2L2

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$ .

3.1step 2.1F2F1

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$ .

4.1step 2.1step 3.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$ .

5.1L1step 3.1step 4.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$ .

6.1step 4.1step 5.1discharge-contradiction∎

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.

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.1given

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.

2.1step 1.1F1F2L1

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.

3.1givenstep 2.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.

4.1givenA1step 3.1construct

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.

5.1step 4.1F3L2

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$ .

5.2step 3.1step 4.1L3

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.

6.1step 2.1step 4.1step 5.1step 5.2

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$ .

7.1step 3.1step 6.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.

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.1givenF1F2

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.

2.1step 1.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.

3.1step 2.1L1L2

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)$ .

3.2step 1.1step 2.1

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.

4.1step 3.1step 3.2F1F2∎

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.

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.1givenF2

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.

2.1step 1.1F2L1

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.

3.1step 2.1L1

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)$ .

4.1step 2.1step 3.1L1

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.

5.1step 4.1F1∎

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.

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.1givenF2

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$ .

2.1step 1.1F3L1

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$ .

3.1step 2.1F2F3L2

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.

4.1step 1.1step 3.1F1F3

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.

5.1step 2.1step 3.1step 4.1F3L1

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.

6.1step 5.1F4L1

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.

7.1step 6.1F2F3L1

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.

8.1step 5.1step 7.1F3∎

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.

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.1given

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

2.1step 1.1F1F3F4

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.

2.2step 1.1F1F2

$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}$ .

3.1step 2.1F2F3F4

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.

4.1step 2.2F1F2∎

$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.

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.1assume-hypF2

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.

1.2assume-hypgiven

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.

2.1step 1.2F1

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.

3.1step 2.1F1F4L1

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.

4.1step 2.1step 3.1F3

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}$ .

5.1step 1.1step 4.1∎

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

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.1assume-hypF1

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

2.1step 1.1F2

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.

3.1step 1.1step 2.1F2F3∎

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.

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-adaptedOpen item page →

A consistent BPI counterexample theory obstructs a proof of DMC

Statement

If $Z F + B P I + \neg U R Y$ is consistent, then $Z F + B P I$ does not prove DMC. Here BPI and DMC are the principles of The Boolean prime ideal principle and Dependent multiple choice in finite-level tree form, and $U R Y$ is Urysohn separation in normal spaces (Normal spaces and $T_{4}$ spaces, with the source disagreement over whether normality includes $T_{1}$ stated explicitly).

No consistency of the counterexample theory or existence of its model is asserted; the hypothesis is an additional consistency premise, not a consequence of $Con (Z F)$ established here.

Facts & Assumptions

Given: Consistency of $T = Z F + B P I + \neg U R Y$ .

[F1]

ZF proves DMC implies Urysohn's lemma (DMC implies Urysohn's lemma).

Proof

1.1givenF1

If $Z F + B P I$ proved DMC, the same finite derivation would be a $T$ derivation, since $T$ extends that theory. The ZF derivation F1 would then give $U R Y$ in $T$ .

2.1givenstep 1.1∎

The axiom $\neg U R Y$ of $T$ would combine with that derivation to give a contradiction, contrary to the given consistency. Thus $Z F + B P I$ cannot prove DMC under the stated hypothesis.

CorollaryStatement: AI-adaptedProof: AI-adaptedOpen item page →

A failure of Urysohn separation forces failure of DMC

Statement

Over ZF, failure of Urysohn's lemma implies failure of DMC (Dependent multiple choice in finite-level tree form). In particular, if any consistent theory $T$ extends ZF and includes $\neg U R Y$ , then ZF does not prove DMC. No existence or consistency of such a $T$ is asserted.

Facts & Assumptions

Given: ZF, with $\neg U R Y$ for the first claim; and a consistent extending theory $T$ containing $\neg U R Y$ for the second claim.

[F1]

Over ZF, DMC implies Urysohn's lemma (DMC implies Urysohn's lemma).

Proof

1.1givenF1

Under $\neg U R Y$ , DMC would give $U R Y$ by F1, a contradiction. Therefore $\neg D M C$ holds. This proves the internal implication over ZF.

2.1givenF1step 1.1∎

If ZF proved DMC, the same finite derivation would hold in the extending $T$ , and the finite ZF proof F1 would give $U R Y$ in $T$ . Together with its axiom $\neg U R Y$ this contradicts consistency of $T$ . Thus ZF cannot prove DMC under the stated additional consistency hypothesis.

RemarkRemark: Literature-sourcedProof: Not applicableOpen item page →

The proved Stone theorem and its effective strengthening

Statement

AC proves that every metric space is paracompact (Stone's theorem, under choice: every metric space is paracompact). The stronger assertion that every open cover of every discrete metrizable space has a point-finite refinement equipped with a refinement map implies AC (Effective metacompactness for discrete metric spaces implies AC).

Remarks

The ordinary theorem. The AC hypothesis in the local Stone theorem is sufficient for its proof. The theorem supplies a locally finite open refinement of every open cover; it asserts no global refinement operator.
The effective strengthening. The refinement map is part of the hypothesis in Effective metacompactness for discrete metric spaces implies AC, and the local proof recovers a choice function from that map. This stronger assertion is not identified with the ordinary existential Stone theorem.
The separate DC row. Relative consistency of DC with failure of Stone's theorem is the existing supplier for the conditional comparison with DC. The present amendment removes the unsupported BPI transfer comparison and makes no claim about the current research status of the exact ordinary theorem.

RemarkRemark: Literature-sourcedProof: Not applicableOpen 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, and the cited proof is specifically over $Z F$ . 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 base theory matters. The two local implications above are stated over ZF. A statement proved over ZF is not thereby proved over ZFA; any comparison over a theory with atoms needs its own proof and hypotheses.
Consumers. DC implies DMC by the cited local theorem. The strictness of that implication is not asserted here.

CorollaryStatement: AI-adaptedProof: AI-adaptedOpen item page →

Consistency of a Urysohn counterexample theory obstructs a ZF proof

Statement

Let $T$ be any first-order theory extending ZF and containing the negation of Urysohn's lemma for normal spaces (Normal spaces and $T_{4}$ spaces, with the source disagreement over whether normality includes $T_{1}$ stated explicitly). If $T$ is consistent, then ZF does not prove Urysohn's lemma.

This is a conditional criterion. It asserts neither consistency of such a $T$ nor existence of a model or a counterexample space.

Facts & Assumptions

Given: A consistent theory $T$ containing every ZF axiom and the sentence $\neg U R Y$ , where $U R Y$ asserts continuous separation of disjoint closed sets in every normal space.

[F1]

A finite derivation using axioms of a subtheory is a derivation in the extending theory, since each axiom used is still available.

Proof

1.1givenF1assume-contra

Suppose ZF proves $U R Y$ . The same finite derivation is a $T$ derivation by F1 and the given inclusion of axioms.

2.1givenstep 1.1discharge-contradiction∎

Since $T$ also has $\neg U R Y$ as an axiom, it would derive a contradiction. This contradicts the assumed consistency of $T$ ; therefore ZF does not prove $U R Y$ .

RemarkRemark: Literature-sourcedProof: Not applicableOpen item page →

The converse from Urysohn separation to DMC: a comparison question

Statement

Over ZF, DMC implies Urysohn's lemma (DMC implies Urysohn's lemma). One may ask whether the converse holds. This item states no answer or current research status for that question.

Remarks

A failure of Urysohn's lemma implies failure of DMC by contraposition (A failure of Urysohn separation forces failure of DMC) and also failure of bounded Tietze extension (A Urysohn separation obstruction also obstructs bounded Tietze extension). These conditional implications establish no countermodel existence. Even if a counterexample to Urysohn's lemma were supplied, it would satisfy $\neg U R Y \land \neg D M C$ and would not refute the converse $U R Y \Rightarrow D M C$ ; that requires a witness of $U R Y \land \neg D M C$ instead.

RemarkRemark: AI-adaptedProof: Not applicableOpen 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; failure of Urysohn separation implies failure of DMC and bounded Tietze extension; the local positive implication does not provide a countermodel; Stone follows from AC, while the separate DC supplier states, relative to the consistency of ZF, that DC is 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; 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 proves the positive implication, and A failure of Urysohn separation forces failure of DMC proves its contraposition. A Urysohn separation obstruction also obstructs bounded Tietze extension proves that any supplied normal-space separation obstruction also obstructs bounded Tietze extension; it asserts no countermodel existence. The converse comparison is posed as a question in The converse from Urysohn separation to DMC: a comparison question.
Stone rows. Stone's theorem, under choice: every metric space is paracompact is the AC row. The separate Relative consistency of DC with failure of Stone's theorem is the existing DC-comparison supplier. No BPI-to-Stone nonimplication is supplied here. Effective metacompactness for discrete metric spaces implies AC proves the effective strengthening with a refinement map; the distinction from the ordinary theorem is explained in The proved Stone theorem and its effective strengthening.
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. A consistent BPI counterexample theory obstructs a proof of DMC gives only the conditional criterion: if ZF+BPI+not Urysohn is consistent, ZF+BPI cannot prove DMC. No consistency of that counterexample theory is established by that corollary; the base-theory qualifications and the separate reversal question 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.