直観主義論理

同義語：intuitionistic logic

概要

前提知識: 命題論理, 論理式, 排中律, Heyting代数

直観主義論理は、「証明できた」ことを「真である」ことの意味とみなす論理であり、排中律 $\varphi\lor\lnot\varphi$ を一般的な原理としては認めない。次の証明を考える。「無理数 $a,b$ で $a^b$ が有理数になるものがある。実際、$\sqrt2^{\sqrt2}$ が有理数なら $a=b=\sqrt2$ とすればよく、無理数なら $a=\sqrt2^{\sqrt2}$、$b=\sqrt2$ とすれば $a^b=\sqrt2^2=2$ である。」これは古典論理では正しい証明だが、「$\sqrt2^{\sqrt2}$ は有理数か無理数かのどちらかである」という排中律に頼っており、どちらの組が答えなのかを教えない。直観主義論理では、「$A$ または $B$」を証明するには $A$ か $B$ のどちらかを実際に証明しなければならないので、この議論は存在の証明にならない（この命題自体は、$a=\sqrt2$、$b=\log_29$ とすれば $a^b=3$ となり、$\log_29$ が無理数であることも直接示せるので、直観主義論理でも証明できる）。このように直観主義論理は、古典論理から排中律を除き、証明の構成的な内容を保つ論理である。

定義

本記事では命題論理を扱う。命題変数 $p_0,p_1,\dots$ と定数 $\bot$（矛盾）から、結合子 $\land,\lor,\to$ で作られる式を論理式とし、否定は $\lnot\varphi:=(\varphi\to\bot)$ で定める。数理論理学の記事の定義「命題論理の論理式」は $\lnot$ を基本の記号とし $\bot$ をもたないが、直観主義論理では $\bot$ を基本とし $\lnot$ を略記とする流儀が標準的であり（TvD88 第 2 章、vDa13 第 5 章）、本記事もそれに従う。$\varphi\leftrightarrow\psi$ は $(\varphi\to\psi)\land(\psi\to\varphi)$ の略記である。

直観主義命題論理の公理系

任意の論理式 $\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$ について、論理式の有限列 $\chi_1,\dots,\chi_m$ で、各 $\chi_k$ が公理であるか、$\Gamma$ の元であるか、前の 2 つ $\chi_i$ と $\chi_j=(\chi_i\to\chi_k)$（$i,j< k$）から 前件肯定（modus ponens）で得られるものを、$\Gamma$ からの導出という。$\varphi$ で終わる導出があるとき $\Gamma\vdash_{\mathrm{I}}\varphi$ と書き、$\Gamma=\emptyset$ なら $\vdash_{\mathrm{I}}\varphi$ と書いて、$\varphi$ は 直観主義論理で証明可能 であるという。この公理系を 直観主義命題論理（intuitionistic propositional logic）という。

公理 1〜7 に 排中律 $\varphi\lor\lnot\varphi$ を公理として加えた体系で証明可能であることを $\vdash_{\mathrm{C}}\varphi$ と書く。これは古典論理の命題論理であり、$\vdash_{\mathrm{C}}\varphi$ であることと、$\varphi$ がすべての真理値割り当てで真になる恒真式であることは同値である（命題論理の完全性定理。vDa13 第 2 章）。ここで $\bot$ はつねに偽と解釈する。公理 1〜7 はすべて恒真式なので、直観主義論理で証明可能な式は古典論理でも証明可能である。直観主義論理は古典論理の弱い部分体系であり、古典論理と矛盾する原理を加えたものではない。

証明による意味づけ（BHK 解釈）

直観主義論理の結合子は、次のように「何が証明になるか」で意味づけられる。この説明は Brouwer・Heyting・Kolmogorov の名をとって BHK 解釈と呼ばれる（TvD88 第 1 章）。

