Glivenkoの定理

同義語：Glivenko's theoremグリヴェンコの定理

概要

前提知識: 直観主義論理, 命題論理, 演繹定理

Glivenko の定理（Glivenko's theorem）とは、命題論理の論理式 $\varphi$ について、$\varphi$ が古典論理で証明できることと、$\lnot\lnot\varphi$ が直観主義論理で証明できることが同値であるという定理である。Glivenko が 1929 年に示した（Mos22 §4.1）。古典論理で証明した命題論理の式は、二重否定を付ければ排中律を使わずに証明でき、特に否定の形 $\lnot\psi$ の式は、古典論理で証明できればそのまま直観主義論理で証明できる。
この記事では、仮定の集合 $\Gamma$ を許した形 $\Gamma\vdash_{\mathrm C}\varphi\iff\Gamma\vdash_{\mathrm I}\lnot\lnot\varphi$ を、古典論理の導出の各行に二重否定を付けるという方法で証明する。帰結として、否定の形の式や「否定的な式」についての保存、矛盾が生じるかどうかの一致、$\lnot\lnot\varphi$ の直観主義論理での証明可能性が真理値表で判定できることを示す。述語論理と、矛盾からは何でも出るという公理を除いた最小論理では、この形の定理は成り立たない。

定義

記法は直観主義論理の記事に合わせる。命題論理の 論理式 は、命題変数 $p,q,\dots$ と定数 $\bot$（矛盾）から結合子 $\land,\lor,\to$ で作り、否定を $\lnot\varphi:=(\varphi\to\bot)$ で定める。

3 つの命題論理の体系

任意の論理式 $\varphi,\psi,\chi$ について、次の形の論理式を考える。

$\varphi\to(\psi\to\varphi)$
$(\varphi\to(\psi\to\chi))\to((\varphi\to\psi)\to(\varphi\to\chi))$
$(\varphi\land\psi)\to\varphi$、$(\varphi\land\psi)\to\psi$
$\varphi\to(\psi\to(\varphi\land\psi))$
$\varphi\to(\varphi\lor\psi)$、$\psi\to(\varphi\lor\psi)$
$(\varphi\to\chi)\to((\psi\to\chi)\to((\varphi\lor\psi)\to\chi))$
$\bot\to\varphi$
論理式の集合 $\Gamma$ からの導出とは、論理式の有限列で、各項が公理であるか、$\Gamma$ の元であるか、前の 2 つの項 $\chi$ と $\chi\to\chi'$ から 前件肯定 で得られる $\chi'$ であるものをいう。公理を 1〜7 とする体系を 直観主義命題論理、1〜6 とする体系を 最小論理、1〜7 に 排中律 $\varphi\lor\lnot\varphi$ を加えた体系を 古典命題論理 という。$\Gamma$ から $\varphi$ で終わる導出があることを、それぞれ $\Gamma\vdash_{\mathrm I}\varphi$、$\Gamma\vdash_{\mathrm M}\varphi$、$\Gamma\vdash_{\mathrm C}\varphi$ と書き、$\Gamma=\emptyset$ のときは $\Gamma$ を省く。$\Gamma\cup\{\psi\}$ を $\Gamma,\psi$ と書く。

直観主義命題論理は直観主義論理の記事の定義「直観主義命題論理の公理系」と同じものである。$\vdash_{\mathrm C}\varphi$ であることと $\varphi$ が恒真式（$\bot$ を偽と解釈し、すべての真理値の割り当てで真になる式）であることは同値である（同記事の定義の直後の段落。命題論理の完全性定理）。
3 つの体系はどれも、推論規則が前件肯定だけで、公理 1・2 を含む。したがって演繹定理の定理「演繹定理」により、どの体系でも
$$ \Gamma,\psi\vdash\chi\iff\Gamma\vdash\psi\to\chi $$
が成り立つ。以下これを断らずに使う。$\vdash\varphi\to\varphi$ も同記事の補題「恒等式の導出」による。

主張

Glivenko の定理

命題論理の論理式の集合 $\Gamma$ と論理式 $\varphi$ について、
$$ \Gamma\vdash_{\mathrm C}\varphi\iff\Gamma\vdash_{\mathrm I}\lnot\lnot\varphi . $$
特に $\Gamma=\emptyset$ のとき、$\vdash_{\mathrm C}\varphi$ と $\vdash_{\mathrm I}\lnot\lnot\varphi$ は同値である。

