Alphabeta Math
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: Examples and Counterexamples

1 · Prerequisites

2 · Summary

Worked examples and counterexamples for the choice-strength pair. The page computes the canonical least-ball selection in the separable Baire proof, the finite-menu intersection in the DMC Urysohn construction, the failure of closedness for the cofinite coordinate set, and the isolated-point repair that recovers a choice function from a compact T1 product; it also records the false statement that the Boolean prime ideal principle proves Stone's theorem for metric spaces, refuted by the transferred Corson model.

3 · Logical flowchart

4 · Definitions, theorems and proofs

None yet.

5 · Examples, counterexamples and false statements

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

Canonical least-ball selection removes choice

Example

A coded least-pair rule is an alternative to the lexicographic rule in Separable complete metric spaces are Baire in ZF. Given a nonempty open G and ρ>0, call (k,m) admissible when m≥1, 1/m≤ρ and Bˉ(s(k),1/m)⊆G. Choose the admissible pair of least code under P(k,m)=2k(2m+1)−1. The following three-stage calculation permits repetitions in the dense enumeration and spends no choice.

Facts & Assumptions

Given: Work in ZF. Let (X,d) be a nonempty separable complete metric space, let s:N→X have dense range, let (Un)n∈N be a specified sequence of dense open subsets of X, and let W be nonempty open. Set G0=W∩U0 and use radius bound 2−(n+2) at stage n.

[F2]

Density of the range of s means it meets every nonempty open set (Separability: the existence of an at most countable dense subset). The metric triangle inequality and symmetry hold (Metric space: d(x,y)=0 iff x=y, symmetry, and the triangle inequality; pseudometric and ultrametric); for every ε>0 some integer m≥1 has 1/m<ε (For every ε>0 in a complete ordered field there is a natural n≥1 with 1/n<ε).

[F3]

The explicit P=σ−1∘J in N×N≈N is a bijection N2→N. Every nonempty subset of N has a least element (The well-ordering principle), so the least element of P[A] decodes to a unique member of every nonempty admissible set A.

[F4]

A specified self-map of a set and an initial state determine a unique natural-number sequence by The recursion theorem.

Verification

1.1givenF1F2

For nonempty open G and ρ>0, fix y∈G and r>0 with B(y,r)⊆G. By [F2] take m≥1 with 1/m<min⁡(r/3,ρ) and k with s(k)∈B(y,1/m). For z∈Bˉ(s(k),1/m) the triangle inequality gives d(z,y)≤d(z,s(k))+d(s(k),y)<2/m<r. Thus Bˉ(s(k),1/m)⊆G, proving the admissible set nonempty. This is one finite existence argument for arbitrary G,ρ, not a simultaneous choice of witnesses.

2.1givenF1step 1.1

Density of U0 makes G0 nonempty, and it is open. Thus step 1.1 with bound 1/4 supplies an admissible pair.

3.1step 2.1F1F3given

Decode the least code to (k0,m0) and put x0=s(k0), r0=1/m0. Then Bˉ(x0,r0)⊆G0. The set G1=B(x0,r0)∩U1 is nonempty by density of U1, because the open ball contains x0; it is open by finite intersection.

4.1step 1.1step 3.1F1F3given

Apply the same rule to G1 with bound 1/8, and then to G2=B(x1,r1)∩U2 with bound 1/16. At each stage density of the specified next Un keeps Gn nonempty open, and step 1.1 and [F3] supply the unique next pair. Repeated values of s do not affect uniqueness of the index-radius pair.

5.1step 4.1F1F3construct

For a concrete example take X={p}, d(p,p)=0, s(k)=p for every k, and W=Un=X for every n. The metric axioms hold, every sequence converges to p, and the range of s is dense, so the given hypotheses hold. All positive-radius open and closed balls equal X. At stages n=0,1,2 admissibility is exactly m≥2n+2. Since P(k,m)≥2m, with equality exactly when k=0, the least pairs are (0,4),(0,8),(0,16), with codes 8,16,32 and radii 1/4,1/8,1/16. All centers are the same point p, as required for an enumeration with repetitions.

6.1step 1.1step 2.1step 3.1step 4.1F3F4∎

