A definability paradox for infinite binary sequences Consider the set of infinite binary sequences $\{0,1\}^\omega$. Also consider some finite alphabet $\Sigma$, the set of all finite symbol sequences $\Sigma^{\mathbb{N}}$ that can be made from the elements of $\Sigma$, and some formal language $L\subset\Sigma^{\mathbb{N}}$ consisting of every conceivable definition of a specific binary sequence. As an example, suppose $L$ consists of mathematical definitions in English, and $\Sigma$ would contain the English alphabet, punctuation marks, and mathematical symbols.
Now consider some function $D: L \to \{0,1\}^\omega$ that assigns every definition to a specific infinite binary sequence. Since $L$ is at most countable and $\Sigma$ is finite, we can enumerate every element of $L$ in standard lexicographical order on a (potentially) infinite list, which by extension creates a specific list of elements in $\{0,1\}^\omega$ via $D(L)$. If $L$ is countably infinite, Cantor's diagonal argument would then immediately generate a specific element of $\{0,1\}^\omega$ that is not present within $D(L)$, and is therefore not definable in the formal language described above. Define this specific infinite binary sequence as $\mathfrak{a}$.
THE QUESTION: For a countably infinite $L$, the above two paragraphs consist of a specific definition of $\mathfrak{a}\in \{0,1\}^\omega$ in the English language using punctuation marks and mathematical symbols, and so the above statement should belong to $L$. However, if that was true, $\mathfrak{a}\in D(L)$, which is a contradiction to the diagonal argument presented above. How does one resolve this apparent "paradox"?
POSSIBLE APPROACHES: This is likely a decidability/semantics problem, and presumably has some resolution akin to stating that it is impossible to determine whether or not $\mathfrak{a}$ is definable. It may also be true that $L$ is ill-defined in some way, although I have not seen such concerns brought up in mild variations of this argument applied to other problems (i.e. decidability of 1-ary relations on the natural numbers).
 A: Good question! This is called Richard's paradox, and is closely related to the Berry paradox and to Turing's 1936 paper where he defines Turing machines, the contents of which are also summarized on Wikipedia.
To fix ideas, let's take our formal language $L$ to consist of Turing machines, so that we are describing the computable binary sequences. Then in order to compute the diagonalization we would have to compute an enumeration of the Turing machines $T_n$ which output infinite binary sequences, then compute for each such Turing machine $T_n$ the $n^{th}$ bit it outputs. So the argument implies that this is impossible.
You might respond: wait, but can't we take this Turing machine to be a universal Turing machine? This doesn't work, and for an interesting reason: while a universal Turing machine $U$ is capable of simulating any other Turing machine $T$, while simulating the $n^{th}$ Turing machine $T_n$ to compute the $n^{th}$ bit it outputs, $T_n$ might run forever, so the computation never finishes. In order to rule out this possibility, $U$ has to be able to compute in advance whether a given Turing machine will output at least $n$ bits without running forever (or, if you only want to diagonalize over the sequences outputted by Turing machines which output infinite sequences of bits, $U$ has to be able to compute in advance whether a Turing machine will do this). So what the diagonalization argument implies is that no Turing machine can do this: this is the unsolvability of the halting problem, and this is actually the reason Turing defined Turing machines and the halting problem, in order to carry out this argument (for computable reals rather than computable sequences but the distinction is very minor).
The basic argument is much more general than this, though. For example, if we take $L$ to be Peano arithmetic, then we are discussing the definable-in-PA binary sequences. You can consider a binary sequence to be defined by a sentence $\varphi(n)$ with one free parameter, where the $n^{th}$ bit is $0$ or $1$ depending on whether or not $\varphi(n)$ is false or true. In order to define the diagonalization we would have to define an enumeration $\varphi_n$ of the sentences of Peano arithmetic with one free parameter (which we can do), then determine for each $n$ whether $\varphi_n(n)$ is true or false.
So the diagonalization argument implies that no sentence in Peano arithmetic can do this. This means that no sentence in Peano arithmetic can decide whether sentences of Peano arithmetic are true or false; this is  Tarski's undefinability theorem.
In addition, instead of directly asking whether $\varphi_n(n)$ is true or false we could ask whether it's provable or disprovable in Peano arithmetic. Since it is possible for Peano arithmetic to discuss the provability or disprovability of sentences in Peano arithmetic, the diagonalization argument implies that there exist sentences which cannot be proven or disproven in Peano arithmetic; this is the first incompleteness theorem.
So, in summary: the real problem is that $D$ is not necessarily a (total) function, since some sentences in $L$ may not actually define infinite binary sequences, and the diagonalization argument shows that $L$ cannot fix this problem, meaning that $L$ cannot figure out which sentences in $L$ actually define infinite binary sequences.
