§E16.4命題論理の証明体系

証明. 次の各行は H1 または H2 の代入例と modus ponens からなる。

ゆえに主張が成り立つ。▨

証明. 左辺を仮定し、$\delta_1,\ldots,\delta_k=\beta$を対応する導出とする。各$i$について$\Gamma\vdash_{\mathrm{PL}}\alpha\to\delta_i$を示す。

$\delta_i=\alpha$の場合は補題 1.4を用いる。$\delta_i\in\Gamma$または$\delta_i$が公理の代入例である場合、まず$\Gamma\vdash_{\mathrm{PL}}\delta_i$であり、H1 の代入例

と modus ponens によって$\Gamma\vdash_{\mathrm{PL}}\alpha\to\delta_i$を得る。

$\delta_i$が$\delta_j$と$\delta_j\to\delta_i$から得られた場合、帰納法の仮定は

を与える。H2 と二回の modus ponens により$\Gamma\vdash_{\mathrm{PL}}\alpha\to\delta_i$を得る。有限列に関する帰納法の末項で$\Gamma\vdash_{\mathrm{PL}}\alpha\to\beta$となる。

逆に$\Gamma\vdash_{\mathrm{PL}}\alpha\to\beta$とする。前提を増やしても同じ導出を用いることができ、$\Gamma\cup\{\alpha\}$では$\alpha$も前提である。modus ponens により$\Gamma\cup\{\alpha\}\vdash_{\mathrm{PL}}\beta$である。▨

証明.$\Gamma$からの$\varphi$の導出を一つ固定する。導出は有限列であるから、定義 1.2の第1条件によって正当化される項として現れる$\Gamma$の要素は有限個である。それらの集合を$\Gamma_0$とすると、同じ有限列の各項は$\Gamma_0$の要素、公理の代入例、または先行する二項への modus ponens のいずれかである。したがって同じ列が$\Gamma_0$からの導出であり、$\Gamma_0\vdash_{\mathrm{PL}}\varphi$が成り立つ。▨

証明. まず二つの派生操作を準備する。$\vdash\rho\to\sigma$と$\vdash\sigma\to\tau$から$\vdash\rho\to\tau$を得ることができる。実際、H1 と modus ponens により$\rho\to(\sigma\to\tau)$を得て、H2 と$\rho\to\sigma$へ modus ponens を適用すればよい。以下ではこの有限導出を含意の推移と呼ぶ。また、仮定$\rho$と$\rho\to\sigma$から$\sigma$を得て演繹定理を二回適用すると

を得る。

二重否定除去を導く。$\theta=\alpha\to(\alpha\to\alpha)$と置くと、$\theta$は H1 の代入例である。H3 の二つの代入例

と含意の推移から

を得る。H1 は$\neg\neg\alpha\to(\neg\neg\theta\to\neg\neg\alpha)$を与えるので、再び含意の推移を用いて

を得る。(A) を$\rho=\theta,\sigma=\alpha$として用い、定理$\theta$に modus ponens を適用すると$(\theta\to\alpha)\to\alpha$を得る。したがって含意の推移により

である。(B) で$\alpha$を$\neg\alpha$に置き換え、H3 の代入例

へ modus ponens を適用すると D1 を得る。

D2 を示す。H1 の代入例$\neg\alpha\to(\neg\beta\to\neg\alpha)$と H3

を含意の推移で結べばよい。

次に対偶化

を導く。$\alpha\to\beta$を仮定する。(B)、仮定、D1 を含意の推移で結ぶと$\neg\neg\alpha\to\neg\neg\beta$を得る。H3 の代入例

へ modus ponens を適用し、演繹定理で仮定を外すと (C) を得る。

(A) は$\alpha\to((\alpha\to\beta)\to\beta)$を与える。(C) で前件を$\alpha\to\beta$、後件を$\beta$とすると

を得る。この式を (A) と含意の推移で結ぶと D3 が従う。

