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?
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$.