$\varphi\land\psi$ の証明は、$\varphi$ の証明と $\psi$ の証明の組である。
$\varphi\lor\psi$ の証明は、$\varphi$ と $\psi$ のどちらを証明するかの指定と、その証明の組である。
$\varphi\to\psi$ の証明は、$\varphi$ の任意の証明を $\psi$ の証明に変換する手続きである。
$\bot$ には証明がない。したがって $\lnot\varphi$ の証明は、$\varphi$ の証明から矛盾を導く手続きである。
この解釈のもとで $\varphi\lor\lnot\varphi$ の証明とは、$\varphi$ を証明するか反駁するかを実際に決めることであり、一般の $\varphi$ についてそれができるとは限らない。一方 $\lnot\lnot\varphi$ の証明は「$\varphi$ の反駁はありえない」ことの証明にすぎず、$\varphi$ の証明を与えない。BHK 解釈は形式的な定義ではなく、上の公理系を選ぶ動機である。述語論理では、$\exists x\,\varphi(x)$ の証明は具体的な $t$ と $\varphi(t)$ の証明の組、$\forall x\,\varphi(x)$ の証明は各 $x$ に $\varphi(x)$ の証明を対応させる手続きと読む。

直感

古典論理では命題は真か偽かのどちらかに決まっており、「偽でないなら真」（$\lnot\lnot\varphi\to\varphi$）が成り立つ。直観主義論理では、命題は「すでに証明された」「すでに反駁された」「まだどちらでもない」という情報の状態で考える。情報は増えるだけで、いったん証明されたものは証明されたままである。$\lnot\varphi$ は「将来どれだけ情報が増えても $\varphi$ は証明されない」ことを意味する。すると「$\varphi$ は証明も反駁もまだされていないが、将来証明される可能性がある」状態では、$\varphi$ も $\lnot\varphi$ も成り立たず、$\varphi\lor\lnot\varphi$ も成り立たない。一方「$\varphi$ の反駁がありえない」ことが分かっても、$\varphi$ の証明が手に入ったわけではないので、$\lnot\lnot\varphi$ から $\varphi$ は出ない。この情報の状態を真理値とみなしたものが Heyting代数の元であり（thm-intuitionistic-logic-soundness）、位相空間の開集合の全体はその典型例である。

例と反例

直観主義論理で証明できる式

次の式は直観主義論理で証明可能である（prop-intuitionistic-logic-derivations）。

$\varphi\to\lnot\lnot\varphi$（二重否定の導入）。逆向きの $\lnot\lnot\varphi\to\varphi$ は証明できない（cor-intuitionistic-logic-unprovable）。
$\lnot\lnot\lnot\varphi\to\lnot\varphi$。したがって否定は 3 重になると 1 重に戻る（1 と合わせて $\lnot\lnot\lnot\varphi\leftrightarrow\lnot\varphi$）。
$(\varphi\to\psi)\to(\lnot\psi\to\lnot\varphi)$（対偶の一方向）。逆向きの $(\lnot\psi\to\lnot\varphi)\to(\varphi\to\psi)$ は、すべての $\varphi,\psi$ については証明できない。$\varphi:=\lnot\lnot p$、$\psi:=p$ とすると前件 $\lnot p\to\lnot\lnot\lnot p$ は 1 により証明可能なので、この式が証明可能なら前件肯定で $\lnot\lnot p\to p$ が証明可能になってしまうからである。
$\lnot\lnot(\varphi\lor\lnot\varphi)$。排中律そのものは証明できないが、排中律の否定を仮定すると矛盾する。直観主義論理は排中律を否定するのではなく、一般には証明できないとするだけである。
$\lnot\bot$ は $\bot\to\bot$ であり、これは証明可能（prf-intuitionistic-logic-deduction の $\varphi\to\varphi$）なので、公理 5 により $\bot\lor\lnot\bot$ は証明可能である。排中律の個々の例が証明できることはある。

反例：3 元の鎖と排中律

3 元の全順序集合 $H=\{0< h<1\}$ は、$x\land y=\min\{x,y\}$、$x\lor y=\max\{x,y\}$、含意を $x\le y$ のとき $x\Rightarrow y=1$、$x>y$ のとき $x\Rightarrow y=y$ として Heyting代数になる（Heyting代数の記事の例「反例：排中律は一般には成り立たない」）。否定は $\lnot0=1$、$\lnot h=h\Rightarrow0=0$、$\lnot1=0$ である。命題変数 $p$ に $h$ を割り当てると、def-intuitionistic-logic-heyting-value の意味で次のようになる。

$p\lor\lnot p$ の値は $h\lor0=h\ne1$。
$\lnot\lnot p\to p$ の値は $\lnot\lnot h=1$ なので $1\Rightarrow h=h\ne1$。
Peirce の法則 $((p\to q)\to p)\to p$ は、$q$ に $0$ を割り当てると、$h\Rightarrow0=0$、$0\Rightarrow h=1$、$1\Rightarrow h=h\ne1$。
これらはすべて古典論理の恒真式だが、thm-intuitionistic-logic-soundness により直観主義論理では証明できない。破る含意は「恒真式ならば直観主義論理で証明可能」である。

