自然演繹 — 導入規則と除去規則
証明体系を実際に組み立てる
初級（大学1-2年レベル）
このページの目標
各論理結合子に与えられる導入規則と除去規則を理解し、仮定の放電を伴う証明木を読み書きできるようになる。これが証明検査カーネルの命題層の正体であることを知る。
1. 自然演繹の発想
入門では推論規則の考え方に触れた。自然演繹は、その推論規則を結合子ごとに体系的にそろえた証明体系である。鍵は、各結合子に二種類の規則を対で与えることである。
- 導入規則（introduction）：その結合子を作る規則
- 除去規則（elimination）：その結合子を使う規則
数学者が普段おこなう「$A$ と $B$ が言えたから $A$ かつ $B$」「$A$ かつ $B$ だから $A$ が言える」という自然な推論を、そのまま規則にしたものである。Gentzen と Prawitz によって整備された。
2. 結合子ごとの規則
まず、規則の「読み方」
これから出てくる規則は、すべて横線の形で書く。横線の上に並ぶのが前提（すでに言えていること）、下にあるのが結論（新しく言えること）である。
$$\dfrac{\text{前提}_1 \quad \text{前提}_2 \quad \cdots}{\text{結論}}$$つまり「横線の上がぜんぶ言えたなら、下が言える」と読む。
右に添えた $(\land\text{I})$ などは規則の名前で、2 文字に分けて読む。先頭の記号（$\land$, $\lor$, $\to$ など）は「どの結合子についての規則か」を指し、続く I は導入 (introduction)＝その結合子を作る規則、E は除去 (elimination)＝その結合子を使う規則を表す。したがって $(\land\text{I})$ は「$\land$ の導入規則」＝連言 $A \land B$ を作る規則と読む。
名前の $\land$ が、結論に現れる結合子 $\land$ と同じ記号なのは偶然ではなく、「これはその $\land$ についての規則だ」と示すためである。同じ理屈で、$\lor$ を作る規則は $(\lor\text{I})$、$\to$ を作る規則は $(\to\text{I})$ と、結合子ごとに導入・除去の名前がそろう。
導入 $\land$I：$A$ と $B$ が別々に言えていれば、合わせて $A \land B$（$A$ かつ $B$）が言える。
除去 $\land$E：$A \land B$ が言えていれば、そこから $A$ だけ、あるいは $B$ だけを取り出せる。
左は「上の $A$ と $B$ から、下の $A\land B$」、右の二つは「上の $A\land B$ から、下の $A$（または $B$）」と読む。
まず分かりやすい除去 $\to$E（モーダスポネンス）から：$A \to B$（$A$ ならば $B$）と $A$ が両方言えていれば、$B$ が言える。
$$\dfrac{A \to B \quad A}{B}\ (\to\text{E})$$導入 $\to$I は自然演繹で最も特徴的な規則：$A \to B$（「$A$ ならば $B$」）を言うには、まず $A$ を仮に正しいとして置く。この「仮に置いた $A$」を角括弧つきで $[A]$ と書く。その仮定のもとで何ステップか導出し（縦の点 $\vdots$ が「途中の導出」を表す）、$B$ にたどり着けたら、$A \to B$ を結論する。同時に、置いた仮定 $[A]$ は役目を終えて取り下げられる（これを放電という。次の §3 で詳しく扱う）。
$$\dfrac{\begin{matrix}[A] \\[2pt] \vdots \\[2pt] B\end{matrix}}{A \to B}\ (\to\text{I})$$図の縦並びは上から順に「$A$ を仮定 → … 途中の導出 … → $B$ が出た」を表し、横線の下で「だから $A \to B$」と結ぶ。日常語の「もし $A$ だとしたら、$B$ になる。ゆえに $A$ ならば $B$」という議論そのものである。
導入 $\lor$I：$A$ が言えていれば、「$A$ または $B$」（$A \lor B$）も当然言える（$B$ から $A \lor B$ も同様）。
$$\dfrac{A}{A \lor B}\ (\lor\text{I}) \qquad \dfrac{B}{A \lor B}\ (\lor\text{I})$$除去 $\lor$E（場合分け）：$A \lor B$ が言えていて、かつ「もし $A$ なら $C$」と「もし $B$ なら $C$」の両方が示せるなら、$A$・$B$ のどちらが本当であっても結論は $C$ になる。これは数学でおなじみの場合分けそのものである。
例：「$n$ は偶数または奇数」が言えていて、「偶数なら $n(n+1)$ は偶数」「奇数なら $n(n+1)$ は偶数」の両方を示せれば、どちらにせよ「$n(n+1)$ は偶数」と結論できる。
導入と除去は釣り合っている。たとえば $A \land B$ を $\land$I で作り、すぐ $\land$E で $A$ を取り出すのは遠回りで、最初から $A$ を使えばよい。この「作ってすぐ使う」無駄を消す操作が簡約であり、計算に対応する（λ計算）。
3. 仮定の放電と証明木
含意の導入 $\to$I が、自然演繹のいちばん特徴的な操作である。$A \to B$ を示すには、まず $A$ を仮定として置き、その下で $B$ を導く。導けたら、仮定 $A$ を角括弧 $[A]$ で囲んで放電（閉じる）し、$A \to B$ を結論する。放電された $A$ はもう未解決の仮定ではなくなる。
このとき、仮定には番号を振る（$[A]^1$ ＝「1 番の仮定 $A$」）。放電する規則は、規則名にその番号を添えて $(\to\text{I}, 1)$ と書く。こうすると「この $\to$I がどの仮定を閉じたのか」が一意に分かる。$[A]^1$ の上付き $1$ と $(\to\text{I}, 1)$ の $1$ は同じ仮定を指すラベルである（別の数ではない）。仮定が複数あるとき取り違えないための仕組みである。
この番号は形式的な注記で、$\to$I に必須の情報（どの仮定を放電したか）であって、自由なコメントではない。逆に、仮定を放電しない規則 ― $(\to\text{E})$・$(\land\text{I})$・$(\land\text{E})$・$(\lor\text{I})$ ― は規則名だけで完結し、後ろに番号は付かない。
図 1 の証明木をテキストで読む
- 仮定 $[A]^1$ と前提 $A \to B$ に $\to$ 除去（$\to$E）を適用して $B$ を得る。
- その $B$ と前提 $B \to C$ に $\to$ 除去（$\to$E）を適用して $C$ を得る。
- 仮定 $[A]^1$ を放電する $\to$ 導入（$\to$I, 1）を適用して、結論 $A \to C$ を得る。
仮定を置いて最後に閉じるこの操作は、Curry–Howard 対応のもとで関数を作る（ラムダ抽象）操作にぴたりと一致する。$A$ を仮定して $B$ を作り $A \to B$ を結論することは、$A$ 型の引数を受けて $B$ 型の値を返す関数を定義することに等しい。
4. 証明検査カーネルの命題層
自然演繹は紙の上の道具にとどまらない。証明アシスタントや証明検査カーネルの命題層は、まさにこの導入・除去規則を実装したものである。各規則は「前提の形が合っているか」を照合するだけで適用の正しさが決まるので、機械的に検査できる（証明とは何か）。
論理結合子に加えて量化子 $\forall, \exists$ の導入・除去規則をそろえれば、述語論理の自然演繹になる。これらの規則が「正しい推論だけを許す」ことの保証が、次章の健全性である。
まとめ
この章のポイント
- 自然演繹：各結合子に導入規則（作る）と除去規則（使う）を対で与える
- 導入と除去は釣り合い、「作ってすぐ使う」無駄を消す操作が簡約
- 仮定の放電：$A$ を仮定して $B$ を導き、$\to$I で閉じて $A \to B$
- 放電はラムダ抽象（関数を作る）に対応する（Curry–Howard）
- 自然演繹は証明検査カーネルの命題層の正体である
よくある質問
自然演繹とは何か
各論理結合子に「導入規則」（作る規則）と「除去規則」（使う規則）を対で与える証明体系である。Gentzen と Prawitz によって整備され、数学者の自然な推論に近い形で証明を組み立てられる。証明は規則の適用を積み重ねた証明木で表される。
導入規則と除去規則はどう違うのか
導入規則は結合子を結論に作り出す規則（$A$ と $B$ から $A \land B$）、除去規則は結合子を前提として使う規則（$A \land B$ から $A$）である。各結合子で導入と除去が釣り合っており、作ったものをすぐ使うと元に戻る（簡約できる）調和した関係にある。
仮定の放電とは何か
含意 $A \to B$ を導入するとき、いったん $A$ を仮定して $B$ を導き、その後で仮定 $A$ を閉じる操作である。放電すると $A$ は未解決の仮定でなくなり、$A \to B$ が仮定なしで成り立つ。証明アシスタントで仮定を導入し最後にラムダ抽象で閉じる操作に対応する。