For the general recursion use the set of states (n,G) with G nonempty open, together with a default state. The unique least-code pair defines the successor state (n+1,B(s(k),1/m)∩Un+1) on each such state; let the default state map to itself. The preceding nonemptiness argument makes this a total self-map. Apply [F4] from (0,G0) and take the uniquely defined centers and radii. This is set recursion, not a choice of points from an arbitrary family; it gives the same closed-ball inclusions and radius bounds needed in the cited theorem, though its pairs need not equal the lexicographically least pairs there.

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

Finite-menu intersection in the DMC Urysohn construction

Example

In the DMC construction of DMC implies Urysohn's lemma each level n of the dyadic scale is obtained by intersecting, coordinatewise, the finitely many nodes of the menu at that level. The example computes the first two levels and verifies that the closure inclusions survive the intersection and that the predecessor coherence of the menus is preserved.

Facts & Assumptions

Given: A normal space X with disjoint closed sets F,G; nodes ⟨U1,…,U2n⟩ of open sets with Ui‾⊆Ui+1 for 1≤i<2n, F⊆U1 and U2n=X∖G; and nonempty finite menus Mn,Mn+1 of nodes of levels n and n+1, respectively. The successor relation used here is the one fixed in DMC implies Urysohn's lemma: for a∈Mn and b∈Mn+1, aSb means b2i=ai for every 1≤i≤2n. Every a∈Mn has an S-successor in Mn+1, and every b∈Mn+1 has an S-predecessor in Mn.

[F3]

Abstract DMC supplies successor menus, without prescribing their levels (Dependent multiple choice in finite-level tree form). Here level alignment and both coverage properties are explicit Given hypotheses; their construction in DMC implies Urysohn's lemma is context, not an additional premise of this finite calculation. Natural numbers include zero (The natural numbers N (von Neumann)).

Verification

1.1givenF2

Let a(1),…,a(m) be the nodes of the menu at level n, with entries ai(j), and put Ui:=⋂1≤j≤mai(j) for 1≤i≤2n; each Ui is a finite intersection of open sets, hence open.

2.1step 1.1F1

For each 1≤i<2n the inclusion Ui‾⊆Ui+1 holds: Ui‾ is contained in ⋂1≤j≤mai(j)‾ by [F1], and each ai(j)‾⊆ai+1(j) by hypothesis, so Ui‾⊆⋂1≤j≤mai+1(j)=Ui+1.

2.2step 1.1F2

The boundary values are preserved: F⊆U1 because F is contained in every a1(j), and U2n=X∖G because every a2n(j) equals X∖G.

2.3step 1.1given

Predecessor coherence is preserved: the Given predecessor property and the definition of S show that every 2i-th entry occurring in the level-(n+1) menu is an i-th entry occurring in the level-n menu. Conversely, the successor property in the Given data makes every level-n node occur as the predecessor of some level-(n+1) node, so every level-n i-th entry occurs among those 2i-th entries. The two indexed families of sets therefore have the same range, and their intersections are equal.

3.1step 2.1step 2.2step 2.3givenF1F3∎

At level 0 the only possible node is ⟨X∖G⟩, so its intersection is X∖G. A finite menu at level 1 consists of nodes ⟨Vj,X∖G⟩, 1≤j≤m, with F⊆Vj and Vj‾⊆X∖G. Its two intersections are V=⋂1≤j≤mVj and X∖G. Steps 2.1 and 2.2 give F⊆V⊆V‾⊆X∖G; the second intersection equals the level-0 value as in step 2.3. When m=1 these are just the original entries. All finite enumerations here concern one fixed menu; no sequence of enumerations is selected.

CounterexampleConstruction: Literature-sourcedVerification: AI-adaptedaudited 2026-09-22Open item page →

Kelley's cofinite set is not closed

Statement refuted

The following two related claims both fail, but they are not equivalent instances of one claim:

  1. in the cofinite space on an infinite set A, every infinite subset with infinite complement is closed; and
  2. the coordinate set A is closed in the cofinite topology on A∪{∞} when A is infinite (The discrete, indiscrete, cofinite, cocountable, particular-point and Sierpinski topologies, Topology on a set, open and closed sets, clopen sets, the closed-set axiomatisation, and the coarser/finer comparison).

Counterexample

Take A=N with the cofinite topology (The natural numbers N (von Neumann), Finite, countably infinite, countable, uncountable) and let E⊆N be the set of even naturals. For the second claim, give Y=N∪{∞} its cofinite topology.

Facts & Assumptions

Given: The cofinite spaces on A=N and Y=N∪{∞}, and the set E of even naturals.

[F1]

