自然演繹

同義語：自然演繹体系natural deduction

概要

前提知識: 命題論理, 一階論理の証明体系

数学の証明では、「$A$ を仮定すると $B$ が示せる。よって $A$ ならば $B$」「$A$ の場合も $B$ の場合も $C$ になる。よって $A$ または $B$ なら $C$」「$A$ でないと仮定すると矛盾する。よって $A$」のように、仮定を一時的に置いて議論し、結論を得たところでその仮定を外す。自然演繹（natural deduction）は、この推論の型を論理結合子ごとの規則として形式化した証明体系である。各結合子には、それを含む式を結論として作る 導入規則 と、それを含む式を使う 除去規則 が 1 組ずつある。導出は論理式を並べた木で、葉に置いた仮定のうち、途中の規則で外されずに残ったものが結論の前提になる。
一階論理の証明体系の記事の Hilbert 流の体系では、推論規則は前件肯定だけで、「$A$ を仮定して $B$ を導けば $A\to B$」は演繹定理として導出の外で示す定理だった。自然演繹では、これが規則 $\to\mathrm I$ そのものになる。本記事では命題論理の自然演繹を 1 つ固定し、導出を正確に定義したうえで、導出できる式はすべて恒真式であること（健全性）と、Hilbert 流の体系で導出できる式は自然演繹でも導出できることを証明する。最後に量化記号の規則を述べる。

定義

論理式

命題論理の論理式・付値・恒真式・論理的帰結は命題論理の記事の定義「論理式」「付値と真理値」「恒真式・充足可能性・論理的帰結」による。ただし本記事では、命題変数のほかに定数 $\bot$（矛盾）も論理式とし、付値はつねに $v(\bot)=\mathrm F$ とする。論理式の集合 $\Gamma$ と論理式 $A$ について、$\Gamma$ のすべての元を真にする付値がすべて $A$ を真にすることを $\Gamma\models A$ と書く。

推論規則

自然演繹の推論規則を次に示す。横線の上が前提、下が結論である。$[A]^{n}$ は、その上の部分で番号 $n$ を付けた仮定 $A$ を置き、横線の右に同じ番号を付けた規則でその仮定を外す（discharge する）ことを表す。縦の点は、仮定から前提までの導出を表す。規則の形は Zac25 §11.2（pp. 195–196）の命題の規則と同じである。
$$ \dfrac{A\qquad B}{A\land B}\ {\scriptstyle\land\mathrm I}\qquad \dfrac{A\land B}{A}\ {\scriptstyle\land\mathrm E}\qquad \dfrac{A\land B}{B}\ {\scriptstyle\land\mathrm E}\qquad \dfrac{A}{A\lor B}\ {\scriptstyle\lor\mathrm I}\qquad \dfrac{B}{A\lor B}\ {\scriptstyle\lor\mathrm I} $$
$$ \dfrac{A\lor B\qquad\begin{array}{c}[A]^{n}\\ \vdots\\ C\end{array}\qquad\begin{array}{c}[B]^{n}\\ \vdots\\ C\end{array}}{C}\ {\scriptstyle\lor\mathrm E^{n}}\qquad \dfrac{\begin{array}{c}[A]^{n}\\ \vdots\\ B\end{array}}{A\to B}\ {\scriptstyle\to\mathrm I^{n}}\qquad \dfrac{A\to B\qquad A}{B}\ {\scriptstyle\to\mathrm E} $$
$$ \dfrac{\begin{array}{c}[A]^{n}\\ \vdots\\ \bot\end{array}}{\lnot A}\ {\scriptstyle\lnot\mathrm I^{n}}\qquad \dfrac{\lnot A\qquad A}{\bot}\ {\scriptstyle\lnot\mathrm E}\qquad \dfrac{\bot}{A}\ {\scriptstyle\bot_{\mathrm I}}\qquad \dfrac{\begin{array}{c}[\lnot A]^{n}\\ \vdots\\ \bot\end{array}}{A}\ {\scriptstyle\bot_{\mathrm C}^{\,n}} $$
$\to\mathrm E$ は前件肯定（modus ponens）である。$\bot_{\mathrm I}$ は「矛盾からは何でも出る」、$\bot_{\mathrm C}$ は背理法（$A$ でないと仮定して矛盾を導けば $A$）であり、$\lnot\mathrm I$ は否定を結論とする背理法である。

