Talk:Diagonal lemma/Diagonal formula as a representation of a recursive function

Gödel numbering

Let us fix a Gödel numbering for the object language:

Symbols

$\lnot$	0
$\land$	1
$\lor$	2
$\leftarrow$	3
$\rightarrow$	4
$\leftrightarrow$	5
$\forall$	6
$\exists$	7
$=$	8
$\neq$	9
$0$	10
$s$	11
$+$	12
$\cdot$	13
$x_{0}$	14
$x_{i}$	$i+13$

Sequences

Main article: Gödel numbering for sequences

Let us denote sequences of sigs

• using the fundamental theorem of arithmetic, but we may use more sophisticated methods (Chinese remainder theorem)
• let us store also the length of the sequence (e.g. let us store a surplus item of the sequence, which stores the length of the remaining sequence. Here, let us reserve the first (indexed as zeroth) item for this. E.g., if we use fundamental theorem, we use a pattern $2^{n}\cdot p_{1}^{\alpha _{0}}\cdot \dots \cdot p_{n-1}^{\alpha _{n-1}}$: a product of a 2-power (storing the length) and an ecoding of the remaining sequence (using fundamental theorem of artihmetic, of course, 2 is not among its primes). But, as mentioned, there are more advanced tricks for representing length-aware sequences, e.g. using the Chinese remainder theorem and the pairing function in a spohisticated way — see the main article of the section.
• use Polish notation (prefix notation), so that we can avoid using parantheses-like auxiliary signs

If we have already selected an appropriate method for coding/decoding sequences, sometimes, let us hide the details, and denote

$\epsilon$

empty sequence,

$x:s$

the sequence made from x as first token of it and s as the reamining (tail) sequence.

In short, let us use list-like notation (like in modern functional languages). It will be useful if recursion will be discussed.

But in many other cases, we may use also the $\left\langle \dots \right\rangle$ notation.

Recursion

The following two facts can lead to different solutions

Parsing	Evaluating
Terms, formulas are things which are built of subterms/subformulae.	Formulas/terms can be coded by parsing long sequences.
Thus, we may code a term/formula as a short sequence, simply consisting of the number of the functor name/predicate, then the respective codes of its arguments.	Thus, we may code a formula/term as a long sequence where each subterm/subformula are is expanded as an own sequence, and the resulting sequence is simply the appropriate concatenation of all sequences
(maybe accompanied by some auxiliary signs, but it may be avoided if consequent Polish notation has been chosen).
Of course the arguments are also sequences, but they are not expanded in the main sequence.	Thus, the arguments are not boxed in conceptually in a new coding/decoding procedure.
They must be decoded if necessary.	They must be parsed approiariately
E.g. $\forall x_{0}\;sx_{0}\neq 0$ is regarded as
$\left\langle \forall ,x_{0},\lnot ,=,s,x_{0},0\right\rangle$	$\left\langle \forall ,x_{0},\left\langle \lnot ,\left\langle =,\left\langle s,x_{0}\right\rangle ,0\right\rangle \right\rangle \right\rangle$
(here I do deliberately do not use $\neq$, because I want to illustrate the scheme for a more complicated case)
If using fundamental theorem, it will be aritmethized as
$2^{7}\cdot 3^{7}\cdot 5^{14}\cdot 7^{1}\cdot 11^{9}\cdot 13^{11}\cdot 17^{14}\cdot 19^{10}$	$2^{3}\cdot 3^{\forall }\cdot 5^{x_{0}}\cdot 7^{sx_{0}\neq 0}$ $\rightsquigarrow$ $2^{3}\cdot 3^{7}\cdot 5^{14}\cdot 7^{2^{2}\cdot 3^{\lnot }\cdot 5^{sx_{0}=0}}$ $\rightsquigarrow$ $2^{3}\cdot 3^{7}\cdot 5^{14}\cdot 7^{2^{2}\cdot 3^{\lnot }\cdot 5^{2^{3}\cdot 3^{sx_{0}}\cdot 5^{0}}}$ $\rightsquigarrow$ $\dots$
Thus subterms/subformulae are not handled by “subcoding”.

Obsolete section!

$\mathrm {diag} (s,u)=\mathrm {subst} (s,u,s)$

$\mathrm {subst} (\epsilon ,u,s)=\epsilon$

$\mathrm {subst} (x:s,u,q)={\begin{cases}{\mathfrak {R}}_{q}\frown \mathrm {subst} (s,u,q)&x=u+13\\{\mathfrak {R}}_{x}\frown \mathrm {subst} (s,u,q)&x\neq u+13\end{cases}}$

looks lke a good (Haskell-like) definition for what we expect from diagonalization. In fact, we should take care of the scope of variables, and avoid substituion of bound variables.

But how to achieve, that the above Haskell-like definitions can be exressed

• in the realm of recursive functions (a rather asketic world, compared to Haskell)
• and how to represent it ith first-order formulae?

Sequences (again) can be used for this, because sequences can store the path of recursive calls, thus appropriate tricks can solve the problem of recursion.