§E16.26直観主義論理

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

証明.$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$である。すべての構文形について持続性を示した。▨

証明.$\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$である。▨

証明. 上の二世界モデルを用いる。$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$が従う。▨