反例：開集合と De Morgan の法則

実数直線 $\mathbb{R}$ の開集合全体 $\operatorname{Op}(\mathbb{R})$ は、$U\Rightarrow V=\operatorname{int}((\mathbb{R}\setminus U)\cup V)$、$\lnot U=\operatorname{int}(\mathbb{R}\setminus U)$ により Heyting 代数になる（Heyting代数の記事の例「開集合の束」）。$p$ に $U=(-\infty,0)$、$q$ に $V=(0,\infty)$ を割り当てる。$U\cap V=\emptyset$ なので $\lnot(p\land q)$ の値は $\operatorname{int}\mathbb{R}=\mathbb{R}$ である。一方 $\lnot U=(0,\infty)$、$\lnot V=(-\infty,0)$ なので $\lnot p\lor\lnot q$ の値は $\mathbb{R}\setminus\{0\}$ である。よって $\lnot(p\land q)\to(\lnot p\lor\lnot q)$ の値は $\operatorname{int}\bigl(\emptyset\cup(\mathbb{R}\setminus\{0\})\bigr)=\mathbb{R}\setminus\{0\}\ne\mathbb{R}$ であり、この De Morgan の法則の片側は直観主義論理で証明できない。$p$ に $U$ を割り当てれば $p\lor\lnot p$ の値も $\mathbb{R}\setminus\{0\}$ で、点 $0$ が「どちらとも決まらない」場所になっている。
逆向きの $(\lnot p\lor\lnot q)\to\lnot(p\land q)$ は直観主義論理で証明可能である（prop-intuitionistic-logic-derivations の 5）。

性質

演繹定理と基本的な導出

演繹定理

論理式の集合 $\Gamma$ と論理式 $\varphi,\psi$ について、$\Gamma\cup\{\varphi\}\vdash_{\mathrm{I}}\psi$ ならば $\Gamma\vdash_{\mathrm{I}}\varphi\to\psi$ である。逆も成り立つ。

まず $\vdash_{\mathrm{I}}\varphi\to\varphi$ を示す。公理 2 の $\psi:=(\varphi\to\varphi)$、$\chi:=\varphi$ の場合と、公理 1 の 2 つの例 $\varphi\to((\varphi\to\varphi)\to\varphi)$、$\varphi\to(\varphi\to\varphi)$ に前件肯定を 2 回使えばよい。
$\Gamma\cup\{\varphi\}$ からの導出 $\chi_1,\dots,\chi_m$ の長さについての帰納法で、各 $k$ について $\Gamma\vdash_{\mathrm{I}}\varphi\to\chi_k$ を示す。$\chi_k$ が公理か $\Gamma$ の元なら、$\Gamma\vdash_{\mathrm{I}}\chi_k$ と公理 1 の $\chi_k\to(\varphi\to\chi_k)$ から前件肯定で得られる。$\chi_k=\varphi$ なら上で示した。$\chi_k$ が $\chi_i$ と $\chi_j=(\chi_i\to\chi_k)$ から前件肯定で得られたなら、帰納法の仮定により $\Gamma\vdash_{\mathrm{I}}\varphi\to\chi_i$ と $\Gamma\vdash_{\mathrm{I}}\varphi\to(\chi_i\to\chi_k)$ であり、公理 2 の $(\varphi\to(\chi_i\to\chi_k))\to((\varphi\to\chi_i)\to(\varphi\to\chi_k))$ に前件肯定を 2 回使って $\Gamma\vdash_{\mathrm{I}}\varphi\to\chi_k$ を得る。
逆は、$\Gamma$ からの $\varphi\to\psi$ の導出の後に $\varphi$ と $\psi$ を付け加えれば、$\Gamma\cup\{\varphi\}$ からの $\psi$ の導出になることによる。$\square$

この証明は公理 1・2 と前件肯定しか使っていないので、古典論理でも同じく成り立つ。以下、$\Gamma\cup\{\varphi\}$ を $\Gamma,\varphi$ と書く。

直観主義論理で証明できる式

任意の論理式 $\varphi,\psi$ について、次の式は直観主義論理で証明可能である。