導出

導出を、結論と「外されずに残った仮定」の集合とともに、木の組み立てに沿って定める。

自然演繹の導出

導出 $D$ と、その結論 $\mathrm{concl}(D)$、開いた仮定 の集合 $\mathrm{Open}(D)$ を次で帰納的に定める。

論理式 $A$ を 1 つだけ置いた木は導出で、結論は $A$、開いた仮定の集合は $\{A\}$ である。
$D_1,\dots,D_k$ が導出で、それらの結論 $\mathrm{concl}(D_1),\dots,\mathrm{concl}(D_k)$ を前提として規則を 1 回使って結論 $C$ を得るとき、$D_1,\dots,D_k$ を並べてその下に $C$ を置いた木 $D$ は導出で、$\mathrm{concl}(D)=C$ である。$\mathrm{Open}(D)$ は、$\mathrm{Open}(D_1)\cup\cdots\cup\mathrm{Open}(D_k)$ から規則が外す仮定を除いたもので、具体的には次のとおりである。

$\to\mathrm I$（$D_1$ の結論が $B$、$C=A\to B$）と $\lnot\mathrm I$（$D_1$ の結論が $\bot$、$C=\lnot A$）では $\mathrm{Open}(D)=\mathrm{Open}(D_1)\setminus\{A\}$。
$\bot_{\mathrm C}$（$D_1$ の結論が $\bot$）では $\mathrm{Open}(D)=\mathrm{Open}(D_1)\setminus\{\lnot C\}$。
$\lor\mathrm E$（$D_1,D_2,D_3$ の結論が $A\lor B$、$C$、$C$）では $\mathrm{Open}(D)=\mathrm{Open}(D_1)\cup(\mathrm{Open}(D_2)\setminus\{A\})\cup(\mathrm{Open}(D_3)\setminus\{B\})$。
ほかの規則では $\mathrm{Open}(D)=\mathrm{Open}(D_1)\cup\cdots\cup\mathrm{Open}(D_k)$。
論理式の集合 $\Gamma$ と論理式 $A$ について、結論が $A$ で $\mathrm{Open}(D)\subset\Gamma$ となる導出 $D$ があるとき、$A$ は $\Gamma$ から 導出可能 であるといい、$\Gamma\vdash A$ と書く。$\emptyset\vdash A$ を $\vdash A$ と書き、$A$ を定理という。

規則は仮定を外すことを「許す」だけで、外すべき仮定が導出の中になくてもよい。たとえば $\to\mathrm I$ は、$A$ を仮定していない $B$ の導出からも $A\to B$ を結論してよい（Zac25 pp. 196, 200）。上の定義では、外せる仮定はすべて外すことにしているが、外さずに残しても開いた仮定の集合が大きくなるだけなので、$\Gamma\vdash A$ の意味は変わらない。証明図では、どの規則がどの仮定を外したかを番号で示す。
定義から、開いた仮定の集合はいつも有限集合である。したがって、$\Gamma\vdash A$ なら有限部分集合 $\Gamma_0:=\mathrm{Open}(D)\subset\Gamma$ について $\Gamma_0\vdash A$ であり、$\Gamma\subset\Delta$ かつ $\Gamma\vdash A$ なら $\Delta\vdash A$ である（同じ導出を使えばよい）。

直感

自然演繹の導出は、「いま何を仮定しているか」を木の上で追跡する。仮定 $A$ を置いた地点から、それを外す規則までが、その仮定の有効範囲である。導入規則は結合子を含む式を「作る」方法を、除去規則は「使う」方法を与え、両者は対になっている。たとえば $A\land B$ は $A$ と $B$ から作り、作った $A\land B$ からは $A$ と $B$ が取り出せる。$A\to B$ は「$A$ を仮定して $B$」から作り、$A\to B$ と $A$ からは $B$ が出る。この対応があるので、自然演繹の導出は普通の数学の証明の筋をそのままなぞる形になる（Zac25 §9.3、pp. 156–157）。

