The function $z(x)$ that associates to each formula $\alpha$ of $P$ its Gödel number $z(\alpha)$ is external to the system. How then can expressions in which $z(x)$ be involved be expressed in $P$? For example: how to express $\alpha(z(\alpha))$ in $P$, when $P$ doesn't know anything about $z(\alpha)$?. How to express in $P$ that $z(\alpha)$ is the Gödel number of $\alpha$, when $z(x)$ is something defined a posteriori?. There may, indeed, be a formula in $P$ that represents the relation "x is not a proof of $\alpha(z(\alpha))$", but this relation is defined outside the system and it is not possible "express" it in $P$. Gödel's second incompleteness theorem is based on the fact that it is possible to formalize the demonstration the first one in $P$. Is this formalization possible?
1 Answer
Yes, for the reasons you mention, it is important to define your Gödel coding in such a way that the syntactic operations you want to undertake with assertions in the language are indeed expressible in the theory. Otherwise, you are right, the theory will know nothing of the syntactic coding. (And indeed there are bad codings, which lack this expressibility feature.)
Fortunately, it is possible to define the coding so that the syntactic operations on the codes are available inside the theory. Peano arithmetic, for example, has a robust manner of arithmetizing finite sequences of numbers, and one can use that to produce codes of formulas in such a way that we can express all the basic syntactic operations, involving parse trees, substitution, provability, and so forth, using only the codes. One declares that certain numbers will represent variable symbols, and others the logical symbols, and so forth, and so the numbers representing suitable sequences of those symbols can be recognized as codes of formulas, if indeed they are the result of a valid parsing construction. All this can be represented in the theory by a detailed use of sequences, which are expressible in the theory.
In this way, we can express that one number is the code of the formula obtained by conjunction of the formulas represented by two other codes. We can express that a number is the code of a proof of a certain assertion whose code is another given number. And so on.
When someone refers to Gödel coding, they always intend that all these basic syntactic features are internally expressible in this way.
People sometimes say that one of Gödel's profound insights was the realization that arithmetization is possible. How remarkable that with only basic arithmetic, using only the language of addition and multiplication, with quantifiers and logical connectives, we can express assertions that make statements about what kind of statements there are and whether they are provable. Ultimately, with the fixed-point lemma, we can even form self-referential statements in this purely arithmetic language, statements that refer to their own nonprovability. It is incredible.
