Hello can someone explain me exacty how in this fragment of the paper (SELF-REFERENCE AND THE LANGUAGES OF ARITHMETIC, RICHARDG.HECK,JR.):

  • (9) Tr(x) ≡∃y(rhs(x,y)∧¬Tr(y)), where rhs(x,y) is a formula representing the relation: y is (Gödel number of) the right-hand side of the biconditional (whose Gödel number is) x. Diagonalization then yields a formula G such that PAs (Paeno arithmetic , 's' stands for standard language)


  • (10) G≡[Tr(G)≡∃y(rhs(G,y)∧¬Tr(y))], where, as usual, G abbreviates the numeral denoting the Gödel number of the formula G.

How (10) can be derived from (9) trough Diagonalization?

  • See e.g. Gödel’s Incompleteness Theorems. – Mauro ALLEGRANZA Oct 30 '19 at 13:33
  • I don't see how following the steps of the "diagonalization lemma" referenced there takes one from (9) to (10) – Noname Oct 30 '19 at 13:40
  • But then G in (10) must be equivalent to (9) , how then in (10) is it equivalent to the right-hand side of the equivalence(10)? – Noname Oct 30 '19 at 13:54

See e.g. Gödel’s Incompleteness Theorems : Diagonalization: it is a general result of FOL that :

Let A(x) be an arbitrary formula of the language of F with only one free variable. Then a sentence D can be mechanically constructed such that F ⊢ D ≡ A(⌈D⌉).

In Heck's paper, page 2, the author applies this general result to formula (9) above (of system PA), which is of "form" A(x) [variable y is bound].

Thus, there is a sentence (closed formula) G such that : PA ⊢ G ≡ A(⌈G⌉), i.e. a formula G such that PA proves:

G ≡ [T (⌈G⌉) ≡ ∃y(rhs(⌈G⌉, y)∧¬T (y))].

| improve this answer | |
  • Thanks, altough this: G ≡ [T (G) ≡ ∃y(rhs(G, y)∧¬T (y))]. Supposed to be --> G ≡ [T (⌈G⌉) ≡ ∃y(rhs(⌈G⌉,y)∧¬T (y))]. – Noname Oct 30 '19 at 14:43

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.