In the cofinite topology on a set S, the open sets are ∅ and the sets with finite complement, and the closed sets are S and the finite subsets; hence every finite set, in particular every singleton, is closed (The discrete, indiscrete, cofinite, cocountable, particular-point and Sierpinski topologies, A space is T1 if and only if every singleton is closed, if and only if every finite subset is closed, if and only if its topology contains the cofinite topology, T0 (Kolmogorov) and T1 (Frechet) spaces).

[F2]

The repaired coordinate of The isolated-point repair of Kelley's choice space is a different space: there A is closed because the added point is isolated, which is why the cofinite presentation on A∪{∞} is not the coordinate used in the product argument.

Verification

1.1givenF1

E is infinite: the map k↦2k is injective from N onto E, so E is countably infinite.

1.2given

N∖E, the set of odd naturals, is infinite: k↦2k+1 is injective from N into it, so it is not finite.

1.3givenF1

In the cofinite space Y, the coordinate set A=N is not closed. Indeed, its complement is the singleton {∞}; this set is nonempty but is not open because its complement A is infinite.

2.1step 1.1step 1.2F1

E is not closed: if E were closed then its complement N∖E would be open. It is nonempty because 1 is odd, and it is not cofinite because its complement E is infinite by step 1.1. Thus N∖E is neither empty nor cofinite, contrary to [F1].

3.1step 2.1step 1.3F2∎

Step 2.1 refutes the first claim using an infinite subset whose complement is infinite, whereas step 1.3 separately refutes the coordinate claim using a subset whose complement is finite. The isolated-point repair of [F2] meets the latter closedness obligation by making {∞} open.

ExampleConstruction: AI-adaptedVerification: AI-generatedaudited 2026-09-22Open item page →

The isolated-point repair recovers a choice function

Example

Take the three nonempty sets A0={0,1}, A1=N and A2=R, and form the repaired coordinates XAj of The isolated-point repair of Kelley's choice space. Assume the compact-T1 product hypothesis: every product of compact T1 spaces is compact. In the product X:=XA0×XA1×XA2 the closed constraints Cj:={x:xj∈Aj} have the finite intersection property, so compactness of X produces a point whose three coordinates are a choice tuple.

Facts & Assumptions

Given: The three sets, their repaired coordinates XAj=Aj⊔{∞j}, and the hypothesis that every product of compact T1 spaces is compact.

[F1]

Each XAj is compact T1 and Aj is a closed subspace of it (The isolated-point repair of Kelley's choice space, T0 (Kolmogorov) and T1 (Frechet) spaces).

[L1]

Let A={A0,A1,A2}. If a product point x satisfies xj∈Aj for every j∈{0,1,2}, then for each S∈A let j(S) be the least j∈{0,1,2} with S=Aj and define g(S)=xj(S). The least index exists because S occurs in the displayed finite list, and g(S)=xj(S)∈Aj(S)=S. Hence g has domain A and is a choice function on A (Choice function, Every natural-number-indexed list of nonempty sets has a choice function on its family of values).

Verification

1.1givenF1F2

The three cylinders C0,C1,C2 are closed in X by [F1] and [F2].

1.2givenF1

Each single cylinder is nonempty: the point with one coordinate 0 (or any other element of Aj) and the artificial values ∞ at the other two coordinates lies in it; the artificial values are available because ∞k∈XAk for every k.

2.1step 1.2F2

For the pair {j,k} the point with prescribed values in Aj and Ak and ∞ in the remaining coordinate lies in Cj∩Ck, so the family has the finite intersection property; for the triple the point (0,0,0) lies in C0∩C1∩C2.

3.1step 2.1F2F3L1

By [F3] the product X is compact, so by [F2] the intersection C0∩C1∩C2 is nonempty. Choose x in this intersection. Then xj∈Aj for all three indices, and the function g defined in [L1] has domain A={A0,A1,A2} and satisfies g(S)∈S for every S∈A. Thus g is the required choice function.

4.1

For a finite list of n sets, the same least-index construction converts a point in the n closed cylinders into a choice function on the underlying set-family. In the general AC argument the factors are instead indexed by the family A itself, so a product point x with xA∈A directly defines the choice function A↦xA; compactness supplies such a point after finite choice verifies the cylinders' finite-intersection property. [step 3.1, F2, L1, Every natural-number-indexed list of nonempty sets has a choice function on its family of values] ∎

Sources