Yhyjyk

There is only one problem I have with Goedel's proof as explained in Nagel & Newman's book.

It assumes that you can actually construct a G statement along the lines described in the proof in PM, but as far as I'm aware there is no guarantee that such a G statement can be written down in finitude. In fact, the term denoted by sub(n, 17,n) itself looks like it needs to have a greater Goedel number than sub(n, 17,n), which is by definition the Goedel number of the entire G statement (which implies it's represented by a longer string / formula than the statement it's a part of)! We already know that in order for any formula to have a Goedel number associated with it, it needs to be able to be represented by a finite string of signs!

It appears to me that you would encounter the same problem regardless of what formal system you use. Using the sample PM the authors introduce would get you stuck writing the statement ad infinitum!

Thanks in advance for any help.

edit 1:
The G sentence in the book is defined as: ~(E x) Dem (x, Sub (n, 17, n)) , where n is the g-number of the statement "~(E x) Dem (x, Sub (y, 17, y))" (lets call this A). Therefore G basically means that the statement you obtain by substituting for variable "y" in A is not provable, and since replacing y in A gives you G itself, we understand that G refers to itself. The problem I have is that G by definition has a g-number g = sub (n, 17, n), which is a substring of G. Since representing G would require using both the numeral of Sub( n , 17, n) and some other signs, the resulting statement would have a g-number greater than sub(n, 17, n). (Even the representation of the number sub(n, 17, n) alone in PM has a g-number greater than sub(n, 17, n), just as representing 4 as "ssss0" would have a greater g-number than 4). So, how can we actually write down such a statement?

You are right that there's no reason to believe that we can write down a sentence which includes (the numeral for) its Godel number as a subterm; however, that's not what we actually need to do here.

Below, $T$ is the particular theory we're looking at - e.g. PA - and I write "$underlinen$" for the numeral corresponding to the number $n$.

Before addressing Nagel/Newman's presentation, let me first give a self-contained summary of what we're trying to do; then I'll say exactly what's going on with their exposition in particular.

On the face of it, we might consider a formula $varphi$ to be self-referential if $underlinevarphi$ (or $underlinevarphi(t)$ for some term $t$) occurs in $varphi$ as a term. However, as you correctly observe this is an extremely hard to satisfy property, and perhaps no such formulas exist.

Instead, fixing a given Godel numbering function $mu$, we'll be satisfied with a weaker notion of self-reference:

Fix a formula $varphi$ with one free variable. We say that a sentence $theta$ asserts its own $varphi$-ness via $mu$ if $$Tvdash[thetaiffvarphi(underlinemu(theta))].$$

Note that we do not require $theta$ to literally be the sentence $varphi(underlinemu(theta))$, merely that these two sentences be ($T$-provably) equivalent. Now there is no "size barrier" to self-reference at all; perhaps $theta$ looks nothing like $varphi(underlinemu(theta))$ on the face of it! (And indeed this can happen.)

The choice of $mu$ matters, of course - there's no reason to suspect a priori that sentences which are assert their own $varphi$-ness via $mu$ actually exist. This is where most of the work of Godel's argument comes in: picking a "good enough" map $mu$ and analyzing it appropriately.

Now how is this reflected in Nagel/Newman?

Well, we have a formula in one free variable $y$ (not a sentence; this matters a bit) which I'll abbreviate $H$; it has some Godel number $n$ with corresponding numeral $underlinen$.

Now the expression $G=H(underlinen)$ - by which I mean the string you get by replacing each "$y$" in $H$ by the string $underlinen$ - clearly makes sense. Note that $n$ is fixed before I do this, so there's no self-referentiality shenanigans going on here.

OK, now where do we get self-reference? Well, the resulting sentence $G$ has its own Godel number $k$, and presumably $knot=n$. However, we are nonetheless able to prove that $$Tvdash Giff H(underlinek).$$ Note that the expression $H(underlinek)$ has its own Godel number $j$, which - again - presumably is neither $m$ nor $k$.

So there's no "perfect" self-reference going on, only the weaker "coincidental" version we've described above; but this is enough for our purposes.

EDIT: A lingering question, after all this, is whether "strong" self-reference is possible at all. Note that it's easy to rule out strong self-reference for some specific Godel numberings, but that doesn't mean that there aren't approaches which do allow strong self-reference.

It turns out that this is indeed possible! So that's neat. In my opinion, though, the approach above is more fundamental: the "punchline theorem" is that any Godel numbering method satisfying a list of non-syntactical properties automatically allows weak self-reference, whereas there doesn't seem to be a similarly non-syntactical condition guaranteeing strong self-reference.

Long comment

We have $text sub(a, x, b)$ (where $a$ stands for a formula, $x$ for a variable, and $b$ for a term. The operation output the formula that results from formula $a$ if in $a$ we replace $x$, wherever it is free, by $b$.

Obviously, $text sub(a, x, b)$ is different from $a$.

Consider e.g. as $a$ the formula $(x=0)$ and as the term $b$ the numeral $1$; then $text sub(a, v, b)$ will be $(1=0)$.

We arrive at the formula $lnot text Dem(x, text sub(y, 17, y)).$

It is a formula $Q(x,y)$ with two free vars.

Consider its universal closure $P(x)= forall x Q(x,y)$, i.e. $lnot exists x text Dem(x, text sub(y, 17, y)).$

It is a formula with only one free var : $y$.

This formula has a code (its Godel-number) $p = ulcorner P(y) urcorner$.

Finally, we use the number $p$ and replace the free variables $y$ in the above formula with the said term. We get a new formula $G$ with its own code :

$ulcorner G urcorner = text sub(p, 17, p)$.

The new formual $G$ has no more free variables, because the only free variable $y$ of the formula $P(y)$ has been "filled" withe the number term $p$ (using the corresponding numeral $S(S( ldots (0) ldots)$, i.e. a term with no variables inside).

This process is called diagonalization :

This is the idea of taking a wff $varphi(y)$, and substituting (the numeral for) its own code number in place of the free variable. Think of a code number as a way of referring to a wff. Then the operation of ‘diagonalization’ allows us to form a wff that as it were indirectly refers to itself (refers to itself via the Gödel coding). We will use this trick [...] to form a Gödel sentence that encodes ‘I am unprovable in $mathsfPA$’.

Thus, if formula $Q(x, y)$ above "means" : "$x$ does not prove the formula obtained from the formula with code $y$ by subst of the numeral for $y$ in place of the (only) free variable", we have that $P(x) = forall x Q(x,y)$ means : "for all $x$, $x$ does not prove the formula obtained from the formula with code $y$ by subst of the numeral for $y$ in place of its only free variable".

I.e. $P(x)$ means "the formula ... is unprovable".

This formula has a code $p$; repeat the process and what we get is a sentence $G$ that says...