An implication for the real numbers given decidability on formal systems . A friend and I were looking through Peter Smith's book, An Introduction to Godel's Theorem, when we discovered the following.
Ideally, for an axiomatized system with a language $\mathcal{L}$ (assuming $\mathcal{L}$), we would want that if P is a string, then it is decidable whether $P$ is a valid $\mathcal{L}$-sentence. Or more simply, whether it is an $\mathcal{L}$-wff.
However, a direct consequence of this is that the set of wffs, or sentences, must be effectively enumerable. Which leads to the following bizarre statement.
If $W$ is the set of wffs of a given theory $T$, capable of describing real arithmetic, then as $\mathbb{R}$ is uncountable, and $W$ is countable, there exists $\alpha \in \mathbb{R}$ such that we can never express $\alpha$ as an $\mathcal{L}$-wff.
Is our conclusion correct and if so, is there a stronger version of it?
 A: The discussion in IGT is in the context of working up to a definition of an effectively axiomatized theory (on p. 31 in the second edition); and yes, here we do need, inter alia, for the formal language $\mathcal{L}$ in which the theory is couched to be such that it is effectively decidable what is an $\mathcal{L}$-wff. And yes, the wffs (and sentences) of such a theory will be effectively enumerable. It is theories with such languages to which Gödel's incompleteness theorems can be applicable. And yes, in such a theory, not every real (for example) can get a term denoting it, as the terms will be countable. Not a "bizarre" result but an obvious consequence of the limitation of effectively presented formalized languages (of a kind actually usable-as-a-language-to-think-with by idealised but finite mathematicians). 
Model theorists use an extended notion of languages in which there can be, e.g., a primitive constant for every item in an uncountable domain. And such "languages" are very useful abstract objects to consider in deriving results about effectively axiomatized theories with effectively decidable syntaxes. They are  languages qua abstract objects, which can be themselves the subject of mathematical theories (they are abstract objects to be theorised about), but not languages we can, as it were, completely get our finite heads around (not languages to be theorised in). (As noted in footnote 7 on p. 28 of IGT2).
