直観主義論理 | 数理論理 | 天游ヶ丘数理学院

1 論理式と自然演繹

命題変数の集合を $P$ とする。論理式は

A ::= p\mid\bot\mid A\land A\mid A\lor A\mid A\to A \qquad(p\in P)

によって帰納的に生成する。否定は $\neg A:=A\to\bot$ と定義する。前提集合 $\Gamma$ は論理式の有限集合とする。

定義 1.1. 判断 $\Gamma\vdash_I A$ を、次の規則から生成される有限導出木の存在として定める。

\frac{A\in\Gamma}{\Gamma\vdash_I A}(\mathrm{Ax}) \qquad \frac{\Gamma\vdash_I A\qquad\Gamma\vdash_I B} {\Gamma\vdash_I A\land B}(\land I)

\frac{\Gamma\vdash_I A\land B}{\Gamma\vdash_I A}(\land E_1) \qquad \frac{\Gamma\vdash_I A\land B}{\Gamma\vdash_I B}(\land E_2)

\frac{\Gamma\vdash_I A}{\Gamma\vdash_I A\lor B}(\lor I_1) \qquad \frac{\Gamma\vdash_I B}{\Gamma\vdash_I A\lor B}(\lor I_2)

\frac{\Gamma\vdash_I A\lor B\qquad \Gamma\cup\{A\}\vdash_I C\qquad \Gamma\cup\{B\}\vdash_I C} {\Gamma\vdash_I C}(\lor E)

\frac{\Gamma\cup\{A\}\vdash_I B}{\Gamma\vdash_I A\to B}(\to I) \qquad \frac{\Gamma\vdash_I A\to B\qquad\Gamma\vdash_I A} {\Gamma\vdash_I B}(\to E)

\frac{\Gamma\vdash_I\bot}{\Gamma\vdash_I A}(\bot E)

含意導入では、表示した前提 $A$ を解除する。排中律 $A\lor\neg A$ 、二重否定除去 $\neg\neg A\to A$ 、および背理法は規則として加えない。

前提を増やしても既存の導出木はそのまま用いることができる。

補題 1.2. $\Gamma\vdash_I A$ かつ $\Gamma\subseteq\Delta$ ならば $\Delta\vdash_I A$ である。

証明. $\Gamma\vdash_I A$ の導出木に関して帰納法を用いる。公理の場合、 $A\in\Gamma\subseteq\Delta$ なので $\Delta\vdash_I A$ である。各導入規則と除去規則では、すべての直前の判断へ帰納法の仮定を適用し、同じ規則を再び適用する。含意導入では $\Gamma\cup\{B\}\subseteq\Delta\cup\{B\}$ を用いる。選言除去の二つの枝でも同じ包含を用いる。従って全規則について結論が保たれる。▨

例 1.3 (連言の交換). $A\land B\vdash_I B\land A$ を導出する。前提 $A\land B$ へ $(\land E_2)$ と $(\land E_1)$ を適用して、それぞれ $B$ と $A$ を得る。二つの導出へ $(\land I)$ を適用すると $B\land A$ を得る。この導出は排中律を用いない。

2 Kripke モデル

Kripke 意味論では、世界を情報状態とみなし、 $w\le v$ を「 $v$ が $w$ 以上の情報をもつ」と解釈する。原子命題が一度成立した後で不成立へ戻らないことを、付値の上方閉性として課す。

定義 2.1. 直観主義命題論理の Kripke モデル (Kripke model) は三つ組

\mathcal K=(W,\le,V)

であり、次を満たす。

$W$ は空でない集合であり、 $\le$ は $W$ 上の半順序である。
$V(p)\subseteq W$ は各命題変数 $p$ に対応する上方閉集合である。すなわち、 $w\in V(p)$ かつ $w\le v$ ならば $v\in V(p)$ である。

強制関係 $w\Vdash A$ を論理式の構造に関して次のように定める。

