「自然演繹100本ノック」をシークエント計算で解こう

自然演繹100本ノックという教材を公開しています。論計舎 web shopより無料にてDLいただけます。近く第五版がDL可能になります (今は第四版) 。
最小命題論理、直観主義命題論理、古典命題論理、古典述語論理それぞれで証明可能な論理式に関する自然演繹の証明図を100個書いていただこうという趣旨です。

とある論計舎の生徒さんがこれを一通り自然演繹で解いたあと、シークエント計算でも挑戦してくださり、さらに学びが深まったとおっしゃってくださいました。

実は「シークエント計算100本ノック」も作成しようと思っているのですが、単なる論理式とシークエントの構造的複雑さが段違いなので苦戦しています。

そこで本記事では、「自然演繹100本ノック」にシークエント計算で挑戦しようという方に向けて、まず (古典述語論理の) シークエント計算を提示した上で、つづいて自然演繹とシークエント計算の同等性が「自然演繹100本ノック」で紹介されている体系で成立することを紹介します。

シークエント計算

シークエント計算 sequent calculus とは、論理式ではなくシークエントを単位とする推論 (規則) の体系である。
シークエントとは、論理式の有限列$${\Gamma, \Delta}$$からなる$${\Gamma \Rightarrow \Delta}$$というかたちの表現のことである。
なお、$${\Gamma}$$や$${\Delta}$$は空列でもよい。

シークエント$${\Gamma \Rightarrow \Delta}$$を素朴に解釈すると、「$${\Gamma}$$から$${\Delta}$$への帰結関係」とか「$${\Gamma}$$から$${\Delta}$$への推論」とかとみなせる。しかし、$${\Gamma}$$や$${\Delta}$$が有限列でない構造であるシークエントも存在し、その都度さまざまに解釈する必要がある。

しかし、ここでは古典述語論理を想定して紹介しているので、「結論部分$${\Delta}$$」には複数の論理式が出現する。
このようなシークエントを複数結論シークエント multiple-conclusion sequent などという。
これの解釈としては以下のようなものがいいだろう。
すなわち、「$${\varphi_0, \dots, \varphi_m \Rightarrow \psi_0, \dots, \psi_n}$$が証明可能であるとは、$${\varphi_0, \dots, \varphi_m}$$が全て真になりかつ$${\psi_0, \dots, \psi_n}$$がすべて偽になることはない」と。
これはRestall2005から始まる複数結論シークエントの解釈にまつわる諸研究の結果を私なりに数学向けに噛み砕いた説明である。

古典述語論理のシークエント計算の規則表

古典命題論理の推論規則は、以上の表から (かたちの上では) 量化子に関する規則を取り除いたものであり、直観主義命題論理の規則はそこからさらに$${\Rightarrow}$$の右側に出現できる論理式を一個ないし零個に制限したものが一般的である。さらに否定$${\lnot}$$に関する左右の規則と$${\bot \Rightarrow}$$を除くと最小論理に関する規則表が得られる。

なお、本記事では触れないが、(Cut) 規則を用いないでも証明は可能である。

自然演繹とシークエント計算の同等性

主定理

$${\Gamma}$$を論理式の列とするとき、つぎの二つの条件は同値である。

1. 古典述語論理のシークエント計算で$${\Gamma \Rightarrow \varphi}$$が証明可能である。

2. 古典述語論理の自然演繹で$${\Gamma}$$が解消されていない仮定からなる列であり$${\varphi}$$が結論である自然演繹の導出図が存在する。

古典述語論理を本記事で触れている他の3つの体系と置き換えても同様の定理が成立する。

証明について

定理の (2) から (1) は、$${\Gamma \vdash \varphi}$$に関する自然演繹の導出の構造に関する帰納法で容易に証明可能である。逆向きも同様の直接証明は可能であるが、容易とは言えないだろう。
しかし、シークエント計算の導出から自然演繹の導出に変換するうちに証明の道筋はわかるものと思われる。

なお、直観主義命題論理について主定理の証明は幾分容易になる。古典命題論理について以下のGlivenkoの定理を用いることで比較的簡潔な証明を得ることができる。

Glivenkoの定理

以下の二つの条件は同値である。

1. 古典命題論理のシークエント計算で$${\Gamma \Rightarrow \Delta}$$が証明可能である。

2. 直観主義命題論理のシークエント計算で$${\lnot \Delta, \Gamma \Rightarrow}$$が証明可能である。

なお、$${\lnot \Delta}$$は、以下のように定義される:

1. $${\Delta}$$が空列のとき、$${\lnot \Delta}$$は空列である。

2. $${\Delta}$$が$${\Delta_0, \delta}$$のとき、$${\lnot \Delta}$$は$${\lnot \Delta_0, \lnot \delta}$$である。

おわりに

自然演繹100本ノックをシークエント計算で解くことにより、本記事で紹介した主定理をより理解できるようになると想像します。
また、「シークエント計算100本ノック」も公開した際にはぜひDLし挑戦してみて下さい。

それでは最後までお読みくださいありがとうございました。