User:IssaRice/Computability and logic/Diagonalization lemma: Difference between revisions
| Line 22: | Line 22: | ||
Let <math>B</math> be <math>A(\mathrm{diag}(x))</math>, and let <math>G</math> be <math>B(\ulcorner B\urcorner)</math>. | Let <math>B</math> be <math>A(\mathrm{diag}(x))</math>, and let <math>G</math> be <math>B(\ulcorner B\urcorner)</math>. | ||
Then <math>G</math> is <math>A(\mathrm{diag}(\ulcorner B\urcorner))</math>. | Then <math>G</math> is <math>A(\mathrm{diag}(\ulcorner B\urcorner))</math>, by substituting <math>x = \ulcorner B\urcorner</math> in the definition of <math>B</math>. | ||
Revision as of 02:40, 8 February 2019
Rogers's fixed point theorem
Let be a total computable function. Then there exists an index such that .
(simplified)
Define (this is actually slightly wrong, but it brings out the analogy better).
Consider the function . This is partial recursive, so for some index .
Now since . This is equivalent to by definition of . Thus, we may take to complete the proof.
Diagonalization lemma
(semantic version)
Let be a formula with one free variable. Then there exists a sentence such that iff .
Define to be where . In other words, given a number , the function finds the formula with that Godel number, then diagonalizes it (i.e. substitutes the Godel number of the formula into the formula itself), then returns the Godel number of the resulting sentence.
Let be , and let be .
Then is , by substituting in the definition of .