\begin{aligned} w\Vdash p&\iff w\in V(p),\\ w\nVdash\bot&\quad\text{は常に成り立つ},\\ w\Vdash A\land B&\iff w\Vdash A\ \text{かつ}\ w\Vdash B,\\ w\Vdash A\lor B&\iff w\Vdash A\ \text{または}\ w\Vdash B,\\ w\Vdash A\to B&\iff \forall v\ge w\,(v\Vdash A\Rightarrow v\Vdash B). \end{aligned}

$w\Vdash\Gamma$ は、すべての $A\in\Gamma$ について $w\Vdash A$ が成り立つことを表す。

含意の定義は現在の世界だけでなく、すべての将来の世界を量化する。特に、

w\Vdash\neg A \quad\Longleftrightarrow\quad \forall v\ge w\,v\nVdash A

である。

補題 2.2. 任意の Kripke モデル $\mathcal K$ 、世界 $w,v\in W$ 、および論理式 $A$ について、

w\le v\ \text{かつ}\ w\Vdash A \quad\Longrightarrow\quad v\Vdash A

である。

証明. $A$ の構造に関して帰納法を用いる。原子命題の場合は $V(p)$ の上方閉性から従う。 $\bot$ の場合は前件が成立しない。連言と選言の場合は、それぞれの直下の論理式へ帰納法の仮定を適用する。

$A=B\to C$ とし、 $w\Vdash B\to C$ かつ $w\le v$ と仮定する。 $v\le u$ かつ $u\Vdash B$ を満たす任意の $u$ を取る。推移性から $w\le u$ であるため、 $w\Vdash B\to C$ の定義により $u\Vdash C$ となる。従って、含意の定義から $v\Vdash B\to C$ である。すべての構文形について持続性を示した。▨

定義 2.3. $\Gamma\models_K A$ とは、任意の Kripke モデル $\mathcal K$ と任意の世界 $w$ について、 $w\Vdash\Gamma$ ならば $w\Vdash A$ であることをいう。 $\varnothing\models_K A$ を $\models_K A$ と略記する。

3 自然演繹の健全性

定理 3.1 (Kripke 意味論に関する健全性). 任意の有限前提集合 $\Gamma$ と論理式 $A$ について、

\Gamma\vdash_I A \quad\Longrightarrow\quad \Gamma\models_K A

である。

証明方針は、自然演繹の最後の規則に関する帰納法である。含意導入では将来世界へ移った後も前提が持続することを用いる。選言除去では、強制された選言の左右を場合分けし、対応する枝の帰納法の仮定を用いる。

証明. $\Gamma\vdash_I A$ の導出を一つ固定し、その導出木に関して帰納法を用いる。Kripke モデル $\mathcal K$ と $w\Vdash\Gamma$ を任意に取る。

$(\mathrm{Ax})$ の場合、 $A\in\Gamma$ なので $w\Vdash A$ である。

$(\land I)$ の場合、帰納法の仮定から $w\Vdash A$ かつ $w\Vdash B$ であり、強制の定義から $w\Vdash A\land B$ である。 $(\land E_1)$ と $(\land E_2)$ の場合は、 $w\Vdash A\land B$ の定義から対応する成分を得る。

$(\lor I_1)$ と $(\lor I_2)$ の場合は、帰納法の仮定から得た一方の選言肢を用いて $w\Vdash A\lor B$ を得る。

$(\lor E)$ の場合、最初の帰納法の仮定から $w\Vdash A\lor B$ である。強制の定義により、 $w\Vdash A$ または $w\Vdash B$ である。前者では $w\Vdash\Gamma\cup\{A\}$ なので、第2の枝に対する帰納法の仮定から $w\Vdash C$ を得る。後者では、第3の枝に対する帰納法の仮定から同じ結論を得る。二つの場合が選言の定義を尽くすため $w\Vdash C$ である。

$(\to I)$ の場合、直前の導出は $\Gamma\cup\{A\}\vdash_I B$ である。 $w\le v$ かつ $v\Vdash A$ を満たす任意の $v$ を取る。補題 2.2により、 $w\Vdash\Gamma$ から $v\Vdash\Gamma$ が従う。従って $v\Vdash\Gamma\cup\{A\}$ であり、帰納法の仮定から $v\Vdash B$ を得る。 $v$ は任意であるため、含意の定義から $w\Vdash A\to B$ である。

