[proofplan] The proof has two halves, each an application of the fixed-point sentence $G$ (constructed prior to the theorem) and the soundness of PA. The first half shows $\mathrm{PA} \not\vdash G$ by assuming provability, deriving that $G$ is true in $\mathbb{N}$ (by soundness), and observing that the content of $G$ asserts its own unprovability — a contradiction. The second half concludes that $G$ is in fact true in $\mathbb{N}$ (because it correctly asserts the unprovable status just established) and then rules out $\mathrm{PA} \vdash \neg G$ by soundness again: PA cannot prove a sentence false in $\mathbb{N}$. The hypothesis consumed throughout is that $\mathbb{N}$ is a model of PA, which guarantees soundness of PA with respect to arithmetic truth. [/proofplan] [step:Fix the diagonal sentence $G = \varphi(N)$ and record its defining equivalence] Let $\mathrm{Prov}_\mathrm{PA}(x, y)$ be the primitive recursive relation "$y$ is a Gödel code of a PA-proof of the formula with Gödel code $x$", and let $\mathrm{Pr}_\mathrm{PA}(x) := \exists y\,\mathrm{Prov}_\mathrm{PA}(x, y)$ be the provability predicate. Using the Diagonal Lemma, fix the sentence $G$ together with its Gödel code $N := \ulcorner G \urcorner$ such that \begin{align*} \mathrm{PA} \vdash G \;\leftrightarrow\; \neg \mathrm{Pr}_\mathrm{PA}(\overline{N}), \end{align*} where $\overline{N}$ is the numeral denoting $N$. Write $\chi(x) := \neg \mathrm{Pr}_\mathrm{PA}(x)$ for the unprovability formula, so that $G \leftrightarrow \chi(\overline{N})$ is a theorem of PA. In particular, because PA is sound with respect to $\mathbb{N}$, the biconditional also holds in $\mathbb{N}$: \begin{align*} \mathbb{N} \models G \;\iff\; \mathbb{N} \models \chi(\overline{N}) \;\iff\; G \text{ is not provable in PA}. \end{align*} [guided] Before proving either non-derivability claim, we record the tool that does all the work: the self-referential sentence $G$ obtained by diagonalisation. The Diagonal Lemma produces, for any formula $\psi(x)$ with a single free variable, a sentence $S$ such that $\mathrm{PA} \vdash S \leftrightarrow \psi(\ulcorner S \urcorner)$. Applied to $\psi(x) := \chi(x) = \neg \mathrm{Pr}_\mathrm{PA}(x)$, it yields the sentence $G$ with Gödel code $N := \ulcorner G \urcorner$ satisfying \begin{align*} \mathrm{PA} \vdash G \;\leftrightarrow\; \chi(\overline{N}) \;=\; \neg \mathrm{Pr}_\mathrm{PA}(\overline{N}). \end{align*} Informally: "$G$ says that $G$ is not provable." Why do we need the equivalence to hold in $\mathbb{N}$ and not merely in PA? Because the theorem statement asserts truth in $\mathbb{N}$, and we will argue about provability via **soundness**: everything PA proves is true in $\mathbb{N}$. Since $\mathrm{PA} \vdash G \leftrightarrow \chi(\overline{N})$, soundness transfers the biconditional to $\mathbb{N}$: \begin{align*} \mathbb{N} \models G \;\iff\; \mathbb{N} \models \chi(\overline{N}). \end{align*} Next, the formula $\mathrm{Pr}_\mathrm{PA}(x)$ is constructed (using the representability of primitive recursive relations in PA) so that for every natural number $n$, \begin{align*} \mathbb{N} \models \mathrm{Pr}_\mathrm{PA}(\overline{n}) \;\iff\; \text{there exists a PA-proof of the formula coded by } n. \end{align*} Therefore $\mathbb{N} \models \chi(\overline{N}) = \neg \mathrm{Pr}_\mathrm{PA}(\overline{N})$ is equivalent to the metamathematical assertion "$G$ has no PA-proof". Combining the two equivalences: \begin{align*} \mathbb{N} \models G \;\iff\; G \text{ is not provable in PA}. \tag{$\ast$} \end{align*} This is the single fact we will exploit in both halves of the proof. [/guided] [/step] [step:Show $\mathrm{PA} \not\vdash G$ by invoking soundness to derive a contradiction] Suppose for contradiction that $\mathrm{PA} \vdash G$. Because $\mathbb{N}$ is a model of PA, PA is sound with respect to $\mathbb{N}$, so every PA-theorem is true in $\mathbb{N}$. Hence $\mathbb{N} \models G$. By the equivalence established in the previous step, \begin{align*} \mathbb{N} \models G \;\iff\; G \text{ is not provable in PA}, \end{align*} so $G$ is not provable in PA, contradicting the supposition $\mathrm{PA} \vdash G$. Therefore $\mathrm{PA} \not\vdash G$. [guided] We argue by contradiction. Suppose $\mathrm{PA} \vdash G$. We want to produce an explicit contradiction using the soundness of PA. **Soundness of PA.** A formal system $T$ is sound with respect to a structure $M$ iff every $T$-theorem is true in $M$. To verify soundness of PA with respect to $\mathbb{N}$, observe that $\mathbb{N}$ is a model of PA — every axiom of PA (the usual axioms for $0$, successor, addition, multiplication, and the induction schema) is satisfied in $\mathbb{N}$. By the [Soundness Theorem](/theorems/1453) of first-order logic, if $\mathrm{PA} \vdash \varphi$ then $M \models \varphi$ for every model $M$ of PA. Taking $M = \mathbb{N}$, we conclude: $\mathrm{PA} \vdash \varphi \implies \mathbb{N} \models \varphi$ for every sentence $\varphi$. Applying soundness to our assumed theorem $G$: \begin{align*} \mathrm{PA} \vdash G \;\implies\; \mathbb{N} \models G. \end{align*} Now invoke the equivalence ($\ast$) from the previous step: \begin{align*} \mathbb{N} \models G \;\iff\; G \text{ is not provable in PA}. \end{align*} The left-hand side is true, hence so is the right: $G$ is not provable in PA. But this directly contradicts the hypothesis $\mathrm{PA} \vdash G$. Why does the argument work? The informal content of $G$ is "I am not provable." If PA proves $G$, then $G$ is true (by soundness), so what $G$ says is the case — namely, $G$ is not provable. Formalisation of this intuition is precisely the deduction above. The only ingredient beyond the construction of $G$ is soundness of PA with respect to $\mathbb{N}$, which holds because $\mathbb{N} \models \mathrm{PA}$. Hence $\mathrm{PA} \not\vdash G$. [/guided] [/step] [step:Conclude $G$ is true in $\mathbb{N}$ from its own unprovability] By the previous step, $G$ is not provable in PA. Applying the equivalence ($\ast$) in the direction \begin{align*} G \text{ is not provable in PA} \;\implies\; \mathbb{N} \models G, \end{align*} we obtain $\mathbb{N} \models G$. Thus $G$ is true in the standard model. [guided] Having established that $G$ is not provable in PA, we read off its truth value in $\mathbb{N}$ directly from what $G$ "says." Recall equivalence ($\ast$): \begin{align*} \mathbb{N} \models G \;\iff\; G \text{ is not provable in PA}. \end{align*} We have just proved the right-hand side is true. Therefore the left-hand side is true: $\mathbb{N} \models G$. This step is short but conceptually striking. It exhibits a sentence of arithmetic — $G$ — that is true (in the intended structure $\mathbb{N}$) but not derivable in PA. The existence of such a sentence is the core content of incompleteness. The remaining step rules out the symmetric possibility $\mathrm{PA} \vdash \neg G$, which would also yield incompleteness but in a weaker sense (inconsistency rather than genuine gap). [/guided] [/step] [step:Show $\mathrm{PA} \not\vdash \neg G$ via soundness applied to a false sentence] Suppose for contradiction that $\mathrm{PA} \vdash \neg G$. By soundness of PA with respect to $\mathbb{N}$, every PA-theorem is true in $\mathbb{N}$, so $\mathbb{N} \models \neg G$. By the standard semantics of negation, $\mathbb{N} \models \neg G$ iff $\mathbb{N} \not\models G$. But in the previous step we established $\mathbb{N} \models G$. These two facts are contradictory. Hence $\mathrm{PA} \not\vdash \neg G$. [guided] Again we argue by contradiction. Suppose $\mathrm{PA} \vdash \neg G$. We aim to contradict the truth of $G$ in $\mathbb{N}$ established in the previous step. As in the second step, apply soundness of PA with respect to $\mathbb{N}$: \begin{align*} \mathrm{PA} \vdash \neg G \;\implies\; \mathbb{N} \models \neg G. \end{align*} By the semantics of negation in first-order logic, \begin{align*} \mathbb{N} \models \neg G \;\iff\; \mathbb{N} \not\models G. \end{align*} Therefore $\mathbb{N} \not\models G$. But the previous step gave $\mathbb{N} \models G$. The sentence $G$ cannot both hold and fail in the same structure, so we have a contradiction. Note which hypothesis powers this step. We do **not** need the diagonal equivalence or any specific property of the formula $G$ beyond its already-established truth in $\mathbb{N}$. What we use is soundness: PA cannot prove a sentence that is false in $\mathbb{N}$. So once we know $G$ is true in $\mathbb{N}$, we automatically know $\neg G$ is false in $\mathbb{N}$, and false sentences are not PA-theorems. Hence $\mathrm{PA} \not\vdash \neg G$. [/guided] [/step] [step:Assemble the three conclusions into the theorem] From the second step, $\mathrm{PA} \not\vdash G$; from the fourth step, $\mathrm{PA} \not\vdash \neg G$; and from the third step, $\mathbb{N} \models G$. Thus $G$ is a sentence of the language of arithmetic that is neither provable nor refutable in PA, yet true in $\mathbb{N}$. This is exactly the statement of the theorem, completing the proof. [/step]