最後に D4 を示す。$U=\alpha\to\chi$と$V=\neg\alpha\to\chi$を仮定する。さらに$\neg\chi$を仮定する。(C) を$V$に適用すると$\neg\neg\alpha$を得て、(B) により$\alpha$を得る。D3 から$\neg\chi\to\neg U$を得るので、追加した仮定$\neg\chi$から$\neg U$を得る。演繹定理により

である。H3 の代入例$(\neg\chi\to\neg U)\to(U\to\chi)$に modus ponens を適用し、仮定$U$も用いると$\chi$を得る。演繹定理で$V$、次に$U$を外すと D4 を得る。

以上の各段階は H1–H3、modus ponens、証明済みの演繹定理の有限回の適用である。▨

証明.$\delta_1,\ldots,\delta_k=\varphi$を$\Gamma$からの導出とし、$\Gamma$のすべての論理式を真にする付値$v$を任意に取る。各$i$について$v\models\delta_i$を帰納的に示す。

前提の行は$v$の選択により真である。H1 と H2 は含意が偽になる場合を調べれば恒真である。H3 が偽であると仮定すると、$\neg\beta\to\neg\alpha$は真、$\alpha$は真、$\beta$は偽である。後二条件から$\neg\beta$は真で$\neg\alpha$は偽となり、最初の含意が偽になるので矛盾する。したがって H3 も恒真である。

modus ponens の行では、$v\models\alpha$と$v\models\alpha\to\beta$から含意の真理値規則により$v\models\beta$が従う。ゆえに末項$\varphi$も真である。$v$は任意であるから$\Gamma\models_{\mathrm{PL}}\varphi$である。▨

証明.$\theta$に関する構造帰納法を用いる。$\theta=p_i$の場合、$p_i^a$は$\Delta_a$の元である。

$\theta=\neg\alpha$とする。$v_a\models\neg\alpha$なら$\theta^a=\neg\alpha$であり、帰納法の仮定が同じ式を与える。$v_a\not\models\neg\alpha$なら$v_a\models\alpha$である。帰納法の仮定から$\Delta_a\vdash\alpha$を得て、D1 と modus ponens により$\Delta_a\vdash\neg\neg\alpha=\theta^a$を得る。

$\theta=\alpha\to\beta$とする。$v_a\models\theta$で$v_a\models\beta$の場合、帰納法の仮定から$\beta$を得る。H1 と modus ponens により$\alpha\to\beta$を得る。$v_a\models\theta$で$v_a\not\models\alpha$の場合、帰納法の仮定から$\neg\alpha$を得る。D2 と modus ponens により$\alpha\to\beta$を得る。含意が真である場合はこの二場合の少なくとも一方である。

$v_a\not\models\theta$の場合、$v_a\models\alpha$かつ$v_a\not\models\beta$である。帰納法の仮定は$\alpha$と$\neg\beta$の導出を与える。D3 と二回の modus ponens により$\neg(\alpha\to\beta)=\theta^a$を得る。▨

証明. まず、恒真な論理式$\chi$は証明可能であることを示す。$\chi$に現れる変数を$p_1,\ldots,p_n$とする。各$a\in\mathbf2^n$について、補題 4.2は$\Delta_a\vdash\chi$を与える。

$p_n$以外の符号付きリテラルを固定する。$p_n=1$の行と$p_n=0$の行に演繹定理を適用すると、残りのリテラルから$p_n\to\chi$と$\neg p_n\to\chi$を導くことができる。D4 と二回の modus ponens により、残りのリテラルだけから$\chi$を導く。$p_n,p_{n-1},\ldots,p_1$の順に同じ操作を繰り返すと$\vdash\chi$を得る。

$\Gamma=\{\gamma_1,\ldots,\gamma_m\}$とする。$\Gamma\models_{\mathrm{PL}}\varphi$なら、右結合した論理式