例と反例

連言の入れ替え

$\vdash(A\land B)\to(B\land A)$ である。仮定 $A\land B$ から $B$ と $A$ を取り出して組み直し、最後に仮定を外す。
$$ \begin{prooftree} \AxiomC{$[A\land B]^{1}$} \RightLabel{$\land$E} \UnaryInfC{$B$} \AxiomC{$[A\land B]^{1}$} \RightLabel{$\land$E} \UnaryInfC{$A$} \RightLabel{$\land$I} \BinaryInfC{$B\land A$} \RightLabel{$\to$I$^{1}$} \UnaryInfC{$(A\land B)\to(B\land A)$} \end{prooftree} $$
仮定 $A\land B$ は 2 つの葉に現れるが、どちらも最後の $\to\mathrm I$ で外される。開いた仮定は残らない。

二重否定の除去と排中律

$\vdash\lnot\lnot A\to A$ である。$\lnot A$ を仮定すると $\lnot\lnot A$ と矛盾するので、$\bot_{\mathrm C}$ で $A$ を得る。
$$ \begin{prooftree} \AxiomC{$[\lnot\lnot A]^{2}$} \AxiomC{$[\lnot A]^{1}$} \RightLabel{$\lnot$E} \BinaryInfC{$\bot$} \RightLabel{$\bot_{\mathrm C}^{\,1}$} \UnaryInfC{$A$} \RightLabel{$\to$I$^{2}$} \UnaryInfC{$\lnot\lnot A\to A$} \end{prooftree} $$
排中律 $\vdash A\lor\lnot A$ も導出できる。$\lnot(A\lor\lnot A)$ を仮定すると、まず $A$ を仮定して $A\lor\lnot A$ を作れば矛盾するので $\lnot A$ が得られ、その $\lnot A$ から $A\lor\lnot A$ を作るとふたたび矛盾する。
$$ \begin{prooftree} \AxiomC{$[\lnot(A\lor\lnot A)]^{2}$} \AxiomC{$[\lnot(A\lor\lnot A)]^{2}$} \AxiomC{$[A]^{1}$} \RightLabel{$\lor$I} \UnaryInfC{$A\lor\lnot A$} \RightLabel{$\lnot$E} \BinaryInfC{$\bot$} \RightLabel{$\lnot$I$^{1}$} \UnaryInfC{$\lnot A$} \RightLabel{$\lor$I} \UnaryInfC{$A\lor\lnot A$} \RightLabel{$\lnot$E} \BinaryInfC{$\bot$} \RightLabel{$\bot_{\mathrm C}^{\,2}$} \UnaryInfC{$A\lor\lnot A$} \end{prooftree} $$
OLT26 Example 10.6（pp. 147–148）も、組み立て方は少し違うが、$\bot_{\mathrm C}$ を使って排中律を導出している。上の 2 つの導出はどちらも $\bot_{\mathrm C}$ を使っている。$\bot_{\mathrm C}$ を除くと $\lnot\lnot p\to p$ は導出できなくなる（prop-natural-deduction-intuitionistic）。

仮定の外し方や規則の条件を崩すと、何が成り立たなくなるかを表にまとめる。

外す条件	反例	成り立たなくなること
仮定は規則で外したときだけ閉じる	葉 $p$ 1 つだけの木を、開いた仮定のない $p$ の導出とみなす	健全性（$\vdash p$）
$\to\mathrm I$ で外すのは前件 $A$ の仮定だけ	葉 $q$ に $\to\mathrm I$ を使い、仮定 $q$ を外して $p\to q$ を結論する	健全性（$\vdash p\to q$）
$\lor\mathrm E$ は 2 つの場合の両方を使う	$p\lor q$ と、$p$ を仮定した $p$ の導出だけから $p$ を結論する	健全性（$\{p\lor q\}\vdash p$）
$\bot_{\mathrm C}$ がある	$\bot_{\mathrm C}$ を除いた体系	恒真式 $\lnot\lnot p\to p$ の導出（完全性）
$\forall\mathrm I$ の固有変数の条件	「量化記号の規則」の節の $\exists x\,P(x)$ から $\forall x\,P(x)$ への導出	健全性（$\{\exists x\,P(x)\}\vdash\forall x\,P(x)$）

