Can the functions in Gödel's Incompleteness proof be expressed as Gödel numbers?

Question

I'm trying to understand the entirety of Gödel's incompleteness theorem, and Gödel's proof.

Going by this English translation Gödel defines 45 functions (relations) which build on each other to make the function of provability, there called $Bew(x)$, which returns a true if $x$ is a provable statement, and false if $x$ is an unprovable statement.

The symbols assigned Gödel numbers are $0, f, ¬, ∨, ∀, (, )$

Can each of the 45 functions actually be encoded as Gödel numbers?

Or are the functions merely manipulation and inspection that we do from the outside to create new Gödel numbers and statements?

My confusion is that many of the symbols in the functions $(\leq, \epsilon, \exists, \cdot, etc)$ are not simple logical statements. Much is made of the primitive recursion of these statements, but nothing is said about how to actually "write them out"

Answer 1

The set $S := \{n \in \mathbb{N} | \hat{n}$ is provable$\}$, where $\hat{n}$ is the proposition with Gödel number $n$, is a recursive set. This means that there exists a partial recursive function $f$ such that $f(n)$ is defined if and only if $n \in S$.

However, $S$ is not a decidable set. There is no total recursive function $f$ such that $f(n) = 0$ iff $n \in S$. This is because the halting problem would be solvable if there were such a total recursive function.

Answer 2

Gödel numbers are assigned to expressions of the language, i.e. to finite strings of basic symbols through the code assigned to the (finite) list of basic symbols of the language: $(, ), \lnot, \lor, \exists, s, 0, +,\ldots$

The basic symbol $+$ has a code, but the sum function: $+(x,y)$ has different codes for every value of the arguments $x$ and $y$.

Thus, we can compute the code of the term $1+0$ as well as the code of the formula $1+0=1$ [i.e. $=(+(s0,0),s0)$]: in both cases the result will be a (very huge) natural number.

What the process of arithmetization can do is to generate codes for expressions (formulas) and sequences of formulas.

The meta-mathematical relations and functions, like e.g. $\text {Fml}, \text {Ax}$ and $\text {Bew}$ are relations about numbers that are expressed by formulas.

Thus, due to the fact that we can prove in $\mathsf {PA}$ the theorem $1+0=1$, we can compute its code $c$ and compute the code $d$ of the corresponding derivation (it is a sequence of formulas) and thus we can assert $\text {Bew}(c,d)$.

There is no a "basic" code for e.g. $\text {Bew}$ because it is not a symbol of the language.

But, the provability predicate $\text {Bew}$ is primitive recursive and the machinery of G's Th is based on the proof the p.r. functions and predicates can be "expressed" in $\mathsf {PA}$ (in fact, $\mathsf Q$ is enough), where:

a two-place numerical relation $R$ is expressed by the open formula $ϕ(x, y)$ with two free variables iff, for any $m, n$, if $m$ has the relation $R$ to $n$ [i.e. $R(m,n)$ holds], then $ϕ(m, n)$ is true, etc.

And also:

The theory $T$ captures the two-place relation $R$ by the open wff $ϕ(x, y)$ iff, for any $m, n$, if $m$ has the relation $R$ to $n$, then $T \vdash ϕ(m, n)$, etc.

In conclusion, $\mathsf {PA}$ captures $\text {Bew}$ and thus we have a formula $ϕ(m, n)$ corresponding to it.

This formula is an expression of the language; thus (in principle) we can compute its code.