ゲーデル数
ゲーデル数（Gödel number）とは、数理論理式で用いられる論理式に対し、一意的に割り当てられた自然数です。ゲーデル数は、ゲーデルが不完全性定理を証明するために用いられました。
ゲーデル数により、論理式や証明というようなものの全てを、自然数によって一意的に代表させることができます。
原始記号のゲーデル数
原始記号のゲーデル数は、ペアノの公理系のような公理系で用いられる原始記号に対し、以下のように割り当てられた素数です。尚、この割り当ての方法は一通りではありません。
| $0$ | $s$ | $=$ | $\in$ | $N$ | $\neg$ | $\to$ | $($ | $)$ | $\cdots$ |
| $2$ | $3$ | $5$ | $7$ | $11$ | $13$ | $17$ | $19$ | $23$ | $\cdots$ |
論理式のゲーデル数
論理式のゲーデル数は、有限個の原始記号の並び（記号列）に対して割り当てられた自然数です。原始記号の並びを $a_1a_2a_3\cdots a_m$ とし、各記号のゲーデル数を $n_1n_2n_3\cdots n_m$ とすると、記号列のゲーデル数 $n$ は、素数列 $p_1p_2\cdots$ により以下で定義されます。
$$n=p_1^{n_1}p_2^{n_2}p_3^{n_3}\cdots p_m^{n_m}=2^{n_1}3^{n_2}5^{n_3}\cdots p_m^{n_m}$$
例えば、論理式 $0\in N$ の各記号のゲーデル数は $2,7,11$ であるため、記号式のゲーデル数は以下のように計算することができます。
$$n=2^23^75^{11}=427,148,437,500$$
逆に任意の自然数が与えられると、素因数分解は一意的に定まるため、一意的に（意味を持たないものを含め）記号の並びに割り当てることができます。
式系列のゲーデル数
式系列のゲーデル数は、有限個の式系列の並び（証明）に割り当てられた自然数です。式系列の並びを $S_1S_2S_3\cdots S_m$ とし、各記号列のゲーデル数を $n_1n_2n_3\cdots n_m$ とすると、式系列のゲーデル数 $n$ は以下で定義されます。
$$n=p_1^{n_1}p_2^{n_2}p_3^{n_3}\cdots p_m^{n_m}=2^{n_1}3^{n_2}5^{n_3}\cdots p_m^{n_m}$$
証明の形式化
ゲーデル数を使うことで証明を形式化することができます。
直接の結論
直接の結論とは以下の場合を指します。
- ２つの論理式$A$ と $A\to B$ から論理式 $B$ を導くこと。
- 論理式 $A$ から論理式 $\forall aA$ を導くこと。
形式化された証明
形式化された証明とは、論理式の式系列 $K$ について、
$$K: A_1,A_2,\cdots,A_n$$
全ての $A_i$（ $i=1,2,\cdots,n$ ）に対して、以下が成り立っていることを指します。
- $A_i$ は公理である。
- $A_i$ は、$A_i$ より前に表れる１つまたは２つの論理式の直接の結論である。
式系列の表現可能性
表現可能とは、ある関係が論理式で表現できることを言います。式系列 $K$ に属する論理式 $A$ のゲーデル数 $g(A)$ の集合を $\kappa$ と置き、
$$\kappa=\{g(A)|A\in K\}$$
このとき、ゲーデル数 $x$ が $x\in\kappa$ である場合、$K$（または $\kappa$ ）は表現可能と言います。
論理式の証明可能性
論理式が証明可能とは、その論理式の証明になるような式系列が存在するということです。論理式 $A$ が証明可能であることを $P_r(g(A))$ で表します。
式系列 $K$ において、最後の論理式 $A_n$ のゲーデル数を $y$ とすると、ゲーデル数 $x$（ $x\in\kappa$ ）が $y$ の証明になっている場合、$P(x,y)$ で表します。従って、以下のように表されます。
$$P_r(y)=\exists xP(x,y)$$