反例：規則を崩した導出

表の 1〜3 行目の「導出」が健全性を破ることを確かめる。どれも、前提を真にして結論を偽にする付値がある。

$\vdash p$ となるが、$p$ を偽にする付値があるので $p$ は恒真式でない。
$\vdash p\to q$ となるが、$p$ を真、$q$ を偽にする付値で $p\to q$ は偽である。規則どおりの $\to\mathrm I$ では、葉 $q$ から $p\to q$ を結論しても仮定 $q$ は開いたまま残り、$\{q\}\vdash p\to q$ が得られるだけである。これは正しい（$q$ が真なら $p\to q$ は真）。
$\{p\lor q\}\vdash p$ となるが、$p$ を偽、$q$ を真にする付値で $p\lor q$ は真、$p$ は偽である。規則どおりの $\lor\mathrm E$ では、$q$ を仮定した場合にも $p$ を導出しなければならず、それはできない（後の thm-natural-deduction-soundness による）。

4 行目は prop-natural-deduction-intuitionistic、5 行目は「量化記号の規則」の節で確かめる。

性質

健全性

自然演繹の健全性

論理式の集合 $\Gamma$ と論理式 $A$ について、$\Gamma\vdash A$ ならば $\Gamma\models A$ である。とくに、自然演繹の定理はすべて恒真式である。

導出の組み立てに沿った帰納法

すべての導出 $D$ について $\mathrm{Open}(D)\models\mathrm{concl}(D)$ であることを、$D$ の組み立て（def-natural-deduction-derivation）に沿った帰納法で示す。これが示せれば、$\Gamma\vdash A$ のとき $\mathrm{Open}(D)\subset\Gamma$ なので、$\Gamma$ を真にする付値は $\mathrm{Open}(D)$ を真にし、$A$ を真にする。
以下、付値 $v$ が集合 $S$ のすべての元を真にすることを「$v$ は $S$ を満たす」という。$D$ の最後の規則の前提の導出を $D_1,D_2,D_3$ とし、帰納法の仮定として $\mathrm{Open}(D_j)\models\mathrm{concl}(D_j)$ を使う。$v$ を $\mathrm{Open}(D)$ を満たす付値とし、$v$ が $\mathrm{concl}(D)$ を真にすることを示す。

