排中律
概要
排中律（law of excluded middle）とは、どの命題 $P$ についても「$P$ であるか $P$ でないか」のどちらかが成り立つという原理で、論理式 $P\lor\lnot P$ で表され、直観主義論理に公理図式として加えると古典論理になる。直観主義論理では一般には証明できないが否定もできず、命題論理では、排中律を使って証明できる式は二重否定を付ければ排中律なしで証明できる（Glivenko の定理）。弱い排中律 $\lnot P\lor\lnot\lnot P$ は De Morgan の法則の片側と同値で排中律より真に弱く、直観主義論理の上の集合論では選択公理が排中律を導く（Diaconescu の定理）。
「どんな命題 $P$ についても、$P$ であるか $P$ でないかのどちらかである」という原理を 排中律（law of excluded middle）という。論理式では $P\lor\lnot P$ と書く。通常の数学は排中律を自由に使う。「$P$ のときは…、$P$ でないときは…」という場合分けや背理法はその典型である。排中律を使うと、どちらの場合が実際に起きているかを決めないまま結論を出せる。その代わり、存在を主張する定理を証明しても、存在する対象を具体的に示さないことがある。
排中律を一般の原理としては認めない論理が直観主義論理であり、そこに排中律を加えると古典論理になる。この記事では排中律を定義し、何を主張して何を主張しないかを例で確かめたうえで、次の 3 つを証明する。命題論理では、排中律を使って証明できる式は、二重否定を付ければ排中律なしで証明できる（Glivenko の定理）。弱い排中律 $\lnot P\lor\lnot\lnot P$ は De Morgan の法則の片側と同値で、排中律より真に弱い。直観主義論理の上で集合論を展開するとき、選択公理は排中律を導く（Diaconescu の定理）。
定義
記法は 直観主義論理 の記事に合わせる。命題論理の論理式は、命題変数と定数 $\bot$（矛盾）から結合子 $\land,\lor,\to$ で作り、否定を $\lnot\varphi:=(\varphi\to\bot)$ で定める。同記事の定義「直観主義命題論理の公理系」の公理 1〜7 と前件肯定による導出可能性を $\Gamma\vdash_{\mathrm{I}}\varphi$ と書き、公理の番号もその定義に従う。
論理式 $\varphi$ について、論理式 $\varphi\lor\lnot\varphi$ を $\varphi$ についての 排中律（law of excluded middle）という。すべての論理式 $\varphi$ について $\varphi\lor\lnot\varphi$ を公理とすることを、公理図式としての排中律 という。直観主義命題論理の公理 1〜7 に公理図式としての排中律を加えた体系での導出可能性を $\Gamma\vdash_{\mathrm{C}}\varphi$ と書く。
述語論理では、自由変数 $x_1,\dots,x_n$ をもつ論理式 $\varphi$ について $\forall x_1\cdots\forall x_n\,(\varphi\lor\lnot\varphi)$ を排中律という。
$\vdash_{\mathrm{C}}$ は古典命題論理の導出可能性であり、$\vdash_{\mathrm{C}}\varphi$ は $\varphi$ が恒真式であることと同値である（直観主義論理 の記事の定義「直観主義命題論理の公理系」の直後の段落）。排中律の代わりに二重否定除去 $\lnot\lnot\varphi\to\varphi$ や Peirce の法則 $((\varphi\to\psi)\to\varphi)\to\varphi$ を公理図式として加えても、証明できる式は変わらない（同記事の命題「排中律と二重否定除去」と注意「Peirce の法則」。排中律と二重否定除去の同値は OLT26 Theorem 24.2 にもある）。
- 論理式の集合 $T$ と論理式 $\varphi$ について、$T\vdash_{\mathrm{I}}\varphi\lor\lnot\varphi$ のとき、$\varphi$ は $T$ のもとで 決定可能（decidable）であるという。
- 論理式 $\lnot\varphi\lor\lnot\lnot\varphi$ を $\varphi$ についての 弱い排中律（weak law of excluded middle）という。
古典論理ではどの式も決定可能である。
- 無矛盾律 $\lnot(\varphi\land\lnot\varphi)$ は直観主義論理で証明できる。公理 3 により $\varphi\land\lnot\varphi\vdash_{\mathrm{I}}\varphi$ かつ $\varphi\land\lnot\varphi\vdash_{\mathrm{I}}\lnot\varphi$ なので、前件肯定で $\varphi\land\lnot\varphi\vdash_{\mathrm{I}}\bot$ となり、直観主義論理 の記事の命題「演繹定理」により $\vdash_{\mathrm{I}}\lnot(\varphi\land\lnot\varphi)$ である。「$\varphi$ と $\lnot\varphi$ が同時に成り立つことはない」と「$\varphi$ と $\lnot\varphi$ の少なくとも一方が成り立つ」は別の主張であり、排中律は後者である。
- 二値原理 は、「各命題の真理値は真と偽のちょうど一方である」という意味論の主張である。排中律は論理式についての主張であり、二値原理とは別のものである。真理値を一般の Boole代数 の元にとると、排中律はつねに最大元 $1$ を値にとるが、命題そのものの値は $0$ でも $1$ でもないことがある（ex-lem-boolean）。
直感
直観主義論理 の記事の注意「証明による意味づけ（BHK 解釈）」の読み方では、$\varphi\lor\psi$ の証明は「どちらを証明するかの指定」とその証明の組である。したがって $\varphi\lor\lnot\varphi$ の証明とは、$\varphi$ を証明するか反駁するかを実際に決めることであり、排中律を公理図式として認めることは、すべての命題についてそれができると主張することになる。この読み方では、排中律は「真理は私たちが知っているかどうかと無関係に決まっている」という前提の表明であり、自明な論理法則ではない。
一方で、排中律を否定することもできない。$\lnot\lnot(\varphi\lor\lnot\varphi)$ は直観主義論理で証明できる（同記事の命題「直観主義論理で証明できる式」の 4、OLT26 Example 58.7）。「$\varphi$ でも $\lnot\varphi$ でもない」と仮定すると、$\lnot\varphi$ が出て、それが $\lnot\varphi$ でないことと矛盾するからである。排中律を認めない立場は、排中律が偽だと言うのではなく、すべての式についての一様な証明がないと言うのである。後で示す Glivenko の定理は、この観察を命題論理全体に広げたものになっている。
例
実数 $x$ について、「$x+\sqrt2$ と $x-\sqrt2$ の少なくとも一方は無理数である」。実際、両方が有理数なら差 $(x+\sqrt2)-(x-\sqrt2)=2\sqrt2$ が有理数になり、$\sqrt2$ が有理数でないこと（有理数 の記事の命題「2の平方根は有理数でない」）に反する。
この証明が直接示すのは、$A$ を「$x+\sqrt2$ は有理数」、$B$ を「$x-\sqrt2$ は有理数」として $\lnot(A\land B)$ である。結論 $\lnot A\lor\lnot B$ を得るには De Morgan の法則の片側 $\lnot(A\land B)\to(\lnot A\lor\lnot B)$ を使っており、これは排中律なしには証明できない（De Morganの法則 の記事の「例と反例」の節）。後の prop-lem-weak-demorgan によれば、ここで必要なのは $A$ についての弱い排中律 $\lnot A\lor\lnot\lnot A$ である。$x=\sqrt2$ のように $x$ が具体的に分かっていればどちらが無理数かも分かる（$x-\sqrt2=0$ は有理数なので $x+\sqrt2=2\sqrt2$ が無理数）が、証明そのものはその情報を含まない。
自然数 $n$ について、$n$ が $4$ 以上の偶数で $2$ つの素数の和で表せず、しかも $4\le m< n$ を満たすすべての偶数 $m$ が $2$ つの素数の和で表せるとき $a_n:=1$、そうでないとき $a_n:=0$ とする。各 $a_n$ は有限回の計算で決まり、$a_n=1$ となる $n$ は高々 $1$ つ（$2$ つの素数の和で表せない最小の偶数）である。
$$
r:=\sum_{n=0}^{\infty}a_n2^{-n}
$$
とおくと、$0\le r\le1$ であり、$\left\lvert r-\sum_{n=0}^{N}a_n2^{-n}\right\rvert\le\sum_{n>N}2^{-n}=2^{-N}$ なので、$r$ はいくらでも精密に計算できる。さらに $r=0$ であることは、すべての $a_n$ が $0$ であること、すなわち $4$ 以上のすべての偶数が $2$ つの素数の和で表せること（Goldbach予想）と同値である。$2$ つの素数の和で表せない偶数があれば、その最小のものを $n_0$ として $r=2^{-n_0}>0$ だからである。
したがって排中律の例 $r=0\lor r\ne0$ を BHK 解釈の意味で証明することは、Goldbach 予想を証明するか反証することにほかならない。OLT26 §58.3 は、証明も反証もされていない命題の例として Goldbach 予想を挙げ、こうした命題のために排中律は一般には主張できないと説明している。もちろん古典論理では $r=0\lor r\ne0$ は正しく、$\lnot\lnot(r=0\lor r\ne0)$ は直観主義論理でも成り立つ。
- $\vdash_{\mathrm{I}}\varphi$ なら公理 5 により $\vdash_{\mathrm{I}}\varphi\lor\lnot\varphi$、$\vdash_{\mathrm{I}}\lnot\varphi$ でも同様である。たとえば $\bot\lor\lnot\bot$ は証明できる（直観主義論理 の記事の例「直観主義論理で証明できる式」の 5）。排中律の個々の例が証明できることはある。
- 「$n$ は素数である」のように、有限回の計算で真偽が決まる性質では、BHK 解釈の意味での「どちらであるかの指定」は計算そのものが与える。場合分けを計算の手順に置き換えられる。
- 自己停止集合 $K$（停止問題 の記事の定義「停止問題」）について、各 $e$ で $e\in K\lor e\notin K$ は古典的に正しいが、$e$ を受け取ってどちらかを答える Turing 機械は存在しない（同記事の定理「停止問題の決定不能性」）。BHK 解釈の「指定」を計算可能な手続きと読むと、$\forall e\,(e\in K\lor e\notin K)$ には一様な証明がない。この読み方を正確にした話題は 計算可能性理論 と結びつく。
$X=\{1,2\}$ の冪集合 $B=\{\emptyset,\{1\},\{2\},X\}$ は、和集合・共通部分・補集合で 4 元の Boole 代数になる（最小元 $\emptyset$、最大元 $X$）。命題変数 $p$ に $\{1\}$ を割り当てると、古典論理 の記事の定義「Boole 代数での値」の意味で
$$
[\![p\lor\lnot p]\!]=\{1\}\cup\{2\}=X
$$
であり、排中律は最大元をとる。$p\lor\lnot p$ は恒真式なので、これはどの Boole 代数・どの付値でも同じである（同記事の定理「Boole 代数に関する妥当性」）。しかし $p$ 自身の値 $\{1\}$ は最小元でも最大元でもない。
これに対し、3 元の鎖 $\{0< h<1\}$ を Heyting代数 とみて $p$ に $h$ を割り当てると、$p\lor\lnot p$ の値は $h\ne1$ である（直観主義論理 の記事の例「反例：3 元の鎖と排中律」）。排中律が成り立つかどうかを分けるのは、真理値の個数ではなく、各元が補元をもつ（Boole 代数である）かどうかである。
性質
二重否定と Glivenko の定理
排中律を使った証明から排中律を取り除くとき、結論に二重否定を付ければ足りる。その鍵は、二重否定が前件肯定と両立することである。
任意の論理式 $\varphi,\psi$ について
$$
\vdash_{\mathrm{I}}\lnot\lnot(\varphi\to\psi)\to(\lnot\lnot\varphi\to\lnot\lnot\psi)
$$
である。
$\Gamma:=\{\lnot\lnot(\varphi\to\psi),\ \lnot\lnot\varphi,\ \lnot\psi\}$ とおく。$\Gamma,\varphi\to\psi,\varphi$ からは前件肯定で $\psi$ が出て、$\lnot\psi$ と合わせて $\bot$ が出る。演繹定理（直観主義論理 の記事の命題「演繹定理」）により $\Gamma,\varphi\to\psi\vdash_{\mathrm{I}}\lnot\varphi$ であり、これと $\lnot\lnot\varphi=(\lnot\varphi\to\bot)$ から $\Gamma,\varphi\to\psi\vdash_{\mathrm{I}}\bot$ となる。再び演繹定理により $\Gamma\vdash_{\mathrm{I}}\lnot(\varphi\to\psi)$ であり、$\lnot\lnot(\varphi\to\psi)$ と合わせて $\Gamma\vdash_{\mathrm{I}}\bot$ である。演繹定理を 3 回使うと
$$
\vdash_{\mathrm{I}}\lnot\lnot(\varphi\to\psi)\to\bigl(\lnot\lnot\varphi\to(\lnot\psi\to\bot)\bigr)
$$
を得る。$\lnot\psi\to\bot$ は $\lnot\lnot\psi$ そのものである。$\square$
命題論理の論理式 $\varphi$ について、$\vdash_{\mathrm{C}}\varphi$ であることと $\vdash_{\mathrm{I}}\lnot\lnot\varphi$ であることは同値である。
主張は 直観主義論理 の記事の定理「Glivenko の定理」と同じである。
$\vdash_{\mathrm{C}}\varphi$ とし、$\varphi$ で終わる導出 $\chi_1,\dots,\chi_m$ をとる。各 $\chi_k$ は公理 1〜7 のどれかであるか、排中律 $\psi\lor\lnot\psi$ の形であるか、前の 2 つから前件肯定で得られる。$k$ についての帰納法で $\vdash_{\mathrm{I}}\lnot\lnot\chi_k$ を示す。
- $\chi_k$ が公理 1〜7 のどれかなら $\vdash_{\mathrm{I}}\chi_k$ である。直観主義論理 の記事の命題「直観主義論理で証明できる式」の 1 により $\vdash_{\mathrm{I}}\chi_k\to\lnot\lnot\chi_k$ なので、前件肯定で $\vdash_{\mathrm{I}}\lnot\lnot\chi_k$ である。
- $\chi_k=\psi\lor\lnot\psi$ なら、同じ命題の 4 により $\vdash_{\mathrm{I}}\lnot\lnot(\psi\lor\lnot\psi)$ である。
- $\chi_k$ が $\chi_i$ と $\chi_j=(\chi_i\to\chi_k)$（$i,j< k$）から前件肯定で得られたなら、帰納法の仮定により $\vdash_{\mathrm{I}}\lnot\lnot\chi_i$ かつ $\vdash_{\mathrm{I}}\lnot\lnot(\chi_i\to\chi_k)$ である。lem-lem-nn-mp の $\varphi:=\chi_i$、$\psi:=\chi_k$ の場合に前件肯定を 2 回使って $\vdash_{\mathrm{I}}\lnot\lnot\chi_k$ を得る。
$k=m$ として $\vdash_{\mathrm{I}}\lnot\lnot\varphi$ である。
逆に $\vdash_{\mathrm{I}}\lnot\lnot\varphi$ とする。公理 1〜7 は古典論理の体系にも含まれるので $\vdash_{\mathrm{C}}\lnot\lnot\varphi$ である。直観主義論理 の記事の命題「排中律と二重否定除去」の証明の前半により $\vdash_{\mathrm{C}}\lnot\lnot\varphi\to\varphi$ なので、前件肯定で $\vdash_{\mathrm{C}}\varphi$ である。$\square$
証明は、古典論理の導出の各行に $\lnot\lnot$ を付けると直観主義論理の導出の骨組みになることを示している。排中律の行は、直観主義論理で証明できる $\lnot\lnot(\psi\lor\lnot\psi)$ に置き換わる。
命題論理の論理式について、次が成り立つ。
- $\vdash_{\mathrm{C}}\lnot\psi$ であることと $\vdash_{\mathrm{I}}\lnot\psi$ であることは同値である。否定の形の結論を示すときは、排中律を使わなくてよい。
- $\vdash_{\mathrm{C}}\bot$ であることと $\vdash_{\mathrm{I}}\bot$ であることは同値である。特に、直観主義命題論理に公理図式としての排中律を加えても矛盾は生じない。
- $\varphi$ が恒真式なら $\vdash_{\mathrm{I}}\lnot\lnot\varphi$ である。
1 は thm-lem-glivenko と $\lnot\lnot\lnot\psi\to\lnot\psi$ から、2 は $\lnot\bot$ が証明可能であることから、3 は恒真式が古典論理で証明可能であることから従う。
詳細
1. $\vdash_{\mathrm{C}}\lnot\psi$ なら thm-lem-glivenko により $\vdash_{\mathrm{I}}\lnot\lnot\lnot\psi$ であり、直観主義論理 の記事の命題「直観主義論理で証明できる式」の 3（$\lnot\lnot\lnot\psi\to\lnot\psi$）と前件肯定で $\vdash_{\mathrm{I}}\lnot\psi$ である。逆向きは公理 1〜7 が古典論理の体系にも含まれることによる。
2. $\vdash_{\mathrm{C}}\bot$ なら thm-lem-glivenko により $\vdash_{\mathrm{I}}\lnot\lnot\bot$、すなわち $\vdash_{\mathrm{I}}(\lnot\bot)\to\bot$ である。$\lnot\bot=(\bot\to\bot)$ は証明可能（同記事の命題「演繹定理」の証明の冒頭の $\varphi\to\varphi$）なので、前件肯定で $\vdash_{\mathrm{I}}\bot$ である。逆向きは 1 と同じ理由による。直観主義命題論理では $\bot$ が証明できない（同記事の系「直観主義論理で証明できない式」）ので、$\vdash_{\mathrm{C}}\bot$ でもない。
3. 恒真式は古典命題論理で証明可能である（def-lem-main の直後の段落）ので、thm-lem-glivenko による。$\square$
述語論理では、結論全体に二重否定を付けるだけでなく、原子論理式・選言・存在記号に二重否定を入れる Gödel–Gentzen の二重否定翻訳 $\varphi\mapsto\varphi^N$ を使い、$\varphi$ が古典論理で証明可能なら $\varphi^N$ は直観主義論理で証明可能である（OLT26 Theorem 24.3）。
弱い排中律と De Morgan の法則
ex-lem-sqrt2 で使った De Morgan の法則の片側は、排中律のすべてを必要とするわけではない。
任意の論理式 $\varphi,\psi$ について、次が成り立つ。
- $\lnot\varphi\lor\lnot\lnot\varphi\vdash_{\mathrm{I}}\lnot(\varphi\land\psi)\to(\lnot\varphi\lor\lnot\psi)$。
- $\lnot(\varphi\land\lnot\varphi)\to(\lnot\varphi\lor\lnot\lnot\varphi)\vdash_{\mathrm{I}}\lnot\varphi\lor\lnot\lnot\varphi$。
したがって、直観主義命題論理に公理図式として弱い排中律を加えた体系と、公理図式として $\lnot(\varphi\land\psi)\to(\lnot\varphi\lor\lnot\psi)$ を加えた体系は、同じ式を証明する。
1 は弱い排中律 $\lnot\varphi\lor\lnot\lnot\varphi$ で場合を分け、$\lnot\lnot\varphi$ の場合に $\lnot\psi$ を導く。2 は無矛盾律 $\lnot(\varphi\land\lnot\varphi)$ が証明できることから従う。
詳細
1. $\Gamma:=\{\lnot\varphi\lor\lnot\lnot\varphi,\ \lnot(\varphi\land\psi)\}$ とおく。公理 5 により $\Gamma\vdash_{\mathrm{I}}\lnot\varphi\to(\lnot\varphi\lor\lnot\psi)$ である。次に $\Gamma,\lnot\lnot\varphi,\psi,\varphi$ を考えると、公理 4 により $\varphi\land\psi$ が出て、$\lnot(\varphi\land\psi)$ と合わせて $\bot$ が出る。演繹定理により $\Gamma,\lnot\lnot\varphi,\psi\vdash_{\mathrm{I}}\lnot\varphi$ であり、$\lnot\lnot\varphi$ と合わせて $\Gamma,\lnot\lnot\varphi,\psi\vdash_{\mathrm{I}}\bot$、したがって $\Gamma,\lnot\lnot\varphi\vdash_{\mathrm{I}}\lnot\psi$ である。公理 5 と演繹定理で $\Gamma\vdash_{\mathrm{I}}\lnot\lnot\varphi\to(\lnot\varphi\lor\lnot\psi)$ を得る。公理 6 の $$ (\lnot\varphi\to\chi)\to\bigl((\lnot\lnot\varphi\to\chi)\to((\lnot\varphi\lor\lnot\lnot\varphi)\to\chi)\bigr),\qquad\chi:=\lnot\varphi\lor\lnot\psi $$ に前件肯定を 3 回使うと $\Gamma\vdash_{\mathrm{I}}\lnot\varphi\lor\lnot\psi$ であり、演繹定理で 1 を得る。
2. 無矛盾律 $\lnot(\varphi\land\lnot\varphi)$ は直観主義論理で証明できる（rem-lem-bivalence）ので、前件肯定による。
最後の主張は、1 により前者の体系で後者の公理がすべて証明でき、2 で $\psi:=\lnot\varphi$ とすると後者の体系で前者の公理がすべて証明できることによる。演繹定理は公理を加えても成り立つ（直観主義論理 の記事の命題「演繹定理」の証明は公理 1・2 と前件肯定しか使わない）。$\square$
1 の証明で使った弱い排中律は $\varphi$ についての 1 つだけである。ex-lem-sqrt2 の議論は、「$x+\sqrt2$ は有理数」という 1 つの命題についての弱い排中律があれば排中律なしに完結する。
$\varphi$ についての弱い排中律は、$\lnot\varphi$ についての排中律 $\lnot\varphi\lor\lnot\lnot\varphi$ そのものである。したがって公理図式としての排中律は弱い排中律を含む。逆は成り立たない。
$p$ を命題変数とする。弱い排中律の例 $\chi_1,\dots,\chi_n$（それぞれある論理式 $\varphi_i$ について $\chi_i=\lnot\varphi_i\lor\lnot\lnot\varphi_i$）をどのように有限個とっても、$\chi_1,\dots,\chi_n\vdash_{\mathrm{I}}p\lor\lnot p$ とはならない。したがって、直観主義命題論理に公理図式として弱い排中律を加えた体系では、$p\lor\lnot p$ は証明できない。
3 元の鎖 $\{0< h<1\}$ では弱い排中律の例の値がすべて $1$ になるが、$p$ に $h$ を割り当てると $p\lor\lnot p$ の値は $h$ になることを、健全性と組み合わせる。
詳細
3 元の鎖 $H=\{0< h<1\}$ を 直観主義論理 の記事の例「反例：3 元の鎖と排中律」の Heyting 代数とする。否定は $\lnot0=1$、$\lnot h=0$、$\lnot1=0$ なので、どの $a\in H$ についても $\lnot a\in\{0,1\}$ であり、$\lnot a=0$ なら $\lnot\lnot a=1$、$\lnot a=1$ なら $\lnot a$ 自身が $1$ である。よって $\lnot a\lor\lnot\lnot a=\max\{\lnot a,\lnot\lnot a\}=1$ である。したがって、どの付値 $v$ についても、弱い排中律の例の値はすべて $1$ である（同記事の定義「Heyting 代数での値」）。
$\chi_1,\dots,\chi_n\vdash_{\mathrm{I}}p\lor\lnot p$ と仮定すると、演繹定理を $n$ 回使って $$ \vdash_{\mathrm{I}}\chi_1\to\bigl(\chi_2\to\cdots\to(\chi_n\to(p\lor\lnot p))\cdots\bigr) $$ となる。$v(p)=h$ とする付値をとる。同記事の定理「Heyting 代数に関する健全性」により、この式の値は $1$ である。一方、Heyting 代数では $c\le(1\Rightarrow b)\iff c\land1\le b\iff c\le b$ なので $1\Rightarrow b=b$ であり、各 $\chi_i$ の値は $1$ なので、この式の値は $[\![p\lor\lnot p]\!]_v=h\lor0=h\ne1$ に等しい。これは矛盾である。
体系での導出は、使った有限個の公理の例を仮定とする直観主義論理の導出なので、後半が従う。$\square$
$\{0< h<1\}$ のように全順序をなす Heyting 代数では否定の値が $0$ か $1$ しかないので、弱い排中律はつねに成り立つ。排中律が破れるのは中間の値 $h$ 自身が補元をもたないからである。弱い排中律は「$\varphi$ が不可能か、$\lnot\varphi$ が不可能か」と読め、否定の形の命題についてだけ排中律を認めることに当たる。
選択公理と排中律
ZFC公理系 は古典論理の上の理論であり、排中律ははじめから使える。集合論を直観主義論理の上で展開すると、どの公理が排中律を引き込むかが問題になる。ここでは、直観主義述語論理（等号を含む）の上で、次の公理を仮定する（Shu18 §2 の形）。
- 外延性：$x=y$ と $\forall z\,(z\in x\leftrightarrow z\in y)$ は同値である。
- 空集合と対：空集合 $\emptyset$ と、任意の $x,y$ について $z\in\{x,y\}\leftrightarrow(z=x\lor z=y)$ を満たす集合 $\{x,y\}$ がある。
- 分出：任意の論理式 $\varphi(x)$ と集合 $a$ について、$x\in\{x\in a\mid\varphi(x)\}\leftrightarrow(x\in a\land\varphi(x))$ を満たす集合がある。
- 選択：集合 $a$ のどの元 $x$ も元をもつ（$\exists y\ y\in x$）なら、$a$ を定義域とする関数 $f$ で、すべての $x\in a$ について $f(x)\in x$ となるものがある。
関数 $f$ は順序対の集合で、定義域の各元にただ一つの値を対応させるものである。特に $x=x'$ なら $f(x)=f(x')$ である。直観主義論理では「空でない」（$\lnot\forall y\ y\notin x$）と「元をもつ」（$\exists y\ y\in x$）は一般に同値でないので、選択公理は後者の形で述べる。
$0:=\emptyset$、$1:=\{\emptyset\}=\{0,0\}$、$2:=\{0,1\}$ とおく。$0\in1$ かつ $0\notin0$ なので、$0=1$ と仮定すると等号の性質から $0\in0$ となって矛盾し、$0\ne1$ である。対の公理により、$x\in2$ は $x=0\lor x=1$ と同値である。
上の公理のもとで、任意の論理式 $\varphi$ について $\varphi\lor\lnot\varphi$ が証明できる。
$\varphi$ を論理式とし、変数 $x$ は $\varphi$ に自由に現れないとする。分出により
$$
A:=\{x\in2\mid x=0\lor\varphi\},\qquad B:=\{x\in2\mid x=1\lor\varphi\}
$$
をとる。$0\in A$、$1\in B$ なので、$A,B$ はどちらも元をもつ。対の公理により $a:=\{A,B\}$ をとると、$a$ の元は $A$ か $B$ に等しいので、どれも元をもつ。選択公理により、$a$ 上の関数 $f$ で $f(A)\in A$、$f(B)\in B$ となるものがある。$A,B\subset2$ なので
$$
(f(A)=0\lor f(A)=1)\land(f(B)=0\lor f(B)=1)
$$
である。この 2 つの選言で場合を分ける。
- $f(A)=1$ の場合：$f(A)\in A$ から $1=0\lor\varphi$ である。$1=0$ からは $\bot$ が出て公理 7 により $\varphi$ が出るので、どちらの場合も $\varphi$ であり、$\varphi\lor\lnot\varphi$ が成り立つ。
- $f(B)=0$ の場合：同様に $f(B)\in B$ から $0=1\lor\varphi$ であり、$\varphi$ が成り立つ。
- $f(A)=0$ かつ $f(B)=1$ の場合：$\lnot\varphi$ を示す。$\varphi$ を仮定する。すると任意の $x$ について $x\in A$ と $x\in2$ と $x\in B$ はどれも同値になる（$x=0\lor\varphi$ も $x=1\lor\varphi$ も $\varphi$ から成り立つ）。外延性により $A=B$ であり、$f$ は関数なので $f(A)=f(B)$、すなわち $0=1$ となって矛盾する。よって $\lnot\varphi$ であり、$\varphi\lor\lnot\varphi$ が成り立つ。
$f(A)$ と $f(B)$ の値の組 $(1,0),(1,1)$ は 1 つ目の場合に、$(0,0)$ は 2 つ目の場合に、$(0,1)$ は 3 つ目の場合に入るので、どの場合も $\varphi\lor\lnot\varphi$ が成り立つ。場合分けに使ったのは、与えられた選言についての公理 6 の推論だけであり、排中律は使っていない。$\square$
効いているのは、$2$ の元が $0$ か $1$ に決まること、$f$ が等しい集合に同じ値を返す関数であること、分出が任意の論理式に許されていることの 3 つである。
詳細
- 場合分けができたのは、$2$ の元について $x=0\lor x=1$ が対の公理から出るからである。等しいかどうかが決定可能な集合 $2$ に値をとる選択関数が、任意の命題の真偽を $2$ の値の比較に写している。
- 3 つ目の場合で効いているのは、$f$ が関数であること、つまり等しい集合に同じ値を返すことである。$A$ から $0$ を、$B$ から $1$ を別々に選ぶことは選択公理なしでいつでもできるが、それでは $A=B$ のときに選んだ元が一致することを導けない（ex-lem-counterexamples の 5 行目）。
- 分出を任意の論理式について認めたので、$\varphi$ はどんな論理式でもよかった。Shu18 p. 6 は、分出を任意の論理式に認めると、量化記号の範囲を集合に限った論理式（$\Delta_0$ 論理式）についての排中律から任意の論理式についての排中律が出ることを示し、p. 7 は、選択公理と冪集合公理から Diaconescu の議論で $\Delta_0$ 論理式についての排中律が出ると述べている。型理論の言葉で同じ主張を述べた版は UFP13 Theorem 10.1.14 にある。
このため、直観主義論理の上の集合論（構成的集合論）は、選択公理を一般の形では採らず、可算選択などの弱い形に限ることが多い。UFP13 §10.1.4 の末尾（p. 345）は、トポス の理論でも選択公理が排中律の十分条件としてよく知られていることを述べている。
反例：条件を外すと成り立たない
| 外す条件 | 反例 | 成り立たなくなること |
|---|---|---|
| 結論に二重否定を付ける（thm-lem-glivenko） | $p\lor\lnot p$ | 古典論理で証明できる式が、直観主義論理で証明できること |
| 加える公理が排中律（弱い排中律に弱める） | 3 元の鎖 $\{0< h<1\}$ で $p$ に $h$ を割り当てる | $p\lor\lnot p$ が導けること（prop-lem-weak-strict） |
| 二重否定除去をすべての式に加える（1 つの命題変数 $p$ についての $\lnot\lnot p\to p$ だけにする） | $\mathbb{R}$ の開集合の Heyting 代数で $p$ に $(-\infty,0)$ を割り当てる | $p\lor\lnot p$ が導けること |
| 真理値が $0$ と $1$ の 2 つ（Boole 代数に広げる） | 4 元の Boole 代数で $p$ に $\{1\}$ を割り当てる | 排中律が成り立つなら各命題の値が $0$ か $1$ であること |
| $f$ が関数である（$A$、$B$ から別々に元を選ぶだけにする） | $A$ から $0$、$B$ から $1$ を選ぶ | thm-lem-diaconescu の 3 つ目の場合で $\lnot\varphi$ を導くこと |
各行の反例は本文の例と命題、直観主義論理 の記事の系で確かめられる。
詳細
1 行目：$p\lor\lnot p$ は古典論理で証明できるが、直観主義論理 の記事の系「直観主義論理で証明できない式」により直観主義論理では証明できない。thm-lem-glivenko が直観主義論理での証明を保証するのは、二重否定を付けた $\lnot\lnot(p\lor\lnot p)$ だけである。
2 行目：prop-lem-weak-strict の証明そのものである。
3 行目：直観主義論理 の記事の注意「Peirce の法則」の次の段落による。$U=(-\infty,0)$ では $\lnot\lnot U=U$ なので $\lnot\lnot p\to p$ の値は $\mathbb{R}$ だが、$p\lor\lnot p$ の値は $\mathbb{R}\setminus\{0\}$ である。prop-lem-weak-strict の証明と同じく、健全性により $\lnot\lnot p\to p\vdash_{\mathrm{I}}p\lor\lnot p$ ではない。命題「排中律と二重否定除去」は、すべての式についての公理図式どうしの比較である。
4 行目：ex-lem-boolean による。$p\lor\lnot p$ の値は最大元 $X$ だが、$p$ の値 $\{1\}$ は $\emptyset$ でも $X$ でもない。
5 行目：$0\in A$、$1\in B$ なので、この選び方は $\varphi$ について何も仮定せずにできる。$\varphi$ が成り立って $A=B$ となっても、「$A$ から $0$、$B$ から $1$」という 2 つの選び方は矛盾しない。$A=B$ のとき $\{(A,0),(B,1)\}$ は 1 つの元に 2 つの値を対応させるので関数ではなく、選択公理の与える $f$ にはならない。$f$ が関数であることを使わないと、3 つ目の場合で矛盾を導けない。
補足
- トポスの内部論理：トポス の内部論理は一般に直観主義論理であり、内部論理で排中律が成り立つトポスはブール的であるという（直観主義論理 の記事の注意「トポスの内部論理」）。ex-lem-boolean の Boole 代数と 3 元の鎖の違いは、この区別の最も小さな形である。
- 計算との関係：ex-lem-decidable の 3 のように、排中律の例を「どちらかを答える計算手続き」と読むと、決定可能性は計算可能性の問題になる。どの集合が決定可能か、決定不能な問題どうしの難しさをどう比べるかを扱うのが 計算可能性理論 である。
- 背理法との関係：$\lnot P$ を仮定して矛盾を導き $P$ を結論する形の背理法は二重否定除去を使い、公理図式としては排中律と同じ強さである。$P$ を仮定して矛盾を導き $\lnot P$ を結論する形は否定の定義そのものであり、排中律を使わない（背理法 の記事の節「直観主義論理との関係」）。cor-lem-glivenko の 1 は、否定の形の結論についてはどちらの形の背理法を使っても証明できる命題が変わらないことを述べている。
参照箇所
- OLT26 §24.5 Theorem 24.2（p. 376、排中律・二重否定除去と同値な公理図式）、Theorem 24.3（p. 377、二重否定翻訳）、§58.3 Example 58.7（p. 811、BHK 解釈による $\lnot\lnot(\varphi\lor\lnot\varphi)$ と排中律の説明）。
- Shu18 §2（p. 5：外延性・空集合・対・分出などの基本公理、p. 6：任意の論理式の分出と $\Delta_0$ 論理式の排中律、p. 7：選択公理と Diaconescu の議論）。
- UFP13 §10.1.4 の末尾と §10.1.5（p. 345）、Theorem 10.1.14（p. 346、選択公理は排中律を導く）。
関連項目
参考文献
Mathpediaは寄付と、参考文献の書籍リンク（Amazonアソシエイト）の紹介料で運営されています。 支援について ／ 寄付する
