A. H. Stone's theorem that every metric space is paracompact is not choice-free

Stone's theorem. Every metric space is paracompact.

The following are relative to the consistency of ZF.

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

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

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

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

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

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

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