は恒真である。実際、いずれかの$\gamma_i$が偽なら対応する含意が真となり、すべてが真なら仮定から$\varphi$が真となる。前半により$\vdash\chi$である。$\gamma_1,\ldots,\gamma_m$を前提として順に modus ponens を適用すれば$\Gamma\vdash\varphi$を得る。$m=0$の場合は前半そのものである。▨

証明.$\Gamma=\bigcup_{i\in I}\Gamma_i$と置き、ある$\psi$について$\Gamma\vdash_{\mathrm{PL}}\psi$かつ$\Gamma\vdash_{\mathrm{PL}}\neg\psi$であると仮定する。系 1.6を二つの導出へ適用すると、有限部分集合$\Delta_1,\Delta_2\subseteq\Gamma$で$\Delta_1\vdash_{\mathrm{PL}}\psi$と$\Delta_2\vdash_{\mathrm{PL}}\neg\psi$を満たすものが存在する。$\Delta=\Delta_1\cup\Delta_2$は$\Gamma$の有限部分集合である。

$\Delta$が空である場合には、族が空でないことから要素$\Gamma_{i_0}$を一つ取る。$\Delta$が空でない場合には、$\Delta$の各要素についてそれを含む$\Gamma_i$を一つずつ取り、有限個の添字を得る。この取り出しは有限個の対象についての選択であり、有限個の選択は ZF のもとで有限回の存在量化子の除去として行うことができるので、選択原理には当たらない。族は包含関係で全順序付けられているから、この有限個の集合には包含関係についての最大元が存在する。それを$\Gamma_{i_0}$とする。どちらの場合にも$\Delta\subseteq\Gamma_{i_0}$である。

前提を増やしても同じ導出を用いることができるので、$\Gamma_{i_0}\vdash_{\mathrm{PL}}\psi$かつ$\Gamma_{i_0}\vdash_{\mathrm{PL}}\neg\psi$となる。これは$\Gamma_{i_0}$が構文的に無矛盾であることに反する。▨

証明.$\Gamma$を含む構文的に無矛盾な$\operatorname{Form}(P)$の部分集合全体を$\mathcal C$とし、包含関係で順序づける。$\Gamma$自身が$\mathcal C$に属するので$\mathcal C$は空でない。

$\mathcal C$に含まれる鎖$\mathcal D$を任意に取る。$\mathcal D$が空なら、$\Gamma$が$\mathcal D$の上界である。$\mathcal D$が空でないなら、補題 5.2により$\bigcup\mathcal D$は構文的に無矛盾であり、$\mathcal D$の各要素が$\Gamma$を含むので$\bigcup\mathcal D$も$\Gamma$を含む。したがって$\bigcup\mathcal D$は$\mathcal C$に属し、$\mathcal D$の上界である。

Zorn の補題（§E1.20 定理 2.1の§E1.20 定理 2.1 (3)）を$\mathcal C$へ適用すると、極大元$\Gamma^*$が存在する。$\Gamma^*$は構文的に無矛盾であり$\Gamma$を含む。$\Gamma^*\subsetneq\Gamma'\subseteq\operatorname{Form}(P)$を満たす構文的に無矛盾な$\Gamma'$が存在すれば、$\Gamma'$も$\Gamma$を含むので$\Gamma'$は$\mathcal C$に属し、$\mathcal C$における$\Gamma^*$の極大性に反する。ゆえに$\Gamma^*$は定義 5.3の意味で極大無矛盾である。▨

