直観主義論理の「自然さ」(2) シーケント計算

f直観主義論理の「自然さ」(1)で、直観主義論理に対する自然演繹の体系を与えた。この体系を少し改造して、直観主義論理についての別の演繹システムを作ってみる。

表記の変更
新しい演繹規則
カットについて

(※本文中、証明図の中の式の位置や大きさが変になっているところがあるけど、直すのが面倒なので変なままになっている)

表記の変更

自然演繹では、仮定として置かれる論理式は取り除かれるまでずっと同じ形をしていた。結論の式については演繹規則があって式が次々に変形されていくけれど、仮定の式に対しては取り除くという以外の操作は無かった。そこで、仮定の式を変形する規則を追加してみる。
しかしそうしようとすると自然演繹で使ったような表記ではうまくいかなくなる。仮定が変形するような規則が追加されると、どんな式が仮定されているのかが証明の各段階で変わるので、それを明示しておく必要がある。そこで証明の各段階を

$A_1, \ldots , A_n \Rightarrow B$

のように書くことにする(この形の式をシーケントと呼ぶ)。 $\Rightarrow$ の左側に書かれているのが仮定で、右側が導出された論理式。この書き方をすると
$\frac{[A ]{}_2 \qquad [ B ]{}_1}{\large{\frac{A \wedge B}{ \large{\frac{B \to A \wedge B}{A \to (B \to A\wedge B)}\small{2} } }\small{1} }}$ と書かれていた証明図は、 $\frac{A \Rightarrow A \qquad B \Rightarrow B }{\large{\frac{ A,B \Rightarrow A \wedge B}{ \large{\frac{A \Rightarrow B \to A \wedge B}{ \Rightarrow A \to (B \to A\wedge B)} } } } }$ と書かれる。
ただし、この時点では表記を変えただけでシステム自体は自然演繹のまま。

新しい演繹規則

論理積

まず
$\begin{array}{c} A \\ \vdots \\ C \end{array}$
という証明図があったとする。この証明図に論理積の除去則
$\frac{A \wedge B}{A}$
を繋ぎなわせると、
$\begin{array}{c} \large{\frac{A \wedge B}{A}}\\ \vdots \\ C \end{array}$
という証明図ができる。つまりAを仮定してCが証明できるなら、A∧Bを仮定してCが証明できる。シーケントを使って言えば、 $A, P_1, \ldots , P_n \Rightarrow B$ が証明できるなら、 $A \wedge , P_1, \ldots , P_n \Rightarrow B$ も証明できる。これは仮定の形が変化する規則になっている。そこでこれを新しい推論規則に加えることにする。

(∧左)
$\frac{\large{A, \qquad P_1, \ldots , P_n \Rightarrow B}}{\large{A \wedge B, \quad P_1, \ldots , P_n \Rightarrow B}} \qquad \qquad \frac{ \large{B, \qquad P_1, \ldots , P_n \Rightarrow B} }{\large{A \wedge B, \quad P_1, \ldots , P_n \Rightarrow B}}$

この∧左規則と∧の除去則は実質的に同じことをいっているのだから、∧左を追加したかわりに、∧の除去則を取り除いても良いように思える。しかし実際には∧左規則だけでは「 $P_1, \ldots , P_n \Rightarrow A \wedge B$ が証明できれば、 $P_1, \ldots , P_n \Rightarrow A$ も証明できる」(∧除去則をシーケントで書いたもの)を示すことができない。つまりこのままでは∧除去則を推論規則から外すことはできない。
なぜうまくいかないのか。自然演繹の体系で∧左が成り立つことを示すときに、二つの証明図をつなぎ合わせて一つの証明図にするという操作をした。証明図をつなげる操作はシーケントの形でいえば、 $P_1, \ldots, P_m \Rightarrow A$ の証明図と $A, Q_1, \ldots, Q_n \Rightarrow B$ の証明図をつなぎ合わせて、 $P_1, \ldots, P_m, Q_1, \ldots, Q_n \Rightarrow B$ の証明図を作る、となる。自然演繹の証明図についてこのようなことができるのは、自然演繹では仮定された式が変形されないから。仮定された式の形が変わることがないので、証明の最後に演繹された論理式について使われている仮定は、必ず証明図の上端のどこかに登場している。そのため、証明図の上端にある仮定の式と、別の証明図の下端にある結論の式をつなげることができる。
しかし∧左を使うと、仮定の式が変形されるので、ある証明図の結論と別の証明図の仮定が同じ式のときに、それらの証明図をつなげられるとはかぎらなくなってしまう。
そこで、自然演繹で証明図をつなげることに対応する操作を明示的な規則として追加することにする。この規則はカットと呼ばれる。

