Gödelの不動点補題
主張
$ v_0のみを自由変項とする任意の論理式$ \Phi(v_0)に対し，次を満たす文$ \sigmaが存在する．
$ \mathsf{PA} \vdash \sigma \leftrightarrow \Phi(\overline{\ulcorner \sigma \urcorner})
また，$ \Phi(v_0)が$ \Sigma_n論理式なら$ \sigmaは$ \Sigma_n文であり，$ \Pi_n論理式なら$ \sigmaは$ \Pi_n文である．
注意
証明
1. 次の$ \mathsf{f}:\N^2 \to \Nは原始再帰関数である．
$ \mathsf{f}(a,b) = \ulcorner \varphi_a(\overline{b}) \urcorner
$ aが$ v_0のみを自由変項とする論理式$ \varphi_a(v_0)のGödel数であるとき，すなわち，$ a = \ulcorner \varphi_a(v_0) \urcorner
$ \mathsf{f}(a,b) = 0
2. $ \mathsf{f}を表す関数記号$ fを$ \sf{PA}の言語$ \mathscr{L}_\mathsf{PA}に追加する．
3. $ \gamma(v_0) \equiv \Phi(f(v_0,v_0))とする．
4. 定義より，$ \mathsf{f}(\ulcorner \gamma(v_0) \urcorner,\ulcorner \gamma(v_0) \urcorner) = \ulcorner \gamma(\overline{\ulcorner \gamma(v_0) \urcorner}) \urcorner
5. 4より，$ \mathsf{PA} \vdash f\left(\overline{\ulcorner \gamma(v_0) \urcorner}, \overline{\ulcorner \gamma(v_0) \urcorner}\right) = \overline{\ulcorner \gamma(\overline{\ulcorner \gamma(v_0) \urcorner}) \urcorner}
6. 等号に関する公理より，$ \mathsf{PA} \vdash \Phi\left(f\left(\overline{\ulcorner \gamma(v_0) \urcorner}, \overline{\ulcorner \gamma(v_0) \urcorner}\right)\right) \leftrightarrow \Phi\left(\overline{\ulcorner \gamma(\overline{\ulcorner \gamma(v_0) \urcorner}) \urcorner} \right)
7. ところで，定義より$ \Phi\left(f\left(\overline{\ulcorner \gamma(v_0) \urcorner}, \overline{\ulcorner \gamma(v_0) \urcorner}\right)\right) \equiv \gamma \left( \overline{\ulcorner \gamma(v_0) \urcorner} \right)である．
8. 文$ \Psi \equiv \Phi\left(f\left(\overline{\ulcorner \gamma(v_0) \urcorner}, \overline{\ulcorner \gamma(v_0) \urcorner}\right)\right) \equiv \gamma \left( \overline{\ulcorner \gamma(v_0) \urcorner} \right)とおく．
9. $ \Psiを使って6を書き換えると，$ \mathsf{PA} \vdash \Psi \leftrightarrow \Phi(\overline{\ulcorner \Psi \urcorner})が得られる．❏ 帰結
$ \lnot \mathrm{Pr}(x) \equiv \lnot\exists_y\mathrm{Proof}(x,y)についてこの定理を当てはめると
$ xをGödel数とする論理式$ \varphi_xについての証明のGödel数$ yは存在しない，すなわち，$ \varphi_xは証明できない． $ \mathsf{PA} \vdash G \leftrightarrow \lnot\mathrm{Pr}(\overline{\ulcorner G \urcorner})
その他
が，証明を追えば明らかとは言え対角線論法を用いている感覚が定理を利用するときは実感がわかないので，このプロジェクトでは不動点補題として呼ぶ．
不動点補題と書くとどの？となるので，一応Gödelのと付けておいた．が，この補題がGödelに帰するものなのかは知らない．