I'm trying to reconstruct the proof of Godel's first theorem (Rosser's strong version) from the uncomputability of the Halting function. If we just started with the language $\mathcal{L}=\{0, S, +, \cdot\}$ and we took Robinson arithmetic $Q$, we could show $Q$ is incomplete in the following way: Let $U$ be a Turing Machine that takes as input a pair $\langle M,x\rangle$ where $M$ is a TM. With some work we can show that $U$ can write down an $\mathcal{L}$-formula $\phi_{M,x}(t)$, such that if we took the standard model $\mathbb{N}$ of $Q$ and $n\in\mathbb{N}$, $\mathbb{N}\models\phi_{M,x}(n)$ if and only if $M$ halts in at most $n$ steps on input $x$. This works because each computation step, which at most flips one bit, can be treated as an arithmetic operation on the string. From there it's easy to show $Q$ must be incomplete, otherwise we could ask $U$ to enumerate all strings until it encountered a proof or disproof of $\exists t\phi_{M,x}(t)$.

More generally, this construction should hold in any consistent recursively axiomatizable theory $T$ over any language $\mathcal{L}$ (where $\mathcal{L}$ is finite since the TM only takes finite alphabets), as long as we can get the Turing Machine $U$ to write down an $\mathcal{L}$-formula $\phi_{M,x}(t)$, such that there is some model $\mathcal{M}$ of $T$ where, for $m\in\mathcal{M}$, $\mathcal{M}\models\phi_{M,x}(m)$ if and only $m$ is a natural number and $M$ halts on input $x$ in at most $m$ steps. So the theory $T$ should be such that there is enough arithmetic that there is a model $\mathcal{M}$ of $T$ which has $\mathbb{N}$ as a definable substructure (so that $T$ knows what a “natural number” is) and such that the interpretation the formula $\phi_{M,x}(t)$ in $\mathcal{M}$ is "$t\in\mathbb{N}$ and $M$ halts on $x$ in at most $t$ steps". But what does this mean in a general case where we have some language which may not contain arithmetic symbols?

For example, if you just took the language $\mathcal{L}=\{\in\}$, you could write down the sentence “There is a minimal inductive set $\mathbb{N}$ and there are subsets $+,\cdot\subseteq\mathbb{N}^3$ satisfying Robinson arithmetic", and then in some model of ZFC the sentence “There is a minimal inductive set $\mathbb{N}$ and there are subsets $+,\cdot\subseteq\mathbb{N}^3$ satisfying Robinson arithmetic and there exists an $n\in\mathbb{N}$ such that $\phi_{M,x}(n)$” would be true if and only if $M$ halted on input $x$, which is what we want. But in general, what is the formal, general way to state the condition that $T$ is a r.a $\mathcal{L}$-theory that has “enough arithmetic” that we can interpret the formula $\phi_{M,x}(t)$ in the correct way in some model of $T$?

write down the sentence “There is, where does that sentence finish? $\endgroup$ – David Roberts Apr 1 '14 at 6:53Godel's incompleteness theorems(Oxford - 1992). $\endgroup$ – Mauro ALLEGRANZA Apr 1 '14 at 12:24