1 つの葉 $A$：$\mathrm{Open}(D)=\{A\}$ なので $v(A)=\mathrm T$ である。
仮定を外さない規則（$\land\mathrm I$、$\land\mathrm E$、$\lor\mathrm I$、$\to\mathrm E$、$\lnot\mathrm E$、$\bot_{\mathrm I}$）：$\mathrm{Open}(D)$ は各 $\mathrm{Open}(D_j)$ を含むので、$v$ は各 $\mathrm{Open}(D_j)$ を満たし、帰納法の仮定により前提はすべて $v$ で真である。$\land\mathrm I$、$\land\mathrm E$、$\lor\mathrm I$、$\to\mathrm E$ では、付値の規則から結論も真である（たとえば $\to\mathrm E$ では $v(A\to B)=v(A)=\mathrm T$ から $v(B)=\mathrm T$）。$\lnot\mathrm E$ では前提 $\lnot A$ と $A$ がともに真になり、これは不可能なので、$\mathrm{Open}(D)$ を満たす $v$ はない。$\bot_{\mathrm I}$ では前提 $\bot$ が真になり、$v(\bot)=\mathrm F$ に反するので、やはりそのような $v$ はない。どちらの場合も主張は成り立つ。
$\to\mathrm I$（$D_1$ の結論 $B$ から $A\to B$）：$v(A)=\mathrm F$ なら $v(A\to B)=\mathrm T$ である。$v(A)=\mathrm T$ なら、$\mathrm{Open}(D_1)\subset\mathrm{Open}(D)\cup\{A\}$ なので $v$ は $\mathrm{Open}(D_1)$ を満たし、帰納法の仮定から $v(B)=\mathrm T$、よって $v(A\to B)=\mathrm T$ である。
$\lnot\mathrm I$（$D_1$ の結論 $\bot$ から $\lnot A$）：$v(A)=\mathrm T$ と仮定すると、上と同様に $v$ は $\mathrm{Open}(D_1)$ を満たし、帰納法の仮定から $v(\bot)=\mathrm T$ となって矛盾する。よって $v(A)=\mathrm F$、$v(\lnot A)=\mathrm T$ である。
$\bot_{\mathrm C}$（$D_1$ の結論 $\bot$ から $A$）：$v(A)=\mathrm F$ と仮定すると $v(\lnot A)=\mathrm T$ であり、$\mathrm{Open}(D_1)\subset\mathrm{Open}(D)\cup\{\lnot A\}$ なので $v$ は $\mathrm{Open}(D_1)$ を満たし、$v(\bot)=\mathrm T$ となって矛盾する。よって $v(A)=\mathrm T$ である。
$\lor\mathrm E$（結論 $A\lor B$、$C$、$C$ の $D_1,D_2,D_3$ から $C$）：$v$ は $\mathrm{Open}(D_1)$ を満たすので $v(A\lor B)=\mathrm T$ である。$v(A)=\mathrm T$ なら、$\mathrm{Open}(D_2)\subset\mathrm{Open}(D)\cup\{A\}$ なので $v$ は $\mathrm{Open}(D_2)$ を満たし、$v(C)=\mathrm T$ である。$v(B)=\mathrm T$ なら同様に $D_3$ から $v(C)=\mathrm T$ である。
規則はこれで尽きる。$\square$

この証明の各場合は、規則ごとに「前提が（外した仮定を加えれば）真なら結論も真」を確かめているだけである。Zac25 の Theorem 11.27（p. 216）は、量化記号の規則を含む一階論理の自然演繹について同じ定理を示している（証明の一部は演習）。健全性の対偶から、$\Gamma\vdash A$ でないことを示すには、$\Gamma$ を真にして $A$ を偽にする付値を 1 つ見つければよい。

Hilbert 流の体系との関係

一階論理の証明体系の記事の体系 $\mathbf H$ の命題論理の部分を $\mathbf H_0$ とする。すなわち、論理式は命題変数から $\lnot,\to$ だけで作り、公理は次の公理図式の実例、推論規則は前件肯定（MP）だけとする。

(A1) $\varphi\to(\psi\to\varphi)$
(A2) $(\varphi\to(\psi\to\chi))\to((\varphi\to\psi)\to(\varphi\to\chi))$
(A3) $(\lnot\psi\to\lnot\varphi)\to((\lnot\psi\to\varphi)\to\psi)$
$\Gamma$ からの $\mathbf H_0$ の導出とは、各行が公理か $\Gamma$ の元か、前の 2 行から MP で得られる論理式の有限列であり、$\varphi$ で終わる導出があることを $\Gamma\vdash_{\mathbf H_0}\varphi$ と書く（同記事の定義「証明体系・導出・証明可能性」）。

Hilbert 流の導出は自然演繹に移せる

$\lnot,\to$ だけで作った論理式の集合 $\Gamma$ と論理式 $\varphi$ について、$\Gamma\vdash_{\mathbf H_0}\varphi$ ならば、自然演繹で $\Gamma\vdash\varphi$ である。

公理の自然演繹での導出と、MP を →E に置き換えること

