Tarskiの真理不可能性定理の証明のメモ
参考文献
文部科学省，小学校学習指導要領，第2章第3節，算数
用語について
我々が1個とか2個とか普通に使っている自然数の集合を，普通の自然数$ \mathcal{N}と呼ぶ．
普通の自然数の上では，足し算や掛け算，冪算を普通に行うことが出来る．
例えば，$ 3+4=7や$ 4 \times 3 = 12，$ 2 \uparrow 3 = 8である．
足し算と掛け算については小学一年生や小学二年生の教科書など，冪算は中学生の教科書などを参考のこと．
ここからは言語について考える
定義: 言語
言語$ \mathscr{L}とは以下の要素で構成される．
アルファベット$ \Sigma_\mathscr{L}
記号$ f_0,\dots,f_{n-1},P_0,\dots,P_{n-1}に何個までプライムを付けてよいか？の宣言
定義: アルファベット
言語$ \mathscr{L}のアルファベット$ \Sigma_\mathscr{L}とは次の8個以上の記号のことである．
1. $ '
2. $ v
3. $ f_0,f_1,\dots,f_{n-1}
ただし，ある$ \Sigma_\mathscr{L}のには$ f_2はあるが$ f_1は無い，といったケースも許す．
4. $ P_0,P_1,\dots,P_{n-1}
ただし，ある$ \Sigma_\mathscr{L}のアルファベットには$ P_2はあるが$ P_1は無い，といったケースも許す．
5. $ \mathbin{\lnot}
6. $ \mathbin{\to}
7. $ \exists
8. $ (
9. $ )
10. $ ,
定義: プライムの個数の宣言
言語$ \mathscr{L}のアルファベット$ \Sigma_\mathscr{L}に記号$ f_iが存在するとき
「$ f_iに何個プライムを付けてよいか？」というのは言語$ \mathscr{L}で宣言されていなければならない．
同様に，言語$ \mathscr{L}のアルファベット$ \Sigma_\mathscr{L}に記号$ P_iが存在するとき
「$ P_iに何個プライムを付けてよいか？」というのは言語$ \mathscr{L}で宣言されていなければならない．
定義: $ \mathscr{L}の項
言語$ \mathscr{L}に対し，以下のように定まる記号列は$ \mathscr{L}の項と呼ばれる．
1. $ vの後に任意個の$ 'を付けた記号列$ v^{\overbrace{\prime\dots\prime}^{0 \leq m}}は$ \mathscr{L}の項である．
例 $ vと$ v'と$ v''は$ \mathscr{L}の項である．
特にこれらは$ \mathscr{L}の変項と呼ぶ．
2. $ \Sigma_\mathscr{L}が$ f_0を持っているなら，$ f_0に付けて良いプライムの最大個数までの任意個のプライムを付けた記号列は$ \mathscr{L}の項である．
例
$ \mathscr{L}では$ f_0に2個までのプライムを付けてよいと宣言されているとき，$ f_0と$ f_0'と$ f_0''は$ \mathscr{L}の項である．
$ \mathscr{L}では$ f_0にプライムを付けてはならないと宣言されているとき，$ f_0は（$ f_0だけが）$ \mathscr{L}の項である．
3. 1以上の$ iに対し，$ \Sigma_\mathscr{L}が$ f_iを持っているなら，
$ \tau_0,\cdots,\tau_{i-1}を項，$ mを$ f_iに付けて良いプライムの最大個数とし，
以下のような記号列は$ \mathscr{L}の項である．
$ f_i^{\overbrace{\prime\dots\prime}^{0 \leq m}}(\tau_0,\cdots,\tau_{i-1})
例
$ \mathscr{L}では$ f_2に2個までのプライムを付けて良いと宣言されているとき，項$ \tau_0,\tau_1として，
記号列$ f_2(\tau_1,\tau_2)と$ f_2'(\tau_1,\tau_2)と$ f_2''(\tau_1,\tau_2)は$ \mathscr{L}の項である．
*. 上記以外の定義で$ \mathscr{L}の項であるものは存在しない．
例
$ \mathscr{L}のアルファベット$ \Sigma_\mathscr{L}には$ f_0,f_1,f_2を持ち，次の制約があるとする．
$ f_0にはプライムを付けてはならない．
$ f_1にはプライムを1個付けて良い．
$ f_2にはプライムを2個付けて良い
次の記号列は項である
$ f_0
$ f_1'(f_0)
$ f_2'(f_1'(v''),f_1(f_0))
コンマやカッコも含め，項に現れるものは全て$ \mathscr{L}のアルファベットの構成要素である．
以下，$ \mathscr{L}が明らかなら$ \mathscr{L}の項を略して単に項と呼ぶ．
定義: $ \mathscr{L}の論理式
言語$ \mathscr{L}に対し，以下のように定まる記号列は$ \mathscr{L}の論理式と呼ばれる．
1. $ \Sigma_\mathscr{L}が$ P_0を持っているなら，$ P_0に付けて良いプライムの最大個数までの任意個のプライムを付けた記号列は$ \mathscr{L}の論理式である．
例$ \mathscr{L}では$ P_0に2個までのプライムを付けてよいと宣言されているとき，$ P_0と$ P_0'と$ P_0''は$ \mathscr{L}の項である．
2. 1以上の$ iに対し，$ \Sigma_\mathscr{L}が$ P_iを持っているなら，
$ \tau_0,\cdots,\tau_{i-1}を項，$ mを$ P_iに付けて良いプライムの最大個数とし，
以下のような記号列は$ \mathscr{L}の論理式である．
$ P_i^{\overbrace{\prime\dots\prime}^{0 \leq m}}(\tau_0,\cdots,\tau_{i-1})
例
$ \mathscr{L}では$ P_2に2個までのプライムを付けて良いと宣言されているとき，項$ \tau_0,\tau_1として，
記号列$ P_2(\tau_1,\tau_2)と$ P_2'(\tau_1,\tau_2)と$ P_2''(\tau_1,\tau_2)は$ \mathscr{L}の項である．
3, $ \varphi,\psiが論理式であるとき，記号列$ \lnot\varphiと$ \varphi\to\psiは論理式である．
4. $ \varphiが論理式で$ wが変項であるとき，記号列$ \exists_w \varphiは論理式である．
例$ \varphiが論理式なら$ \exists_{v}\varphiと$ \exists_{v'}\varphiと$ \exists _{v''}\varphiなどは論理式である．
*. 上記以外の定義で$ \mathscr{L}の論理式であるものは存在しない．
以下，$ \mathscr{L}が明らかなら$ \mathscr{L}の論理式を略して単に論理式と呼ぶ．
定義: 言語を問わない略記
以下の略記は$ \mathscr{L}によらず用いて良いものとする．
論理式$ \varphi,\psi，変項$ wに対して
$ \varphi \lor \psiは$ \lnot \varphi \to \psiの略記とする．
$ \varphi \land \psiは$ \lnot(\lnot\varphi \lor \lnot\psi)の略記とする．
$ \varphi \leftrightarrow \psiは$ (\varphi \to \psi) \land (\psi \to \varphi)の略記とする．
$ \forall_w \varphiは$ \lnot \exists_w \lnot \varphiの略記とする．
$ v_mは$ v^{\overbrace{\prime\dots\prime}^{0 \leq m}}の略記とする．
すなわち，$ vに付いているプライムの個数を添字づけている．
定義: $ \mathscr{L}の定項
$ \mathscr{L}の項のうち，変項を含まない項は$ \mathscr{L}の定項と呼ばれる．
ここからは言語$ \mathscr{L}の上の意味論を定める．
定義: 構造
言語$ \mathscr{L}の上の構造$ \mathcal{M}_\mathscr{L}とは次の要素で構成される．このことを$ \mathcal{M}_\mathscr{L} = \lang D,F\rangと表記する．
領域$ D
割り当て$ F
領域
領域$ Dは何かしらの集合とする．
割り当て
割り当て$ Fは$ \Sigma_\mathscr{L}の記号列に対して関数を割り当てる部分写像である．
1. $ \mathscr{L}の記号列$ f_i^{\overbrace{\prime\dots\prime}^{0 \leq m}}に対して関数$ f_i^m:D^i \to Dを割り当てる．
とくに$ i=0のときは何らかの$ d \in Dが割り当てられる．
2. $ \mathscr{L}の記号列$ P_i^{\overbrace{\prime\dots\prime}^{0 \leq m}}に対して関数$ P_i^m:D^i \to \mathbb{B}を割り当てる．
$ \mathbb{B} = \{\top,\bot\}とする．
とくに$ i=0のときはどちらかの$ b \in \mathbb{B}が割り当てられる．
3. それ以外の記号列には何も割り当てない．
定義: 解釈
言語$ \mathscr{L}の上の構造$ \mathcal{M}_\mathscr{L}について，$ \mathcal{M}_\mathscr{L}の上での解釈$ \mathcal{I}_{\mathcal{M}_\mathscr{L}}とは次の要素で構成される．このことを$ \mathcal{I}_\mathscr{L} = \lang \mathcal{M}_\mathscr{L},V\rangと表記する．
$ \mathscr{L}上の構造$ \mathcal{M}_\mathscr{L} = \lang D,F\rang
付値関数$ V
付値
付値$ Vは$ \Sigma_\mathscr{L}の記号列に領域の要素$ d \in Dを割り当てる部分写像である．
変項$ v_iに対して，$ d_{v_i} \in Dを割り当てる．
それ以外の記号列には何も割り当てない．
付値の変異
付値$ Vの$ v_i変異$ V_{\lbrack v_i \to d\rbrack}を次のように定める．ただし$ d \in Dである．
$ V_{\lbrack v_i \to d\rbrack}(v_i) \mapsto d
$ v_i以外の変項$ v \neq v_iに対しては$ V_{\lbrack v_i \to d\rbrack}(v) \mapsto V(v)
それ以外の記号列には何も割り当てない．
解釈の変異
解釈$ \mathcal{I}_{\mathcal{M}_\mathscr{L}} = \lang \mathcal{M}_\mathscr{L},V\rangの$ v_i変異$ \mathcal{I}_{\mathcal{M}_\mathscr{L},\lbrack v_i \to d\rbrack} = \lang \mathcal{M}_\mathscr{L},V_{\lbrack v_i \to d\rbrack}\rangとする．
解釈
$ \mathscr{L}の記号列$ \sigma \in \Sigma_\mathscr{L}^*を$ \mathcal{I}_{\mathcal{M}_\mathscr{L}}で解釈することを$ \llbracket \sigma \rrbracket_\mathcal{I_{\mathcal{M}_\mathscr{L}}}と表記する．
$ \llbracket \sigma \rrbracket_\mathcal{I_{\mathcal{M}_\mathscr{L}}}は以下のように定義される．
ただし$ \mathcal{I}_{\mathcal{M}_\mathscr{L}} = \lang \mathcal{M}_\mathscr{L},V\rangとし，
$ \mathcal{M}_\mathscr{L} = \lang D, F \rangとする．
項の解釈
項$ \tauの解釈$ \llbracket \tau \rrbracket_\mathcal{I_{\mathcal{M}_\mathscr{L}}}
$ \tauが変項$ v_iであるなら，$ \llbracket \tau \rrbracket_\mathcal{I_{\mathcal{M}_\mathscr{L}}} \Rightarrow V(v_i) \in Dとする．
$ \tauが定項$ aであるなら，項の定義の2か3のどちらかであるので，
2. $ \tau = f_0^{\overbrace{\prime\dots\prime}^{0 \leq m}}であるとき，$ \llbracket f_0^{\overbrace{\prime\dots\prime}^{0 \leq m}} \rrbracket_\mathcal{I_{\mathcal{M}_\mathscr{L}}} \Rightarrow F(f_0^{\overbrace{\prime\dots\prime}^{0 \leq m}}) \mapsto f^m_0 \in Dと定める．
3. $ \tau = f_i^{\overbrace{\prime\dots\prime}^{0 \leq m}}(\tau_0,\dots,\tau_{i-1})であるとき，
$ \llbracket f_i^{\overbrace{\prime\dots\prime}^{0 \leq m}}(\tau_0,\dots,\tau_{i-1}) \rrbracket_{\mathcal{I}_{\mathcal{M}_\mathscr{L}}} \Rightarrow F( f_i^{\overbrace{\prime\dots\prime}^{0 \leq m}})(F(\tau_0),\dots,F(\tau_{i-1})) \mapsto f^m_i(F(\tau_0),\dots,F(\tau_i)) \in Dと定める
上記より明らかに，項の解釈は必ず停止して，必ず何らかの領域の要素$ d \in Dとして解釈される．
論理式の解釈
論理式$ \varphiの解釈$ \llbracket \varphi \rrbracket_\mathcal{I_{\mathcal{M}_\mathscr{L}}}
1. $ \varphi = P_0^{\overbrace{\prime\dots\prime}^{0 \leq m}}であるとき，$ \llbracket P_0^{\overbrace{\prime\dots\prime}^{0 \leq m}} \rrbracket_\mathcal{I_{\mathcal{M}_\mathscr{L}}} \Rightarrow F(P_0^{\overbrace{\prime\dots\prime}^{0 \leq m}}) \mapsto P^m_0 \in \mathbb{B}と定める．
2. $ \varphi = P_i^{\overbrace{\prime\dots\prime}^{0 \leq m}}(\tau_0,\dots,\tau_{i-1})であるとき，
$ \llbracket P_i^{\overbrace{\prime\dots\prime}^{0 \leq m}}(\tau_0,\dots,\tau_{i-1}) \rrbracket_{\mathcal{I}_{\mathcal{M}_\mathscr{L}}} \Rightarrow F( P_i^{\overbrace{\prime\dots\prime}^{0 \leq m}})(\llbracket \tau_0 \rrbracket_{\mathcal{I}_{\mathcal{M}_\mathscr{L}}},\dots,\llbracket \tau_{i-1} \rrbracket_{\mathcal{I}_{\mathcal{M}_\mathscr{L}}}) \mapsto P^m_i(d_0,\dots,d_i) \in \mathbb{B}と定める．
3.1. 論理式$ \lnot \varphiについては次のように定める．
$ \llbracket \varphi \rrbracket_{\mathcal{I}_{\mathcal{M}_\mathscr{L}}} \Rightarrow \top$ \implies$ \llbracket \lnot \varphi \rrbracket_{\mathcal{I}_{\mathcal{M}_\mathscr{L}}} \Rightarrow \bot
$ \llbracket \varphi \rrbracket_{\mathcal{I}_{\mathcal{M}_\mathscr{L}}} \Rightarrow \bot$ \implies$ \llbracket \lnot \varphi \rrbracket_{\mathcal{I}_{\mathcal{M}_\mathscr{L}}} \Rightarrow \top
3.2 論理式$ \varphi \to \psiについては次のように定める．
$ \llbracket \varphi \rrbracket_{\mathcal{I}_{\mathcal{M}_\mathscr{L}}} = \topかつ$ \llbracket \psi \rrbracket_{\mathcal{I}_{\mathcal{M}_\mathscr{L}}} \Rightarrow \top$ \implies$ \llbracket \varphi \to \psi \rrbracket_{\mathcal{I}_{\mathcal{M}_\mathscr{L}}} \Rightarrow \top
$ \llbracket \varphi \rrbracket_{\mathcal{I}_{\mathcal{M}_\mathscr{L}}} = \topかつ$ \llbracket \psi \rrbracket_{\mathcal{I}_{\mathcal{M}_\mathscr{L}}} \Rightarrow \bot$ \implies$ \llbracket \varphi \to \psi \rrbracket_{\mathcal{I}_{\mathcal{M}_\mathscr{L}}} \Rightarrow \bot
$ \llbracket \varphi \rrbracket_{\mathcal{I}_{\mathcal{M}_\mathscr{L}}} = \botかつ$ \llbracket \psi \rrbracket_{\mathcal{I}_{\mathcal{M}_\mathscr{L}}} \Rightarrow \top$ \implies$ \llbracket \varphi \to \psi \rrbracket_{\mathcal{I}_{\mathcal{M}_\mathscr{L}}} \Rightarrow \top
$ \llbracket \varphi \rrbracket_{\mathcal{I}_{\mathcal{M}_\mathscr{L}}} = \botかつ$ \llbracket \psi \rrbracket_{\mathcal{I}_{\mathcal{M}_\mathscr{L}}} \Rightarrow \bot$ \implies$ \llbracket \varphi \to \psi \rrbracket_{\mathcal{I}_{\mathcal{M}_\mathscr{L}}} \Rightarrow \top
これで全てのパターンは網羅できている．
4. 論理式$ \exists v_i\varphiについては次のように定める．
$ \llbracket \exists v_i\varphi \rrbracket_{\mathcal{I}_{\mathcal{M}_\mathscr{L}}} \Rightarrow \top$ \iff$ \llbracket \varphi \rrbracket_{\mathcal{I}_{{\mathcal{M}_\mathscr{L}},\lbrack v_i \to d}\rbrack} \Rightarrow \topとなる$ d \in Dが存在する．
逆に，
$ \llbracket \exists v_i\varphi \rrbracket_{\mathcal{I}_{\mathcal{M}_\mathscr{L}}} \Rightarrow \bot
$ \iff$ \llbracket \varphi \rrbracket_{\mathcal{I}_{{\mathcal{M}_\mathscr{L}},\lbrack v_i \to d\rbrack}}\Rightarrow \topとなる$ d \in Dは存在しない．
$ \iff全ての$ d \in Dについて$ \llbracket \varphi \rrbracket_{\mathcal{I}_{{\mathcal{M}_\mathscr{L}},\lbrack v_i \to d}\rbrack} \Rightarrow \bot．
項の解釈とは対照的に，$ \varphiの解釈が必ず停止するかは一般には言えない．
4について$ Dが無限集合だった場合は停止しない．
真，偽，充足
論理式$ \varphiが$ \topとして解釈されることを，$ \varphiは真であるという．
逆に$ \botとして解釈されるなら$ \varphiは偽であるという．
論理式$ \varphiがある解釈$ \mathcal{I}_\mathscr{L}の上で真なら，$ \mathcal{I}_\mathscr{L}は$ \varphiを充足するという．
定義: 論理
論理$ \mathsf{L}とは，言語$ \mathscr{L}_\mathsf{L}とその上に定まる構造$ \mathcal{M}_{\mathscr{L}_\mathsf{L}}の組である．
論理$ \mathsf{L}の言語$ \mathscr{L}_\mathsf{L}のアルファベットを論理$ \mathsf{L}のアルファベット$ \Sigma_\mathsf{L}と呼ぶ．
論理$ \mathsf{L}の言語$ \mathscr{L}上に定まる項と論理式をそれぞれ$ \mathsf{L}の項，$ \mathsf{L}の論理式と呼ぶ．
論理$ \mathsf{L}の言語$ \mathscr{L}上に定まる構造$ \mathcal{M}_{\mathscr{L}_\mathsf{L}}を$ \mathsf{L}の構造$ \mathcal{M}_\mathsf{L}と呼ぶ．
論理$ \mathsf{L}の構造$ \mathcal{M}_\mathsf{L}の領域と対応付けをそれぞれ$ \mathsf{L}の領域$ D_\mathsf{L}，$ \mathsf{L}の対応付け$ F_\mathsf{L}と呼ぶ．
論理$ \mathsf{L}の構造$ \mathcal{M}_\mathsf{L}の上の解釈を$ \lang \mathcal{M}_\mathsf{L}, V \rangを$ \mathsf{L}の解釈$ \mathcal{I}_\mathsf{L}と呼ぶ．
ここからは具体的な論理$ \mathsf{AE}を考える．
定義: 冪乗付き算術
これから定義する論理$ \mathsf{AE}は，冪乗付き算術(Arithmetic with Exponentiantion)と呼ばれる．
定義: 冪乗付きの算術の言語$ \mathscr{L}_\mathsf{AE}
$ \mathscr{L}_\mathsf{AE}は冪乗付き算術の言語と呼ぶ．
$ \mathscr{L}_\mathsf{AE}のアルファベット$ \Sigma_{\mathscr{L}_\mathsf{AE}}は記号$ f_0,f_1,f_2, P_2を含んだ12個の記号であるとする．
また，プライムに関する個数の宣言は以下とする．
$ f_0にはプライムを付けてはならない．
$ f_1にはプライムを付けてはならない．
$ f_2には2個までプライムを付けて良い．
$ P_2には1個までプライムを付けて良い．
略記に関して
非常に煩雑になるため，以下の略記を用いる．$ \tau_0,\tau_1は項，$ \varphiは論理式，$ wは変項．
$ \mathtt{z}は$ f_0の略記．
$ \mathtt{s}(\tau_0)は$ f_1(\tau_0)の略記．
特に，$ \tt 1は$ \tt s(z)，$ \tt 2は$ \tt s(1)，$ \tt 3は$ \tt s(2)のように略記する．
$ (\tau_0 + \tau_1)は$ f_2(\tau_0,\tau_1)の略記．
$ (\tau_0 \times \tau_1)は$ f_2'(\tau_0,\tau_1)の略記．
$ ({\tau_0}\uparrow{\tau_1})は$ f_2''(\tau_0,\tau_1)の略記．
$ (\tau_0 = \tau_1)は$ P_2(\tau_0,\tau_1)の略記．
$ (\tau_0 < \tau_1)は$ P_2(\tau_0,\tau_1)の略記．
$ (\tau_0 \neq \tau_1)は$ \lnot(\tau_0 = \tau_1)の略記．
$ (\tau_0 \leq \tau_1)は$ \tau_0 < \tau_1 \lor \tau_0 = \tau_1の略記．
$ \exists_{w < \tau_0}\varphiは$ \exists_w((w < \tau_0) \land \varphi)の略記．
$ \exists_{w \leq \tau_0}\varphiは$ \exists_w((w \leq \tau_0) \land \varphi)の略記．
$ \forall_{w < \tau_0}\varphiは$ \forall_w((w < \tau_0) \land \varphi)の略記．
$ \forall_{w \leq \tau_0}\varphiは$ \forall_w((w \leq \tau_0) \land \varphi)の略記．
カッコ$ (,)は，常識的な範囲で省略できるとする．
また，読みやすさのため明らかなら変項$ v_0,v_1,v_2,v_3を$ x,y,z,wと表記する．
例
以下は$ \mathscr{L}_\mathsf{AE}の項であり，定項である．
$ \tt 1+2
$ \tt 2 \times 3
$ \tt 2 \uparrow 3
以下は$ \mathscr{L}_\mathsf{AE}の項であるが，定項ではない．
$ \mathtt{4} + v_0
$ \mathtt{2} \uparrow ({\mathtt{3} + v_0})
以下は$ \mathscr{L}_\mathsf{AE}の論理式である．
$ \tt 1 = 0
$ \tt 5 < 3 \times 3
$ \exists_{v_1 < \mathtt{5}}(\mathtt{14} = v_1 \times \mathtt{2} )
メモ
じつは$ \mathsf{AE}の$ P_2のプライムの個数は0個に制限できる．
$ \tau_1 \leq \tau_2は$ \exists_{v_0} (\tau_1 + v_0 = \tau_2)の略記とする．
$ \tau_1 < \tau_2は$ \tau_1 \leq \tau_2 \land \tau_1 \neq \tau_2 の略記とする．
定義: 冪乗付き算術の標準構造
以下のように定義される$ \mathcal{M}_\mathsf{AE}は冪乗付き算術の標準構造と呼ぶ．
$ \mathscr{L}_\mathsf{AE}の構造$ \mathcal{M}_\mathsf{AE} \coloneqq \lang \mathcal{N},F \rangとする．
$ \mathcal{N}は普通の自然数．
$ Fは以下の対応付けとする．
ただし
ここでは$ \mathscr{L}_\mathsf{AE}上の略記$ \mathtt{z},\mathtt{s},+,\times,\uparrow,=,<を
$ \mathtt{z}_{\mathscr{L}_\mathsf{AE}}, \mathtt{s}_{\mathscr{L}_\mathsf{AE}},+_{\mathscr{L}_\mathsf{AE}},\times_{\mathscr{L}_\mathsf{AE}},\uparrow_{\mathscr{L}_\mathsf{AE}},=_{\mathscr{L}_\mathsf{AE}},<_{\mathscr{L}_\mathsf{AE}}と書く，
$ F(\mathtt{z}_{\mathscr{L}_\mathsf{AE}})は$ \mathcal{N}上の普通の自然数$ 0へ，
$ F(\mathtt{s}_{\mathscr{L}_\mathsf{AE}})は$ \mathcal{N}上の普通の後者関数$ \mathsf{succ}へ，
$ F(+_{\mathscr{L}_\mathsf{AE}})は$ \mathcal{N}上の普通の足し算$ +へ，
$ F(\times_{\mathscr{L}_\mathsf{AE}})は$ \mathcal{N}上の普通の掛け算$ +へ．
$ F(\times_{\mathscr{L}_\mathsf{AE}})は$ \mathcal{N}上の普通の冪算$ \uparrowへ．
$ F(=_{\mathscr{L}_\mathsf{AE}})は$ \mathcal{N}上の普通の等号$ =へ．
$ F(<_{\mathscr{L}_\mathsf{AE}})は$ \mathcal{N}上の普通の大小比較$ <へ．
例: 冪乗付き算術の解釈
$ \mathscr{L}_\mathsf{AE}は冪乗付き算術の言語，$ \mathcal{M}_\mathsf{AE}は冪乗付き算術の標準構造であるとする．
任意の解釈$ \mathcal{I}_\mathsf{AE} \coloneqq \lang {\mathcal{M}_\mathsf{AE}}, V \rangについて（すなわち任意の付値関数$ Vについて）
項$ \mathtt{1+2}を$ \mathcal{I}_\mathsf{AE}で解釈$ \llbracket \mathtt{1+2} \rrbracket_{\mathcal{I}_\mathscr{L_\mathsf{AE}}}すると
$ \Rightarrow $ \llbracket \mathtt{s(z)} \rrbracket_{\mathcal{I}_\mathsf{AE}} + \llbracket \mathtt{s(s(z))} \rrbracket_{\mathcal{I}_\mathsf{AE}}
$ \Rightarrow$ \mathsf{succ}\left( \llbracket \mathtt{z} \rrbracket_{\mathcal{I}_\mathsf{AE}} \right) + \mathsf{succ}\left( \llbracket \mathtt{s(z)} \rrbracket_{\mathcal{I}_\mathsf{AE}} \right)
$ \Rightarrow$ \mathsf{succ}(0) + \mathsf{succ}(\mathsf{succ}(0))
$ \mapsto$ 3 \in \mathcal{N}となる．
すなわち，$ \mathsf{AE}の項は適当な解釈$ \mathcal{I}_\mathsf{AE}で普通の自然数$ \mathcal{N}に解釈される．
論理式$ \varphiが$ \exists_{v_1}(v_0 = \mathtt{2} \times v_1)であるとする．
$ \llbracket \exists_{v_1}(v_0 = \mathtt{2} \times v_1) \rrbracket_{\mathcal{I}_\mathsf{AE}} \Rightarrow \top
$ \iff$ \llbracket v_0=\mathtt{2}\times v_1 \rrbracket_{\mathcal{I}_{\mathsf{AE},\lbrack v_1 \to d\rbrack}} \Rightarrow \topとなる$ d \in Dが存在する．
付値$ Vについて，$ V(v_0) \mapsto 8を固定する．
変異$ V_{\lbrack v_1 \to 3 \rbrack}による解釈$ \mathcal{I}_{\mathscr{L_\mathsf{AE}},\lbrack v_1\to 3 \rbrack} \coloneqq \left\lang \mathcal{M}_{\mathscr{L}_\mathsf{AE}}, V_{\lbrack v_1 \to 3 \rbrack} \right\rangは$ v_0=\mathtt{2}\times v_1を充足しない．
実際解釈すると，$ 8 = 2 \times 3となり，これは$ \mathcal{N}の上では偽$ \botとして解釈される．
変異$ V_{\lbrack v_1 \to 4 \rbrack}による解釈$ \mathcal{I}_{\mathsf{AE},\lbrack v_1\to 4 \rbrack} \coloneqq \left\lang \mathcal{M}_{\mathsf{AE}}, V_{\lbrack v_1 \to 4 \rbrack} \right\rangは$ v_0=\mathtt{2}\times v_1を充足する．
実際解釈すると，$ 8 = 2 \times 4となり，これは$ \mathcal{N}の上では真$ \topとして解釈される．
したがって，$ \varphiは$ V(v_0) \mapsto 8が固定された解釈$ \mathcal{I}_\mathsf{AE} = \lang \mathcal{M}_{\mathsf{AE}}, V \rangの上では真である．
同様に，$ V(v_0) \mapsto 2や$ V(v_0) \mapsto 4などに固定された解釈の上でも$ \varphiは真である．
定義: 開論理式
論理$ \mathsf{L}の言語$ \mathscr{L}_\mathsf{L}と構造$ \mathcal{M}_{\mathsf{L}} = \lang D,F\rangについて，
$ \mathscr{L}_\mathsf{L}の論理式中の変項$ v_iに対して，$ v_iへの付値を固定しなければ$ \top,\botとして解釈出来ない論理式は，（$ \mathsf{L}の）開いた論理式または（$ \mathsf{L}の）開論理式という．
また，固定しなければならない変項$ v_iは自由変項と呼ばれる．
より細かく言うときは，「$ \varphiは$ v_iで開いている」ともいう．
例: $ \mathsf{AE}の論理式$ \exists_{v_1}(v_0 = \mathtt{2} \times v_1)は開論理式である．実際，自由変項$ v_0に関して付値を固定しなければ$ \top,\botとして解釈できない．（上の例参照．）
開論理式を閉じる
$ \mathsf{L}の開論理式$ \varphiの自由変項が$ v_iであるとき，
「$ \varphiの解釈は$ v_iをある$ d \in Dに割り当てる付値$ Vを持つことを前提とする」という宣言を，$ \varphi \lbrack v_i \coloneqq d \rbrackという略記で表す．
このことを「開論理式$ \varphiの$ v_iを$ dで閉じる」と言う．
自由変数が2つ以上あるときは，$ v_i,v_j,\dotsとして$ \varphi\lbrack v_i \coloneqq d_i, v_j \coloneqq d_j,\dots\rbrackと略記する．
特に$ \varphiの自由変数が1つで自明であるときは，$ \varphi \lbrack v_i \coloneqq d\rbrackを更に$ \varphi \lbrack d \rbrackと略記する．
カッコは適宜補ってもよいとする．
例:
$ \exists_{v_1}(v_0 = \mathtt{2} \times v_1)は$ \mathsf{AE}の開論理式あったので，
$ \exists_{v_1}(v_0 = \mathtt{2} \times v_1) \lbrack v_0 \coloneqq 8\rbrackと書いて，$ v_0を$ 8で閉じているという．
この論理式の解釈には「$ v_0は$ 8として割り当てる付値を持つことを前提とする」と宣言している，
また，自由変数は$ v_0ただ一つで自明なので，$ \exists_{v_1}(v_0 = \mathtt{2} \times v_1)\lbrack 8 \rbrackとして略記することも出来る．
どこを閉じているのか分かりづらいので，適当にカッコを補って以下のようにしてもよい．
$ (\exists_{v_1}(v_0 = \mathtt{2} \times v_1))\lbrack 8 \rbrack
注意
開論理式を閉じても，元の論理式は書き換わっていないということに注意．
すなわち，
$ (\exists_{v_1}(v_0 = \mathtt{2} \times v_1))\lbrack 8 \rbrackはあくまで解釈するときに$ V(v_0) = 8という制約が付くというだけであり，
解釈される論理式は依然$ \exists_{v_1}(v_0 = \mathtt{2} \times v_1)のままである．
定義: 開論理式による部分集合の言及
$ \mathsf{L}の構造の領域を$ D_\mathsf{L}とする．
$ \mathsf{L}の開論理式が$ n個の自由変数$ v_0,\dots,v_{n-1}について開いているとき，
$ \varphi\lbrack v_0 \coloneqq d_0,\dots,v_{n-1} \coloneqq d_{n-1} \rbrackを真とする$ (d_0,\dots,d_{n-1}) \in D_{\mathsf{L}}^nを全て集めることで，$ D_\mathsf{L}^n上の部分集合を言及することが出来る．
このことを，「部分集合$ P_\mathsf{L} \sube D_\mathsf{L}^nは$ \varphiに言及される」と呼び，$ P_\mathsf{L} \coloneqq \{ (d_0,\dots,d_{n-1}) \mid \varphi\lbrack v_0 \coloneqq d_0,\dots,v_{n-1} \rbrack \}と表す．
$ 2<nのとき部分集合$ P_\mathsf{L} \sube D^n_\mathsf{L}は関係と呼ばれるので，「$ \varphiは関係を定義する」とも呼ぶ．
$ n = 1のときは「$ \varphiは$ D上の性質を定義する」とも呼ぶ．
例:
$ \mathsf{AE}の開論理式$ \varphiが$ \exists_{v_1}(v_0 = \mathtt{2} \times v_1)であるなら，$ \varphiによって言及される集合$ \mathcal{E} \sube \mathcal{N}は $ \mathcal{N}上の偶数の集合に一致する．
すなわち，$ \mathcal{E} \coloneqq \{ n \mid \varphi\lbrack n \rbrack \} = \{0,2,4,6,\dots\}である．
$ \varphiは偶数を定義すると言える．
$ \mathsf{AE}の開論理式$ \varphiが$ v_0 = \mathtt{2} \uparrow v_1であるなら，$ \varphiによって言及される集合$ \mathcal{P} \sube \mathcal{N}^2は$ \{ (0,1),(1,2),(2,4),(4,8),\dots \}に一致する．
定義: 文，文の真偽
論理$ \mathsf{L}の論理式$ \varphiが開論理式ではないとき，$ \varphiは（$ \mathsf{L}の）文という．
文は，必ず真か偽のどちらかに解釈される．
すなわち何も付値を固定しなくても，$ \mathsf{L}の任意の解釈で真か偽のどちらか一方に解釈される．
$ \mathsf{L}の解釈$ \mathcal{I}_1で$ \varphiが真であるなら，別の解釈$ \mathcal{I}_2でも$ \varphiは真である．
逆に$ \mathsf{L}の解釈$ \mathcal{I}_1で$ \varphiが偽であるなら，別の解釈$ \mathcal{I}_2でも$ \varphiは偽である．
これをもって，「文$ \varphiは（$ \mathsf{L}で）真である」や「文$ \varphiは（$ \mathsf{L}で）偽である」という．
例
$ \mathsf{AE}において，
$ \tt 1 = 0は真な文である．
$ \tt 1 = 1は偽な文である．
$ \exists_{v_1}(v_0 = \mathtt{2} \times v_1)は文ではない．$ v_0で開いている．
定義: 条件付き文
論理式に現れる自由変項$ v_0,v_1,\dotsを全て$ d_0,d_1,\dots \in D_\mathsf{L}で閉じた$ \mathsf{L}論理式は（$ \mathsf{L}の$ v_0=d_0,v_1=d_1,\dotsという条件下での）条件付き文であるという．
$ v_0=d_0,v_1=d_1,\dotsという条件下での条件付き文の解釈には「$ v_0,v_1,\dotsをそれぞれ$ d_0,d_1,\dots \in Dに割り当てる付値$ Vを持つ」という制約がつく．
例
$ v_0を$ 8で閉じた論理式$ (\exists_{v_1}(v_0 = \mathtt{2} \times v_1))\lbrack 8 \rbrackは$ \mathsf{AE}での条件付き文である．
この文の解釈には「$ v_0は必ず$ 8として割り当てる付値を持つ」という制約が付いている．
注意
論理$ \mathsf{AE}で言及可能な，自然数$ \mathcal{N}上の関数族と関係族を定義する．
定義: 冪乗付き算術のクラス$ \mathcal{A_E}
関係について
$ 1 \leq mで，$ \mathcal{N}上の関係$ R \sube \mathcal{N}^mが$ \mathsf{AE}の論理式で言及可能なら，関係$ Rは冪乗付き算術のクラス$ \mathcal{A_E}に属するまたは関係$ Rは冪乗付き算術的な関係であるという．
長いので，$ Rは$ \mathcal{A_E}関係であるとも言う．
特に，$ m = 1なら$ Rは$ \mathcal{A_E}集合であるとも言う．
関数について
一般に，$ 0 \leq m，普通の自然数上の関数$ f:\mathcal{N}^{m+1} \to \mathcal{N}と任意の自然数$ n_0,\dots,n_{m},n_{m+1} \in \mathcal{N}について，
$ f(n_0,\dots,n_{m}) = n_m$ \iff R_f(n_0,\dots,n_{m},n_{m+1})が真
となるような関係$ R_f \sube \mathcal{N}^{m+2}は必ず存在する．
今，$ R_fが$ \mathcal{A_E}関係であるなら，関数$ fは冪乗付き算術のクラス$ \mathcal{A_E}に属するまたは関数$ fは冪乗付き算術的であるという．
長いので，$ fは$ \mathcal{A_E}関数であるとも言う．
端的に
ある$ 2 \leq m項関係$ y = f(\vec{x})が$ \mathcal{A_E}関係なら$ m-1項関数$ fは$ \mathcal{A_E}関数である．
系
以下の関係は$ \mathcal{A_E}関係である．
2項関係$ \mathsf{div}(x,y)：「$ xは$ yを割り切る」
証明:$ \exists_{z \leq y}(y = x \times z)で言及可能．
2項関係$ \mathsf{power}_p(x): 「$ xは素数$ pの累乗である」
証明:$ \forall_{z \leq x}((\mathsf{div}(z,x) \land z \neq 1)\to \mathsf{div}(p,z))で言及可能．
自然数$ xと素数$ pについて次のことが成り立つ．
$ xが$ pの累乗である$ \iff$ xの1以外の約数が全て$ pで割り切れる
3項関係$ y = \mathsf{lastpow}_p(x): 「$ xより大きな素数$ pの累乗のうち最小のものと$ yが等しい」
証明: $ x < y \land \mathsf{power}_p(y) \land \lnot\exists_{z \leq y}(x \leq z \land \mathsf{power}_p(x))で言及可能．
例: $ \mathsf{lastpow}_2(17) = 32：$ 17より大きい$ 2の累乗は$ 32である．
定義: 連結
一般の自然数$ \mathcal{N}について定義する．
$ pは素数とする．10進数の自然数$ xを$ p進数の数として書いたときに得られる文字列を$ x_pと書くとする．
例
$ 14_2 = \mathsf{1110}
$ 7_2 = \mathsf{110}
10進数の自然数$ x,yに対して文字列$ x_p,y_pが定まる．
これを連結した文字列$ x_py_pを$ p進数の数として解釈することで得られる10進数の自然数を「$ xと$ yの$ p進数での連結」と呼んで，$ x *_{p} yと表記する．
例
$ 14 *_2 7 = 118
$ 14と$ 7の2進数での文字列は↑で求めたように$ \mathsf{1110}と$ \mathsf{110}なので，連結すると$ \mathsf{1110110}．
$ \mathsf{1110110}は2進数の数として解釈すると$ 118．
連結は左結合であるとする．すなわち，$ x *_p y *_p z = (x *_p y) *_p zである．
系
以下の関係は$ \mathcal{A_E}関係である．
4項関係$ z = x *_p y: 「$ zは$ xと$ yの$ p進数での連結である」
証明: $ z = x \times \mathsf{lastpow}_p(y) + yで言及可能．
ここからは論理$ \mathsf{L}の言語$ \mathscr{L}_\mathsf{L}にだけ着目し，$ \mathscr{L}_\mathsf{L}の記号列に一意な普通の自然数$ n \in \mathcal{N}を割り振ることを考える．
この試みはGödel数化やGödelナンバリングなどと呼び，記号列に割り振られる自然数はGödel数と呼ぶ． 定義: アルファベットのGödel数
言語$ \mathscr{L}_\mathsf{L}のアルファベット$ \Sigma_{\mathscr{L}_\mathsf{L}}の要素に対して，次のように普通の自然数$ n \in \mathcal{N}を割り振る写像$ \ulcorner \cdot \urcorner^\Sigma :\Sigma_{\mathscr{L}_\mathsf{L}} \to \mathcal{N}を定義する．
$ \ulcorner ' \urcorner^\Sigma \coloneqq 1
$ \ulcorner \lnot \urcorner^\Sigma \coloneqq 2
$ \ulcorner \to \urcorner^\Sigma \coloneqq 3
$ \ulcorner \exists \urcorner^\Sigma \coloneqq 4
$ \ulcorner ( \urcorner^\Sigma \coloneqq 5
$ \ulcorner ) \urcorner^\Sigma \coloneqq 6
$ \ulcorner , \urcorner^\Sigma \coloneqq 7
$ \ulcorner v \urcorner^\Sigma \coloneqq 8
$ \ulcorner f_i \urcorner^\Sigma \coloneqq 9+2i
$ \ulcorner P_i \urcorner^\Sigma \coloneqq 10+2i
アルファベットに割り振られた普通の自然数は（アルファベットの）Gödel数と呼ばれる．
定義: 記号列のGödel数
まず，アルファベット$ \Sigma_{\mathscr{L}_\mathsf{L}}の要素$ \sigma_{\mathscr{L}_\mathsf{L}}のうち$ \ulcorner \sigma_{\mathscr{L}_\mathsf{L}} \urcornerの最大値を$ mとする．
$ mより大きい最小の素数を$ pとする．
例$ \mathscr{L}_\mathsf{AE}の$ pは17である．（$ m = \ulcorner P_2 \urcorner = 14．14より大きい最小の素数は17である．）
アルファベットの記号列$ \Sigma_{\mathscr{L}_\mathsf{L}}^*に対して再帰的に普通の自然数$ n \in \mathcal{N}を割り振る写像$ \ulcorner \cdot \urcorner :\Sigma_{\mathscr{L}_\mathsf{L}}^* \to \mathcal{N}を定義する．
アルファベットの各要素$ \sigma_1,\dots,\sigma_{n-1},\sigma_{n} \in \Sigma_{\mathscr{L}_\mathsf{L}}とし，記号列$ \sigma \in \Sigma_{\mathscr{L}_\mathsf{L}}^*とする．
1. $ \sigma = \sigma_0なら，$ \ulcorner \sigma \urcorner = \ulcorner \sigma_0 \urcorner^\Sigma
すなわち1文字の記号列はアルファベットのGödel数として扱う．
2. $ \sigma = \sigma_0\dots\sigma_{n-1}\sigma_{n}なら，$ \ulcorner \sigma \urcorner = \ulcorner\sigma_0\dots\sigma_{n-1} \urcorner \times p + \ulcorner \sigma_0 \urcorner^\Sigma
すなわち$ n文字の記号列なら，前半の$ n-1文字の部分と最後の文字に1分割してGödel数を計算し，足し合わせる．
記号列に割り振られた普通の自然数はGödel数は記号列のGödel数と呼ばれる．
注意: 記号列のGödel数は単射だが全射ではない
記号列のGödel数は単射だが，一般に全射ではない．
すなわち
異なる$ \mathsf{L}の記号列$ \sigma_1 \neq \sigma_2には違うGödel数が割り振られる$ \ulcorner \sigma_1 \urcorner \neq \ulcorner \sigma_2 \urcornerが，
ある自然数$ n \in \mathcal{N}に対して$ \ulcorner \sigma \urcorner = nとなるような$ \mathsf{L}の記号列$ \sigmaが常に存在するとは限らない．
例: $ \mathscr{L}_\mathsf{AE}について
$ \mathscr{L}_\mathsf{AE}について，$ pは17である．
$ \timesは$ f_2'の略記であった．よって
$ \ulcorner \times \urcorner
$ = \ulcorner f_2' \urcorner
$ = \ulcorner f_2 \urcorner \times 17 + \ulcorner ' \urcorner^\Sigma
$ = \ulcorner f_2' \urcorner^\Sigma \times 17 + 1
$ = 222
$ \ulcorner \lnot (0 = 1) \urcorner
$ = \ulcorner \lnot P_2(f_0,f_1(f_0)) \urcorner
$ = 2 \times 17^9 + 14 \times 17^8 + 5 \times 17^7 + 9 \times 17^6 + 7 \times 17^5 + 11 \times 17^4 + 5 \times 17^3 + 9 \times 17^2 + 6 \times 17^1 + 6 \times 17
系
しかし，「$ nは$ \mathsf{L}のある記号列のGödel数である」すなわち「$ nに対応する$ \mathsf{L}の記号列$ \sigma_nが存在する」という関係は$ \mathcal{A_E}関係である．
1項関係$ \mathsf{string}_\mathsf{L}(x):「$ xに対応する$ \mathsf{L}の記号列$ \sigma_nが存在する」は$ \mathcal{A_E}関係である．
証明
まず，$ \Sigma_\mathsf{L}及び$ \ulcorner \cdot \urcorner^{\Sigma_\mathsf{L}}に沿って，
$ x = \mathtt{1} \lor x = \mathtt{2} \lor \cdots \land x = \mathtt{9} \lor x=\mathtt{11} \lor \cdots \lor x=\mathtt{10} \lor x=\mathtt{12} \cdots という論理式を立てる
次に，$ \ulcorner \cdot \urcornerの定義に沿って
$ \exists_y(x = \mathtt{1} \times \mathtt{17} + y) \lor \exists_y(x = \mathtt{2} \times \mathtt{17} + y) \lor \cdots \lor \exists_y(x = \mathtt{9} \times \mathtt{17} + y) \cdots \lor \exists_y(x = \mathtt{10} \times \mathtt{17} + y) \cdots という論理式を立てる．
最後にこれらを$ \lorで繋げば良い．すなわち，$ \mathsf{string}_\mathsf{L}(x)は次の論理式で言及可能．
$ x = \mathtt{1} \lor x = \mathtt{2} \lor \cdots \land x = \mathtt{9} \lor \cdots \lor x=\mathtt{10} \cdots \\ \lor \exists_y(x = \mathtt{1} \times \mathtt{17} + y) \lor \exists_y(x = \mathtt{2} \times \mathtt{17} + y) \lor \cdots \lor \exists_y(x = \mathtt{9} \times \mathtt{17} + y) \cdots \lor \exists_y(x = \mathtt{10} \times \mathtt{17} + y) \cdots
系
$ \mathsf{L}の記号列$ \sigma_1,\sigma_2を繋げた$ \sigma_1\sigma_2のGödel数は
$ \ulcorner \sigma_1 \urcorner *_{p} \mathsf{lastpow}_{p}(\ulcorner \sigma_2 \urcorner ) + \ulcorner \sigma_2 \urcornerで計算出来る．
$ pは 記号列のGödel数のときに定義した素数であるとする．
3項関係$ z=\mathsf{concat}_\mathsf{L}(x,y): 「$ xをGödel数とする$ \mathsf{L}の記号列$ \sigma_xと，$ yをGödel数とする$ \mathsf{L}の記号列$ \sigma_yを連結した$ \mathsf{L}の記号列$ \sigma_x\sigma_yのGödel数は$ zと等しい」は$ \mathcal{A_E}関係である．
証明: TODO
定義: 項，論理式，文のGödel数
論理$ \mathsf{L}の項と論理式および文はもちろん記号列であるので，それらのGödel数を項のGödel数，論理式のGödel数，文のGödel数と呼ぶ．
まずはGödelの不完全性定理と関係が深いTarskiの問題を考える
問題1: Tarskiによる
$ \mathsf{AE}で真な文のGödel数の集合$ \mathcal{T} \sube \mathcal{N}を言及する論理式$ \varphi_\mathcal{T}は構成できるか？
この問題は次のようにも言い換えられる．
$ \mathcal{T} \coloneqq \{ n \mid \varphi_\mathcal{T}\lbrack n \rbrack \}な，自由変数が一つある$ \mathsf{AE}の開論理式$ \varphi_\mathcal{T}は構成できるか？
$ \mathcal{T}は$ \mathcal{A_E}集合か？
定義: 数項と論理式の書き換え
$ \mathsf{AE}で$ n \in \mathcal{N}に解釈される項を$ \overline{n}と表記し，$ nの数項と呼ぶ．
$ \mathsf{AE}の論理式$ \varphiは自由変数$ v_0,v_1,\cdotsを持つ開論理式とする．
任意の$ n_0,n_1,\dots \in \mathcal{N}に対し，$ \varphiの$ v_0,v_1,\cdotsを数項$ \overline{n_0},\overline{n_1},\dotsに書き換えて文にした論理式を$ \varphi_{\lbrack v_0 \to n_0,v_1\to n_1,\dots \rbrack}と表記する．
注意
すなわちここでは，論理式の形そのものを変えている．
例
$ 4 \in \mathcal{N}に対し，$ 4の数項$ \overline{4}とは$ \tt s(s(s(s(z))))またはその略記$ \tt{4}のことを指す．
$ \exists_{v_1}(v_0 = \mathtt{2} \times v_1)の$ v_0を$ \overline{4}で書き換えると以下のようになる．
$ \exists_{v_1}(\overline{4} = \mathtt{2} \times v_1)
すなわち，
$ (\exists_{v_1}(v_0 = \mathtt{2} \times v_1))_{\lbrack v_0 \to 4 \rbrack}は$ \exists_{v_1}(\overline{4} = \mathtt{2} \times v_1)と等しい．
今カッコは適当に補った．
系
$ \mathsf{AE}において，条件付き文の解釈に関する制約と，論理式の書き換えの関係については次のことが言える．
$ \varphiは自由変数$ v_0,v_1,\cdotsを持つ任意の$ \mathsf{AE}の開論理式とする．
任意の$ n_0,n_1,\dots \in \mathcal{N}に対して，次の2つのことが成り立つ．
$ v_0 = n_0,v_1=n_1,\dotsという条件下での条件付き文$ \varphi\lbrack v_0 \coloneqq n_0,v_1\coloneqq n_1 ,\dots \rbrackが真$ \iff文$ \varphi_{\lbrack v_0 \to n_0,v_1\to n_1 ,\dots \rbrack}が真
$ v_0 = n_0,v_1=n_1,\dotsという条件下での条件付き文$ \varphi\lbrack v_0 \coloneqq n_0,v_1\coloneqq n_1 ,\dots \rbrackが偽$ \iff文$ \varphi_{\lbrack v_0 \to n_0,v_1\to n_1 ,\dots \rbrack}が偽
注意
表しているものに注意
左側は，文$ \varphiを$ v_0,v_1,\dotsをそれぞれ$ d_0,d_1,\dots \in Dに割り当てる付値$ Vを持つ任意の解釈で解釈すると真（または偽）であるという事実を表している．
右側は，文$ \varphi_{\lbrack v_0 \to n_0,v_1\to n_1,\dots \rbrack}を任意の解釈で解釈すると真（または偽）であるという事実を表している．
系
1項関係$ \mathsf{string}_\mathsf{AE}(x):「$ xに対応する$ \mathsf{AE}の記号列$ \sigma_nが存在する」は$ \mathcal{A_E}関係である．
3項関係$ \mathsf{concat}_\mathsf{AE}(x,y): 「$ xをGödel数とする$ \mathsf{AE}の記号列$ \sigma_xと，$ yをGödel数とする$ \mathsf{AE}の記号列$ \sigma_yを連結した$ \mathsf{AE}の記号列$ \sigma_x\sigma_yのGödel数は$ zと等しい」は$ \mathcal{A_E}関係である．
系
任意の$ n \in \mathcal{N}について，$ \mathsf{AE}の数項$ \overline{n}のGödel数$ \ulcorner \overline{n} \urcornerは
$ \underbrace{\ulcorner f_1( \urcorner *_{17} \ulcorner f_1( \urcorner *_{17}}_\text{$n$ times} \ulcorner f_0 \urcorner \underbrace{*_{17} \ulcorner ) \urcorner }_\text{$n$ times} として計算可能
1項関係$ \mathsf{numtm}_n(x): 「$ xは$ \mathsf{AE}の数項$ \overline{n}のGödel数である」は$ \mathcal{A_E}関係である．
証明: TODO
問題1の否定的解決
ある自然数$ n \in \mathcal{N}が何らかの性質$ Fを満たすことを$ F(n)と表す．
自由変数を一つ$ v_0とした$ \mathsf{AE}の論理式$ \varphi_Fによって性質$ Fが定義出来るとする．
今，次のことが成り立っている，任意の$ n \in \mathcal{N}に対し
$ F(n)$ \iff文$ \varphi_{F, \lbrack v_0 \to n \rbrack}は真．
任意の記号列$ \sigmaと$ n \in \mathcal{N}に対し次の写像$ R:\Sigma_\mathsf{AE}^* \times \mathcal{N} \to \Sigma_\mathsf{AE}^*を定義する．
$ R(\sigma,n) は記号列$ \forall_{v_0} (v_0 = \overline{n} \to \sigma)を返す．
$ R(\sigma,n)によって返ってくる記号列にも当然Gödel数が割り当てられる．
$ \sigmaのGödel数を$ \ulcorner \sigma \urcornerとする
$ \forall v_0は$ \lnot \exists_{v_0} \lnotの略記であったことに留意する．
$ \ulcorner R(\sigma,n) \urcorner = \ulcorner \lnot\exists_{v_0}\lnot(v_0 = \urcorner *_{17} \ulcorner \overline{n} \urcorner *_{17} \ulcorner \to \urcorner *_{17} \ulcorner \sigma \urcorner *_{17} \ulcorner ) \urcornerとして計算可能．
3項関係$ z = \mathsf{repr}(x,y): 「$ xをGödel数とする記号列$ \sigma_xと$ y \in \mathcal{N}に対し，$ zは記号列$ \forall_{v_0} (v_0 = \overline{n} \to \sigma)のGödel数である」は$ \mathcal{A_E}関係である．
証明: ほとんど自明なのでTODO
2項関数$ \mathsf{repr}(x,y)は表現関数と呼ばれる．
対角化関数$ \mathsf{diag}(x)\coloneqq \mathsf{repr}(x,x)を定める．
2項関係$ y = \mathsf{diag}(x)は$ \mathcal{A_E}関係である．
証明: 自明．
集合$ Aが$ \mathcal{A_E}集合であるとき，$ A \coloneqq \{ n \in \mathcal{N} \mid \varphi_A\lbrack v_0 \coloneqq n\rbrack \}となる$ \mathsf{AE}の論理式$ \varphi_Aが必ず存在している．これに注意すると
$ \mathsf{AE}の論理式$ \varphi_Aによって定まる集合$ Aに対し
$ x \in A
部分集合$ D_A \coloneqq \{ n \mid \mathsf{diag}(n) \in A \} \sube \mathcal{N} を考える．