20260708_1

20260624_1

---

暗記は基本的にはないけど導入や除去はできるように

---

等号 $=$

なぜ等号が必要か

「$Fx$ を満たすものはただ一つ存在する」はどう表現する？

$\exists xFx$ では不十分（2つ以上ある可能性を排除できない）

$$\exists x(Fx\wedge \forall y(Fy\to x=y))$$

→ アイデア：$Fx$ を満たすものが少なくとも一つ存在して、他にどんなものがそれを満たしても $x$ と一致する

---

等号の公理

$$\frac{}{t=t}=Ax$$

ただし $t$ は任意の個体変項ないしは個体定項。

公理とは証明を必要とせずにいつでも用いてよい論理式。閉じた仮定として利用する。

---

等号の除去

$$\frac{s=tA(s)}{A(t)}=E$$

ただし $s,t$ は任意の個体変項ないしは個体定項。

意味：$s$ と $t$ が等しければ、$s$ について成り立つことは $t$ についても成り立つ（ライプニッツの法則）

---

等号と唯一性

「高々一つ」

$$\forall x\forall y(Fx\wedge Fy\to x=y)$$

→ $F$ を満たすものがいても1つまで

「一意に存在する」（ちょうど一つ）

$$\exists xFx\wedge \forall x\forall y(Fx\wedge Fy\to x=y)$$

「少なくとも二つ存在する」

$$\exists x\exists y(Fx\wedge Fy\wedge x\ne y)$$

「ちょうど二つ存在する」

$$\exists x\exists y(Fx\wedge Fy\wedge x\ne y\wedge \forall z(Fz\to z=x\vee z=y))$$

---

意味論と証明論の関係

2つの「正しさ」

	証明論（⊢）	意味論（⊨）
何を扱う？	証明木・推論規則	モデル・真理値
得意なこと	証明を1つ作ればいい	反例を1つ作ればいい（反証）
性質	有限的（証明は有限列）	無限的（モデルは大きくできる）

---

健全性と完全性

$$\Gamma ⊢A\iff \Gamma \models A$$

• 健全性（→）：証明できれば真。比較的に容易。
• 完全性（←）：真なら証明できる。こちらが大変。

→ これらのズレがないことを保証するのが完全性定理。

---

三つの課題

1. 形式化：妥当な推論の判定のために自然言語の推論を形式言語に置き換える
2. 意味論：妥当な推論を真・偽の概念を用いて特徴付ける
3. 証明論：妥当な推論を証明の概念を用いて特徴付ける

完全性定理：この2つのアプローチの関係性を確立する

---

1. 命題論理の完全性定理

1.1 健全性定理 (Soundness)

$$\Gamma ⊢A\Rightarrow \Gamma \models A$$

証明のアイデア

証明木 $D$ の構造に関する帰納法で示す。

各推論規則について「この規則を使っても真が保たれる」ことを確認する。

基底：$D$ が1つの式のみ → $A\in \Gamma$ → 明らかに $\Gamma \models A$

∧I：結論が $A\wedge B$

• 帰納法の仮定：$\Gamma \models A$, ${\Gamma }^{\prime }\models B$
• 新しい仮定集合 ${\Gamma }^{\prime \prime }\supseteq \Gamma \cup {\Gamma }^{\prime }$ を考える
• $[[A]{]}_v=T$ かつ $[[B]{]}_v=T$ → $[[A\wedge B]{]}_v=T$

∧E：結論が $A$ または $B$

• $\Gamma \models A\wedge B$ → $\Gamma \models A$ かつ $\Gamma \models B$

→I：結論が $A\to B$

• ${\Gamma }^{\prime }\cup \{A\}\models B$ を仮定
• $[[A]]=T$ かつ ${\Gamma }^{\prime }$ の式が全て真 → $[[B]]=T$
• →の真理表より $[[A\to B]]=T$

⊥E：

• $\Gamma \models \perp$ だが $[[\perp ]]=F$
• → $\Gamma$ の全式を真にする評価は存在しない → 結論が従う

RAA：

• $\Gamma \models \perp$
• もし $\Gamma /\models A$ なら $[[\neg A]{]}_v=T$ となる評価 $v$ が存在
• ${\Gamma }^{\prime }=\Gamma \cup \{\neg A\}$ は ${\Gamma }^{\prime }\models \perp$ → 矛盾
• よって $\Gamma \models A$

