共 1 条公理,或者说「公理模式」。
将前提中的任意一项拿出来都能做为结论(显然)。
$$ \Gamma\cup\{A\}\vdash A\qquad(\in) $$
这里没有列出 $\neg\neg$(双重否定)和 $\leftrightarrow$ 相关的规则,是因为它们都很显然。
即 $B\to(A\to B)$,往前提中加料仍然能让原命题成立。
$$ \frac{\Gamma\vdash B}{\Gamma\cup\{A\}\vdash B}\qquad(+) $$
即 $\neg A\to(A\to B)$,自相矛盾的原理,也可以理解为拆前件($A$ 和 $\neg A$ 都不影响正确性,那 $A$ 就没有什么存在意义了)。
$$ \frac{\Gamma;A\vdash B,\Gamma;\neg A\vdash B}{\Gamma\vdash B}\qquad(-) $$
即 $A\to A\vee B$,结论随便析取,反正原来那部分总是成立的。
$$ \frac{\Gamma\vdash A}{\Gamma\vdash A\vee B}\qquad(\vee+) $$
即 $(A\vee B)\wedge(A\to C)\wedge(B\to C)\to C$。
$$ \frac{\Gamma;A\vdash C,\Gamma;B\vdash C;\Gamma\vdash A\vee B}{\Gamma\vdash C}\qquad(\vee-) $$