冪乗のある一階算術の中でGödelの不完全性定理を最初から全部証明する
趣旨
ただし，考えるのは弱い体系である冪乗のある一階算術の中でとする．
冪乗を考えることが出来ると素数の$ n乗というのが扱うことが出来て結果的にGödel数の計算が楽になるからである
実は冪乗を取って普通の一階算術にするのはそんなに苦ではないことが知られている
本当か？
多分，言語に関してはかなり独特な形式化を取っていて，これで最後までうまく行くかどうかは怪しい．
TODO
$ \mathscr{L}の論理式を定義する
$ \mathscr{L}_\mathtt{PAP}上に定められる一階算術の意味論$ \mathscr{N}を定義する
冪乗のある一階算術の言語についての定義の位置をもう少し考える
ここからの目標設定
言語とは何か？なるべくミニマルに設計する．
定義: 言語$ \mathscr{L}
言語$ \mathscr{L}とは，次の2つを持ったシステムであるとする．
記号の集まり（アルファベット）$ \Sigma
項，論理式の構成方法
定義: 言語$ \mathscr{L}のアルファベット$ \Sigmaの制約
$ \Sigmaには次のものを要素に含む．
プライム: $ '
変数記号: $ v
$ nアリティの演算子記号: $ f_n
特に，0アリティの演算子は，定項と呼ばれる．
ただし，無くても良い．
$ nアリティの述語記号: $ P_n
注意: 特に0アリティの述語記号は，その値域が$ \topとか$ \botとかと書かれる．
ただし，無くても良い．
1変数の論理関数: $ \lnot
2変数の論理関数: $ \to
量化子: $ \exists
左カッコ: $ (
右カッコ: $ )
コンマ$ ,
注意: プライム$ 'とは何か？
非形式的には，
プライム$ 'は，変数，演算子，述語記号の後に$ n個つくことで，$ n番目の変数，演算子，述語記号として読むということを表す．
例: 冪乗のある一階算術の言語$ \mathscr{L}_\mathtt{PAP}TODO: これをもう少し後に持っていくあるいは整理する
$ \mathscr{L}_\mathtt{PAP}のアルファベットは，次のように読むことが出来る．
実際に$ \mathscr{L}のアルファベットにこのような記号があるわけではない．
だから単に，読むことが出来る，という形でしか表すことが出来ない．
$ f_0を$ \mathsf{0}として読むことが出来る．
それ以外の$ f_0'などは何としても読めない．
$ f_1(\cdot)を$ \mathbin{s}として読むことが出来る．
それ以外の$ f_1'などは何としても読めない．
$ f_2(\cdot,\cdot)を$ \cdot + \cdot，$ f_2'(\cdot,\cdot)を$ \cdot \times \cdot，$ f_2''(\cdot,\cdot)を$ \cdot^\cdotとして読むことが出来る．
$ \cdotには後で言うように普通は項や論理式が入る．（単に記号列が入ることもある）
$ +,\timesは中置記法という方法で読んだほうが普通は自然である．
それ以外の$ f_2'''などは何としても読まない．
$ P_0と$ P_1は何としても読むことは出来ない．
$ P_2(\cdot,\cdot)を$ \cdot = \cdot，$ P_2'(\cdot,\cdot)を$ \cdot \leq \cdotとして読むことが出来る．
同様に，$ =,\leqは中置記法という方法で更に直して読んだほうが普通は自然である．
それ以外の$ P_2'などは何としても読めない．
定義: Gödel数 TODO: Gödel数の定義は別に言語に関して特に関係がないので移す 言語$ \mathscr{L}のアルファベット$ \Sigmaを並べた記号の列を$ \sigma_1\sigma_2\cdots\sigma_nと表す．
0文字を含めた$ \mathscr{L}のアルファベット$ \Sigmaの記号列の全ての集合を$ \Sigma^*とする．
$ \Sigma^*の要素の数は高々可算無限である．
0文字の記号列は$ \varepsilonと表すことにする．
次のような関数$ \xi:\Sigma^* \mapsto \Nを考える．$ \Nは自然数である．
0文字の記号列$ \varepsilonに対しては，$ \xi(\varepsilon) = 0
1文字の記号列，すなわち$ \Sigmaの要素に対しては次のように$ \xiの値を定める
$ \xi\lbrack\lnot\rbrack=1
$ \xi\lbrack\to\rbrack=2
$ \xi\lbrack\exists\rbrack=3
$ \xi\lbrack(\rbrack= 4
$ \xi\lbrack)\rbrack = 5
$ \xi\lbrack,\rbrack = 6
$ \xi\lbrack\prime\rbrack = 7
$ \xi\lbrack v\rbrack = 8
$ \xi\lbrack f_n\rbrack = 10+2n
$ \xi\lbrack P_n\rbrack = 11+2n
$ 9は？それは後に明らかになる
2文字以上の記号列の場合，$ \xi\lbrack\sigma_1\sigma_2\cdots\sigma_n\rbrackとすると
$ i番目の素数を$ p_iとして
$ \xi\lbrack\sigma_1\sigma_2\cdots\sigma_n\rbrack = \prod^n_{i = 1} p_i^{\xi(\sigma_i)}とする．
明らかに，$ \xiは単射だが全射ではない．
たとえば，
ある言語$ \mathscr{L}及び$ \mathscr{L}のアルファベット$ \Sigmaについて，$ P_1 \notin \Sigmaなら，$ \xi\lbrack\sigma_1\cdots\sigma_n\rbrack=2^{13} \cdot 3^{4} \cdot 5^5となるような$ \Sigmaの記号列$ \sigma_1\cdots\sigma_nは構成できない．
$ \xi\lbrack P_1\rbrack = 13だが，そのような$ P^1がないと言っているので．
例: $ \mathscr{L}_\mathtt{PAP}のGödel数について
$ \mathscr{L}_\mathtt{PAP}のアルファベット$ \Sigmaには$ f_0,f_1,f_2,P_2 \in \Sigmaなので，
$ \xi\lbrack f_0\rbrack = 10，$ \xi\lbrack f_1\rbrack = 12，$ \xi\lbrack f_2\rbrack = 14，$ \xi\lbrack P_2\rbrack := 15である．
記号列$ \mathop{\to}\mathop{\to}\mathop{\lnot}は
$ \mathscr{L}_\mathtt{PAP}では（というかどこでも）$ \mathop{\to}\mathop{\to}\mathop{\lnot}と読める．（特に読み替える必要はない．）
$ \xi\lbrack\mathop{\to}\mathop{\to}\mathop{\lnot}\rbrack = 2^2 \cdot 3^2 \cdot 5^1である．
記号列$ f_1(f_1(f_0))は
$ \mathscr{L}_\mathtt{PAP}では$ ss\mathsf{0}と読み変えることが出来る．
更に，$ s\mathsf{0}を$ \mathsf{1}，$ s\mathsf{1}を$ \mathsf{2}とする省略記法を導入すると$ \mathsf{2}とも読む事が出来る．
$ \xi\left\lbrack f_1(f_1(f_0)) \right\rbrack = 2^{12} \cdot 3^{4} \cdot 5^{12} \cdot 7^{4} \cdot 11^{10} \cdot 13^{5} \cdot 17^{5}である．
先程の読み替えを使えば，$ \xi\lbrack \mathsf{2} \rbrack = 2^{12} \cdot 3^{4} \cdot 5^{12} \cdot 7^{4} \cdot 11^{10} \cdot 13^{5} \cdot 17^{5}である．
記号列$ P_2(f_1(f_1(f_1(f_0))), f_2(f_1(f_0),f_1(f_1(f_0))))は
$ \mathscr{L}_\mathtt{PAP}では$ sss\mathsf{0} = s\mathsf{0} + ss\mathsf{0}と読み変えることが出来る．
先程に続いて，$ s\mathsf{2}を$ \mathsf{3}とする省略記法を導入すると$ \mathsf{3} = \mathsf{1}+\mathsf{2}とも読むことが出来る．
ここからの目標設定
ここまでは，$ \mathscr{L}のアルファベット$ \Sigmaの部分にだけ着目してきた．
次は，記号列集合$ \Sigma^*の要素の中でも特に意味のある記号列である項と論理式について，その構成方法について説明する．
定義: 言語$ \mathscr{L}の項
$ \Sigma^*の要素の内，項とは次のように定義される．
1. $ vの後に，0個以上の$ 'が付いて終わる記号列は項である．
このとき，$ v, v', v''は項である．
2. $ \Sigma \in f_0のとき，$ f_0の後に，0個以上かつ$ \mathscr{L}によって決まっている$ f_0に付けて良い最大個数以下の$ 'が付いて終わる記号列は項である．
例: $ \mathscr{L}では$ f_0に最大2個まで$ 'を付けて良いとする．
このとき，$ f_0, f_0', f_0''は項であり，$ f_0''',f_0''''は項ではない．
3. $ 1 \leq nについて$ f_n \in \Sigmaのとき，
$ n個の記号列$ \tau_1から$ \tau_nが項であり，
$ f_nに0個以上かつ$ \mathscr{L}によって決まっている$ f_nに付けて良い最大個数以下の$ 'が付いた記号列$ f_n^{\prime\cdots\prime}に対して
$ f_n^{\prime\dots\prime}(\tau_1,\dots,\tau_n)の形をした記号列は項である．
注意: $ \dots以外の全ての記号（$ nアリティ演算子記号$ f_n，プライム$ '，カッコ$ (, )及びコンマ$ ,）は$ \Sigmaの要素である
例: $ \mathscr{L}では$ f_2には最大1個，$ f_1には最大2個$ 'を付けて良いとする．
$ f_2'(v,v')や$ f_1(f_1'(f_1''(f_0)))は項である．
$ f_2''(v,v'')は項ではない．
4. それ以外は項ではない．
注意: 演算子記号に付けて良い$ 'の個数について
「$ \mathscr{L}によって決まっている，演算子$ f_nに$ 'を付けてよい最大個数」という非常に恣意的に見えるものが現れている．
しかしこれは実はそんなに恣意的ではない．
今までは（というか普通は）この要素をアルファベットの定義側に押し付けていたのである
すなわち通常は，
言語$ \mathscr{L}のアルファベットとして$ nアリティの演算子記号を$ f_1,f_2,\dotsがあるとして，
$ nアリティ演算子記号$ fと項$ \tau_1,\dots,\tau_nに対して$ f(\tau_1,\dots,\tau_n)は項だ
と定義してきたのである．
例: $ \mathscr{L}_\mathtt{PAP}の項について
$ f_0は項である．$ \mathscr{L}_\mathtt{PAP}では$ \mathsf{0}として読む．
$ \mathscr{L}_\mathtt{PAP}では$ f_0に付けてよい$ 'の数は0個だけなので，$ f_0''は$ \mathscr{L}_\mathtt{PAP}では項ではない．
$ f_1は$ \mathscr{L}_\mathtt{PAP}では項ではない．
$ f_1(f_1(f_0))は項である．$ \mathscr{L}_\mathtt{PAP}では$ \mathsf{2}として読む．
$ f_2(f_1(f_0),f_1(f_1(f_0)))は項である．$ \mathscr{L}_\mathtt{PAP}では$ \mathsf{1}+\mathsf{2}として読む．
$ \mathscr{L}_\mathtt{PAP}では$ f_2に付けて良い$ 'は2個以下である．よって，$ f_2''(f_1(f_1(f_0)),f_2(f_1(f_0),f_1(f_1(f_0))))は項である．$ \mathscr{L}_\mathtt{PAP}では$ \mathsf{2}^\mathsf{1+2}として読む．
観察: 項とは結局何なのか？
まだ意味を定めていないから実際には意味は無い，
しかし，見て分かるように$ \mathscr{L}_\mathtt{PAP}の項は何らかの自然数あるいはその加算/乗算/冪算として読める．
項に対して我々が普段行っているそれらの演算の意味を与えることで，$ \mathscr{L}_\mathtt{PAP}の項は何らかの自然数の値を表すものへと解釈されるのだろうと察せられる．
ここで，$ \mathscr{L}_\mathtt{PAP}の項$ \mathsf{2}のGödel数が$ \xi \left\lbrack \mathsf{2} \right\rbrack = 2^{11} \cdot 3^{4} \cdot 5^{11} \cdot 7^{4} \cdot 11^{9} \cdot 13^{5} \cdot 17^{5}であったことを思い出すと，
Gödel数が$ 2^{12} \cdot 3^{4} \cdot 5^{12} \cdot 7^{4} \cdot 11^{10} \cdot 13^{5} \cdot 17^{5}であるような$ \mathscr{L}_\mathtt{PAP}の記号列とは$ \mathsf{2}という項である．
ということが言える．$ \mathscr{L}_\mathtt{PAP}の上に更に意味を適切に定めることで，
Gödel数が$ 2^{12} \cdot 3^{4} \cdot 5^{12} \cdot 7^{4} \cdot 11^{10} \cdot 13^{5} \cdot 17^{5}であるような$ \mathscr{L}_\mathtt{PAP}の記号列が意味するものは2という値である．
定義: 言語$ \mathscr{L}の論理式
定義: Gödel数の論理式列についての拡張
論理式の列$ \varphi_1 \rightsquigarrow \varphi_2 \rightsquigarrow \cdots \rightsquigarrow \varphi_nのGödel数は次のように定める．
$ i番目の素数を$ p_iとして
$ \xi\left\lbrack \varphi_1 \rightsquigarrow \varphi_2 \rightsquigarrow \cdots \rightsquigarrow \varphi_n \right\rbrack = \prod^n_{i = 1} p_i^{\xi\left\lbrack \varphi_i \right\rbrack }とする．