証明のGödel数
証明$ \mathcal{P}とは論理式の列である．
以下$ \mathcal{P} \coloneqq \varphi_0,\varphi_1,\dots,\varphi_{n-1}とする．
定義
Cantorの対関数$ \mathrm{pair}(x,y) \coloneqq \frac{(x+y)(x+y+1)}{2} + x $ \mathrm{1st}(z) \coloneqq \mu_x.\left( \exists_{y < z+1}.(z=\mathrm{pair}(x,y)) \right)
$ \mathrm{2nd}(z) \coloneqq \mu_y.\left( \exists_{x < z+1}.(z=\mathrm{pair}(x,y)) \right)
補題.1
自然数の任意の有限列$ x_0,x_1,\dots,x_{n-1}に対し，
証明$ \mathcal{P}に対して次を満たす自然数$ eを一意に取ることが出来る．
$ \mathrm{decode}(e,0) = \ulcorner \varphi_0 \urcorner
$ \mathrm{decode}(e,1) = \ulcorner \varphi_0 \urcorner
$ \vdots
$ \mathrm{decode}(e,n-1) = \ulcorner \varphi_{n-1} \urcorner