直観主義論理の「自然さ」(3)古典論理のシーケント計算と自然演繹

直観主義論理の「自然さ」(2)で直観主義論理のシーケント計算を与えた。その続き。

仮定と結論の対称性と古典論理のシーケント計算

直観主義論理のシーケント計算の∧左規則と∨右規則を比べてみると、左右に関してだいたい逆の形になっている。

(∧左)
$\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}}$

(∨右)
$\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 }}$

同様のことが、∧右と∨左や、¬左と¬右についてもいえる。

(¬左)
$\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}}$

またカットについては、それ自身が左右対称に近いかたちになっている。

(カット)
$\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}}$

でも対称に近いだけで、ちゃんとした対称形にはなっていない。そもそもシーケントの左側には何個でも論理式が置けるのに右側にはひとつ(矛盾の場合はゼロ個)しか論理式が置けないので、正確な対称形にはならない。
なので何となく、シーケントの右側にいくつでも論理式が置けるように変更して推論規則も変更してみたくなる。これは、適切な演繹体系を作ろうという動機とはあまり関係なくて、単にそうやって変更したら何か面白い体系ができるかもしれないという考えによる。

そのように変更すること自体は難しくない。それぞれの推論規則について、右側にいくつでも論理式が置ける形に変えるだけ。でもそうやって変更してみて最初に考える必要があるのは、シーケントの右側にいくつも論理式があるのはいったい何を表しているのか、ということ。これに関しては次のことが成り立つ。

$\cdots \Rightarrow A_1, \ldots , A_n$ が証明できるなら、 $\cdots \Rightarrow A_1 \vee \ldots \vee A_n$ が証明できる。逆もなりたつ。
これにより、シーケントの右辺に複数の論理式がある場合は、それらの論理式が∨でつながっているのとだいたい同じだと考えることができる。

右辺をそのように考えて、各推論規則が直観主義論理の場合とどれくらい違うのかを調べてみると、ほとんどの推論規則は直観主義論理でも既に成立していたものだということがわかる。
直観主義論理では成立しない規則になっているのは、→右と¬右の二つだけ。また、このうち片方の推論規則を認めるとそれを使ってもう片方の規則は導くことができる。そしてこれらの推論規則は、直観主義論理に追加すると古典論理になる推論規則のうちのひとつになっている。

こう書くと→右と¬右が重要な役割を果たしているみたいだけど、実際はそうではない。一番重要なのは、説明していなかったけど次の規則。右辺に同じ式があったらそれをまとめて一つにして良いというもの。

$\frac{\large{P_1,\ldots,P_m \Rightarrow A, A, Q_1, \ldots, Q_n}}{\large{P_1,\ldots,P_m \Rightarrow A, Q_1, \ldots, Q_n}}$

この規則があるから、
$\cdots \Rightarrow A_1, \ldots , A_n$ と $\cdots \Rightarrow A_1 \vee \ldots \vee A_n$ とを同じとみなすことができる。
ということで、適切な演繹体系を作るというのとは関係なく、シーケントの左側と右側、仮定と結論について対称な体系を作ってみたら、古典論理の体系が得られた。古典論理で∧と∨の双対性が成り立ったり、ド・モルガンの規則が成り立つなどの綺麗な性質や単純さを持っているのは、仮定と結論を対称的に扱う結果だという見方もできるかもしれない。

たいていの論理学の本では、まず古典論理のシーケント計算を導入して、その後に、シーケントの右辺を制限して直観主義論理のシーケント計算を得るという話の流れで説明をおこなう。でも直観主義論理の説明を先にする方がわかりやすい気がする。
古典論理のシーケント計算の説明で、まず最初にわかりにくい場所はシーケントの右辺の説明だと思う。論理式がない場合は矛盾を表し複数の論理式は「または」でつながっているとみなすというのは、いきなりは納得しにくい。右辺における論理式はただ一つ(空白は矛盾記号が省略されていると考える)の方が演繹体系としては自然な感じがする。古典論理の体系は自然さを捨て対称性を取ったという印象がある。

古典論理に対する自然演繹

シーケント計算で、シーケントの右辺(結論)の論理式を複数にすることで古典論理の体系が得られた。同様のことが自然演繹でも成り立つ。
まず、結論に複数の論理式がある場合は $\{A,B ,C \}$ みたいに{}で囲んで表記することにする。それから、二つの規則を追加する。
ひとつは、結論に任意の論理式を追加して良いという規則。

$\frac{\large{\begin{array}{c} \vdots \\ \{P_1, \ldots, P_n \} \end{array}}}{\large{ \{A, P_1, \ldots, P_n \} }}$

もうひとつは、結論に同じ論理式があったら一つにまとめて良いという規則。

$\frac{\large{\begin{array}{c} \vdots \\ \{A , A, P_1, \ldots, P_n \} \end{array}}}{\large{ \{A, P_1, \ldots, P_n \} }}$

この変更で古典論理に対する演繹体系が得られている。たとえば排中律は次のように証明できる。
$\frac{\frac{\frac{\frac{\frac{\large{ [ A ]{}_{\small{1}}}}{\large{A \vee \neg A}}}{ \large{ \{ \bot , A \vee \neg A \} }}}{\large{ \{ \neg A , A \vee \neg A \} }}\small{1} }{\large{ \{ A \vee \neg A , A \vee \neg A \} } }}{\large{ A \vee \neg A } }$

また二重否定除去則は次のようにして得られる。
f:id:lemniscus:20190106162412g:plain