(カット)
$\frac{\large{P_1, \ldots, P_m \Rightarrow A \qquad A, Q_1, \ldots, Q_n \Rightarrow B}}{\large{P_1, \ldots, P_m, Q_1, \ldots, Q_n \Rightarrow B}}$

カットと∧左を使えば、∧の除去則が成り立つことを示せる。
$\frac{\begin{array}{c} \vdots \\ P_1, \ldots , P_n \Rightarrow A \wedge B \end{array} \quad \large{\frac{A \Rightarrow A}{A \wedge B \Rightarrow A}}}{P_1, \ldots, P_n \Rightarrow A}$
それから∧の導入則はそのまま使う。名前だけ変えておく。

(∧右)
$\frac{\large{P_1, \ldots, P_m \Rightarrow A \qquad Q_1, \ldots, Q_n \Rightarrow B}}{\large{P_1, \ldots, P_m, Q_1, \ldots, Q_n \Rightarrow A \wedge B}}$

含意

二つの証明図
$\begin{array}{c}\vdots \\ A \end{array}$
と
$\begin{array}{c} B \\ \vdots \\ C \end{array}$
に仮定 $A \to B$ を追加すると、 →除去則を使って、
$\begin{array}{cc}\frac{\begin{array}{c} \vdots & \\ A & A \to B \end{array}}{ B } \\ \vdots \\ C \end{array}$
のようにつなげることができる。これをシーケントの形で表せば、次の規則が得られる。

(→左)
$\frac{\large{P_1, \ldots, P_m \Rightarrow A \qquad B, Q_1, \ldots , Q_n \Rightarrow C}}{\large{A \to B, P_1, \ldots, P_m, Q_1, \ldots, Q_n \Rightarrow C}}$

導入規則は名前を変えるだけで、そのまま使う。

(→右)
$\frac{\large{A, P_1, \ldots, P_n \Rightarrow B}}{\large{P_1, \ldots, P_n \Rightarrow A \to B}}$

論理和

証明図
$\begin{array}{c} A \\ \vdots \\ C \end{array}$
と
$\begin{array}{c} B \\ \vdots \\ C \end{array}$
に仮定 $A \vee B$ を追加すると、、∨の除去則により
$\frac{ \begin{array}{c} & [ A ]{}_1 & [ B ]{}_1 \\ & \vdots & \vdots \\ A \vee B & C & C \end{array}}{C}\small{1}$
となる。これより次の規則が得られる。

(∨左)
$\frac{ \large{A , P_1, \ldots, P_m \Rightarrow C \qquad B, Q_1, \ldots , Q_n \Rightarrow C}}{ \large{A \vee B, P_1, \ldots, P_m, Q_1, \ldots, Q_n \Rightarrow C} }$

右規則は、自然演繹の導入規則と同じ。

(∨右)
$\frac{\large{P_1, \ldots , P_n \Rightarrow A}}{\large{P_1, \ldots , P_n \Rightarrow A \vee B }} \qquad \qquad \frac{\large{P_1, \ldots , P_n \Rightarrow B}}{\large{P_1, \ldots , P_n \Rightarrow A \vee B }}$

否定と矛盾

証明図
$\begin{array}{c} \vdots \\ A \end{array}$
に、仮定 $\neg$ を追加して¬除去則を使うと、
$\frac{\begin{array}{c} \vdots & \\ A & \neg A \end{array}}{ \bot }$
となることから次の規則が得られる。

(¬左)
$\frac{ P_1, \ldots , P_n \Rightarrow A}{ \neg A, P_1, \ldots , P_n \Rightarrow \bot}$

また¬の除去則と $\bot$ 規則から次が得られる。

(¬右)
$\frac{A , P_1, \ldots, P_n \Rightarrow \bot}{P_1, \ldots, P_n \Rightarrow \neg A}$

( $\bot$ )
$\frac{P_1, \ldots, P_n \Rightarrow \bot}{P_1, \ldots, P_n \Rightarrow A}$

