Gödel's incompleteness 1: construction of the formula relating Gödel number of proof to Gödel number of proven statement

Question

I'm trying to understand the proof sketch of Gödel's Incompleteness Theorem 1 on Wikipedia (https://en.wikipedia.org/wiki/Proof_sketch_for_G%C3%B6del%27s_first_incompleteness_theorem)

In particular, this proof involves the construction of a formula $PF(x,y)$ which holds in case $x$ is the Gödel number of the proof of the statement which has Gödel number $y$. The author says that $PF(x,y)$ is in fact an arithmetical relation, just as $x + y = 6$ is, though a (much) more complicated one" and that the "detailed construction of the formula $PF$ makes essential use of the assumption that the theory is effective."

What would the detailed construction of the formula $PF$ look like?

I understand that one can translate $x$ into its representation as a sequence of arithmetic sentences, and $y$ into its representation as an arithmetic sentence. I assume that assumption that the theory is recursively enumerable implies an effective procedure for checking whether $F(x)$ proves $F(y)$, but how does this imply a formula for $PF(x,y)$? In particular, my understanding is that $PF(x,y)$ must be a finite-length sentence in the language, with $x$ and $y$ as free variables, however, I do not see the way to construct it.

I can imagine (roughly) trying to construct $PF(x,y)$ as the disjunction of all finite sequences of inference rules applied to $F(x)$ but this is not itself finite, even if the set of inference rules is finite.

Answer 1

We define a predicate $Prfseq_T$ which is satisfied by a number $m$ if $m$ Gödel-numbers a sequence of wffs which satisfies the condition of being a well-formed $T$-proof. We can do that because (A) the property expressed is p.r. because -- in arm-waving terms! -- the business of decoding $m$ and then checking that the finite sequence of wffs satisfies the condition of being a proof can done effectively, without any open-ended searches, assuming $T$ is an primitively recursively axiomatized theory of the usual kind. And (B) we've shown that any p.r. property is expressible in the language of first order arithmetic. (Tech note: For $Prfseq_T$ to be p.r. we need $T$ to be not just effectively axiomatised but for it to be primitively recursively decidable whether an expression is an axiom etc.)

Then define $Prf_T(m,n)$ to hold if $m$ numbers a proof sequence in $T$, and $n$ numbers the last wff in that sequence.

If you want more detail, the textbooks will tell you: but for a gentle version, see in particular Ch 15 in the first edition/Ch. 20 of the second edn. of my Introduction to Gödel's Theorems (which should be in the library)

Answer 2

The key point to be aware of is that the formula that defines an "arithmetical relation" can use quantifiers. So $x+y=6$ does not really represent the complexity that's possible. For example we could have $$ \exists a(2\cdot a=x) $$ for "$x$ is even", or $$ x\ne 1 \land \forall a\forall b(a\cdot b \ne x \lor a=1 \lor b = 1) $$ for "$x$ is prime".

The general form is then something like

$\mathit{PF}(x,y) \equiv{}$ There exists $n<x$ such that the $n$th element of $x$ (viewed as a Gödel number for a sequence) equals $y$, and for each $m\le n$ [the $m$th element of $x$ is an axiom or there exist $m_1,m_2 < m$ such that the $m$th element of $x$ follows from the $m_1$th and $m_2$th elements by a single inference rule].

Of course, this needs a lot of further unfolding to argue that the are arithmetical formulas for picking Gödel numbers apart and checking inference rules, etc.

With modern concepts that were not available to Gödel in 1931, the entire construction of $\mathit{PF}$ can be described as:

1. Define a restricted programming language of "first-order function definitions with primitive recursion".

2. Argue that this language is powerful enough to write a program that recognizes valid proofs. In Gödel's 1931 paper, this argument is partially informal. There are 4½ pages full of terse formal descriptions of more and more complex functions that Gödel asserts can be created using primitive recursion, ending with $PF$, but it is up to the reader to figure out the details of how to create each of them using primitive recursion.

3. Argue that any program in the restricted programming language can be systematically converted to an arithmetical definition. Gödel originally used a higher-order logic inspired by Principia Mathematica where this representation is almost trivial, but later in the 1931 paper he presented an alternative translation into what we now recognize as the first-order language of arithmetic, comprising addition, multiplication, symbols for $0$ and $1$ (or successor), equality, logical operators, and quantifiers. A key idea in the latter translation is to use the $\beta$ function to express quantification over finite sequences of numbers rather than just one number at a time.

The result of these multiple steps is a somewhat unwieldy formula that I daresay nobody wrote down explicitly in the 1930s. Today it is would be a more-or-less routine (if long and tedious) exercise for CS undergraduates to program a computer to create it, but seeing the result is not particularly enlightening.