What exactly does $\vdash_T G_T \leftrightarrow \lnot \exists y$ Prf$(\ulcorner G_T \urcorner, y)$ mean?

Question

To me this translates to: $G_T$ is provable in $T$ if and only if there doesn't exist a $y$ such that $y$ is a witness to the provability of $\ulcorner G_T \urcorner$. But I'm not entirely sure what this truly means. My textbook says that it follows from the diagonalization lemma.

What does it mean for something to be provable? And how exactly does the Prf$(\ulcorner G_T \urcorner, y)$ function work?

Any help is truly appreciated.

Answer 1

The formula :

$\vdash_T G_T \leftrightarrow \lnot \exists y$ Prf$(\ulcorner G_T \urcorner, y)$

means :

it is provable in $T$ the equivalence between the sentence $G_T$ and the sentence $\lnot \exists y$ Prf$(\ulcorner G_T \urcorner, y)$ [see also this post].

Assume that we know what is a Formal system like First-order theory of arithmetic based on First-order logic.

If the system $T$ has "certain arithmetical capabilities" (to be specified) we can use them to build up formulae related to the syntactical facts of the theory itself; see Arithmetization of syntax.

One of this formulae is the "proof predicate" Prf; we can define it in $T$ such that Prf$(\ulcorner G_T \urcorner, y)$ holds when $y$ is the "code number" (called Gödel's numeber) of a proof in $T$ of the formula of $T$ whose "code number" is $\ulcorner G_T \urcorner$.

For the details, you need an exposition of Gödel's Incompleteness Theorems; I assume that you can find it in your textbook.

It is usually included in all "major" textbooks, like :

Elliott Mendelson, Introduction to Mathematical Logic (4th ed - 1997)

and :

Herbert Enderton, A Mathematical Introduction to Logic (2nd ed - 2001).

In addition, yu can see this fully-dedicated book : Peter Smith, An Introduction to Gödel's Theorems, Cambridge UP (2nd ed - 2013).