このノートでは、述語論理と等号述語論理、
そして、形式的体系のモデル、そしてゲーデル数の定義
についての解説を行う。
の理解のために、不可欠である。
1. 形式的体系の意味。
形式的体系とは、数学理論を始めとする学問を、記号によって記述し、
学問内部における推論を図形としての記号の組み合わせ論的変形として
解釈するものである。
以下に、具体的な、その方法論の概略を述べる。
1.1 形式的体系 Γ の構成
1.1.1 まず、Γ に必要となる記号に、どんな種類があるのか、列挙する。
1.1.1.1 自由変数と呼ばれる文字の（可算）列 v_1, v_2, v_3, ...
1.1.1.2 束縛変数と呼ばれる文字の（可算）列 u_1, u_2, u_3, ...
1.1.1.3 関数記号と呼ばれる記号 f_1, f_2, f_3, ....
これら関数記号の全体は、有限個または可算個とする。
また、各関数記号 f_i には、その重みと呼ばれる自然数 m=m(i)≧0
が対応し、f_i を m 変数関数記号と呼ぶ。
1.1.1.4 述語記号と呼ばれる記号 p_1, p_2, p_3, ....
これら述語記号の全体は、有限個または可算個とする。
また、各述語記号 p_j には、その重みと呼ばれる自然数 n=n(j)≧0
が対応し、p_j を n 項関係、または n 変数述語記号と呼ぶ。
1.1.1.5 論理記号 ∧, ∨, ⇒, ￢, ∀, ∃
1.1.2 次に、形式的体系 Γ の論理式と対象式と言う概念を、
以下に帰納的に定義する：
1.1.2.1 自由変数は、対象式である。
1.1.2.2 f が m 変数関数記号で、T_1, ..., T_m が m 個の対象式のとき、
記号列 f T_1... T_m は、対象式である。
1.1.2.3 以上によって定義されたものだけが、対象式である。
1.1.2.4 p が n 変数述語記号で T_1, ... , T_n が n 個の対象式のとき、
記号列 p T_1 ... T_n は論理式である。
1.1.2.5 A と B が論理式のとき, ∧AB, ∨AB, ⇒AB, ￢A の 4つの記号列は、
論理式である。(この記法は、ルカシュビッツによる)
1.1.2.6 A が論理式で、x は自由変数で、A(x) により、A に現れる全ての
x を代表して記述することにする。今、u を A に現れない束縛変数
とするとき、∃uA(u) と ∀uA(u) は、論理式である。但し、A(u) は、
A に現れる x を全て u で置き換えたものとする。
1.1.2.7 以上によって定義されたものだけが、論理式である。
1.1.3 論理式の記述に於いて、我々は習慣上、 ∧AB, ∨AB, ⇒AB, を、
それぞれ A∧B, A∨B, A⇒B と書くことにする。このときは、
記号の結合の順序に気をつけなくてはならないので、適宜
(A∧B)⇒C とか、A∧(B⇒C) など、括弧を用いて記述することにする。
1.1.3.1 論理式の直観的意味：
A∧B は 「AかつB」, A∨B は 「AまたはB」, A⇒B は 「AならばB」,
￢A は 「Aでない」, ∀uA(u) は 「全ての u に対して A(u) が成り立つ」,
∃uA(u) は 「ある u が存在して A(u) が成り立つ」である。
これらの記法は、数学基礎論以外の数学でも良く使われるものである。
1.1.4 次の超数学的な定理が成り立つ：
1.1.4.1 T が対象式で U(x) が対象式、x が自由変数のとき、U(x) に現れる x の全てを
T で置き換えて得られた記号列 U(T) も、対象式である。
1.1.4.2 T が対象式で A(x) が論理式、x が自由変数のとき、A(x) に現れる x の全てを
T で置き換えて得られた記号列 A(T) も、論理式である。
1.2 Γの公理
1.2.1 Γの公理の定め方は、2種類ある。
1.2.2 1種類目は、明示的公理を定めるというやり方で、
それは単に、論理式を有限個、「A_1, ... A_n は Γの明示的公理です。」
と約束するだけである。
1.2.3 Γの明示的公理の中に現れる自由変数を、Γの定数と呼ぶ。
定数とは、Γを学問としての理論としてみたとき、その理論における
何か特定の対象という意味合いを持っている。
1.2.4 2種類目は、公理シェーマと呼ばれるものによって公理を設定する方法で、
公理シェーマ S は、次の条件を満たすものとする：S は Γの論理式の一部
を作る方法で、S によってある論理式 A が作られたならば、 A の任意の
自由変数に任意の対象式を代入して得られた論理式も、S によって作られる。
1.2.5 公理シェーマによって作られた論理式のことを、（Γの）非明示的公理と言う。
1.3 Γの定理。Γの論理式がΓの定理であるということを、
以下に帰納的に定義する：
1.3.1 Γの明示的公理と非明示的公理はΓの定理である。
1.3.2 A と A⇒B がΓの定理ならば、B もΓの定理である。
1.3.3 A(x)⇒B がΓの 定理で、x は B に現れない自由変数で
Γの定数でないとき、(∃uA(u))⇒B も、Γの定理である。
ただし、u は A(x) に現れない束縛変数とする。
1.3.4 B⇒A(x) がΓの 定理で、x は B に現れない自由変数で
Γの定数でないとき、B⇒(∀uA(u)) も、Γの定理である。
ただし、u は A(x) に現れない束縛変数とする。
1.3.5 以上によって定義されたものだけが、Γの定理である。
1.4 形式的体系の強さ: Γ、Δ が二つの形式的体系で、Γの記号は
全て Δ の記号で、Γ の公理は全て Δ の定理のとき、Δ は Γよりも
強いと言う。
次が成り立つ：
1.4.1 形式的体系 Γ と Δ について、Δ が Γよりも強いとき、
Γ の定理は全て Δ の定理となる。
2 述語論理, 述語的な理論
2.1 明示的公理がなく、以下の公理シェーマ 2.1.1 ～ 2.1.12 を持つ形式的体系
Γ_1 を、述語論理と呼ぶ。Γ_1 よりも強い形式的体系を、述語的な理論
と呼ぶことにする。
2.1.1 A, B が論理式のとき、論理式 A ⇒ ( B ⇒ A ) は、公理である。
2.1.2 A, B, C が論理式のとき、論理式
( A ⇒ B ) ⇒ ( ( A ⇒ ( B ⇒ C ) ) ⇒ ( A ⇒ C ) )
は、公理である。
2.1.3 A, B が論理式のとき、論理式 A ⇒ ( B ⇒ ( A ∧ B ) ) は、公理である。
2.1.4 A, B が論理式のとき、論理式 ( A ∧ B ) ⇒ A は、公理である。
2.1..5 A, B が論理式のとき、論理式 ( A ∧ B ) ⇒ B は、公理である。
2.1.6 A, B が論理式のとき、論理式 A ⇒ ( A ∨ B ) は、公理である。
2.1.7 A, B が論理式のとき、論理式 B ⇒ ( A ∨ B ) は、公理である。
2.1.8 A, B, C が論理式のとき、論理式
( A ⇒ C ) ⇒ ( ( B ⇒ C ) ⇒ ( ( A ∨ B ) ⇒ C ) )
は、公理である。
2.1.9 A, B が論理式のとき、論理式
( A ⇒ B ) ⇒ ( ( A ⇒ ( ￢B ) ) ⇒ ( ￢A ) )
は、公理である。
2.1.10 A が論理式のとき、論理式 ( ￢￢A ) ⇒ A は、公理である。
2.1.11 A(x) が論理式で、T が対象式で、u が A(x) に現れない束縛変数
のとき、論理式 A(T) ⇒ ∃uA(u) は、公理である。
2.1.12 A(x) が論理式で、T が対象式で、u が A(x) に現れない束縛変数
のとき、論理式 ∀uA(u) ⇒ A(T) は、公理である。
述語的な理論については、以下の超数学的命題が成り立つ：
2.1.13 (エルブランの演繹定理)
Γ は述語的な理論、A, B は Γ の論理式で、Γに明示的公理として
A を追加した形式的体系を Γ^* とする。このとき、もし、B が Γ^* の
定理ならば、A⇒B は Γ の定理である。
注意：エルブランの演繹定理は、公理シェーマ 1.2.11 と 1.2.12 を
使用しなくても、証明できる。
2.2 等号述語論理, 等号を持つ理論
Γ_2 を形式的体系で、2変数述語記号 = を持ち、明示的公理として
以下の 2.2.1 を持ち、公理シェーマとして 2.1.1～2.1.12 と、
以下の 2.2.2 とを持つ理論とする：
2.2.1 ∀u_1=u_1u_1
2.2.2 T, U が 対象式で、A(x) が論理式、x が自由変数のとき、論理式
( T = U ) ⇒ ( A(T) ⇒ A(U) ) は、公理である。
但し、T=U は、 =TU の略記法である。
この形式的体系 Γ_2 を等号述語論理と呼び、Γ_2 よりも強い理論を
等号を持つ理論と呼ぶ。
等号を持つ理論は、もちろん述語的な理論となるから、
エルブランの演繹定理 2.1.13 が、成り立つ。
以上ここまで、詳しい議論については、私がノートをまとめて
スキャナーで pdf 化しています。以下のサイトで公開しています。
3 形式的体系のモデル
以下では、記号 M で空でない集合を表す。集合概念としては、素朴集合論を
知っていれば十分であるが、集合を成しえないような巨大な「集まり」
の導出するパラドックスに対して神経質になるような読者は、
公理的集合論の入門的な素養を身に付けておいたほうが良い。
3.1 述語的な理論のモデル
Γ を述語的な理論とするとき、M が Γのモデルであるとは、M に以下の
構造 2.1.1～2.1.9 が付随しているものを言う：
3.1.1 Γ の定数の全て a_1, ... a_k に対し、M の元 b_1, ... , b_k がそれぞれ
対応している。
3.1.2 Γ の m 変数関数記号 f_i に対し、M^m から M への m 変数関数
g_i が対応している。ここに、M^m は、M の m 個の直積集合。
3.1.3 Γ の n 変数述語記号 p_j に対し、M^n から 二元集合 {0, 1} への
n 変数関数 q_j が対応している。
3.1.4 Γ の自由変数の有限集合 H から M への写像 h で、a_j が H の元
ならば h(a_j) が bj に等しくなるものを、全て Γの M における付値
と呼ぶことにする。
3.1.5 T(x_1 , ... , x_n) を Γの対象式で、その中に現れる自由変数は全て
x_1, ... , x_n の中に現れるとする。h : {x_1 , ... , x_n} →M を Γの M
における付値とするとき、U(T, h) ∈M を、T の構成についての帰納法で
定義する：
3.1.5.1 T が自由変数 x_i のときは、U(T, h) は h(x_i) に等しいとする。
3.1.5.2 T が f T_1... T_m に等しく、f は n 変数関数記号、T_1, ... T_m は
対象式のとき、f に 3.1.2 によって対応する m 変数関数 : M^m → M
を g とするとき、U(T, h) は g(U(T_1, h), ... , U(T_m, h)) に等しいとする。
3.1.6 A(x_1, ... , x_s) を Γ の論理式で、その中に現れる自由変数は全て
x_1, ... , x_s の中に現れるとする。h : {x_1 , ... , x_s} →M を Γの M
における付値とする。このとき、V(A, h) ∈{0, 1} を、A の構成に
ついての帰納法で、以下のように定義する：
3.1.6.1 p が n 変数述語記号で T_1, ... ,T_n が対象式、p に 3.1.3 によって
対応している n 変数関数 を q : M^n → {0, 1} とするとき、
V(pT_1... T_n, h) は q(U(T_1, h), ... , U(T_n, h)) に等しいとする。
3.1.6.2 B, C が論理式のとき、V(B∧C, h) は V(B, h)・V(C, h)に、
V(B∨C, h) は max(V(B, h), V(C, h)) に、V(B⇒C, h) は
1-V(B, h)・(1-V(C, h)) に、V(￢B, h) は 1-V(B, h) に等しいとする。
3.1.6.3 B(y, x_1, ... , x_s) が論理式で、自由変数 y は x_1, ... ,x_s 及び
Γの定数のどれとも異なり、u は B に表れない束縛変数で、
A が ∃uB(u, x_1, ... , x_s) に等しいとき、V(A, h) は
sup V(B(y, x_1, ... , x_s), h') に等しいとする。ここに、上限は、
h' がh'(x_i) = h(x_i) (1≦i≦s), h'(y)∈M なるΓのM における
付値 h' : {y, x_1 , ... , x_n} → M を渡るときの上限を取るとする。
3.1.6.4 B(y, x_1, ... , x_s) が論理式で、自由変数 y は x_1, ... ,x_s 及び
Γの定数のどれとも異なり、u は B に表れない束縛変数で、
A が ∀uB(u, x_1, ... , x_s) に等しいとき、V(A, h) は
inf V(B(y, x_1, ... , x_s), h') に等しいとする。ここに、下限は、
h' がh'(x_i) = h(x_i) (1≦i≦s), h'(y)∈M なるΓのM における
付値 h' : {y, x_1 , ... , x_n} → M を渡るときの下限を取るとする。
3.1.7 Γの任意の明示的公理 A と、Γの M における付値 h で、h(a_i) = b_i
(1≦i≦k) なるものに対し、V(A, h) は 1 に等しい。
3.1.8 Γの任意の非明示的公理 A と Γの M における任意の付置 h に対し、
V(A, h) は 1 に等しい。
3.1.9 Γの論理式 A は、Γ の M における任意の付値 h で A に現れる
自由変数が全て h の定義域に入るものに対して V(A, h) が常に
1に等しいとき、M に於いて恒真であると言う。
次の超数学的命題が成り立つ：
3.1.10 M を述語的な理論 Γのモデル, A をΓの定理とするとき、
A は M に於いて恒真である。
3.1.11 (完全性定理) 述語的な理論 Γ が無矛盾であれば、Γのモデル
M が存在する。
3.2 等号を持つ理論の正規モデル
3.2.1 Γ を等号を持つ理論、M を Γ のモデルとする。もし、M が次の性質
を持てば、M を Γの 正規モデルと言う。
3.2.1.1 Γ の等号記号 = に 2.1.3 によって対応している 二変数関数を
g とするとき、任意の x, y ∈ M に対し、g(x, y) が値 1 を取るための
必要十分条件は、 x と y が M の元として等しいことである。
次の超数学的命題が成り立つ：
3.2.2 （完全性定理 2） 等号を持つ理論 Γ が無矛盾であれば、Γ の
正規モデル M が存在する。
以上で、形式的体系、述語論理、等号述語論理とモデルについての解説を終わる。
4. ゲーデル数
我々は、形式的体系の論理式および対象式のゲーデル数を、
以下のように定義する：
以下、A を記号または記号列とするときの、そのゲーデル数を
G(A) で表す。
4.1 まず、i 番目の素数を P(i) とおく。
4.2 次に、基本的な記号のゲーデル数を定義する。
4.2.1 G(￢) を P(1), G(∨) を P(2), G(∧) を P(3), G(⇒) を P(4),
G(∃) を P(5), G(∀) を P(6), G(v_i) を P(4(i-1)+7) (i≧1),
G(u_j) を P(4(j-1)+8) (j≧1), G(f_i) を P(4(i-1)+9)(i≧1),
G(p_j) を P(4(j-1)+10) (j≧1) にそれぞれ等しいとする。
4.3 次に、1.1.1.1 ～ 1.1.1.5 の記号から成る有限列 s_1 ... s_n に対し、
G(s_1 ... s_n) を (P(1)^G(s_1))×(P(2)^G(s_2))× ... ×(P(n)^G(s_n))
に等しいとする。
4.4 論理式や対象式のゲーデル数は、全て 4.1 ～ 4.3 の方法で定義される。
以上で、ゲーデル数の定義についての解説を終わる。
参考文献
2. 倉田令二郎「入門数学基礎論」河合文化教育出版
3. 福山克「数理論理学」培風館
5. 数理論理学入門
文責: Dr. Kazuyoshi Katogi (加藤木 一好)