証明.(1)を示す。$\sigma\in\Gamma^*$なら、一項だけからなる列$\sigma$が$\Gamma^*$からの導出である。逆に、$\Gamma^*\vdash_{\mathrm{PL}}\sigma$かつ$\sigma\notin\Gamma^*$と仮定する。$\Gamma^*\cup\{\sigma\}$が構文的に無矛盾でないとすると、ある$\psi$について$\Gamma^*\cup\{\sigma\}\vdash_{\mathrm{PL}}\psi$かつ$\Gamma^*\cup\{\sigma\}\vdash_{\mathrm{PL}}\neg\psi$である。定理 1.5 (演繹定理)により$\Gamma^*\vdash_{\mathrm{PL}}\sigma\to\psi$かつ$\Gamma^*\vdash_{\mathrm{PL}}\sigma\to\neg\psi$であり、仮定$\Gamma^*\vdash_{\mathrm{PL}}\sigma$とあわせて modus ponens を適用すると$\Gamma^*\vdash_{\mathrm{PL}}\psi$かつ$\Gamma^*\vdash_{\mathrm{PL}}\neg\psi$となって、$\Gamma^*$の無矛盾性に反する。したがって$\Gamma^*\cup\{\sigma\}$は構文的に無矛盾である。$\sigma\notin\Gamma^*$から$\Gamma^*\subsetneq\Gamma^*\cup\{\sigma\}$であるから、これは$\Gamma^*$の極大性に反する。ゆえに$\sigma\in\Gamma^*$である。

(2)を示す。$\sigma$と$\neg\sigma$が両方$\Gamma^*$に属するなら、どちらも一項の導出をもつので$\Gamma^*$の無矛盾性に反する。次に$\sigma\notin\Gamma^*$とする。極大性により$\Gamma^*\cup\{\sigma\}$は構文的に無矛盾でないから、ある$\psi$について$\Gamma^*\cup\{\sigma\}\vdash_{\mathrm{PL}}\psi$かつ$\Gamma^*\cup\{\sigma\}\vdash_{\mathrm{PL}}\neg\psi$である。補題 2.1の D2 を$\alpha=\psi$、$\beta=\neg\sigma$として得る

へ二回の modus ponens を適用すると、$\Gamma^*\cup\{\sigma\}\vdash_{\mathrm{PL}}\neg\sigma$である。演繹定理により$\Gamma^*\vdash_{\mathrm{PL}}\sigma\to\neg\sigma$を得る。D4 を$\alpha=\sigma$、$\chi=\neg\sigma$として得る

と、補題 1.4が与える$\vdash_{\mathrm{PL}}\neg\sigma\to\neg\sigma$へ二回の modus ponens を適用すると$\Gamma^*\vdash_{\mathrm{PL}}\neg\sigma$を得る。(1)により$\neg\sigma\in\Gamma^*$である。したがって、ちょうど一方が$\Gamma^*$に属する。

(3)を示す。$\tau\in\Gamma^*$の場合、H1 の代入例$\tau\to(\sigma\to\tau)$と modus ponens により$\Gamma^*\vdash_{\mathrm{PL}}\sigma\to\tau$であり、(1)から$\sigma\to\tau\in\Gamma^*$である。$\sigma\notin\Gamma^*$の場合、(2)により$\neg\sigma\in\Gamma^*$であり、D2 の代入例$\neg\sigma\to(\sigma\to\tau)$と modus ponens により同じ結論を得る。逆に$\sigma\to\tau\in\Gamma^*$とする。$\sigma\in\Gamma^*$なら、modus ponens により$\Gamma^*\vdash_{\mathrm{PL}}\tau$であり、(1)から$\tau\in\Gamma^*$である。ゆえに$\sigma\notin\Gamma^*$または$\tau\in\Gamma^*$が成り立つ。▨

証明.定理 5.4 (Lindenbaum の補題)により、$\Gamma$を含む極大無矛盾な集合$\Gamma^*$を取る。付値$v:P\to\mathbf2$を

と定める。各論理式$\varphi$について、$\widehat v(\varphi)=1$であることと$\varphi\in\Gamma^*$であることが同値である、という条件を考える。この条件を満たす論理式全体の集合を$A$とし、$A=\operatorname{Form}(P)$を§E16.1 定理 1.3によって示す。以下では補題 5.5の各項を用いる。

$\varphi$が命題変数$p$である場合、$\widehat v(p)=v(p)$であり、$v$の定義から$v(p)=1$であることと$p\in\Gamma^*$であることは同値である。ゆえに$p\in A$である。