一応これでも良いのだけど、単純化のためにシーケントの右辺が空白の場合は矛盾記号が省略されていると考えることにして、矛盾記号を書かないことにする。すると演繹規則は次のようになる。

(¬左)
$\frac{ \large{P_1, \ldots , P_n \Rightarrow A}}{ \large{\neg A, P_1, \ldots , P_n \Rightarrow }}$

(¬右)
$\frac{\large{A , P_1, \ldots, P_n \Rightarrow} }{\large{P_1, \ldots, P_n \Rightarrow \neg A}}$

( $\bot$ )
$\frac{\large{P_1, \ldots, P_n \Rightarrow} }{\large{P_1, \ldots, P_n \Rightarrow A}}$

まとめ

以上のように、直観主義論理に対する自然演繹の体系の除去則を無くして左規則とカット規則を追加した体系はシーケント計算と呼ばれる。本当は、構造の規則についての規則があるのだけど、シーケントの定義をちゃんとしていないので、そのあたりは省略する。

カットについて

自然演繹とシーケント計算とを対応付けるためにカット規則を追加したけれど、自然演繹の証明をシーケント計算の証明に置きかえる場合に常にカットが必要になるわけではない。
自然演繹の証明図で、除去則が連続して使われていてそのあとに導入則を連続して使っている部分は、シーケント計算の証明図に書きかえてもカットは出てこない。
たとえば、次の自然演繹の証明図
f:id:lemniscus:20190106164219g:plain

を、シーケント計算の証明図に書きかえると
f:id:lemniscus:20190106164303g:plain

となり、カットは出てこない。
逆に導入則(または $\bot$ 規則)のあとに除去則がある場合は、カットが必要になる(正確には、証明図に枝分れがある関係でカットが必要な場合と必要でない場合があるが)。例えば次の証明図
f:id:lemniscus:20190106164417g:plain

をシーケント計算の証明図に移すと
f:id:lemniscus:20190106164433g:plain

となる。最後にカットを使っている。
除去則は一番外側の論理記号を除去する。そのため、導入則の次に除去則がくる場合、同じ論理記号に対する導入則と除去則になっている。つまり、
$\frac{\frac{\large{\begin{array}{c}\vdots \\ A \end{array} \qquad \begin{array}{c} \vdots \\ B \end{array}}}{\large{A \wedge B}}}{\large{\begin{array}{c}A \\ \vdots \end{array}}}$
のような形(∧の導入則と除去則)とか、
f:id:lemniscus:20190106164530g:plain

のような形(→の導入則と除去則)になる。これは導入則で論理記号を導入して直後にその記号を除去するという無駄なことをしている( $\bot$ 規則で新しい論理式を導入して直後に除去則を使うのも同じ無駄をしている)。そのため証明図を簡単化することができる。
例えば、
$\frac{\frac{\large{\begin{array}{c}\vdots \\ A \end{array} \qquad \begin{array}{c} \vdots \\ B \end{array}}}{\large{A \wedge B}}}{\large{\begin{array}{c}A \\ \vdots \end{array}}}$
は、
${\begin{array}{c} \vdots \\ A \\ \vdots \end{array}}$
に書きかえられるし、
f:id:lemniscus:20190106164640g:plain
は、

${\begin{array}{c} \vdots \\ A \\ \vdots \\ B \\ \vdots \end{array} }$
に書きかえられる。
対応するシーケント計算の証明図でも同様の書きかえがおこなえて、同じ論理記号に対する右規則と左規則を使っている部分を消すことができる。この時、必ずカットが消えるわけではないけれど、同様の変形を繰り替えしていけばカットを消していける。
ただし、∨の除去則が介入するためにストレートにはいかない場合がある。例えば次の証明図
f:id:lemniscus:20190106164741g:plain

では、∧の導入則と除去則の間に∨の除去則が入っているので、∧の導入則・除去則を相殺させることができない。このような場合、∧の除去則の位置を移動させる。
f:id:lemniscus:20190106164826g:plain

この変形は、シーケント計算でいえば、
f:id:lemniscus:20190106165031g:plain

を
f:id:lemniscus:20190106164903g:plain

に書きかえることにあたる。
このように自然演繹とシーケント計算を対応させることで、証明図における回り道を単純化していく手続きを見つけることができる。
あと自然演繹には、除去則を使ったあとに導入則を使って同じ式を導出するという逆のまわり道がある。例えば次のようなもの。
f:id:lemniscus:20190106165109g:plain