主張の読み方

右辺の $\lnot\lnot\varphi$ は「$\varphi$ の反駁はありえない」という主張である（直観主義論理の注意「証明による意味づけ（BHK 解釈）」）。定理は、命題論理の範囲では、古典論理で証明できる内容は直観主義論理でちょうどこの弱い形で証明できることを述べる。右辺の二重否定は外せない。$\vdash_{\mathrm C}p\lor\lnot p$ だが $p\lor\lnot p$ は直観主義論理で証明できない（後の反例の表の 1 行目）。

証明

二重否定についての補題

二重否定の基本性質

任意の論理式 $\varphi,\psi$ について、次が成り立つ。どれも公理 1〜6 と前件肯定だけで示せるので、$\vdash_{\mathrm M}$ でも成り立つ。

$\varphi\vdash_{\mathrm I}\lnot\lnot\varphi$。
$\lnot\lnot\lnot\varphi\vdash_{\mathrm I}\lnot\varphi$。
$\lnot\lnot(\varphi\to\psi),\ \lnot\lnot\varphi\vdash_{\mathrm I}\lnot\lnot\psi$。
$\vdash_{\mathrm I}\lnot\lnot(\varphi\lor\lnot\varphi)$。
$\vdash_{\mathrm I}\varphi\to\psi$ ならば $\lnot\lnot\varphi\vdash_{\mathrm I}\lnot\lnot\psi$。

$\chi$ と $\lnot\chi=(\chi\to\bot)$ から前件肯定で $\bot$ が出ることを繰り返し使う。
1：$\varphi,\lnot\varphi\vdash\bot$ なので、演繹定理で $\varphi\vdash\lnot\varphi\to\bot=\lnot\lnot\varphi$。
2：$\lnot\lnot\lnot\varphi,\varphi$ からは、1 により $\lnot\lnot\varphi$ が出て、$\lnot\lnot\lnot\varphi=(\lnot\lnot\varphi\to\bot)$ と合わせて $\bot$ が出る。演繹定理で $\lnot\lnot\lnot\varphi\vdash\lnot\varphi$。
3：$\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\lnot\varphi$。これと $\lnot\lnot\varphi$ から $\Gamma,\varphi\to\psi\vdash\bot$、したがって $\Gamma\vdash\lnot(\varphi\to\psi)$。これと $\lnot\lnot(\varphi\to\psi)$ から $\Gamma\vdash\bot$ であり、演繹定理で $\lnot\psi$ を外して $\lnot\lnot(\varphi\to\psi),\lnot\lnot\varphi\vdash\lnot\lnot\psi$。
4：$\Delta:=\{\lnot(\varphi\lor\lnot\varphi)\}$ とおく。公理 5 により $\Delta,\varphi\vdash\varphi\lor\lnot\varphi$ なので $\Delta,\varphi\vdash\bot$、すなわち $\Delta\vdash\lnot\varphi$。再び公理 5 により $\Delta\vdash\varphi\lor\lnot\varphi$ で、$\Delta\vdash\bot$。演繹定理で $\vdash\lnot(\varphi\lor\lnot\varphi)\to\bot$。
5：1 により $\vdash\lnot\lnot(\varphi\to\psi)$ なので、3 による。
使ったのは前件肯定、演繹定理（公理 1・2）、公理 5 だけである。$\square$

3 は「二重否定の下で前件肯定が使える」こと、4 は「排中律は二重否定の下では直観主義論理で証明できる」ことを述べている。この 2 つが定理の証明の要である。

定理の証明

導出の各行に二重否定を付ける

$\Rightarrow$：$\Gamma$ からの古典命題論理の導出 $\chi_1,\dots,\chi_m=\varphi$ をとる。$k$ についての帰納法で $\Gamma\vdash_{\mathrm I}\lnot\lnot\chi_k$ を示す。$\chi_k$ の正当化に応じて場合を分ける。