$\varphi\in A$とする。$\widehat v(\neg\varphi)=1-\widehat v(\varphi)$であるから、$\widehat v(\neg\varphi)=1$であることと$\widehat v(\varphi)=0$であることは同値である。$\varphi\in A$により、後者は$\varphi\notin\Gamma^*$と同値である。補題 5.5 (2)により、これは$\neg\varphi\in\Gamma^*$と同値である。ゆえに$\neg\varphi\in A$である。

$\varphi,\psi\in A$とする。含意の真理値規則により、$\widehat v(\varphi\to\psi)=1$であることと、$\widehat v(\varphi)=0$または$\widehat v(\psi)=1$であることは同値である。$\varphi,\psi\in A$により、後者は$\varphi\notin\Gamma^*$または$\psi\in\Gamma^*$と同値である。補題 5.5 (3)により、これは$(\varphi\to\psi)\in\Gamma^*$と同値である。ゆえに$(\varphi\to\psi)\in A$である。

構造帰納法により$A=\operatorname{Form}(P)$である。$\Gamma\subseteq\Gamma^*$であるから、各$\gamma\in\Gamma$について$\gamma\in\Gamma^*$であり、したがって$\widehat v(\gamma)=1$、すなわち$v\models\gamma$である。ゆえに$v$は$\Gamma$のすべての論理式を真にする。▨

証明. 左から右は定理 3.1 (Hilbert 系の健全性)である。

右から左を示す。$\Gamma\models_{\mathrm{PL}}\varphi$とする。§E16.1 命題 3.2 (2)により、$\Gamma\cup\{\neg\varphi\}$のすべての論理式を真にする付値は存在しない。定理 6.1の対偶により、$\Gamma\cup\{\neg\varphi\}$は構文的に無矛盾でない。すなわち、ある$\psi$について

が成り立つ。補題 2.1の D2 を$\alpha=\psi$、$\beta=\varphi$として得る$\neg\psi\to(\psi\to\varphi)$へ二回の modus ponens を適用すると、$\Gamma\cup\{\neg\varphi\}\vdash_{\mathrm{PL}}\varphi$である。定理 1.5 (演繹定理)により$\Gamma\vdash_{\mathrm{PL}}\neg\varphi\to\varphi$を得る。

D4 を$\alpha=\varphi$、$\chi=\varphi$として得る

と、補題 1.4が与える$\vdash_{\mathrm{PL}}\varphi\to\varphi$へ二回の modus ponens を適用すると$\Gamma\vdash_{\mathrm{PL}}\varphi$を得る。▨

証明. まず$\Sigma$が構文的に無矛盾であることを示す。ある$\psi$について$\Sigma\vdash_{\mathrm{PL}}\psi$かつ$\Sigma\vdash_{\mathrm{PL}}\neg\psi$であると仮定する。系 1.6を二つの導出へ適用すると、有限部分集合$\Delta_1,\Delta_2\subseteq\Sigma$で$\Delta_1\vdash_{\mathrm{PL}}\psi$と$\Delta_2\vdash_{\mathrm{PL}}\neg\psi$を満たすものが存在する。$\Delta=\Delta_1\cup\Delta_2$は$\Sigma$の有限部分集合であり、前提を増やしても同じ導出を用いることができるので$\Delta\vdash_{\mathrm{PL}}\psi$かつ$\Delta\vdash_{\mathrm{PL}}\neg\psi$である。

仮定により、$\Delta$のすべての論理式を真にする付値$w$が存在する。定理 3.1 (Hilbert 系の健全性)により$\widehat w(\psi)=1$かつ$\widehat w(\neg\psi)=1$となるが、$\widehat w(\neg\psi)=1-\widehat w(\psi)$であるから、これは成り立たない。したがって$\Sigma$は構文的に無矛盾である。

定理 6.1により、$\Sigma$のすべての論理式を真にする付値が存在する。ゆえに$\Sigma$は充足可能である。▨