Jump to content

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

Page contents not supported in other languages.
From Wikipedia, the free encyclopedia

Gödel numbering

[edit]

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

Symbols

[edit]
0
1
2
3
4
5
6
7
8
9
10
11
12
13
14

Sequences

[edit]

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 : 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

empty sequence,
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 notation.

Recursion

[edit]

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. is regarded as
(here I do deliberately do not use , because I want to illustrate the scheme for a more complicated case)
If using fundamental theorem, it will be aritmethized as
Thus subterms/subformulae are not handled by “subcoding”.


Obsolete section!

[edit]

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.