$\chi_k$ が公理 1〜7 のどれか：$\vdash_{\mathrm I}\chi_k$ なので、lem-gl-dn の 1 により $\vdash_{\mathrm I}\lnot\lnot\chi_k$。
$\chi_k$ が排中律 $\psi\lor\lnot\psi$：lem-gl-dn の 4 により $\vdash_{\mathrm I}\lnot\lnot\chi_k$。
$\chi_k\in\Gamma$：$\Gamma\vdash_{\mathrm I}\chi_k$ なので、lem-gl-dn の 1 により $\Gamma\vdash_{\mathrm I}\lnot\lnot\chi_k$。
$\chi_k$ が $\chi_i$ と $\chi_j=(\chi_i\to\chi_k)$（$i,j< k$）から前件肯定で得られた：帰納法の仮定により $\Gamma\vdash_{\mathrm I}\lnot\lnot\chi_i$ と $\Gamma\vdash_{\mathrm I}\lnot\lnot(\chi_i\to\chi_k)$ であり、lem-gl-dn の 3 により $\Gamma\vdash_{\mathrm I}\lnot\lnot\chi_k$。
各場合で得た導出を並べてつなげば $\Gamma$ からの導出になる。$k=m$ として $\Gamma\vdash_{\mathrm I}\lnot\lnot\varphi$ である。
$\Leftarrow$：公理 1〜7 は古典命題論理の公理でもあるので、$\Gamma\vdash_{\mathrm I}\lnot\lnot\varphi$ なら $\Gamma\vdash_{\mathrm C}\lnot\lnot\varphi$ である。古典命題論理で $\lnot\lnot\varphi\vdash_{\mathrm C}\varphi$ を示せばよい。$\lnot\lnot\varphi,\lnot\varphi\vdash\bot$ と公理 7 から $\lnot\lnot\varphi,\lnot\varphi\vdash\varphi$、演繹定理で $\lnot\lnot\varphi\vdash\lnot\varphi\to\varphi$ である。$\vdash\varphi\to\varphi$ と公理 6
$$ (\varphi\to\varphi)\to\bigl((\lnot\varphi\to\varphi)\to((\varphi\lor\lnot\varphi)\to\varphi)\bigr) $$
と排中律 $\varphi\lor\lnot\varphi$ に前件肯定を 3 回使うと、$\lnot\lnot\varphi\vdash_{\mathrm C}\varphi$ を得る。$\square$

古典論理の導出は、各行に $\lnot\lnot$ を付けると直観主義論理の導出の骨組みになる。古典論理に固有の排中律の行は、直観主義論理で証明できる $\lnot\lnot(\psi\lor\lnot\psi)$ に置き換わる。証明は導出を具体的に書き換えているので、古典論理の導出から直観主義論理の導出を作る手続きも与えている。

帰結

Glivenko の定理の帰結

命題論理の論理式の集合 $\Gamma$ と論理式 $\psi,\varphi$ について、次が成り立つ。

$\Gamma\vdash_{\mathrm C}\lnot\psi\iff\Gamma\vdash_{\mathrm I}\lnot\psi$。
$\Gamma\vdash_{\mathrm C}\bot\iff\Gamma\vdash_{\mathrm I}\bot$。つまり、$\Gamma$ が古典論理で矛盾することと直観主義論理で矛盾することは同値である。
$\vdash_{\mathrm I}\lnot\lnot\varphi$ であることは、$\varphi$ が恒真式であることと同値である。特に、$\vdash_{\mathrm I}\lnot\lnot\varphi$ かどうかは真理値表で判定できる。

1：$\Rightarrow$ は thm-gl-main で $\Gamma\vdash_{\mathrm I}\lnot\lnot\lnot\psi$ とし、lem-gl-dn の 2 を使う。$\Leftarrow$ は公理 1〜7 が古典命題論理の公理でもあることによる。
2：thm-gl-main により $\Gamma\vdash_{\mathrm C}\bot\iff\Gamma\vdash_{\mathrm I}\lnot\lnot\bot$ である。$\lnot\lnot\bot=(\lnot\bot\to\bot)$ で、$\lnot\bot=(\bot\to\bot)$ は証明可能なので、前件肯定で $\lnot\lnot\bot\vdash_{\mathrm I}\bot$ である。逆は公理 1 から $\bot\vdash_{\mathrm I}\lnot\bot\to\bot$ による。
3：thm-gl-main の $\Gamma=\emptyset$ の場合と、$\vdash_{\mathrm C}\varphi$ と恒真式であることの同値による。$\square$

