Cantor's diagonal argument meets logic (I'm not normally dealing much with set theory and logic, so excuse me if my choice of words below seems a bit off the traditional terminology.) Where does the following Cantor-inspired argument go wrong?
Let $\Sigma = \{A_0,A_1,A_2,\ldots\}$ be the countable collection of statements with one free variable such that for all $n\ge 0$,
$$
\exists!x_n\in [0,1):A_n(x),
$$
where by $[0,1)$ I mean the interval. ($\Sigma$ is countable, right? Statements must consist of finitely many characters after all.)
Now write $x_n$ in decimals as
$$
x_n =\sum_{k=1}^\infty x_n^{(k)}10^{-k}
$$
where $x_n^{(k)}\in\{0,1,\ldots,9\}$ for all $k\ge 1$ (we make sure never to write e.g. $0.1$ as $0.099999\ldots$). Now put
$$
y^{(k)}=\begin{cases}
1 & \text{if $x_k^{(k)}\neq 1$}\\
2 & \text{else}.
\end{cases}
$$
Unsurprisingly, we put
$$
y:=\sum_{k=1}^\infty y^{(k)}10^{-k}.
$$
Now $y\neq x_n$ for all $n$, just like in Cantor's classical argument. But the above definition of $y\in [0,1)$ should (I think---but this could be where I'm wrong) be possible to formalise in first-order logic. In other words, there exists a statement $A$ such that $y$ is the one and only number in $[0,1)$ such that $A(y)$ is true. Thus $A\in\Sigma$, which is obviously a contradiction.
 A: The statement "can be formalized in first-order logic" is problematic. First-order logic is not just one thing, it is a framework for a lot of things.
You talk about defining an element, so you need to specify the language, the structure and so on. The problem is that you can't quantify over statements, and you have, when you enumerated the statements.
While you can, theoretically, do that within a particular theory (e.g. you can quantify over Godel numbers), the theory needs to have some properties (e.g. the ability to interpret first-order logic internally). And you haven't told us what is the theory.
Even more than just that, if you do manage to have the theory interpret this internally, then you still run into Tarski's theorem which says that the truth is not first-order definable. So you can't quite use a truth predicate for arbitrary formula; so you would have to limit your formulas to a certain class which you can internally define a truth predicate.
If you have done all that, and your theory supports sufficient induction-like arguments, then yes, it is probably doable. But you haven't given us any of the above details.
On the other hand, Cantor's diagonal argument is not in the first-order theory of $\Bbb R$ or any other such structure. It is a set theoretic argument. So it is done in a much broader framework of set theory. This allows us to quantify over sets of real numbers, and preform induction internally to set theory; despite the fact that set theory is a first-order theory.
Why? Because in set theory the sets are the elements of the universe. Much like you can discuss the prime numbers which divide $2^{1379123}-1$ within the theory of arithmetic; you can discuss the subsets of $\Bbb R$ in set theory.
So within set theory, you can formalize all these notions, internally first-order logic, and then talk about this enumeration of formulas and so on, and then define $y$. But this is not done in first-order theory within the structure $[0,1)$. 
