証明論 (2.5): シーケント計算のルール [証明論]

記述を自己完結にするために前回説明できなかったシーケント規則のルールを補足しておく。

まずは、前回も登場した、論理演算子にかかわらない規則を再掲する。なお、太字で書かれたヘディングはルール名、ルールのあとのカッコ内はそのルールの略称を表す。

薄め：$\cfrac{\Gamma \rightarrow \Theta}{\mathfrak{D},\Gamma \rightarrow \Theta} (WL) \quad \cfrac{\Gamma \rightarrow \Theta}{\Gamma \rightarrow \Theta,\mathfrak{D}} (WR)$

縮約：$\cfrac{\mathfrak{D},\mathfrak{D},\Gamma \rightarrow \Theta}{\mathfrak{D},\Gamma \rightarrow \Theta} (CL) \quad \cfrac{\Gamma \rightarrow \Theta,\mathfrak{D},\mathfrak{D}}{\Gamma \rightarrow \Theta,\mathfrak{D}} (CR)$

交換：$\cfrac{\Delta,\mathfrak{D},\mathfrak{E},\Gamma \rightarrow \Theta}{\Delta,\mathfrak{E},\mathfrak{D},\Gamma \rightarrow \Theta} (IL) \quad \cfrac{\Gamma \rightarrow \Theta,\mathfrak{E},\mathfrak{D},\Lambda}{\Gamma \rightarrow \Theta,\mathfrak{D},\mathfrak{E},\Lambda} (IR)$

カット：$\cfrac{\Gamma \rightarrow \Theta, \mathfrak{D} \quad \mathfrak{D}, \Delta \rightarrow \Lambda}{\Gamma, \Delta \rightarrow \Theta, \Lambda} (Cut)$

さて、以下に、前回も登場した論理演算子 $\supset$ のそれも含めて、すべての論理演算子の導入ルールをあげる。

否定：$\cfrac{\Gamma \rightarrow \Theta,\mathfrak{A}}{\neg\mathfrak{A},\Gamma \rightarrow \Theta} (\neg L) \quad \cfrac{\mathfrak{A},\Gamma \rightarrow \Theta}{\Gamma \rightarrow \Theta, \neg \mathfrak{A}} (\neg R)$

連言：
$\cfrac{\mathfrak{A},\Gamma \rightarrow \Theta}{\mathfrak{A}\&\mathfrak{B},\Gamma \rightarrow \Theta} (\&L_1) \cfrac{\mathfrak{B},\Gamma \rightarrow \Theta}{\mathfrak{A}\&\mathfrak{B},\Gamma \rightarrow \Theta} (\&L_2) \cfrac{\Gamma \rightarrow \Theta,\mathfrak{A} \quad \Gamma \rightarrow \Theta,\mathfrak{B}}{\Gamma \rightarrow \Theta,\mathfrak{A}\&\mathfrak{B}} (\&R)$

選言：
$\cfrac{\mathfrak{A},\Gamma \rightarrow \Theta \quad \mathfrak{B},\Gamma \rightarrow \Theta}{\mathfrak{A}\vee\mathfrak{B},\Gamma \rightarrow \Theta} (\vee L) \cfrac{\Gamma \rightarrow \Theta,\mathfrak{A}}{\Gamma \rightarrow \Theta,\mathfrak{A}\vee\mathfrak{B}} (\vee R_1) \cfrac{\Gamma \rightarrow \Theta,\mathfrak{B}}{\Gamma \rightarrow \Theta,\mathfrak{A}\vee\mathfrak{B}} (\vee R_2)$

含意：$\cfrac{\Gamma \rightarrow \Theta,\mathfrak{A} \quad \mathfrak{B},\Delta \rightarrow \Lambda}{\mathfrak{A}\supset\mathfrak{B},\Gamma,\Delta \rightarrow \Theta,\Lambda} (\supset L) \quad \cfrac{\mathfrak{A},\Gamma \rightarrow \Theta,\mathfrak{B}}{\Gamma \rightarrow \Theta,\mathfrak{A}\supset\mathfrak{B}} (\supset R)$