まず、(A1)〜(A3) の実例はどれも、開いた仮定のない自然演繹の導出をもつ。
(A1)：仮定 $\varphi$ に $\to\mathrm I$ を 2 回使う。1 回目は仮定 $\psi$ がなくても $\psi\to\varphi$ を結論してよい。
$$ \begin{prooftree} \AxiomC{$[\varphi]^{1}$} \RightLabel{$\to$I} \UnaryInfC{$\psi\to\varphi$} \RightLabel{$\to$I$^{1}$} \UnaryInfC{$\varphi\to(\psi\to\varphi)$} \end{prooftree} $$
def-natural-deduction-derivation で開いた仮定を計算すると、1 回目の $\to\mathrm I$ の後は $\{\varphi\}\setminus\{\psi\}$、2 回目の後は空集合である。
(A2)：3 つの仮定 $\varphi\to(\psi\to\chi)$、$\varphi\to\psi$、$\varphi$ から $\to\mathrm E$ を 3 回使って $\chi$ を得て、仮定を内側から順に外す。
$$ \begin{prooftree} \AxiomC{$[\varphi\to(\psi\to\chi)]^{3}$} \AxiomC{$[\varphi]^{1}$} \RightLabel{$\to$E} \BinaryInfC{$\psi\to\chi$} \AxiomC{$[\varphi\to\psi]^{2}$} \AxiomC{$[\varphi]^{1}$} \RightLabel{$\to$E} \BinaryInfC{$\psi$} \RightLabel{$\to$E} \BinaryInfC{$\chi$} \RightLabel{$\to$I$^{1}$} \UnaryInfC{$\varphi\to\chi$} \RightLabel{$\to$I$^{2}$} \UnaryInfC{$(\varphi\to\psi)\to(\varphi\to\chi)$} \RightLabel{$\to$I$^{3}$} \UnaryInfC{$(\varphi\to(\psi\to\chi))\to((\varphi\to\psi)\to(\varphi\to\chi))$} \end{prooftree} $$
(A3)：仮定 $\lnot\psi\to\lnot\varphi$、$\lnot\psi\to\varphi$、$\lnot\psi$ から $\lnot\varphi$ と $\varphi$ が出て矛盾するので、$\bot_{\mathrm C}$ で仮定 $\lnot\psi$ を外して $\psi$ を得る。
$$ \begin{prooftree} \AxiomC{$[\lnot\psi\to\lnot\varphi]^{3}$} \AxiomC{$[\lnot\psi]^{1}$} \RightLabel{$\to$E} \BinaryInfC{$\lnot\varphi$} \AxiomC{$[\lnot\psi\to\varphi]^{2}$} \AxiomC{$[\lnot\psi]^{1}$} \RightLabel{$\to$E} \BinaryInfC{$\varphi$} \RightLabel{$\lnot$E} \BinaryInfC{$\bot$} \RightLabel{$\bot_{\mathrm C}^{\,1}$} \UnaryInfC{$\psi$} \RightLabel{$\to$I$^{2}$} \UnaryInfC{$(\lnot\psi\to\varphi)\to\psi$} \RightLabel{$\to$I$^{3}$} \UnaryInfC{$(\lnot\psi\to\lnot\varphi)\to((\lnot\psi\to\varphi)\to\psi)$} \end{prooftree} $$
(A2)・(A3) の図でも、開いた仮定は番号どおりに外れ、最後に空集合になる。
次に、$\Gamma$ からの $\mathbf H_0$ の導出 $\varphi_1,\dots,\varphi_m=\varphi$ をとり、各 $i$ について、結論が $\varphi_i$ で開いた仮定が $\Gamma$ に含まれる自然演繹の導出 $D_i$ を、$i$ に関する帰納法で作る。$\varphi_i$ が公理なら上の導出を、$\varphi_i\in\Gamma$ なら葉 $\varphi_i$ 1 つだけの木をとる。$\varphi_i$ が $\varphi_j$ と $\varphi_k=(\varphi_j\to\varphi_i)$（$j,k< i$）から MP で得られたなら、$D_k$ と $D_j$ に $\to\mathrm E$ を使った木を $D_i$ とする。$\mathrm{Open}(D_i)=\mathrm{Open}(D_k)\cup\mathrm{Open}(D_j)\subset\Gamma$ である。$i=m$ として $\Gamma\vdash\varphi$ を得る。$\square$

