含意の自然演繹

定義 4.1（「単純型付きラムダ計算とカリー＝ハワード対応」§4）

命題変数 $p_1,p_2,\ldots$ から $\to$ で作られる論理式を考える。仮定の集まり $\Delta$ は論理式の有限集合で、判断 $\Delta\vdash A$ を次の規則で帰納的に定める。

\frac{A\in\Delta}{\Delta\vdash A}\ (\mathrm{Ax})\qquad \frac{\Delta\cup\{A\}\vdash B}{\Delta\vdash A\to B}\ ({\to}\mathrm{I})\qquad \frac{\Delta\vdash A\to B\quad\Delta\vdash A}{\Delta\vdash B}\ ({\to}\mathrm{E})

$({\to}\mathrm{I})$ は「 $A$ を仮定して $B$ を示したら、仮定を解消して $A\to B$ 」、 $({\to}\mathrm{E})$ はモーダス・ポネンスである。

閉包の状態

定義

定義は閉包の起点です（証明を要しません）。

印の意味: ✓公理まで証明済み・ △証明あり（閉包未完）・ ※主張のみ。テーマごとの集計は閉包の状況。

証明で明示的に参照している定理は、まだありません。