User:IssaRice/Computability and logic/Diagonalization lemma: Difference between revisions

Revision as of 02:12, 8 February 2019

Rogers's fixed point theorem

Let $f$ be a total computable function. Then there exists an index $e$ such that $\varphi _{e}\simeq \varphi _{f(e)}$ .

Diagonalization lemma

(semantic version)

Let $A$ be a formula with one free variable. Then there exists a sentence $G$ such that $G$ iff $A(\ulcorner G\urcorner )$ .

Define $\mathrm {diag} (x)$ to be $\ulcorner C(\ulcorner C\urcorner )\urcorner$ where $x=\ulcorner C\urcorner$ . In other words, given a number $x$ , the function $\mathrm {diag}$ finds the formula with that Godel number, then diagonalizes it (i.e. substitutes the Godel number of the formula into the formula itself).

Revision as of 02:10, 8 February 2019 (view source) IssaRice (talk \| contribs) (→‎Diagonalization lemma) ← Older edit		Revision as of 02:12, 8 February 2019 (view source) IssaRice (talk \| contribs) (→‎Diagonalization lemma) Newer edit →
Line 10:		Line 10:
	Let <math>A</math> be a formula with one free variable. Then there exists a sentence <math>G</math> such that <math>G</math> iff <math>A(\ulcorner G\urcorner)</math>.		Let <math>A</math> be a formula with one free variable. Then there exists a sentence <math>G</math> such that <math>G</math> iff <math>A(\ulcorner G\urcorner)</math>.

	Define <math>\mathrm{diag}(x)</math> to be <math>\ulcorner C(\ulcorner C\urcorner)\urcorner</math>, where <math>x = \ulcorner C\urcorner</math>.		Define <math>\mathrm{diag}(x)</math> to be <math>\ulcorner C(\ulcorner C\urcorner)\urcorner</math> where <math>x = \ulcorner C\urcorner</math>. In other words, given a number <math>x</math>, the function <math>\mathrm{diag}</math> finds the formula with that Godel number, then diagonalizes it (i.e. substitutes the Godel number of the formula into the formula itself).