I'm reading http://www.math.mcgill.ca/rags/JAC/124/GodelsProof.pdf
Near the final pages, they prove it.
Here's the proof as I understand it:
All symbols in the language of arithmetic are given a unique Godel number (which is a whole number)
All formulas in arithmetic are also given a unique Godel number by the method: $2^{a}3^{b}5^{c}7^{d}…..$, where 2,3,5,7… are the primes and $a,b,c,d$ are the Godel numbers of the symbols which appear in the formula in the order of their appearance.
Every proof in arithmetic is given a unique Godel number using the same method, except this time $a,b,c,d….$ are the Godel numbers of the formulas which appear in the proof in the order of appearance.
$Dem(x,z)$ is an arithmetic predicate which takes two Godel numbers $x$ and $z$. It is true if the proof corresponding to Godel number $x$ results in the formula (or proves the formula) corresponding to the Godel number $z$.
$sub(y,16,y)$ is an arithmetic function of $y$ (I don't know why two y's are used in the notation). It gives us the Godel number of the formula obtained by replacing all instances of the symbol corresponding to Godel number 16, in the formula corresponding to Godel number $y$, by $y$.
Now we start with the formula:
$$\forall(x), \neg Dem(x,sub(y,16,y))$$
Suppose this formula has Godel number $n$, and $y$ has been assigned Godel number $16$. We substitute $n$ for $y$ to get another formula:
$$\forall(x), \neg Dem(x,sub(n,16,n))$$
By definition of $sub(n,16,n)$, the above formula has Godel number $sub(n,16,n)$, as it has been obtained by replacing $y$ by $n$ in the formula of Godel number $n$
Also, this formula is saying "The formula of Godel number $sub(n,16,n)$ (i.e. the formula itself) is not demonstrable".
Now we prove that this formula is true. We assume that it is false. This means the formula is demonstrable. But that means its negation, which says "The formula is demonstrable", is also demonstrable. Since this is a contradiction, we arrive at the conclusion that the formula is true and undemonstrable. Have I understood this all correctly?
My problem
My problem is with the $Dem$ predicate. Given two Godel numbers $x$ and $z$, how do we calculate the truth value of $Dem(x,z)$?
To do that, we prime factorize $x$, and look at the power of the largest prime factor. If that power is equal to $z$, then that means the formula assigned to $z$ is the last formula (or the final result) in the proof assigned to Godel number $x$. So that means $x$ proves $z$, right?
But this method regards any sequence of formulas, ending in the formula corresponding to Godel number $z$, as a proof of the formula having Godel number $z$. This doesn't take into account any transformation rules of the axioms, whether the proof is logically valid or not. For example, $Dem(z,z)$ would be true by this method and hence every formula would be demonstrable.
Best Answer
Here's the basic idea (as Mauro indicates)
To determine whether the relation Dem(m, n) holds, proceed as follows. First decode m (undo the Gödel numbering). That’s a mechanical exercise. Now ask: is the result a sequence of PA wffs? That’s algorithmically decidable (since it is decidable whether the Gödel number decodes into a string which is a sequence of wffs). If it does decode into a sequence of wffs, ask next: is this sequence a properly constructed PA proof? That’s decidable too (check whether each wff in the sequence is either an axiom or is an immediate consequence of previous wffs by one of the rules of inference of PA’s logical system). If the sequence is a proof, ask: does its final wff have the g.n. n? That’s again decidable. Dem(m, n) holds if the sequence coded by $m$ is a proof of the wff coded by $n$.
(So even if you choose a coding where a sequence of one wff gets the same code as the code for that wff, Dem(n, n) won't be true unless $n$ codes an instance of an axiom.)
Putting all that together, there is a computational procedure for telling whether Dem(m, n) holds. Moreover, at each and every stage, the computation involved is once more a straightforward, bounded procedure that can be done with ‘for’-loops. So Dem will be a primitive recursive relation, expessible in PA.
For more on this, see §39 of Gödel Without (too many) Tears, downloadable from https://www.logicmatters.net/igt/godel-without-tears/ Or even better of course the Gödel book of which those notes are the short version.