Assume we know the following for a fact: $L$ is an arithmetic language and contains a formula (abbreviated “$BB(x_i, x_j)$”) expressing the Busy Beaver function, i.e. $BB(k, n)$ is true if and only if the productivity of the most productive (one-symbol) Turing Machine with $k$ states or fewer is $n$.
Prove Gödel's Incompleteness Theorem.
My attempt:
For the sake of contradiction, let $M$ be a Turing machine that decides the truth of sentences of $L$. Then by the fact above, we can use $M$'s program to construct a Turing machine $M^B$ that computes the Busy Beaver function. But the latter is not computable. Contradiction.
Now the question is how do we construct $M^B$?