Gödel数記号
a v f ' ! ⊃ , ∀ ( ) = < #
例えば倫理式（文）$ \forall x \forall y ((x = y) \to (s(x) = s(y)))を
Gödel数記号列の∀v'∀v''(((v'=v''))⊃(f'(v')=f'(v'')))へと翻訳する
全ての翻訳規則を書くことは省略するが，例えば
a'で「1番目の定項$ a」を表す
a''で「2番目の定項$ b」
v fについてはそれぞれ$ n番目の変項と演算子について．
a v f ' ! ⊃ , ∀ ( ) = < #を
1 2 3 4 5 6 7 8 9 0 α β γへと更に13個の記号（数ではない！）を割り振る
こうすることでさっきの記号列は更に
∀v'∀v''(((v'=v''))⊃(f'(v')=f'(v'')))
824824499924α2440069349240α349244000という記号列に翻訳される
この記号列を13進数の自然数として解釈することで，論理式に対して一意なGödel数（自然数）が割り振られる 上の作業は実際には必要がなくa v f ' ! ⊃ , ∀ ( ) = < #という記号を使う13進数の表記と解釈しても構わない．
上では論理式 → Gödel数記号という中間言語 → Gödel数（自然数）を割り振っていたが，実際には逆かつダイレクトで，
ある13進数の自然数が，直接に論理式を指示すると考えたほうがよい．
すなわち824824499924α2440069349240α349244000という自然数が$ \forall x \forall y ((x = y) \to (s(x) = s(y)))を直接指示する．
もちろん，自然数は無限にあるので，意味不明な（論理式や項ではない）記号列を指示する場合もある
一階述語論理の記号の任意の列を式と呼ぶとする．
11111111は$ aaaaaaaaaという無意味な式を表すし，546546546は$ \lnot'\to\lnot'\to\lnot'\toという無意味な式を表す．
残った#というGödel数記号は論理式の列のために用いる．
論理式の有限列$ \varphi_1,\varphi_2,\dots,\varphi_nのGödel数をそれぞれ$ x_1,x_2,\dots,x_nとすると，それを連結するための記号として用いる
例えば$ \varphi_1が111，$ \varphi_2が222，$ \varphi_3が333としよう
有限列$ \varphi_1,\varphi_2,\varphi_3は次のGödel数を持つ
111γ222γ333
これを使ってHilbert流演繹体系における証明（ある規則を持った論理式の有限列）に一意のGödel数を割り振ることが出来る 逆に言えばある自然数が何らかの論理式の証明を指示することがある
参考文献