これらのルールを用いて、前回示した排中律と同様に、矛盾律は以下のように示される。

$\cfrac{\cfrac{\cfrac{\cfrac{\cfrac{\cfrac{A \rightarrow A}{\neg A,A \rightarrow}}{A \& \neg A,A \rightarrow}}{A,A \& \neg A \rightarrow}}{A \& \neg A,A \& \neg A \rightarrow}}{A \& \neg A \rightarrow}}{\rightarrow \neg (A \& \neg A)}$

（使われているルールは上から $\neg L, \& L, IL, \& L, CL, \neg R$ となる）

演習：$A \supset B \equiv \neg A \vee B$ を示せ。

量化子はつぎのように導入される。

全称：$\cfrac{\mathfrak{Fa},\Gamma \rightarrow \Theta}{\forall \mathfrak{x}\mathfrak{Fx},\Gamma \rightarrow \Theta} (\forall L) \quad \cfrac{\Gamma \rightarrow \Theta,\mathfrak{Fa}}{\Gamma \rightarrow \Theta, \forall \mathfrak{xFx}} (\forall R)$

存在：$\cfrac{\mathfrak{Fa},\Gamma \rightarrow \Theta}{\exists \mathfrak{x}\mathfrak{Fx},\Gamma \rightarrow \Theta} (\exists L) \quad \cfrac{\Gamma \rightarrow \Theta,\mathfrak{Fa}}{\Gamma \rightarrow \Theta, \exists \mathfrak{xFx}} (\exists R)$

ここで、$\forall R, \exists L$ にかんしてはとくべつな注意が必要である。つまり、それらにおいて $\mathfrak{x}$ で束縛される $\mathfrak{a}$ は下段に現れてはならない。なぜか？　この禁を破るとつぎのような導出ができてしまうからである。

$\cfrac{\cfrac{\cfrac{\mathfrak{Fa} \rightarrow \mathfrak{Fa}}{\exists \mathfrak{xFx} \rightarrow \mathfrak{Fa}}}{\exists \mathfrak{xFx} \rightarrow \forall \mathfrak{xFx}}}{\rightarrow \exists \mathfrak{xFx} \supset \forall \mathfrak{xFx}}$

この終式によれば「（あるドメイン内の）何かが $\mathfrak{F}$ であれば、（そのドメイン内の）すべてが $\mathfrak{F}$ である（ということがいっぱんに成り立つ）」ということになるが、言うまでもなくそんなことは（いっぱんには）成り立たない。こんなことになってしまったのはひとえに、一段目の $\exists L$ 適用が上で述べた禁を犯しているからである。「$\forall R, \exists L$ において $\forall, \exists$ で束縛される変数は下段に現れてはならない」というルールを「固有変数条件 eigenvariable condition」という。

量化子導入を含むシーケント計算の例：

$\cfrac{\cfrac{\cfrac{\cfrac{\cfrac{\mathfrak{Fa} \rightarrow \mathfrak{Fa}}{\mathfrak{Fa} \rightarrow \exists \mathfrak{xFx}}}{\rightarrow \exists \mathfrak{xFx}, \neg \mathfrak{Fa}}}{\rightarrow \exists \mathfrak{xFx}, \forall \mathfrak{x}\neg\mathfrak{Fx}}}{\neg \forall \mathfrak{x}\neg\mathfrak{Fx} \rightarrow \exists \mathfrak{xFx}}}{\rightarrow \neg \forall \mathfrak{x}\neg\mathfrak{Fx} \supset \exists \mathfrak{xFx}}$

（使われているルールは上から $\exists R, \neg R, \forall R, \neg L, \supset R$ となる）

演習：$\rightarrow \exists \mathfrak{xFx} \supset \neg \forall \mathfrak{x} \neg \mathfrak{Fx}$ を導け。