http://en.wikipedia.org/wiki/Definable_number A definable number is one that satisfies a formula of the form: "There exists a unique x such that P(x)" for some logical formula P. This Wikipedia article asserts that the definable numbers are countable, because the set of all logical formulae is countable. (fine) Then, it continues by concluding that most real numbers are not definable, because the real numbers are uncountable. (...) It strikes me that there is a problem with this paragraph -- in particular, the measure of countability is coming from two different theories! (Compare to Skolem's paradox) The second statement: "the real numbers are uncountable" is fine -- it's proven straightforwardly by Cantor's diagonal argument, and isn't really questionable. In particular, though, it's a theorem of some particular theory. (Say, second-order ZF) The first statement: "the set of all logical formulae is countable" is also fine -- it's proven straightforwardly by induction on the complexity of the formulae. However, this is not a theorem within the same theory! To continue with the example, this statement could be made as a theorem in second-order ZF about the possible first-order formulae of ZF. Or, it might be a theorem of some external theory (say, third-order ZF?) about the possible second-order formulae of ZF. But, it cannot be a theorem of second-order ZF about the possible second-order formulae of ZF! (can it?) Now, it's a familiar fact that measuring sets in different theories leads to conflicting results -- Skolem's paradox. So, I'm entirely unconvinced by the argument given in Wikipedia that most real numbers are not definable. But wait, there's more! Today at work, I was thinking about the axioms of ZF. If we extend the notion of a definable number to that of a definable set, in the obvious way, it seems to me that you would not be able to prove the existance of a set that was not definable! In particular, I conjecture that there does not exist a formula P(x) in ZF for which you can prove: There exists an x such that P(x) but such that no definable number satisfies P. The same goes for ZFC, if you replace the axiom of choice with an actual function that selects particular choice functions! (But that would seem to go against the spirit of this exercise...) Does anyone out there have any further insight they can contribute?