$\varphi\to\lnot\lnot\varphi$
$(\varphi\to\psi)\to(\lnot\psi\to\lnot\varphi)$
$\lnot\lnot\lnot\varphi\to\lnot\varphi$
$\lnot\lnot(\varphi\lor\lnot\varphi)$
$(\lnot\varphi\lor\lnot\psi)\to\lnot(\varphi\land\psi)$

$\lnot\chi=(\chi\to\bot)$ なので、$\chi$ と $\lnot\chi$ から前件肯定で $\bot$ が導かれる。以下 prop-intuitionistic-logic-deduction を繰り返し使う。

$\varphi,\lnot\varphi\vdash_{\mathrm{I}}\bot$ なので $\varphi\vdash_{\mathrm{I}}\lnot\varphi\to\bot=\lnot\lnot\varphi$、よって $\vdash_{\mathrm{I}}\varphi\to\lnot\lnot\varphi$。
$\varphi\to\psi,\lnot\psi,\varphi\vdash_{\mathrm{I}}\bot$（$\varphi$ と $\varphi\to\psi$ から $\psi$、それと $\lnot\psi$ から $\bot$）なので、演繹定理を 3 回使う。
2 を $\varphi$ と $\lnot\lnot\varphi$ に使うと $\vdash_{\mathrm{I}}(\varphi\to\lnot\lnot\varphi)\to(\lnot\lnot\lnot\varphi\to\lnot\varphi)$ であり、1 と前件肯定で得られる。
$\Gamma:=\{\lnot(\varphi\lor\lnot\varphi)\}$ とする。公理 5 により $\Gamma,\varphi\vdash_{\mathrm{I}}\varphi\lor\lnot\varphi$ なので $\Gamma,\varphi\vdash_{\mathrm{I}}\bot$、すなわち $\Gamma\vdash_{\mathrm{I}}\lnot\varphi$ である。再び公理 5 により $\Gamma\vdash_{\mathrm{I}}\varphi\lor\lnot\varphi$ となり、$\Gamma\vdash_{\mathrm{I}}\bot$ である。よって $\vdash_{\mathrm{I}}\lnot(\varphi\lor\lnot\varphi)\to\bot$ である。
公理 3 により $\varphi\land\psi\vdash_{\mathrm{I}}\varphi$ なので $\varphi\land\psi,\lnot\varphi\vdash_{\mathrm{I}}\bot$、すなわち $\varphi\land\psi\vdash_{\mathrm{I}}\lnot\varphi\to\bot$ である。同様に $\varphi\land\psi\vdash_{\mathrm{I}}\lnot\psi\to\bot$ である。公理 6 の $(\lnot\varphi\to\bot)\to((\lnot\psi\to\bot)\to((\lnot\varphi\lor\lnot\psi)\to\bot))$ に前件肯定を 2 回使うと $\varphi\land\psi\vdash_{\mathrm{I}}(\lnot\varphi\lor\lnot\psi)\to\bot$ となり、$\varphi\land\psi,\lnot\varphi\lor\lnot\psi\vdash_{\mathrm{I}}\bot$ である。演繹定理を 2 回使って結論を得る。$\square$

排中律と二重否定除去

直観主義命題論理に、すべての $\varphi$ についての排中律 $\varphi\lor\lnot\varphi$ を公理として加えた体系と、すべての $\varphi$ についての二重否定除去 $\lnot\lnot\varphi\to\varphi$ を公理として加えた体系は、同じ式を証明する。したがって後者も古典論理である。

排中律を加えた体系で $\lnot\lnot\varphi\to\varphi$ を示す。$\lnot\lnot\varphi,\varphi\vdash\varphi$ であり、$\lnot\lnot\varphi,\lnot\varphi\vdash\bot$ から公理 7 で $\lnot\lnot\varphi,\lnot\varphi\vdash\varphi$ である。演繹定理により $\lnot\lnot\varphi\vdash\varphi\to\varphi$ かつ $\lnot\lnot\varphi\vdash\lnot\varphi\to\varphi$ であり、公理 6 と排中律 $\varphi\lor\lnot\varphi$ から $\lnot\lnot\varphi\vdash\varphi$ を得る。
二重否定除去を加えた体系で $\varphi\lor\lnot\varphi$ を示す。prop-intuitionistic-logic-derivations の 4 により $\lnot\lnot(\varphi\lor\lnot\varphi)$ が証明可能であり、二重否定除去の $\varphi\lor\lnot\varphi$ の場合と前件肯定で得られる。
どちらの体系でも他方の追加の公理が証明できるので、証明できる式は一致する。演繹定理は公理を追加しても成り立つ（prf-intuitionistic-logic-deduction は公理 1・2 と前件肯定しか使わない）。$\square$