1 は、否定の形の結論を示すときは、排中律を使っても使わなくても証明できるものが変わらないことを言う。$\lnot$ の形でなくても、次の形の式なら二重否定を付けずに保存される。

否定的な式の保存

論理式の集合 $\mathcal N$ を、次の規則で作られる式の全体とする：$\bot\in\mathcal N$；$\chi_1,\chi_2\in\mathcal N$ なら $\chi_1\land\chi_2\in\mathcal N$；任意の論理式 $\psi$ と $\chi\in\mathcal N$ について $\psi\to\chi\in\mathcal N$。このとき、$\chi\in\mathcal N$ について $\lnot\lnot\chi\vdash_{\mathrm I}\chi$ であり、したがって $\Gamma\vdash_{\mathrm C}\chi\iff\Gamma\vdash_{\mathrm I}\chi$ である。

$\lnot\psi=(\psi\to\bot)$ は $\mathcal N$ に属するので、これは cor-gl-consequences の 1 を含む。

$\chi$ の組み立てについての帰納法で $\lnot\lnot\chi\vdash_{\mathrm I}\chi$ を示す。

$\chi=\bot$：cor-gl-consequences の 2 の証明のとおり $\lnot\lnot\bot\vdash_{\mathrm I}\bot$。
$\chi=\chi_1\land\chi_2$：公理 3 と lem-gl-dn の 5 により $\lnot\lnot(\chi_1\land\chi_2)\vdash_{\mathrm I}\lnot\lnot\chi_i$（$i=1,2$）、帰納法の仮定で $\chi_i$ が出て、公理 4 で $\chi_1\land\chi_2$ が出る。
$\chi=\psi\to\chi'$：$\lnot\lnot(\psi\to\chi'),\psi$ からは、lem-gl-dn の 1 で $\lnot\lnot\psi$、同じ補題の 3 で $\lnot\lnot\chi'$、帰納法の仮定で $\chi'$ が出る。演繹定理で $\lnot\lnot(\psi\to\chi')\vdash_{\mathrm I}\psi\to\chi'$。
後半：$\Gamma\vdash_{\mathrm C}\chi$ なら thm-gl-main により $\Gamma\vdash_{\mathrm I}\lnot\lnot\chi$ で、前半から $\Gamma\vdash_{\mathrm I}\chi$。逆は 1 と同じである。$\square$

例

真理値表で直観主義論理の定理を見つける

次の式はどれも恒真式なので、cor-gl-consequences の 3 により、二重否定を付けた式は直観主義論理で証明できる。

$\varphi$	$\vdash_{\mathrm I}\varphi$ か	$\vdash_{\mathrm I}\lnot\lnot\varphi$ か
$p\lor\lnot p$	いいえ	はい
$\lnot\lnot p\to p$	いいえ	はい
$((p\to q)\to p)\to p$（Peirce の法則）	いいえ	はい
$\lnot(p\land q)\to(\lnot p\lor\lnot q)$	いいえ	はい
$\lnot(p\lor q)\to(\lnot p\land\lnot q)$	はい	はい
$(\lnot\lnot p\to\lnot\lnot q)\to\lnot\lnot(p\to q)$	はい	はい

「いいえ」の 4 つは、直観主義論理の系「直観主義論理で証明できない式」による（Heyting 代数で値が $1$ にならない付値がある）。最後の 2 つは $\mathcal N$ に属する（$\psi\to\chi$ の形で、$\chi$ が $\lnot p\land\lnot q=(p\to\bot)\land(q\to\bot)$、または $\lnot\lnot(p\to q)$）ので、prop-gl-negative により二重否定なしで証明できる。最後の式は、$p\to q$ が偽になる付値（$p$ が真、$q$ が偽）では前件 $\lnot\lnot p\to\lnot\lnot q$ が偽になることから恒真式と分かる。真理値表を調べるだけで、直観主義論理の導出を書かずに証明可能性が分かる。

反例：条件を外すと成り立たない

外す条件	反例	成り立たなくなること
結論に $\lnot\lnot$ を付ける	$p\lor\lnot p$	$\vdash_{\mathrm C}\varphi\Rightarrow\ \vdash_{\mathrm I}\varphi$
$\varphi$ が命題論理の式	1 項関係記号 $P$ について $\forall x\,(P(x)\lor\lnot P(x))$	古典述語論理で証明できる式について、二重否定を付けた式が直観主義述語論理で証明できること
直観主義論理の側に公理 7（$\bot\to\varphi$）がある	$\bot\to p$	$\vdash_{\mathrm C}\varphi\Rightarrow\ \vdash_{\mathrm M}\lnot\lnot\varphi$
prop-gl-negative の $\chi\in\mathcal N$（$\psi\to\chi$ の $\chi$ が否定的）	$\lnot\lnot p\to p$	$\vdash_{\mathrm C}\chi\Rightarrow\ \vdash_{\mathrm I}\chi$

反例の確かめ

1 行目と 4 行目：$p\lor\lnot p$ と $\lnot\lnot p\to p$ は恒真式なので古典論理で証明できるが、直観主義論理の系「直観主義論理で証明できない式」により直観主義論理では証明できない。4 行目の式は $\psi\to\chi$ の形だが $\chi=p$ は $\mathcal N$ に属さない。
2 行目：この式は古典述語論理で証明できるが、$\lnot\lnot\forall x\,(P(x)\lor\lnot P(x))$ は直観主義述語論理で証明できない。世界を自然数全体とし、世界 $k$ で $P$ を $\{m\mid m< k\}$ と解釈する Kripke モデルで確かめられる（黒田の二重否定翻訳の例「反例の確かめ」の 2 行目。Mos22 §4.1 も述語論理では成り立たないことを述べる）。
3 行目：$\bot\to p$ は公理 7 なので $\vdash_{\mathrm C}\bot\to p$ である。$\vdash_{\mathrm M}\lnot\lnot(\bot\to p)$ でないことを示す。3 元の鎖 $H=\{0< h<1\}$ を Heyting 代数とし（含意は $x\le y$ なら $x\Rightarrow y=1$、$x>y$ なら $x\Rightarrow y=y$）、論理式の値を直観主義論理の定義「Heyting 代数での値」と同じ規則で、ただし $\bot$ の値を $0$ でなく $h$ として定める。公理 1〜6 の値がつねに $1$ であることと、前件肯定が値 $1$ を保つことは、同記事の定理「Heyting 代数に関する健全性」の証明のとおりで、その部分は $\bot$ の値を使わない。したがって $\vdash_{\mathrm M}\varphi$ ならこの値は $1$ である。ところが $p$ に $0$ を割り当てると、$\bot\to p$ の値は $h\Rightarrow0=0$、$\lnot(\bot\to p)$ の値は $0\Rightarrow h=1$、$\lnot\lnot(\bot\to p)$ の値は $1\Rightarrow h=h\ne1$ である。thm-gl-main の証明では、公理 7 の行で $\vdash\chi_k$ を使ったところだけが最小論理で通らない。lem-gl-dn は最小論理でも成り立つ。

補足

述語論理の場合

述語論理では、全称記号の直後にも二重否定を入れる翻訳（黒田の二重否定翻訳）や、原子論理式・選言・存在記号に二重否定を入れる Gödel–Gentzen の翻訳（OLT26 Theorem 24.3、p. 377）を使うと、古典論理で証明できる式が直観主義論理で証明できる式に移る。全称記号を含まない式については、この記事の形のまま成り立つ（黒田の二重否定翻訳の系「全称記号を含まない式の Glivenko の定理」）。また、直観主義述語論理に二重否定の移動の原理 $\forall x\,\lnot\lnot B(x)\to\lnot\lnot\forall x\,B(x)$ を加えた体系では、すべての式について「古典論理で証明できる $\iff$ 二重否定を付けた式が証明できる」が成り立つ（Mos22 §4.1、黒田の二重否定翻訳の定理「DNS のもとでの Glivenko の定理」）。

他の論理との関係

古典論理の側を、排中律の代わりに二重否定除去 $\lnot\lnot\varphi\to\varphi$ や Peirce の法則を公理として加えた体系にしても、証明できる式は同じなので定理は変わらない（直観主義論理の命題「排中律と二重否定除去」と注意「Peirce の法則」）。排中律を加えた古典論理が矛盾しないことは、cor-gl-consequences の 2 と、直観主義論理で $\bot$ が証明できないことからも分かる。