---

1.2 完全性定理の証明

準備：無矛盾性

Definition：$\Gamma$ が無矛盾とは

$$\Gamma /⊢\perp$$

Lemma：次の3つは同値

1. $\Gamma$ は無矛盾
2. 任意の $A$ について $\Gamma ⊢A$ かつ $\Gamma ⊢\neg A$ となることはない
3. ある $A$ が存在して $\Gamma /⊢A$

重要：矛盾した集合は全ての命題を証明できてしまう → 数学的に意味がない

極大無矛盾集合

Definition：${\Gamma }^{\ast }$ が極大無矛盾とは

$${\Gamma }^{\ast }\subseteq {\Gamma }^{\prime }\text{ かつ }{\Gamma }^{\prime }\text{ が無矛盾}\Rightarrow {\Gamma }^{\ast }={\Gamma }^{\prime }$$

直観：${\Gamma }^{\ast }$ より真に大きな無矛盾集合は存在しない

リンデンバウムの補題 (Lindenbaum’s Lemma)

任意の無矛盾集合 $\Gamma$ は、ある極大無矛盾集合 ${\Gamma }^{\ast }$ に含まれる。

証明：

1. 全命題を列挙：$A_0,A_1,A_2,\dots$
2. 集合列を帰納的に定義：

$${\Gamma }_0=\Gamma$$ $${\Gamma }_{n+1}=\{\begin{array}{ll}{\Gamma }_n\cup \{A_n\}& \text{if }{\Gamma }_n\cup \{A_n\}\text{ が無矛盾}\\ {\Gamma }_n& \text{otherwise}\end{array}$$

3. ${\Gamma }^{\ast }={\bigcup }_{n\ge 0}{\Gamma }_n$ と定義

極大無矛盾集合の性質 (Lemma 6)

${\Gamma }^{\ast }$ が極大無矛盾のとき：

1. $A\in {\Gamma }^{\ast }$ or $\neg A\in {\Gamma }^{\ast }$ （排中律）
2. $A\in {\Gamma }^{\ast }$ かつ $A\to B\in {\Gamma }^{\ast }$ → $B\in {\Gamma }^{\ast }$
3. $A\wedge B\in {\Gamma }^{\ast }$ ⇔ $A\in {\Gamma }^{\ast }$ かつ $B\in {\Gamma }^{\ast }$
4. $A\vee B\in {\Gamma }^{\ast }$ ⇔ $A\in {\Gamma }^{\ast }$ or $B\in {\Gamma }^{\ast }$

モデルの構成

${\Gamma }^{\ast }$ から評価 $v$ を構成：

$$v(A_i)=\{\begin{array}{ll}T& \text{if }{A}_i\in {\Gamma }^{\ast }\\ F& \text{if }{A}_i\notin {\Gamma }^{\ast }\end{array}$$

真理補題 (Lemma 8)

$$[[A]{]}_v=T\iff A\in {\Gamma }^{\ast }$$

証明：$A$ の構造に関する帰納法

完全性定理の結論

$\Gamma /⊢A$ ならば：

• $\Gamma \cup \{\neg A\}$ は無矛盾
• → 極大無矛盾集合 ${\Gamma }^{\ast }\supseteq \Gamma \cup \{\neg A\}$ が存在
• → ${\Gamma }^{\ast }$ から構成された評価 $v$ は $\Gamma$ の全式を真にし、$A$ を偽にする
• → $\Gamma /\models A$

よって対偶を取って $\Gamma \models A\Rightarrow \Gamma ⊢A$

---

1.3 コンパクト性定理

$$\Gamma \text{ が充足可能}\iff \Gamma \text{ の任意の有限部分集合が充足可能}$$

証明：完全性定理から直ちに従う

応用例：グラフ彩色

グラフ $G=(V,E)$ について：

• 各頂点 $v$ と色 $i$ に命題変数 $P_{v,i}$ を導入
• 条件を式集合 $\Gamma$ で表現：
  1. 各頂点は少なくとも1色：$P_{v,1}\vee \cdots \vee P_{v,k}$
  2. 各頂点は高々1色：$\neg (P_{v,i}\wedge P_{v,j})$
  3. 隣接頂点は異なる色：$\neg (P_{v,i}\wedge P_{w,i})$ for $(v,w)\in E$

→ 任意の有限部分グラフが $k$ 色可能なら、無限グラフ $G$ も $k$ 色可能

---

2. 述語論理の完全性定理

命題論理と同様に $\Gamma ⊢A\iff \Gamma \models A$ が成り立つ。

2.1 証明の全体像

$$\Gamma /⊢A$$ $$\downarrow$$ $$\Gamma \cup \{\neg A\}\text{ は無矛盾}$$ $$\downarrow \text{ヘンキン理論に拡張}$$ $$T_{\omega }\text{（無矛盾ヘンキン理論）}$$ $$\downarrow \text{リンデンバウム}$$ $$T_{\max }\text{（極大無矛盾ヘンキン理論）}$$ $$\downarrow \text{モデル構成}$$ $$\mathfrak{M}\models T_{\max }\supseteq \Gamma \cup \{\neg A\}$$ $$\downarrow$$ $$\Gamma /\models A\text{矛盾！}$$

---

2.2 ヘンキン理論

問題：$\exists xA(x)$ が真でも、具体的にどの項が $A$ を満たすかわからない → モデルを構成しにくい

解決：証人 (witness) を追加

Definition：理論 $T$ がヘンキン理論とは、任意の $\exists xA(x)$ に対し

$$\exists xA(x)\to A(c)$$

が $T$ に含まれる定数 $c$ が存在すること。

ヘンキン理論への拡張

各 $\exists xA(x)$ に対し：

1. 新しい定数 $c_A$ を追加
2. 公理 $\exists xA(x)\to A(c_A)$ を追加

これを繰り返して $T_{\omega }={\bigcup }_{n<\omega }{T}_n$ を得る。

Lemma：$T_{\omega }$ はヘンキン理論であり、$T$ の保存拡大である。

---

2.3 モデルの構成

$T_{\max }$（極大無矛盾ヘンキン理論）からモデル $\mathfrak{M}$ を構成。

等号がない場合

• ドメイン $D$ = 閉項の集合
• 定数の解釈：$I(c)=c$
• 関数の解釈：$I(f(t_1,\dots ,t_k))=f(t_1,\dots ,t_k)$
• 述語の解釈：

$$⟨t_1,\dots ,t_n⟩\in I(P)\iff T_{\max }⊢P(t_1,\dots ,t_n)$$

等号がある場合

同値関係を定義：

$$t\sim s\iff T_{\max }⊢t=s$$

ドメインを商集合 $D/\sim$ にする（商構成）。

---

2.4 真理補題

Lemma：任意の文 $A$ について

$$\mathfrak{M}\models A\iff T_{\max }⊢A$$

証明：$A$ の構造に関する帰納法

---

2.5 モデル存在補題

$$\Gamma \text{ が無矛盾}\Rightarrow \Gamma \text{ はモデルを持つ}$$

証明：

1. $\Gamma$ をヘンキン理論 $T_{\omega }$ に拡張（無矛盾性保存）
2. $T_{\omega }$ を極大無矛盾ヘンキン理論 $T_{\max }$ に拡張（リンデンバウム）
3. $T_{\max }$ からモデル $\mathfrak{M}$ を構成
4. 真理補題より $\mathfrak{M}\models T_{\max }\supseteq \Gamma$

---

2.6 完全性定理 (Gödel)

$$\Gamma \models A\Rightarrow \Gamma ⊢A$$

証明：
もし $\Gamma /⊢A$ なら $\Gamma \cup \{\neg A\}$ は無矛盾。
モデル存在補題より $\mathfrak{M}\models \Gamma \cup \{\neg A\}$ となるモデル $\mathfrak{M}$ が存在。
よって $\Gamma /\models A$ → 矛盾。

---

論理から理論へ

理論の定義

Definition：文の集合 $T$ が理論とは

$$T⊢A\Rightarrow A\in T$$

つまり理論は証明可能性について閉じている。

拡大と保存拡大

• $T^{\prime }\supseteq T$ → $T^{\prime }$ は $T$ の拡大
• $T^{\prime }\cap L=T$ → $T^{\prime }$ は $T$ の保存拡大

（新しい言語を導入しても元の言語の定理は増えない）