Peirce の法則

Peirce の法則 $((\varphi\to\psi)\to\varphi)\to\varphi$ をすべての $\varphi,\psi$ について公理として加えた体系も、prop-intuitionistic-logic-classical の 2 つの体系と同じ式を証明する。実際、$\psi:=\bot$ とすると、Peirce の法則は $((\varphi\to\bot)\to\varphi)\to\varphi$、すなわち $(\lnot\varphi\to\varphi)\to\varphi$ である。公理 7（$\bot\to\varphi$）と演繹定理により $\lnot\lnot\varphi\vdash_{\mathrm{I}}\lnot\varphi\to\varphi$ が示せる（$\lnot\lnot\varphi,\lnot\varphi\vdash_{\mathrm{I}}\bot$ から公理 7 で $\varphi$ が出る）ので、$\psi:=\bot$ の場合の Peirce の法則から $\lnot\lnot\varphi\vdash_{\mathrm{I}}\varphi$ となり、二重否定除去が得られる。逆に、二重否定除去を加えた体系では、$\varphi,\lnot\varphi\vdash\bot$ と公理 7（$\bot\to\psi$）から $\varphi,\lnot\varphi\vdash\psi$、演繹定理により $\lnot\varphi\vdash\varphi\to\psi$ である。したがって $(\varphi\to\psi)\to\varphi,\lnot\varphi\vdash\varphi$（$\lnot\varphi\vdash\varphi\to\psi$ と仮定 $(\varphi\to\psi)\to\varphi$ から）であり、$\varphi,\lnot\varphi\vdash\bot$ と合わせて $(\varphi\to\psi)\to\varphi,\lnot\varphi\vdash\bot$、すなわち $(\varphi\to\psi)\to\varphi\vdash\lnot\lnot\varphi$ となる。二重否定除去で $(\varphi\to\psi)\to\varphi\vdash\varphi$ が得られ、演繹定理により Peirce の法則が証明できる。したがって Peirce の法則をすべての式について加えても古典論理になる。

注意として、この命題は「すべての $\varphi$ について」加える場合の主張である。1 つの命題変数 $p$ について $\lnot\lnot p\to p$ を仮定しても、$p\lor\lnot p$ は導けない。実際 ex-intuitionistic-logic-opens の $U=(-\infty,0)$ では $\lnot\lnot U=\operatorname{int}(\mathbb{R}\setminus(0,\infty))=U$ なので、$p$ に $U$ を割り当てると $\lnot\lnot p\to p$ の値は $\mathbb{R}$、$p\lor\lnot p$ の値は $\mathbb{R}\setminus\{0\}$ である。$\lnot\lnot p\to p\vdash_{\mathrm{I}}p\lor\lnot p$ なら演繹定理により $(\lnot\lnot p\to p)\to(p\lor\lnot p)$ が証明可能になるが、その値は $\mathbb{R}\setminus\{0\}$ なので thm-intuitionistic-logic-soundness に反する。

Heyting 代数による意味論

Heyting 代数での値

$H$ を Heyting代数とし、含意を $\Rightarrow$、否定を $\lnot a:=a\Rightarrow0$ と書く。命題変数から $H$ への写像 $v$ を付値といい、論理式の値 $[\![\varphi]\!]_v\in H$ を
$$ [\![p_i]\!]_v=v(p_i),\quad[\![\bot]\!]_v=0,\quad[\![\varphi\land\psi]\!]_v=[\![\varphi]\!]_v\land[\![\psi]\!]_v,\quad[\![\varphi\lor\psi]\!]_v=[\![\varphi]\!]_v\lor[\![\psi]\!]_v,\quad[\![\varphi\to\psi]\!]_v=[\![\varphi]\!]_v\Rightarrow[\![\psi]\!]_v $$
で帰納的に定める。すべての Heyting 代数 $H$ とすべての付値 $v$ について $[\![\varphi]\!]_v=1$ であるとき、$\varphi$ は Heyting 代数で妥当 であるという。

$H$ が 2 元の Boolean代数 $\{0<1\}$ のときは、$1$ を真、$0$ を偽とみなせば、これは通常の真理値表による値である。