逆向き「$\lnot,\to$ だけの論理式について、自然演繹で $\Gamma\vdash\varphi$ なら $\Gamma\vdash_{\mathbf H_0}\varphi$」も成り立つ。thm-natural-deduction-soundness により $\Gamma\models\varphi$ であり、$\mathbf H_0$ の完全性（Bil03 Theorem 4.12、p. 16。本記事では証明しない）により $\Gamma\vdash_{\mathbf H_0}\varphi$ となるからである。同じ理由で、$\lnot,\to$ だけの論理式については、自然演繹の導出可能性は $\Gamma\models\varphi$ と一致する。$\land,\lor,\bot$ を含む論理式を含めた自然演繹の完全性は OLT26 Corollary 13.7（p. 192）にある。自然演繹の導出を $\mathbf H_0$ の導出に直接書き換える場合、$\to\mathrm I$ にあたるのが一階論理の証明体系の記事の定理「演繹定理」である。

背理法の規則の役割

背理法の規則を除いた体系

自然演繹から規則 $\bot_{\mathrm C}$ を除いた体系では、命題変数 $p$ について $\lnot\lnot p\to p$ は導出できない。

3 つの値をとる付値で健全性を示す

要点：値を $0<\tfrac12<1$ の 3 つに増やした付値を考えると、$\bot_{\mathrm C}$ 以外の規則は健全性の証明と同じ形の議論が通るが、$\lnot\lnot p\to p$ は $p$ に $\tfrac12$ を与えると値 $1$ をとらない。

詳しい証明を開く

$H:=\{0,\tfrac12,1\}$ とし、古典論理の記事の例「反例：3 つの真理値」の Heyting 代数の 3 元の鎖と同じく、$a\wedge b:=\min(a,b)$、$a\vee b:=\max(a,b)$、$a\Rightarrow b:=1$（$a\le b$ のとき）、$:=b$（そうでないとき）と定める。命題変数への値の割り当て $w$ を、$w(\bot):=0$、$w(\lnot A):=w(A)\Rightarrow0$、$w(A\land B):=w(A)\wedge w(B)$、$w(A\lor B):=w(A)\vee w(B)$、$w(A\to B):=w(A)\Rightarrow w(B)$ で広げる。$H$ の元 $x,a,b$ について $x\le(a\Rightarrow b)\iff\min(x,a)\le b$ が成り立つ（$a\le b$ なら両辺とも成り立ち、$a>b$ なら両辺とも $x\le b$ と同値）。

集合 $S$ について $w(S):=\min\{w(B)\mid B\in S\}$（$S=\emptyset$ なら $1$）とおき、$\bot_{\mathrm C}$ を使わないすべての導出 $D$ について $w(\mathrm{Open}(D))\le w(\mathrm{concl}(D))$ を、導出の組み立てに沿った帰納法で示す。$m:=w(\mathrm{Open}(D))$、$m_j:=w(\mathrm{Open}(D_j))$ とおく。

葉：$m=w(A)$ である。
$\land\mathrm I$、$\land\mathrm E$、$\lor\mathrm I$：$m\le m_j\le$（前提の値）から、$\min,\max$ の性質で従う。
$\to\mathrm E$、$\lnot\mathrm E$：$m\le\min(w(A\to B),w(A))\le w(B)$（上の同値で $x:=w(A\to B)$ とする）。$\lnot\mathrm E$ は $B=\bot$ の場合で、結論 $\bot$ の値 $0$ 以下になる。
$\bot_{\mathrm I}$：$m\le w(\bot)=0$ なので $m=0$ で、何の値以下でもある。
$\to\mathrm I$、$\lnot\mathrm I$：$\mathrm{Open}(D_1)\subset\mathrm{Open}(D)\cup\{A\}$ なので $\min(m,w(A))\le m_1\le w(B)$、上の同値で $m\le w(A)\Rightarrow w(B)=w(A\to B)$ である（$\lnot\mathrm I$ は $B=\bot$）。
$\lor\mathrm E$：$m\le w(A)\vee w(B)$ であり、$\min(m,w(A))\le m_2\le w(C)$、$\min(m,w(B))\le m_3\le w(C)$ である。$H$ は全順序なので $m=\min(m,\max(w(A),w(B)))=\max(\min(m,w(A)),\min(m,w(B)))\le w(C)$ である。

