このノートでは、集合論 BGE の土台となる論理体系
についての解説を行う。基本的に、等号述語論理のマイナーチェンジ版である。
1. 形式的体系 Γ の構成
1.1. まず、Γ に必要となる記号に、どんな種類があるのか、列挙する。
1.1.1. 自由集合変数と呼ばれる小文字の（可算）列 v_1, v_2, v_3, ...
1.1.2. 束縛集合変数と呼ばれる小文字の（可算）列 u_1, u_2, u_3, ...
1.1.3. 自由類変数と呼ばれる大文字の（可算）列 V_1, V_2, V_3, ...
1.1.4. 束縛類変数と呼ばれる大文字の（可算）列 U_1, U_2, U_3, ...
1.1.5. 集合関数記号と呼ばれる記号 f_1, f_2, f_3, ....
これら関数記号の全体は、有限個または可算個とする。
また、各関数記号 f_i には、その重みと呼ばれる自然数 m=m(i)≧0
が対応し、f_i を m 変数集合関数記号と呼ぶ。
1.1.6. 類関数記号と呼ばれる記号 g_1, g_2, g_3, ....
これら関数記号の全体は、有限個または可算個とする。
また、各関数記号 g_i には、その重みと呼ばれる自然数 l=l(i)≧0
が対応し、g_i を l 変数類関数記号と呼ぶ。
1.1.7. 述語記号と呼ばれる記号 p_1, p_2, p_3, ....
これら述語記号の全体は、有限個または可算個とする。
また、各述語記号 p_j には、その重みと呼ばれる自然数 n=n(j)≧0
が対応し、p_j を n 項関係、または n 変数述語記号と呼ぶ。
1.1.8. 論理記号 ∧, ∨, ⇒, ￢, ∀, ∃
1.2. 次に、形式的体系 Γ の論理式, 集合を表す対象式, 類を表す対象式
と言う概念を、以下に帰納的に定義する：
1.2.1. 自由集合変数は、集合を表す対象式である。
1.2.2. 自由類変数は、類を表す対象式である。
1.2.3. f が m 変数集合関数記号で、T_1, ..., T_m が m 個の
集合または類を表す対象式のとき、
記号列 f T_1... T_m は、集合を表す対象式である。
1.2.4. g が l 変数類関数記号で、T_1, ..., T_l が l 個の
集合または類を表す対象式のとき、
記号列 f T_1... T_l は、類を表す対象式である。
1.2.5. 以上によって定義されたものだけが、
集合または類を表す対象式である。
1.2.6. 集合または類を表す対象式をまとめて、対象式と呼ぶ。
1.2.7. p が n 変数述語記号で T_1, ... , T_n が n 個の対象式のとき、
記号列 p T_1 ... T_n は論理式である。
1.2.8. A と B が論理式のとき, ∧AB, ∨AB, ⇒AB, ￢A の 4つの記号列は、
論理式である。(この記法は、ルカシュビッツによる)
1.2.9. A が論理式で、x は自由集合変数で、A(x) により、A に現れる全ての
x を代表して記述することにする。今、u を A に現れない束縛集合変数
とするとき、∃uA(u) と ∀uA(u) は、論理式である。但し、A(u) は、
A に現れる x を全て u で置き換えたものとする。
1.2.10. A が論理式で、X は自由類変数で、A(X) により、A に現れる全ての
X を代表して記述することにする。今、U を A に現れない束縛類変数
とするとき、∃UA(U) と ∀UA(U) は、論理式である。但し、A(U) は、
A に現れる X を全て U で置き換えたものとする。
1.2.11. 以上によって定義されたものだけが、論理式である。
1.3. 論理式の記述に於いて、我々は習慣上、 ∧AB, ∨AB, ⇒AB, を、
それぞれ A∧B, A∨B, A⇒B と書くことにする。このときは、
記号の結合の順序に気をつけなくてはならないので、適宜
(A∧B)⇒C とか、A∧(B⇒C) など、括弧を用いて記述することにする。
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) が成り立つ」,∀UA(U) は
「全ての類 U に対して A(U) が成り立つ」, ∃UA(U) は 「ある類 U が
存在して A(U) が成り立つ」である。
1.4. 次の超数学的な定理が成り立つ：
1.4.1. T が対象式で U(ξ) が対象式、ξ が自由集合（または類）変数のとき、
U(ξ) に現れる ξ の全てを T で置き換えて得られた記号列 U(T) も、
対称式である。
1.4.2. T が対象式で A(ξ) が論理式、ξ が自由集合（または類）変数のとき、
A(ξ) に現れる ξ の全てを T で置き換えて得られた記号列 A(T) も、
論理式である。
1.5. Γの公理
1.5.1. Γの公理の定め方は、2種類ある。
1.5.1.1. 1種類目は、明示的公理を定めるというやり方で、
それは単に、論理式を有限個、「A_1, ... A_n は Γの明示的公理です。」
と約束するだけである。
1.5.1.2. Γの明示的公理の中に現れる自由集合（類）変数を、Γの集合定数（類定数）と呼ぶ。
定数とは、Γを学問としての理論としてみたとき、その理論における
何か特定の対象という意味合いを持っている。
1.5.1.3. 2種類目は、公理シェーマと呼ばれるものによって
公理を設定する方法で、公理シェーマ S は、次の条件を
満たすものとする：S は Γの論理式の一部を作る方法で、
S によってある論理式 A が作られたならば、 A の任意の
自由(集合または類)変数に任意の対象式を代入して得られた
論理式も、S によって作られる。
1.5.1.4. 公理シェーマによって作られた論理式のことを、
（Γの）非明示的公理と言う。
1.5.2. Γの定理。Γの論理式がΓの定理であるということを、
以下に帰納的に定義する：
1.5.2.1. Γの明示的公理と非明示的公理はΓの定理である。
1.5.2.2. A と A⇒B がΓの定理ならば、B もΓの定理である。
1.5.2.3. A(x)⇒B がΓの 定理で、x は B に現れない自由集合変数で
Γの定数でないとき、(∃uA(u))⇒B も、Γの定理である。
ただし、u は A(x) に現れない束縛集合変数とする。
1.5.2.4. B⇒A(x) がΓの 定理で、x は B に現れない集合自由変数で
Γの定数でないとき、B⇒(∀uA(u)) も、Γの定理である。
ただし、u は A(x) に現れない束縛集合変数とする。
1.5.2.5. A(X)⇒B がΓの 定理で、X は B に現れない自由類変数で
Γの定数でないとき、(∃UA(U))⇒B も、Γの定理である。
ただし、U は A(X) に現れない束縛類変数とする。
1.5.2.6. B⇒A(X) がΓの 定理で、X は B に現れない自由類変数で
Γの定数でないとき、B⇒(∀UA(U)) も、Γの定理である。
ただし、U は A(X) に現れない束縛類変数とする。
1.5.2.7. 以上によって定義されたものだけが、Γの定理である。
1.6. 形式的体系の強さ: Γ、Δ が二つの形式的体系で、Γの記号は
全て Δ の記号で、Γ の公理は全て Δ の定理のとき、Δ は Γよりも
強いと言う。
次が成り立つ：
1.6.1. 形式的体系 Γ と Δ について、Δ が Γよりも強いとき、
Γ の定理は全て Δ の定理となる。
2. 述語論理, 述語的な理論
明示的公理がなく、以下の公理シェーマ 2.1～2.14 を持つ形式的体系
Γ_1 を、述語論理と呼ぶ。Γ_1 よりも強い形式的体系を、述語的な理論
と呼ぶことにする。
2.1. A, B が論理式のとき、論理式 A ⇒ ( B ⇒ A ) は、公理である。
2.2. A, B, C が論理式のとき、論理式
( A ⇒ B ) ⇒ ( ( A ⇒ ( B ⇒ C ) ) ⇒ ( A ⇒ C ) )
は、公理である。
2.3. A, B が論理式のとき、論理式 A ⇒ ( B ⇒ ( A ∧ B) ) は、公理である。
2.4. A, B が論理式のとき、論理式 (A ∧ B) ⇒ A は、公理である。
2.5. A, B が論理式のとき、論理式 (A ∧ B) ⇒ B は、公理である。
2.6. A, B が論理式のとき、論理式 A ⇒ (A ∨ B) は、公理である。
2.7. A, B が論理式のとき、論理式 B ⇒ (A ∨ B) は、公理である。
2.8. A, B, C が論理式のとき、論理式
( A ⇒ C ) ⇒ ( ( B ⇒ C ) ⇒ ( ( A ∨ B ) ⇒ C ) )
は、公理である。
2.9. A, B が論理式のとき、論理式
( A ⇒ B ) ⇒ ( ( A ⇒ ( ￢B ) ) ⇒ ( ￢A ) )
は、公理である。
2.10. A が論理式のとき、論理式 (￢￢A ) ⇒ A は、公理である。
2.11. A(x) が論理式で、T が集合を表す対象式で、u が A(x) に現れない
束縛集合変数のとき、論理式 A(T)⇒∃uA(u) は、公理である。
2.12. A(x) が論理式で、T が集合を表す対象式で、u が A(x) に現れない
束縛集合変数のとき、論理式 ∀uA(u)⇒A(T) は、公理である。
2.13. A(X) が論理式で、T が対象式で、U が A(X) に現れない束縛類変数のとき、
論理式 A(T)⇒∃UA(U) は、公理である。
2.14. A(X) が論理式で、T が対象式で、U が A(X) に現れない束縛類変数のとき、
論理式 ∀UA(U)⇒A(T) は、公理である。
述語的な理論については、以下の超数学的命題が成り立つ：
2.15. (エルブランの演繹定理)
Γ は述語的な理論、A, B は Γ の論理式で、Γに明示的公理として
A を追加した形式的体系を Γ^* とする。このとき、もし、B が Γ^* の
定理ならば、A⇒B は Γ の定理である。
注意：エルブランの演繹定理は、公理シェーマ 2.11 ～ 2.14 を
使用しなくても、証明できる。
3. 等号述語論理, 等号を持つ理論
Γ_2 を形式的体系で、2変数述語記号 = を持ち、明示的公理として
以下の 3.1, 3.2 を持ち、公理シェーマとして 2.1～2.14 と、
以下の 3.3 とを持つ理論とする：
3.1. ∀u_1=u_1u_1
3.2. ∀U_1=U_1U_1
3.3. T, U が 対象式で、A(ξ) が論理式、ξ が自由集合(または類)変数のとき、
論理式(T=U)⇒(A(T)⇒A(U)) は、公理である。
但し、T=U は、 =TU の略記法である。
この形式的体系 Γ_2 を等号述語論理と呼び、Γ_2 よりも強い理論を
等号を持つ理論と呼ぶ。
等号を持つ理論は、もちろん述語的な理論となるから、
エルブランの演繹定理 2.15 が、成り立つ。
以上で、BGE の土台となる論理体系の解説を終わる。
4. BGE の公理についての若干の注意。
BGE では、最初に与えられた集合または類関数記号は存在しない。
また、最初に与えられた述語記号は = と ∈ (どちらも2変数)である。
4.1. まず、論理式 M(X) については、
M(X) ⇔ ∃u (X = u)
を定義式として使う。つまり、直観的な意味は、
M(X) ⇔ 類 X は集合である。
ここに、X は自由類変数、u は束縛集合変数。
そして公理 A(1) は、正確には
∀X ( ( ∃Y ( X ∈ Y ) ) ⇔ ( ∃u ( u = X ) ) )
となるのである。
また、わかりやすさのために、
∀u∃U(u=U)
(直観的な意味は、「すべての集合は、類である。」となる。)
も、論理的にはダブるかもしれないが公理として認めたほうが良いと思う。
(実際は、公理 A(2), B(2) と述語論理の公理系から導かれる。)
4.2. つぎに、A(X, ξ_1, ... ξ_n) を論理式, ξ_i は類または集合を表す変数で、
BGE から
∀ξ_1...∀ξ_n ∃X ( A(X, ξ_1, ... ξ_n) ∧ ∀Y (A(Y, ξ_1, ... ξ_n) ⇒ X=Y))
が証明可能とすると、BGE に新しい類関数記号 F を付け加えて、
明示的公理
∀ξ_1...∀ξ_n A(F(ξ_1, ... , ξ_n), ξ_1, ... , ξ_n)
を付け加えた形式的体系 を BGE' とおくと、BGE' は BGE の
保存拡大になっている。つまり、F の現れない BGE の論理式 B が
BGE' から証明可能ならば、B は BGE からも証明可能である。
（Menderson の定理; 福山克「数理論理学」培風館に、超限的な証明が載っているが、
有限の立場でも証明可能である。）X の代わりに自由集合変数 x を取り、
F を集合関数記号としても同様である。
さらに、この操作は何度でも繰り返すことが出来て、
BGE' の 論理式 B(X, ζ_1, ... ζ_m) (ζ_j は類または集合を表す変数) に対し、
∀ζ_1...∀ζ_m∃X(B(X, ζ_1, ... ζ_m)∧∀Y(B(Y, ζ_1, ... ζ_m)⇒X=Y))
が BGE' から証明可能とするとき、BGE' に 新しい類関数記号
G を付け加え、明示的公理
∀ζ_1...∀ζ_m B(G(ζ_1, ... ζ_m), ζ_1, ... ζ_m)
を付け加えた形式的体系 BGE'' も、BGE' の保存拡大になっている。
つまり、BGE' の論理式 C が BGE'' から証明可能ならば、C
はすでに BGE' から証明可能である。特に、BGE の論理式
D が BGE'' から証明可能ならば、D はすでに BGE から証明可能である。
やはり、X の代わりに自由集合変数 x を用い、G を集合関数記号としても同様である。
こうして、我々は、論理体系の言語面での表現力を保存拡大の意味で、
豊かにしていくことが出来る。
参考文献
BGE 集合論については
河合文化教育出版「公理論的集合論」倉田令二郎・篠田寿一著
等号述語論理については
河合文化教育出版「入門数学基礎論」倉田令二郎著
を参考にした。
文責: Dr. Kazuyoshi Katogi (加藤木 一好)
