Arithmoquine function in Gödel's proof

Question

Could someone explain as detailed as possible how the Arithmoquine{a,a'} function works or is the defined in Gödel's proof of the incompleteness theorem?

To describe my question better...

In this video after 9:30 there is a definition of an Arithmoquine function, I didn't really understood it very well, could someone more knowledgeable explain it in more details?

Answer 1

The ARITHMOQUINE function is defined with the $Subst$ function.

See Gödel Numbering for a similar function:

$subst(x,y)=z$

and its use in The Diagonalization Lemma.

In a nutshell, via the Arithmetization of syntax we are able to associate to every symbol, and thus to every formula (as a sequence of symbols) a number, its G-number, and this in an algorithmic way; i.e. for every formula we can compute its G-number and we can "unpack" a G-number to recover the corersponding formula.

Thus, given a formula $A(x)$ with free variable $x$, we can compute its G-number $\ulcorner A(x) \urcorner$ and given a numeral $\underline n$, i.e. a term of the language of arithmetic "naming" the number $n$, we can compute its G-number $\ulcorner \underline n \urcorner$.

The function :

$subst(x, y) = z$

is a mathematical operation which maps the pair with the Gödel number of a formula with one free variable and the Gödel number of a numeral to the Gödel number of the closed formula which results from the original formula when the given numeral is substituted for the free variable:

$subst(\ulcorner A(x) \urcorner, \ulcorner \underline n \urcorner) = \ulcorner A(\underline n) \urcorner$.

In other words, the function ARITHMOQUINE compute the G-number corresponding to the sentence obtained from the formula $A(x)$ when the term "naming" the number $n$ is substituted into $A(x)$ in place of the free variable $x$.

---

Example: we can consider the formula $x= \underline 0$ and the term $S(\underline 0)$ "naming" the number $1$. The result of the substitution is the sentence:

$S(\underline 0) = \underline 0$.