> Since there are only a countable number of formulas, there are only countably many definable reals

It always seemed like it should matter that the constructable formula strings include strings that define multiple numbers (e.g. "three; also pi squared") which at least seems like it should be aleph one rather than aleph nought, but smarter people than me assure me it doesn't work that way for (reasons)