Gödel Coding

If $\theta$ is a formula of $\mathcal{L}$, the language of arithmetic, its Gödel code will be a number $┌\theta ┐\in \mathbb{N}$. The code map $\theta \mapsto ┌\theta ┐$ is injective.

Coding Symbols:

Assign to the variable $v_i$ the integer $2i+1$. Thus $v_0\mapsto 1,v_1\mapsto 3,v_2\mapsto 5,\dots$

For the other symbols of $\mathcal{L}$,

\neg \mapsto 2, \ \land \mapsto 4, \ \lor \mapsto 6, \ \rightarrow \mapsto 8, \ ( \mapsto 10, \ ) \mapsto 12, \\ \forall \mapsto 14, \ \exists \mapsto 16, \ = \mapsto 18, \ S \mapsto 20, \ + \mapsto 22, \ \cdot \mapsto 24, \ 0 \mapsto 26. \end{gather*}

Let $a^{\#}$ be the integer assigned to the symbol $a$.

Coding Formulas:

To the string of symbols $a_1\dots a_n$ assign the Gödel code/number $┌a_1\dots a_n┐:=p_1^{a_1^{\#}}\cdot \cdots \cdot p_n^{a_n^{\#}},$ where $p_i$ is the $i^{\text{th}}$ prime.

For example, to the formula $\exists v_0(v_0=2)$ which is an abbreviation of $\exists v_0(v_0=SS0)$, assign $┌\exists v_0(v_0=2)┐:=2^{16}\cdot 3^1\cdot 5^{10}\cdot 7^1\cdot 11^{18}\cdot 13^{20}\cdot 17^{20}\cdot 19^{26}\cdot 23^{12}.$ Given a string of symbols, in particular a term or a formula, we can effectively find the associated Gödel code. Conversely, given an integer, we can effectively find whether or not it is the Gödel code of a string of symbols, and if so we can effectively write out this string.

Primitive Recursive Syntactic Relations and Constructions

Likewise the relations $C$ (Concatenation), $N$(Negation), $E_n$, such that C(a,b,c) \text{ iff } a = \ulcorner \varphi \urcorner, \; b = \ulcorner \psi \urcorner, \; c = \ulcorner \varphi \land \psi \urcorner \quad \text{for some formulas } \varphi, \psi, $$$$ N(a,b) \text{ iff } a = \ulcorner \varphi \urcorner, \; b = \ulcorner \neg \varphi \urcorner \quad \text{for some formula } \varphi, $$$$ E_n(a,b) \text{ iff } a = \ulcorner \varphi \urcorner, \; b = \ulcorner \exists v_n \varphi \urcorner \quad \text{for some formula } \varphi, are all primitive recursive.

Also, the relation Sub defined by $\text{Sub}(x,k,y)\text{ iff }x=┌\phi ┐,y=┌\psi ┐,$ and $\psi$ is obtained from $\phi$ by substituting $k$ for each free occurrence of $v$ in $\phi$, is primitive recursive.

The usual sets of formulas (atomic formulas, sentences, etc.) and operations on formulas (forming the conjunction of two formulas etc.), after coding, are clearly computable. Moreover, they are primitive recursive as their validity does not require unbounded search.

One can then check that the set of Gödel codes of terms, of atomic formulas, of all formulas, of formulas with at most $v$ free, of sentences, of $PA$ axioms etc., are primitive recursive

There is similarly a primitive recursive function $f$ whose range is the set of gödel codes of formulas with at most $v$ free.

That is, $f(n)=┌{\phi }_n(v)┐.$ Composing the primitive recursive functions , the binary function $f(n,m)$ defined by $f(n,m):=┌{\phi }_n(m)┐,$ is also primitive recursive. There are actually much more stuff in Hilbert deductive system that we would code.

Coding Proofs

Just as we coded formulas as integers, so we can code finite sequences of formulas, and in particular formal $PA$ proofs, as integers.

If $p$ is a proof from $PA$, then $p$ is a finite sequence of formulas ${\phi }_1,\dots ,{\phi }_k$. Analogously to (7.2), we code $p$ as the integer $[p]$, where $[p]:=p_1^{┌{\phi }_1┐}\cdot \cdots \cdot p_k^{┌{\phi }_k┐}.$ Conversely, given a natural number $y$ one can (in principle) effectively obtain the corresponding proof, denoted by $\lfloor y\rfloor$. Formula coding uses $┌\dots ┐$ and $└\dots ┘$ while proof coding uses $[\dots ]$ and $\lfloor \dots \rfloor$. This is no big deal, we could also use even integers and odd integers for formulas and proofs respectively, or just rely on context!

A particularly significant for us is the relation $\text{Prf}(x,y)$ defined by $\text{Prf}(x,y)\text{iff}x=┌\phi ┐,y=[p],p\text{ is a }PA\text{ proof of }\phi .$ It is primitive recursive by similar arguments to before.

Arithmetic Representation

The relations $f(n),f(n,m)$ discussed above and the relation $\text{Prf}$ are all primitive recursive. Hence by theorem , they can be represented in $PA$ by ${\Sigma }_1$-formulas. In particular, there is a ${\Sigma }_1$-formula $Prf(x,y)$ (which represents $\text{Prf}$) such that for $a,b\in \mathbb{N}$, $\text{Prf}(a,b)⟹PA⊢Prf(a,b),$ $\neg \text{Prf}(a,b)⟹PA⊢\neg Prf(a,b).$

Similarly, the ternary proof relation $\text{Prf}(u,v,y)$, defined by $\text{Prf}(u,v,y)\text{iff}y=[p],p\text{ is a }PA\text{ proof of }{\phi }_u(v),$ is primitive recursive. It follows that we can effectively exhibit a ${\Sigma }_1$-formula $Prf(u,v,w)$ in the language $\mathcal{L}$ of number theory, such that $\text{Prf}(m,n,y)⟹PA⊢Prf(m,n,y),$ $\neg \text{Prf}(m,n,y)⟹PA⊢\neg Prf(m,n,y)$. (As usual, the formal $PA$ proofs can be written out by mimicking the calculation of the primitive recursive characteristic function of $\text{Prf}$, which comes in turn from its given primitive recursive definition.)

Provability

Consider the set $\text{Prov}\subseteq \mathbb{N}$ of those $a\in \mathbb{N}$ for which there is a proof of the sentence corresponding to $a$. That is, $a\in \text{Prov}\text{ (that is, }\text{Prov}(a))⟺\exists b\text{ such that }\text{Prf}(a,b).$ (Note that this is a statement in the metalanguage.) "$\text{Prov}$" meaning “provable”. Because of the existential quantifier $\exists$, the set $\text{Prov}$ is not primitive recursive, nor is it computable in the broader sense. However, $\text{Prov}$ is computably enumerable in the following sense: we can write a program which will enumerate all possible proofs, and hence enumerate all sentences which are provable

But one cannot know of an arbitrary sentence $\theta$, how long it will take to be listed if it is indeed provable. As we will see later, for some $\theta$ it will be the case that both $\theta$ and its negation $\neg \theta$ will not be provable from $PA$. There is then no algorithmic procedure which will eventually give a “provability” answer for every input $┌\theta ┐$.

Following the definition of $\text{Prov}$ and introduction of the $\mathcal{L}$-formula $Prf(x,y)$, we define the $\mathcal{L}$-formula $Prov(x)$ by $Prov(x):=\exists yPrf(x,y)$The formula $Prov(x)$ is ${\Sigma }_1$, although it does not correspond to a primitive computable (or even a total computable) function. It asserts there is a $PA$ proof of the sentence with Gödel number $x$. Similarly and importantly, define for $m,n\in \mathbb{N}$ $\text{Prov}(m,n)⟺\exists b\text{ such that }\text{Prf}(m,n,b),$ which is the provability relation meaning, in this case, that there is a formal proof from $PA$ of ${\phi }_m(n)$. Then there is a ${\Sigma }_1$-formula $Prov(u,v)$ defined by $Prov(u,v):=\exists yPrf(u,v,y).$ This is the formula in the language of arithmetic corresponding to there is a $PA$ proof of ${\phi }_u(v)$”. More explicitly it corresponds to there is a $PA$ proof coded up by $y$ of ${\phi }_u(v)$.

We can enumerate all formulas with one variable $v_0$, in a primitive recursive computable manner. Similarly for sentences and proofs. Define Prf(p,n) $(\subset {\mathbb{N}}^2)$ to mean $p$ codes a proof of sentence coded by $n$, i.e Prf(p,n) iff $p$ codes a proof of sentence coded by $n$. Then Prf is primitive recursive relation.

So there is a formula, which we can explicitly find, P(u,v) s.t, $\text{Prf}(p,n)⟺PA⊢P(p,n)$ and $P$ is ${\Sigma }_1$. Define Prov(n) $\subset \mathbb{N}$ $\text{Prove}(v):=\exists u\text{Prof}(u,v)$ $PA⊢\phi ⟹PA⊢\text{Prov}(\phi )$