A few standard results (on metrizability and relative separation strength) without choice?

I've been going back over some results from Munkres's Topology, and I'm curious about some things....

I know that Choice principles have some connection to the separation axioms (in ZF, at least)--for example:

Locally compact Hausdorff spaces are Baire if and only if the Axiom of Dependent Multiple Choices holds. [Due to Fossy and Morillon, I believe.]

Complete pseudometric spaces are Baire if and only if the Axiom of Dependent Choices holds.

Still, it seems likely that compactness (or the weaker condition of completeness) and "Baireness" may be playing a substantial part, here.

The link provided below by dfeuer shows that the Urysohn Metrization Theorem--which states that regular, Hausdorff, second-countable spaces are metrizable (or equivalently, that a space is separable and metrizable if and only if it is regular, Hausdorff, and second countable)--holds in ZF, though the Urysohn Lemma--which states that a space is normal Hausdorff if and only if any two disjoint closed sets can be separated by a continuous function--does not. That's a nice result.

I have two questions, then.

First, I wonder if it is known how little Choice is needed for the Urysohn Lemma to hold--the usual proof (cf. Munkres) uses Dependent Choice, and Andreas has suggested that Dependent Multiple Choices may do the trick. Is it known if we can do with even less Choice than that? Is it possible that the Urysohn Lemma is equivalent (in ZF) to some other known Choice principle?

Second, I wonder what is known about how much Choice is needed to prove the following metrization theorems, or whether any of them are known to be equivalent in ZF:

Nagata-Smirnov Metrization Theorem: A topological space $X$ is metrizable if and only if it is $T_3$ and has a basis that is countably locally finite [= $\sigma$-locally finite base].

Smirnov Metrization Theorem: A topological space is metrizable if and only if it is paracompact Hausdorff and locally metrizable.

Bing Metrization Theorem: A topological space $X$ is metrizable if and only if it is $T_3$ and has a basis that is countably locally discrete [= $\sigma$-discrete base].

• Ask and ye shall receive, some: web.mat.bham.ac.uk/C.Good/research/pdfs/horror.pdf indicates that some choice is required for Urysohn's Lemma, but not for Urysohn's Metrization Theorem. – dfeuer Jun 21 '13 at 5:04
• I'd suspect that Bing and Nagata-Smirnov are equivalent in any model, but I'd have to check the proofs. In the text I learnt these from, they were merged into one theorem (Bing-Nagata-Smirnov) as a three-way equivalence. – Henno Brandsma Jun 21 '13 at 5:39
• @dfeuer: Interesting. Thanks! – Cameron Buie Jun 21 '13 at 15:30
• Dependent multiple choice suffices for Urysohn's Lemma. The idea is that, instead of choosing single open sets at each step to interpolate between previous choices, you can choose finitely many open sets and then intersect them. (If I remember correctly, it was David Pincus who pointed out to me that Multiple Choice suffices for Urysohn's Lemma; it's a small step from there to see that Dependent Multiple Choice also suffices.) – Andreas Blass Jun 22 '13 at 1:05
• This was reposted on MO: mathoverflow.net/questions/137152/… – Martin Sleziak Jul 20 '13 at 13:24