Does this proof of Godel's incompleteness theorem rely on soundness?

Question

The proof of Godel's first incompleteness theorem is often paraphrased like this. First, find a sentence $\phi$ which is true exactly if it is not provable. If $\phi$ is false, it must be provable, meaning that it must be true. This is a contradiction. On the other hand, if it $\phi$ is provable, then it must be true, which means that is is not provable, also a contradiction.

In this version of the argument, it is assumed that any sentence that is provable is also true. This seems like some version of soundness. I know that Godel's proof assumes the consistency of the theory $T$ capable of doing arithmetic. Is soundness an additional assumption that must be made, or is it proven as a part of Godel's argument? I know that this is not soundness in the sense of a sound proof system, but maybe it's related? I am worried that the version of the proof I paraphrased also might be conflating provability in $T$, or $T\vdash \phi$ with the provability predicate holding for $\phi$, or $T\vdash \textrm{Pr}(\lceil \phi \rceil)$.

Thanks!

Edit: I learned that the kind of soundness I am referring to is called arithmetical soundness, which means that theorems proven by $T$ are true of the standard model of the natural numbers.

Answer 1

It is true that the incompleteness theorem ultimately requires no extra hypotheses: Rosser improved Godel's original argument to show that (in modern phrasing) any consistent computably axiomatizable first-order theory interpreting $\mathsf{Q}$ is incomplete.

However, the specific argument you sketch in the OP

find a sentence $\phi$ which is true exactly if it is not provable. If $\phi$ is false, it must be provable, meaning that it must be true. This is a contradiction. On the other hand, if it $\phi$ is provable, then it must be true, which means that is is not provable, also a contradiction.

(which can be made fully rigorous) does require soundness. Specifically, we can show that $T\not\vdash\phi$ without any soundness hypothesis (if $T\vdash\phi$ then $T\vdash \mathsf{Prov}_T\phi$ but we also have $T\vdash\phi\leftrightarrow\neg\mathsf{Prov}_T\phi$ so that would give a contradiction), but showing that $T\not\vdash\neg\phi$ requires $\Sigma_1$-soundness: think about a theory like $\mathsf{PA+\neg Con(PA)}$.

---

It's worth noting that there are other natural arguments which require even more soundness. For example, consider the following (I think due to Kotlarski?) which takes us to the two-quantifier level:

Let $f(e)$ be $1+$ the value of the $e$th $T$-provably total recursive function on input $e$. Then $f$ is total recursive, but not $T$-provably total recursive. So "$f$ is total recursive" is a true sentence not provable in $T$.

Answer 2

Godel’s Incompleteness Theorem does not assume soundness or consistency, but states that there is no consistent, recursive, and complete theory of arithmetic. Or: if we have a consistent and recursive set of axioms, then they are not complete.

So why is it called just the Incompleteness Theorem? It’s because we really want consistency and recursiveness, but completeness is ‘merely nice to have’. So, in some sense you are right: once we do assume consistency and recursiveness, then incompleteness follows.

Answer 3

In order to prove that consistency alone suffices, Rosser needed to construct a different sentence than Gödel's.

There's a nice proof from just the standard minimal assumptions (consistent, recursively axiomatizable, extends Robinson arithmetic), that doesn't use Rosser's trick, but uses a bit more computability theory and doesn't give an explicit undecidable sentence:

1. Assume for the sake of contradiction that $T$ is a complete, consistent, recursively axiomatizable theory extending Robinson arithmetic.
2. A recursively axiomatizable, complete and consistent theory is recursively decidable, since one can enumerate all possible proofs and wait for a proof of either $\phi$ or $\lnot\phi.$ Furthermore, any recursively decidable relation is representable in Robinson arithmetic and thus in $T$. Thus there is an arithmetical predicate $F(v)$ such that $T\vdash F(\mathbf n)$ if $n$ is the number of a sentence provable in $T$ and $T\vdash \lnot F(\mathbf n)$ if $n$ is the number of a sentence not provable in $T.$
3. Use the diagonalization lemma to find a sentence $\varphi$ such that $T\vdash \varphi\leftrightarrow \lnot F(\ulcorner \varphi \urcorner).$ If $\varphi$ is provable in $T$ then so is $F(\ulcorner \varphi \urcorner)$ (by representation) and so is $\lnot F(\ulcorner \varphi \urcorner)$ (by equivalence), which is impossible since $T$ is consistent. On the other hand if, $\varphi$ is not provable, then $\lnot F(\ulcorner \varphi \urcorner)$ is provable (by representation), so $\varphi$ is provable (by equiavalence)... an outright contradiction.