Heyting 代数に関する健全性

$\vdash_{\mathrm{I}}\varphi$ ならば、すべての Heyting 代数 $H$ とすべての付値 $v$ について $[\![\varphi]\!]_v=1$ である。

Heyting 代数の定義（Heyting代数の記事の定義「Heyting代数」）により、$c\le(a\Rightarrow b)\iff c\land a\le b$ である。$c=1$ とすると、$a\Rightarrow b=1\iff a\le b$ である（$(\ast)$）。したがって、各公理の値が $1$ であることは、それぞれ次の不等式に帰着する（$a,b,c$ は $\varphi,\psi,\chi$ の値）。

公理 1：$a\le(b\Rightarrow a)$。これは $a\land b\le a$ と同値である。
公理 2：$(a\Rightarrow(b\Rightarrow c))\le((a\Rightarrow b)\Rightarrow(a\Rightarrow c))$。随伴を 2 回使うと、$x:=a\Rightarrow(b\Rightarrow c)$、$y:=a\Rightarrow b$ について $x\land y\land a\le c$ と同値である。$a\land y\le b$、$a\land x\le b\Rightarrow c$ なので、$x\land y\land a\le b\land(b\Rightarrow c)\le c$ である。
公理 3・4・5：$a\land b\le a$、$a\land b\le b$、$a\le b\Rightarrow(a\land b)$（$a\land b\le a\land b$ と同値）、$a\le a\lor b$、$b\le a\lor b$。
公理 6：$x:=a\Rightarrow c$、$y:=b\Rightarrow c$ について $x\land y\land(a\lor b)\le c$ と同値である。Heyting 代数は分配的（Heyting代数の記事の命題「含意から従う式」）なので、左辺は $(x\land y\land a)\lor(x\land y\land b)\le c\lor c=c$ である。
公理 7：$0\le a$。
前件肯定については、$[\![\varphi]\!]_v=1$ かつ $[\![\varphi\to\psi]\!]_v=1$ なら、$(\ast)$ により $1\le[\![\psi]\!]_v$ である。導出の長さについての帰納法により、証明可能な式の値はすべて $1$ である。$\square$

直観主義論理で証明できない式

命題変数 $p,q$ について、$p\lor\lnot p$、$\lnot\lnot p\to p$、$((p\to q)\to p)\to p$、$\lnot(p\land q)\to(\lnot p\lor\lnot q)$ は古典論理の恒真式だが、直観主義論理では証明できない。特に、直観主義命題論理は無矛盾である（$\bot$ は証明できない）。

はじめの 3 つは ex-intuitionistic-logic-three-chain、4 つ目は ex-intuitionistic-logic-opens で、値が $1$ でない付値を与えた。thm-intuitionistic-logic-soundness の対偶により、これらは証明できない。$\bot$ の値はつねに $0\ne1$ である。4 つの式が恒真式であることは、2 元の Boolean 代数で値が $1$ になることを場合分けで確かめればよい。$\square$

健全性の逆、すなわち完全性も成り立つ。

Heyting 代数と Kripke モデルに関する完全性

命題論理の論理式 $\varphi$ について、次は同値である。

$\vdash_{\mathrm{I}}\varphi$ である。
$\varphi$ は Heyting 代数で妥当である。
$\varphi$ はすべての有限の Kripke モデルで成り立つ（rem-intuitionistic-logic-completeness）。

完全性定理の出典と Kripke モデル

1 ⇒ 2 は thm-intuitionistic-logic-soundness である。2 ⇒ 1 は、証明可能な同値で論理式を割った Lindenbaum 代数が Heyting 代数になり、その標準的な付値で値が $1$ になる式がちょうど証明可能な式であることから示される（TvD88b 第 13 章）。Kripke モデル とは、半順序集合 $(W,\le)$ と、各命題変数 $p$ に対し上に閉じた部分集合 $V(p)\subset W$（$w\in V(p)$ かつ $w\le w'$ なら $w'\in V(p)$）を与えたものである。$w\Vdash\varphi\to\psi$ を「$w\le w'$ となるすべての $w'$ で、$w'\Vdash\varphi$ なら $w'\Vdash\psi$」と定め、$w\Vdash p$ を $w\in V(p)$ で定め、$\bot$ はどこでも成り立たないとし、$\land,\lor$ は点ごとに定める。$W$ を情報の状態、$\le$ を情報の増加と読めば、本記事の「直感」の節の説明の形式化である。上に閉じた部分集合の全体は Heyting 代数をなし、Kripke モデルは Heyting 代数の付値の特別な場合である。Kripke モデルに関する完全性は Kripke による。有限の Kripke モデルで足りることも示せる（vDa13 第 5 章、TvD88 第 2 章）。有限モデルで足りることから、$\vdash_{\mathrm{I}}\varphi$ かどうかは有限の手続きで判定できる。

