I have not heard the expression "double diagonalization". But I think I can explain how the Godel sentence is not provable (assuming that the axioms are all true of the natural numbers).
Let's call a formula having one free variable, a "property". For example, "x+x=x*x" is a property. You can think of a property as an infinite vector of values, each value being either "true" or "false". So for example, "x+x=x*x" is the infinite vector [itex][true, false, true, false, false, false, false, ...][/itex], because it's true when [itex]x=0[/itex], false when [itex]x=1[/itex], true when [itex]x=2[/itex], and false for every other nonnegative integer.
Now, imagine listing all possible properties definable in the language of arithmetic. You can think of this as an infinite two-dimensional matrix [itex]T(n,m)[/itex], where entry number [itex](n,m)[/itex] is "true" if property number [itex]n[/itex] holds for value [itex]m[/itex].
For Godel's purposes, we are interested in what's provable, rather than what's true. So let [itex]H(n,m)[/itex] be the two-place predicate meaning "It is provable that property number n holds of value number m". So [itex]H[/itex] is a different infinite two-dimensional matrix, except that element number [itex](n,m)[/itex] is only true if the corresponding element of matrix [itex]T[/itex] is provable. Note that there are two possible differences between [itex]H[/itex] and [itex]T[/itex]. Something could be true, but not provable. Or something could be provable, but not true (if your axioms are wrong, for instance).
Here's where the diagonalization comes in: If you think of [itex]H[/itex] as an infinite two-dimensional matrix, then the "diagonal" of the matrix consists of the elements with label [itex](n,n)[/itex]. So let [itex]D(x)[/itex] be the property "H(x,x)". [itex]D(n)[/itex] is true if and only if it is provable that value number [itex]n[/itex] holds of property number [itex]n[/itex]. So for example, if property number 27 is "x+2=29", then substituting 27 in for "x" in property number 27 results in a provably true statement, "27+2=29". So in that case, [itex]D(27)[/itex] would be true.
The next twist is to negate [itex]D(x)[/itex]. Let [itex]G_0(x)[/itex] be the formula [itex]\neg D(x)[/itex]. This is yet another property. If property number [itex]42[/itex] is "x+1=2", then substituting [itex]42[/itex] for [itex]x[/itex] in property number 42 is the statement [itex]42 + 1 = 2[/itex], which is false. Presumably, we've constructed our axioms so that you can't prove false statements, so there should be no proof of this statement. So [itex]D(42)[/itex] is false. Since [itex]G_0(42)[/itex] is the negation, then [itex]G_0(42)[/itex] will be true.
The final twist is to note that [itex]G_0[/itex] is itself a property definable in arithmetic, so it has a number, say 2017 (it would probably be much, much larger). Now, let's look at the statement [itex]G \equiv G_0(2017)[/itex].
Now, [itex]G[/itex] is some statement of arithmetic. Is it true? Well, let's unravel it. If it's true, that means that [itex]G_0(2017)[/itex] is true, but by definition of [itex]G_0[/itex], that means that [itex]D(2017)[/itex] is false (since [itex]G_0[/itex] is the negation of [itex]D[/itex]). But look at the definition of [itex]D[/itex]: [itex]D(2017)[/itex] is true if it is provable that property number 2017 holds of value number 2017. But property number 2017 is [itex]G_0[/itex]. So [itex]D(2017)[/itex] is true if it is provable that [itex]G_0(2017)[/itex] holds. Since [itex]G_0[/itex] is the negation of [itex]D[/itex], we have:
[itex]G_0(2017)[/itex] is true if it is
not provable that [itex]G_0(2017)[/itex] holds. So in terms of [itex]G \equiv G_0(2017)[/itex]:
[itex]G[/itex] is true if and only if [itex]G[/itex] is not provable.
So there are two possibilities:
- [itex]G[/itex] is true, and it is not provable.
- [itex]G[/itex] is false, and it is provable.
If our axioms are sound (they don't allow us to prove anything false), then possibility number 2 is ruled out, so the conclusion is that [itex]G[/itex] is not provable.