Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedjudge pass (gpt-5.6-terra)audited 2026-09-22
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.

Compact Hausdorff Baire implies DMC

Statement

Over ZF, 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 ZF 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).

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

[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 Tn 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∣≤∣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 ∞ 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∪{∞} 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 ∞∈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 ∞ 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-∞ function is a member.

4.1step 3.1L2

Let K⊆X be the set of those x with: for all m<n, either x(m)=∞, or x(n)=∞, or x(m),x(n)∈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∈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∈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 ∞ lies in K.

5.2step 4.1

For n∈N put Gn:={ x∈K:x(i)≠∞ for some i≥n }, a subset of K.

6.1step 5.2step 2.1L2

Each Gn is open in K: it is the union over i≥n and t∈T of the sets K∩{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⊆X whose trace K∩W is contained in a member of the cover; here the coordinate restrictions in W may be taken to be a singleton {t}, t∈T, or a cofinite neighbourhood of ∞. 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∈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 Gn is dense in K: let N be a nonempty relatively open subset of K, and choose a basic product-open W with ∅≠K∩W⊆N, restricting only the coordinates in a finite set J; choose u∈K∩W. If u(i)≠∞ for some i≥n then u∈N∩Gn and we are done. Otherwise every non-∞ 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-∞ value. Choose N1≥n larger than every index in J and larger than n, and let s∈T be a proper extension of t of length at least N1, which exists by finitely iterating pruning and restricting to the required length if needed (choose a length at least max⁡(N1,dom⁡(t)+1)). Define y by: y(i):=u(i) for i∈J; y(i):=∞ if i∉J and i>N1; y(N1):=s; and y(i):=∞ if i∉J and i<N1. Then y∈K∩W, because the only non-∞ values are the values of u at indices in J together with s at N1, all of which are comparable by the maximality of t and the choice of s; and y(N1)=s≠∞ with N1≥n gives y∈Gn.

7.2step 2.1step 6.2F2F3

In case B, construct families En of closed subsets of X by E0:=E and: if ∞∈πn[E] for every E∈En, let En+1 be En together with E∩πn−1[{∞}] for E∈En, and otherwise let En+1:=En; 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⊆E∩E′ in En gives the lower bound D∩πn−1[{∞}] whenever one or both of the two sets carries the new coordinate constraint. Thus each En 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∈N, t∈T, and πi−1[{∞}], i<n. For such an E, take one finite Boolean expression in the listed generators and let H⊆T be the finite set of node labels tested at coordinate n. No test x(n)=∞ occurs, since all infinity tests have indices less than n. If x∈E and x(n)∉H, replacing only x(n) by ∞ preserves every test and hence membership in E. Therefore ∞∉πn[E] implies πn[E]⊆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 Gn are dense open, so their intersection is dense and in particular nonempty; fix x∈⋂nGn. Let D:={ i∈N:x(i)≠∞ }.

8.2step 6.2step 7.2F2F5

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

9.1step 8.1step 7.1

In case A, D is infinite: for each n the membership x∈Gn gives some i≥n with x(i)≠∞, 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∈D, one can adjoin a cylinder πn−1[{sn}], sn∈Fn, while preserving the finite-intersection property: at that stage include the member En0 from step 8.2, whose n-th projection is the finite set Fn; if no one of the finitely many cells πn−1[{s}], s∈Fn, preserved the finite-intersection property, finitely many witnessing failures, obtained using [F5], would have a common lower bound meeting En0 but none of those cells, a contradiction. Closing under finite intersections gives a downwards-directed family E1∗ of nonempty closed sets which contains E∗ and the chosen cylinders. Define z(n):=sn for n∈D and z(n):=∞ otherwise. Every basic neighbourhood of z meets every E∈E1∗: intersect E with the finitely many chosen singleton cylinders for its coordinates in D and, for coordinates outside D, with the cylinders πn−1[{∞}]∈E∗. Therefore z lies in the closure of every member, hence in every member because they are closed, contradicting the empty intersection of E∗⊆E1∗.

9.3step 6.2step 8.2

In case B, let m<n lie in D and s∈Fm. Then some t∈Fn properly extends s. Otherwise every t∈Fn gives a constraint complement Ct:=X∖{x:x(m)=s, x(n)=t}∈E∗ by step 6.2. Take En0∈E∗ with πn[En0]=Fn from step 8.2, and use downward directedness and the finiteness of Fn to obtain E′∈E∗ with E′⊆En0∩⋂t∈FnCt. Since s∈Fm⊆πm[E′], choose x∈E′ with x(m)=s. But x(n)∈πn[E′]⊆Fn; taking t=x(n) contradicts x∈Ct.

10.1step 4.1step 9.1

In case A, the values x(i) for i∈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 ∞.

10.2step 9.2step 9.3L2

In case B, enumerate D increasingly as m0<m1<⋯ and put F0′:=Fm0 and Fi+1′:={t∈Fmi+1:s is a proper initial segment of t for some s∈Fi′}. By step 9.3, every s∈Fi′ has an extension in Fi+1′; by definition every member of Fi+1′ has a predecessor in Fi′. Thus every Fi′ 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 ⋃iFi′. It is a subtree and has a node at every level r, because any member of Fr′ has length at least r. Its level r is finite: if u∈T′ has length r, choose t∈Fj′ with u an initial segment of t. If j<r, extend t through the successive Fi′ to a member of Fr′; if j>r, follow predecessors down to a member of Fr′. In either case, because initial segments of the same node are comparable and every member of Fr′ has length at least r, u is the length-r initial segment of some member of the finite set Fr′. Hence the level has at most ∣Fr′∣ elements.

11.1step 10.1L2

In case A, let T′ be the set of all initial segments of the nodes x(i), i∈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∈D; for i≤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 Gn; the recursive construction of the families En in case B is a definition by recursion on N and the sets Fi′ are defined, not selected. Case B uses individual existential witnesses and finite choices, never countably many simultaneous selections.

Depends on

Dependency tree · 2 levels

Sources