古典論理との関係

Glivenko の定理

命題論理の論理式 $\varphi$ について、$\vdash_{\mathrm{C}}\varphi$ であることと $\vdash_{\mathrm{I}}\lnot\lnot\varphi$ であることは同値である。特に、$\lnot\psi$ の形の論理式については、古典論理で証明可能なら直観主義論理でも証明可能である。

Glivenko の定理の出典

Glivenko（1929 年）による。証明は TvD88 第 2 章に譲る。後半は前半と prop-intuitionistic-logic-derivations の 3（$\lnot\lnot\lnot\psi\to\lnot\psi$）から従う。この定理により、命題論理の範囲では、古典論理の定理は二重否定を付ければすべて直観主義論理の定理になり、直観主義論理が古典論理と矛盾する定理を含まないこと（def-intuitionistic-logic-hilbert の直後の段落）がさらに精密になる。述語論理ではこの形のままでは成り立たず（たとえば $\lnot\lnot\forall x\,(P(x)\lor\lnot P(x))$ は直観主義述語論理で証明できない）、論理式の各部分に二重否定を入れる Gödel–Gentzen の否定翻訳が代わりに使われる（TvD88 第 2 章）。

選言特性

$\vdash_{\mathrm{I}}\varphi\lor\psi$ ならば、$\vdash_{\mathrm{I}}\varphi$ または $\vdash_{\mathrm{I}}\psi$ である。

選言特性の出典

証明は vDa13 第 5 章、TvD88 第 2 章に譲る（Kripke モデルを 2 つ並べて下に新しい点を付け加える構成による）。この性質は BHK 解釈の「$\varphi\lor\psi$ の証明はどちらを証明するかの指定を含む」を形式的な体系について裏付ける。古典論理はこの性質をもたない。$p\lor\lnot p$ は古典論理で証明可能だが、$p$ も $\lnot p$ も恒真式ではないので古典論理で証明できない。

トポスと型理論

トポスの内部論理

トポスの各対象の部分対象の全体は Heyting 代数をなし、トポスの内部論理は一般に直観主義論理になる（MM92 Chapter IV・VI、トポスの記事）。真理値の対象は部分対象分類子 $\Omega$ であり、$\Omega$ は内部の Heyting 代数になる。たとえば位相空間 $X$ 上の層のトポスでは、終対象の部分対象はちょうど $X$ の開集合であり、ex-intuitionistic-logic-opens の Heyting 代数が真理値の代数として現れる。前層のトポスでは部分前層の Heyting 代数（Heyting代数の記事の定理「部分前層の含意」）が現れ、半順序集合上の前層のトポスは Kripke モデルの一般化になっている。集合の圏の内部論理は古典論理であり、内部論理で排中律が成り立つトポスはブール的であるという（MM92 Chapter VI）。

補足

構成的数学：直観主義論理を用いて数学を展開する立場を構成的数学という。そこでは、存在証明から具体的な対象や手続きを取り出せる。一方で、「実数 $x$ について $x=0$ または $x\ne0$」のように古典的には当然の主張の多くが証明できなくなる（TvD88 第 1 章）。
証明と計算：BHK 解釈の「$\varphi\to\psi$ の証明は手続き」という読みは、直観主義論理の証明と型付きラムダ計算のプログラムを対応させる Curry–Howard 対応として定式化され、型理論の基礎になっている。
排中律を認めないことの意味：直観主義論理は $\lnot(\varphi\lor\lnot\varphi)$ を証明するわけではない（その否定 $\lnot\lnot(\varphi\lor\lnot\varphi)$ が証明可能である。prop-intuitionistic-logic-derivations の 4）。したがって直観主義論理に排中律を加えても矛盾は生じず、古典論理が得られる（prop-intuitionistic-logic-classical）。
文献：直観主義論理の標準的な教科書は TvD88、TvD88b、自然演繹による入門は vDa13 第 5 章である。