I wanted to talk about the characterization of metrizable spaces among the topological spaces. The Nagata-Smirnov metrization Theorem states that a space is metrizable if and only if it is regular and has a countably locally finite basis. So a few definitions are in order:
Let X be a topological space.
A family Ω of subsets of X is said to be locally finite if and only if every point of X has a neighborhood that intersects only finitely many sets of Ω.
A family Ω of subsets of X is siad to be countably locally finite if and only if it is a countable union of locally finite families of subsets of X.
The beautiful thing is that a regular space with a countably locally finite basis is normal, and moreover there is a way of assigning to each pair of disjoint closed sets a pair of disjoint neighborhoods of them; that is there exists a function φ that takes a pair of disjoint closed sets (A,B) and returns a pair of disjoint neighborhoods of them φ(A,B). Such a function exists for any normal space provided we use the axiom of choice. However, in our case we don't need to use choice. This implies that Urysohn's Lemma holds for our space without even having to use the axiom of dependant choice. In fact, we can assign unifomaly to each pair of disjoint closed sets a continuous function that vanishes on one of them and equals 1 on the other. Following the proof of the Nagata-Smirnov Metrization theorem, we see that one direction is provable in ZF. Specifically it is provable in ZF that a regular space with a countably locally finite basis is metrizable. However the other direction uses full choice. I am not sure about the exact strength of the other direction; that is, every metric space has a countably locally finite basis. I know that it is related to the Stone's paracompactness theorem. Here is exactly what I know:
Stone's theorem implies that every metric space has a countably locally finite basis(Assuming countable choice)
Every metric space has a countably locally finite basis implies Stone's theorem(Assuming full choice)
Stone's theorem is independent of ZF.
Specifically about 3, there is a model of ZF in which dependent choice holds and Stone's theorem fails. But this doesn't say much about whether that Every metric space has a countably locally finite basis is independent or not of ZF. So if you know of any paper establishing such results please let me know. The image shows the paper where I found the independent result.