よって開いた仮定のない導出の結論は値 $1$ をとる。ところが $w(p)=\tfrac12$ とすると、$w(\lnot p)=\tfrac12\Rightarrow0=0$、$w(\lnot\lnot p)=0\Rightarrow0=1$、$w(\lnot\lnot p\to p)=1\Rightarrow\tfrac12=\tfrac12$ である。よって $\lnot\lnot p\to p$ は $\bot_{\mathrm C}$ なしでは導出できない。$\square$

この証明で $\bot_{\mathrm C}$ だけが通らないのは、$\min(m,w(\lnot A))\le0$ から $m\le w(A)$ が出ないからである。実際 $m=1$、$w(A)=\tfrac12$ では $w(\lnot A)=0$ なので前者は成り立つが、後者は成り立たない。$\bot_{\mathrm C}$ を除いた体系は直観主義論理の自然演繹であり（OLT26 p. 147）、$\bot_{\mathrm C}$ は古典論理に固有の規則である。直観主義論理の Hilbert 流の体系と、Heyting 代数による同じ種類の議論は直観主義論理の記事にある。

量化記号の規則

一階述語論理の自然演繹では、上の規則に量化記号の規則を加える。Zac25 §11.3（pp. 196–197）の流儀では、導出に現れるのは文（自由変数のない論理式）だけで、$A(x)$ は変数 $x$ が自由に現れうる論理式、$A(t)$ はその $x$ に閉項 $t$ を代入した文、$a$ は定数記号を表す。
$$ \dfrac{A(a)}{\forall x\,A(x)}\ {\scriptstyle\forall\mathrm I}\qquad \dfrac{\forall x\,A(x)}{A(t)}\ {\scriptstyle\forall\mathrm E}\qquad \dfrac{A(t)}{\exists x\,A(x)}\ {\scriptstyle\exists\mathrm I}\qquad \dfrac{\exists x\,A(x)\qquad\begin{array}{c}[A(a)]^{n}\\ \vdots\\ C\end{array}}{C}\ {\scriptstyle\exists\mathrm E^{n}} $$
$\forall\mathrm I$ では、定数記号 $a$ は結論 $\forall x\,A(x)$ にも、前提 $A(a)$ の導出の開いた仮定にも現れてはならない。$\exists\mathrm E$ では、$a$ は $\exists x\,A(x)$ にも $C$ にも、仮定 $A(a)$ 以外の開いた仮定にも現れてはならない。この条件を 固有変数の条件 という。$\forall\mathrm I$ の条件は、「$a$ について何も仮定していないから、$a$ は任意の元の代わりである」ことを保証している。

反例：固有変数の条件を外す

1 項関係記号 $P$ と定数記号 $a$ について、条件を無視すると次の図が作れる（Zac25 p. 198 の例）。
$$ \begin{prooftree} \AxiomC{$\exists x\,P(x)$} \AxiomC{$[P(a)]^{1}$} \RightLabel{$\forall$I} \UnaryInfC{$\forall x\,P(x)$} \RightLabel{$\exists$E$^{1}$} \BinaryInfC{$\forall x\,P(x)$} \end{prooftree} $$
$\forall\mathrm I$ のとき、$a$ は開いた仮定 $P(a)$ に現れているので条件に反する。この図を導出と認めると $\{\exists x\,P(x)\}\vdash\forall x\,P(x)$ となるが、台集合 $\{0,1\}$、$P$ の解釈 $\{0\}$、$a$ の解釈 $0$ の構造では $\exists x\,P(x)$ が真で $\forall x\,P(x)$ が偽なので、健全性が崩れる。

量化記号の規則を加えた体系も健全であり（Zac25 Theorem 11.27、p. 216）、完全である（同書 Theorem 12.20・Corollary 12.21、pp. 245–246）。したがって、文の間の導出可能性は一階論理の証明体系の記事の Hilbert 流の体系 $\mathbf H$ と一致する（同記事の「流儀の比較」の節）。この記事では量化記号の規則についての健全性と完全性を証明しない。