Lack of reference to $\omega$-consistency in this proof of Gödel first incompleteness theorem

Question

Is $\omega$-consistency assumed in this proof? I understand that this proof is very informal, but then I can't seem to identify the step where $\omega$-consistency is (implicitly) used.

Answer 1

Note the following two passages:

It can be proved that we can define, in terms of set theory, a function $T:\mathbb{N}\rightarrow\{0,1\}$ with the following property: if $n$ is a natural number such that it encodes a theorem then $T(n) = 1$, otherwise $T(n) = 0$.

versus

Hence $T(A(m))=1$ is a theorem. So by the property of function $T$, $A(m)$ is an encoded theorem.

There's a subtle mismatch there, between what is true about $T$ and what is provable about $T$.

Going from "$T(A(m))=1$ is a theorem" to "$A(m)$ is an encoded theorem" uses $\omega$-consistency: while it is true that $T(n)$ is true iff $n$ is an encoded theorem, on what grounds can we claim that $T(n)$ is provable in our theory only if $n$ is an encoded theorem (which is what we need here)?

To do this, we need to assume that the things our theory proves are in fact true - or, at least, some weak version of this statement. This is exactly what $\omega$-consistency does.

Answer 2

It is almost too breezy a retelling to make sense of, but something fishy does seem to happen at the part

Hence $T(A(m))=1$ is a theorem. So by the property of function $T$, $A(m)$ is an encoded theorem.

Here, unless I'm mistaken, the only thing we can conclude without $\omega$-consistency is that the theory under consideration thinks that the string $A(m)$ codes for is a theorem -- but perhaps it's wrong about what the theorems are.

That is, it is conceivable that your set theory is consistent and yet has no models whose integers are standard. (One example where this would be the case is if your favorite set theory happens to be ZFC+"ZFC is inconsistent"). And if that happens, one of the non-standard integers in the model might well be something the model thinks is an encoded proof of something that doesn't actually have any finite proof.