$(\to E)$ の場合、帰納法の仮定から $w\Vdash A\to B$ かつ $w\Vdash A$ である。含意の定義を $v=w$ に適用すると $w\Vdash B$ となる。

$(\bot E)$ の場合、帰納法の仮定は $w\Vdash\bot$ を与えるが、 $\bot$ を強制する世界は存在しない。従って、この場合の前件 $w\Vdash\Gamma$ は成立せず、含意は空虚に成り立つ。

すべての自然演繹規則について、 $w\Vdash\Gamma$ から結論の強制を導いた。モデルと世界は任意であったため $\Gamma\models_K A$ である。▨

4 古典論理で妥当な式の反例

排中律 $p\lor\neg p$ は古典命題論理では、 $p$ が真の場合と偽の場合の双方で真である。しかし、Kripke 世界では現在の情報が $p$ も $\neg p$ も支持しない場合がある。

例 4.1 (排中律に対する Kripke 反例). $W=\{w_0,w_1\}$ 、 $w_0<w_1$ とし、 $V(p)=\{w_1\}$ とする。 $V(p)$ は上方閉である。

$w_0\nVdash p$ である。また、 $w_1\ge w_0$ かつ $w_1\Vdash p$ なので、否定の定義から $w_0\nVdash\neg p$ である。従って

w_0\nVdash p\lor\neg p.

ゆえに $\nmodels_K p\lor\neg p$ である。定理 3.1の対偶により、 $\nvdash_I p\lor\neg p$ となる。

同じ二世界モデルは、二重否定除去にも反例を与える。

命題 4.2.

\nmodels_K\neg\neg p\to p

である。

証明. 上の二世界モデルを用いる。 $w_0$ 以上の世界で $\neg p$ を強制する世界は存在しない。実際、 $w_1\Vdash p$ なので $w_1\nVdash\neg p$ であり、 $w_0\nVdash\neg p$ は前例で確認した。従って $w_0\Vdash\neg\neg p$ である。一方、 $w_0\nVdash p$ である。含意の定義で $v=w_0$ を取ると、 $w_0\nVdash\neg\neg p\to p$ が従う。▨

古典論理の Hilbert 系は排中律と二重否定除去を導くが、直観主義自然演繹へ古典公理を移してはいない。Kripke 反例は、二つの体系の差が記号の違いではなく妥当な推論の違いであることを示す。

5 演習

問題 5.1. 次の問いに答えよ。

$w\Vdash A\to B$ の定義で、 $w$ だけでなくすべての $v\ge w$ を量化する理由を、強制の持続性と関連づけて説明せよ。
健全性の証明における $(\to I)$ の場合で、補題 2.2をどの前提へ適用したか。
排中律の反例で $w_0\nVdash\neg p$ となる理由を述べよ。

解答 (確認問題の解答).

1では、将来の情報状態で $A$ の証拠が得られた場合にも $B$ の証拠を与える必要があり、この定義によって含意自身も上方へ持続することを述べる。2では、 $w\Vdash\Gamma$ を $v\Vdash\Gamma$ へ移すために各前提へ持続性を用いる。3では、 $w_0$ の上に $p$ を強制する世界 $w_1$ が存在し、否定の定義が要求する「上方のどの世界も $p$ を強制しない」という条件が破れることを述べればよい。▨

6 境界と次の段階

本記事は自然演繹から Kripke 意味論への健全性を証明した。逆向きの完全性、Heyting 代数による意味論、および自然演繹の正規化は扱っていない。後続の記事は、本記事の含意導入と含意除去だけを単純型付きラムダ計算へ対応させる。

§E16.26直観主義論理

1 論理式と自然演繹

2 Kripke モデル

3 自然演繹の健全性

4 古典論理で妥当な式の反例

5 演習

6 境界と次の段階

参考文献

前提記事