小野寛晰『情報科学における論理』の読書ノート。なるべく練習問題も解いてく。（→前回）
第2章 述語論理（承前）
古典述語論理の形式体系LK
推論規則
古典命題論理での推論規則に加えて次の推論規則を持つ。なお は論理式、
は論理式の列、
は任意の項、
は対象変数を表す。
- ∀ Left (∀L)
- ∀ Right (∀R)
- ∃ Left (∃L)
- ∃ Right (∃R)
∀Rと∃Lを適用するには、 が下式で自由な出現を持ってはならない。この条件を変数条件（eigenvariable condition）と呼び、また
を固有変数（eigenvariable）と呼ぶ。
Cut除去定理
命題論理と同様、述語論理のLKに於いてもcut除去定理が成り立つ。
決定不能性
命題論理と異なり、与えられた式が述語論理のLKで証明可能かどうかは決定不能。
完全性定理
完全性と健全性
命題論理と同様、述語論理のLKも健全かつ完全。
形式理論
閉じた論理式の集合を形式理論（formal theory）または理論と呼ぶ。
理論 に含まれる論理式からなる有限列
を適当に選んで、式
がLKで証明可能になるとき、
は
で証明可能といい、
で表す。（この本が式の導出記号を
でなく
で記述しているのはこういうことかー。式を構成する記号か、公理から式を導出可能なこと表す記号か紛らわしいね）
のとき、つまり式
が証明可能なとき
は矛盾する（inconsistent）という。
モデル
言語 上の理論
と
に対する構造
について、任意の
が
であるとき、
を
のモデルと呼ぶ。
二変数述語記号として が与えられているとき、次の論理式の集合を等号の公理と呼ぶ。以降同記号を含む言語上の理論には等号の公理が含まれるものとする。
（
は
変数関数記号）
（
は
例として次の記号からなる言語 を考える。
- 対象定数：
- 一変数関数記号：
- 二変数関数記号：
- 二変数述語記号：
等号の公理に加えて次の論理式からなる 上の理論
があるとする。
これは明らかに群の定義である。ある群 があり、その単位元や演算を
の各記号に対応させる写像
を取れば、構造
は
のモデルになる。また
のモデルはひとつの群を自然に定める。従ってしばしば群
と構造
を同一視する。
強い形の完全性
- 任意の理論
がモデルを持つならば、
- 任意の理論
2番を強い形の完全性定理という。
練習問題
問2.13
問2.14
問2.15
2-a)
2-b)
3-a)
3-b)
4-a)
4-b)
5-a)
5-b)
6-a)
6-b)
10-a)
10-b)
11-a)
11-b)
12-a)
12-b)
13)
14)
15)
