Sign up ×
MathOverflow is a question and answer site for professional mathematicians. It's 100% free, no registration required.

Does Gödel's diagonal lemma follow from Kleene's recursion theorem? I believe the converse is true, by an argument like the following.

Let e ↦ θe be a bijection between ω and the set of Σ01 formulas in the language of arithmetic having just the variable v0 free.

Let e ↦ We be a numbering of the r.e. subsets of ω such that for all e, We = {n ∈ ω : θe(n) is true}. This is possible because every r.e. set is defined in the standard model of arithmetic by a Σ01 formula.

Let f be any recursive operation on ω. To prove the recursion theorem, we seek a number d such that Wd = Wf(d).

Toward that, let φ(v0, v1) be a Σ01 formula satisfied by a pair (n, e) iff θf(e)(n) is true. For instance, φ might be

Σ01-Tr[ Sub(numeral(v0), 0, f(v1)) ]

so that φ(n, e) says that a true Σ01 sentence results from substituting the numeral for n into the formula with code f(e).

By the diagonal lemma, there is a Σ01 formula θd(v0) such that

∀v0[ θd(v0) ↔ φ(v0, d) ]

is provable in Robinson's arithmetic. Hence

Wd = {n ∈ ω : θd(n) is true} = {n ∈ ω : φ(n,d) is true} = {n ∈ ω : θf(d)(n) is true} = Wf(d)

as desired. The second equality follows by choice of θd.

My question is whether we can prove the diagonal lemma from the recursion theorem. For specificity, here is the lemma I have in mind:

For any formula φ(v0, v1, … vn) in the language of arithmetic, one can find a formula ψ(v1, … vn) in that language, so that Robinson's arithmetic proves ∀φv1…∀φvn[ ψ(v1, … vn) ↔ φ(⌜ψ⌝, v1, … vn) ].

Note that it is not sufficient to prove that for each φ there is a ψ for which the stated equivalence holds; the equivalence must be provable in Robinson's arithmetic.

share|cite|improve this question
You may have already seen this, but in section 5 of the paper below, the "one-formula-at-a-time" version of the Diagonal Lemma is derived from Kleene's (Second) Recursion Theorem: Kleene's amazing Second Recursion Theorem, by Yiannis N. Moschovakis, Bulletin of Symbolic Logic, June 2010, pages 189 — 239, an online copy of which is available at –  Ali Enayat Jul 15 '11 at 21:56
Thanks, Ali. I was unaware of that paper, and will take a look. –  Cole Leahy Jul 15 '11 at 22:09

Your Answer


By posting your answer, you agree to the privacy policy and terms of service.

Browse other questions tagged or ask your own question.