自然演繹からシークエントへ翻訳

今日は思い切って論理学について書こうと思います。

証明論的意味論などの証明論分野では証明図を多用するので，自然演繹を使うかシークエントを使うかで見方が変わったりします。これらの証明体系の説明は省略しますが，ともかく，どちらか一方の証明体系を使って後になって証明体系を変えたいとなった場合，また一から証明を考えるのは二度手間です。そのため翻訳という技が必要になってきます。

今回は直観主義命題論理に限定します。

前置き

翻訳するといったものの，必ずしも１対１に翻訳できるわけではありません。というのも，自然演繹とシークエントではそもそもシステムが全く異なります。自然演繹は導入則と除去則だけで証明しますが，シークエントは少しの公理が必要です。なので，人工的に手を加えることで形を整えます。

翻訳は$${tr.}$$と表します。証明の省略は$${\mathcal D}$$など筆記体で表し，明示しない場合の証明は$${|}$$で表します。また，前提を落とす(discharge)までは$${[~~~~~~]}$$で括らないものとします。

推論規則の直訳

まずは安直に推論規則をそのまま翻訳します。

$${[A]_i~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~\\| ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~\\ \cfrac{B}{A\to B}\small{\to I_i}}$$$${\stackrel{tr.}{\Longrightarrow}}$$$${\cfrac{A\vdash B}{\vdash A\to B}\small{\to R}}$$

$${\cfrac{A~~~~~~A\to B}{B}\small{\to E}}$$$${\stackrel{tr.}{\Longrightarrow}}$$$${A,A\to B\vdash B}$$

$${\cfrac{A~~~~~~B}{A\land B}\small{\land I}}$$$${\stackrel{tr.}{\Longrightarrow}}$$$${A,B\vdash A\land B}$$

$${\cfrac{A_1\land A_2}{A_i}\small{\land E}}$$$${\stackrel{tr.}{\Longrightarrow}}$$$${A_1\land A_2\vdash A_i}$$

$${[A_i]_m~~~~~~~~~~~~~~~~~~~~\\|~~~~~~~~~~~~~~~~~~~~~~\\\cfrac{A_1\land A_2~~~~~~C}{C}\small{\land E_m}}$$$${\stackrel{tr.}{\Longrightarrow}}$$$${\cfrac{A_i\vdash C}{A_1\land A_2\vdash C}\small{\land L}}$$

$${\cfrac{A_i}{A_1\lor A_2}\small{\lor I}}$$$${\stackrel{tr.}{\Longrightarrow}}$$$${A_i\vdash A_1\lor A_2}$$

$${~~~~~~~~[A]_m~[B]_n\\~~~~~~~|~~~~~~~~|\\\cfrac{A\lor B~~~~~~C~~~~~~C}{C}\small{\lor E_{m,n}}}$$
$${\stackrel{tr.}{\Longrightarrow}}$$$${\cfrac{A\vdash C~~~~~~B\vdash C}{A\lor B\vdash C}\small{\lor L}~~~~~~~~~~~~~~}$$

ここでは，自然演繹側の一番上の論理式(ノード)が前提として含まれるため，シークエントの前件に書かれます。つまり，自然演繹ではその論理式より上に証明が無いことを示しています。例えば，$${\land}$$導入則で$${A,B\vdash A\land B}$$が成り立つとき，$${A}$$と$${B}$$が前件に含まれています。このとき，以下の証明図のうち$${\mathcal D}$$と$${\mathcal E}$$は空集合(空列)でもよいことになります。

$${\mathcal D~~~~~~\mathcal E~~~~\\\cfrac{A~~~~~~B}{A\land B}\small{\land I}\\\normalsize\mathcal G~~~~}$$

また，自然演繹側に縦線$${|}$$がある場合はシークエント側で何らかの規則が適用されます。

任意の証明を含む証明図の翻訳

前節の$${\mathcal D}$$と$${\mathcal E}$$に何らかの証明が含まれている場合は，$${A}$$と$${B}$$は前提とは限らないため，$${A,B\vdash A\land B}$$は必ずしも成り立ちません。その代わりに別の論理式が前件に書かれます。特徴付けとしてその別の論理式が$${P}$$と$${Q}$$だとすると，

$${\mathcal D~~~~~~~~~~~~~~\mathcal E~~~~~~\\\cfrac{P\vdash A~~~~~~Q\vdash B}{P,Q\vdash A\land B}\small{\land R}\\\normalsize \mathcal G~~~~~}$$

と翻訳できます。ここでシークエントの規則が適用されていることに注意してください。また，$${\mathcal D}$$と$${\mathcal E}$$と$${\mathcal G}$$は後件にかかっています。実際は$${P}$$から$${\mathcal D}$$の証明を経由して$${A}$$を証明しています。$${Q}$$も同様に$${\mathcal E}$$を経由しています。↓自然演繹

$${P~~~~~~Q\\\mathcal D~~~~~~\mathcal E\\A~~~~~~B}$$

導入則の翻訳

前節に従うと，例えば$${\to}$$導入則は以下のようになります。

$${[A]_i~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~\\\mathcal D~~~~~~~~~~~~~~~~~~~~~~~~~~\mathcal D~~~~~~~~~~\\\cfrac{B}{A\to B}\small{\to I_i}}$$$${\stackrel{tr.}{\Longrightarrow}}$$$${\cfrac{A\vdash B}{\vdash A\to B}\small{\to R}}$$
$${\mathcal G ~~~~~~~~~~~~~~~~~~~~~~~~~~~\mathcal G~~~~~~~~~~}$$

ほとんどの場合はこれで十分に翻訳できます。ですが，証明論的意味論などを考えるときにはこれだけでは不十分です。特に調和(harmony)について上手く表現しきれません。そこで，推論の前提が落とされた状態(discharged)でも，その上の証明を明示できるようにします。実用的には書き換え規則を表現できるようにします。以下の証明を考えます。

$${\mathcal D\\~[A]~\\\mathcal D'\\B\\\mathcal G}$$

$${A}$$は$${[~~~~~~]}$$で括られているので，$${A}$$以下の証明$${\mathcal D'}$$もしくは$${\mathcal G}$$の中で必ず落とされているはずです。ただ，$${B}$$は落とされてないので前提として含まれていません。これをシークエントに翻訳すると，

$${\mathcal D\\A\vdash A\\\mathcal D'\\A\vdash B\\\mathcal G}$$

となります。奇妙な形ですが，これをもとに導入則を翻訳します。

$${\mathcal D ~~~~~~~~~~~~~~~~~~~~~~~~\mathcal D ~~~~~~~~~\\~[A]_i~~~~~~~~~~~~~~~~~~A\vdash A~~~~~~~\\\mathcal D'~~~~~~~~~ \stackrel{tr.}{\Longrightarrow}~~~~~\mathcal D'~~~~~~~~\\\cfrac{B}{A\to B}\small{\to I_i}\normalsize ~~~~~~\cfrac{A\vdash B}{\vdash A\to B}\small{\to R}\normalsize \\\mathcal G~~~~~~~~~~~~~~~~~~~~~~~~~\mathcal G~~~~~~~~~}$$

$${\mathcal D~~~~~~\mathcal E~~~~~~~~~~~~~~~\mathcal D~~~~~~~~~~~\mathcal E~~~~~~~\\\cfrac{A~~~~~~B}{A\land B}\small{\land I}\normalsize\stackrel{tr.}{\Longrightarrow}\cfrac{\vdash A~~~~~~\vdash B}{\vdash A\land B}\small{\land R}\normalsize\\\mathcal G~~~~~~~~~~~~~~~~~~~~~~~~~~~~\mathcal G~~~~~~~~~}$$

$${~\mathcal D~~~~~~~~~~~~~~~~~~~~~~~~~~\mathcal D~~~~~~~~\\\cfrac{A_i}{A_1\lor A_2}\small{\lor I}\normalsize\stackrel{tr.}{\Longrightarrow}\cfrac{\vdash A_i}{\vdash A_1\land A_2}\small{\lor R}\normalsize\\~\mathcal G ~~~~~~~~~~~~~~~~~~~~~~~~~~\mathcal G ~~~~~~~~}$$

除去則の翻訳

除去則は本当に面倒なので手短にやります。

まず，シークエントには除去則というものがなくても良いです。それは$${A\vdash A}$$や$${\bot \vdash A}$$といった公理から証明を構成していくからです。しかし，自然演繹の証明を表現するには除去則が必要になります。以下のように右除去則だけを定義します。

$${\cfrac{\Gamma \vdash A~~~~~~\Sigma \vdash A\to B}{\Gamma,\Sigma \vdash B}\small{\to E}}$$

$${\cfrac{\Gamma \vdash A_1\land A_2}{\Gamma \vdash A_i}\small{\land E}}$$

$${\cfrac{\Gamma\vdash A_1\land A_2~~~~~~\Sigma,A_i\vdash C}{\Gamma,\Sigma\vdash C}\small{\land E}}$$

$${\cfrac{\Gamma \vdash A\lor B~~~~~~A\vdash C~~~~~~B\vdash C}{\Gamma \vdash C}\small{\lor E}}$$

$${\Gamma}$$と$${\Sigma}$$は(空を含む)論理式の集合(列)です。これらをもとに自然演繹の除去則を翻訳します。

$${\to}$$除去則

$${\mathcal D~~~~~~~~~~~\mathcal E~~~~~~~~~~~~\\\cfrac{A~~~~~~A\to B}{B}\small{\to E}\normalsize\\\mathcal G~~~~~~~\\\mathcal D~~~~~~~~~~~~~~~~\mathcal E~~~~\\\stackrel{tr.}{\Longrightarrow}\cfrac{\vdash A~~~~~~\vdash A\to B}{\vdash B}\small{\to E}\normalsize\\\mathcal G}$$

$${~~\mathcal E\\\cfrac{A~~~~~~A\to B}{B}\small{\to E}\normalsize\\\mathcal G~~~~~~~\\~~~~~~~~~~~~~~~~~~\mathcal E\\\stackrel{tr.}{\Longrightarrow}\cfrac{\overline{A\vdash A}~~~~~~\vdash A\to B}{A\vdash B}\small{\to E}\normalsize\\\mathcal G}$$

$${\mathcal D~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~\mathcal D~~~~~~~~~~~~~~~~~~~~~~~~~\\\cfrac{A~~~~~~A\to B}{B}\small{\to E}\normalsize\stackrel{tr.}{\Longrightarrow}\cfrac{\vdash A~~~~~~\overline{B\vdash B}}{A\to B\vdash B}\small{\to L}\normalsize\\\mathcal G~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~\mathcal G~~~~~~~~}$$

$${\land}$$除去則

$${\mathcal D~~~~~~~~~~~~~~~~~~~~~~~~~~~\mathcal D~~~~~~~\\\cfrac{A_1\land A_2}{A_i}\small{\land E}\normalsize\stackrel{tr.}{\Longrightarrow}\cfrac{\vdash A_1\land A_2}{\vdash A_i}\small{\land E}\normalsize\\\mathcal G ~~~~~~~~~~~~~~~~~~~~~~~~~~~\mathcal G ~~~~~~~}$$

$${\cfrac{A_1\land A_2}{A_i}\small{\land E}\normalsize\stackrel{tr.}{\Longrightarrow}\cfrac{\overline{A_i\vdash A_i}}{A_1\land A_2\vdash A_i}\small{\land L}\normalsize\\\mathcal G~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~\mathcal G~~~~~~~~~}$$

$${~~~~~~~~~~~~~~\mathcal D\\~~~~~~~~~~~~~~~~~[A_i]_m\\\mathcal E~~~~~~~~~~~~\mathcal D'\\\cfrac{A_1\land A_2~~~~~~C}{C}\small{\land E_m}\normalsize\\\mathcal G~~~~~~~\\ ~~~~~~~~~~~~~~~~~~~~~~~~~~\mathcal D\\~~~~~~~~~~~~~~~~~~~~~~~~~~~A_i\vdash A_i\\~~~~~~~\mathcal E~~~~~~~~~~~~~~~~~~\mathcal D'\\\stackrel{tr.}{\Longrightarrow}\cfrac{\vdash A_1\land A_2~~~~~~A_i\vdash C}{\vdash C}\small{\land E}\normalsize\\~~\mathcal G}$$

$${~~~~~~\mathcal D~~~~~~~~~~~~~~~~~~~~~~~~~~\mathcal D\\~~~~~~~~~~[A_i]_m~~~~~~~~~~~~~~~~~A_i\vdash A_i\\~~~~~~~\mathcal D'~~~~~~~~~~~~~~~~~~~~~~~~~\mathcal D'\\\cfrac{A_1\land A_2~~~~~~C}{C}\small{\land E_m}\normalsize\stackrel{tr.}{\Longrightarrow}\cfrac{A_i\vdash C}{A_1\land A_2\vdash C}\small{\land L}\normalsize\\\mathcal G~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~\mathcal G~~~}$$

$${\lor}$$除去則

$${~~~~~~~\mathcal D~~~~~~\mathcal E\\~~~~~~~~~~[A]_m~[B]_n\\\mathcal F~~~~~~~~~~\mathcal D'~~~~~\mathcal E'~~~~~\\\cfrac{A\lor B~~~~~~C~~~~~~C}{C}\small{\lor E_{m,n}}\normalsize\\\mathcal G~~~~~~~~~\\~~~~~~~~~~~~~~~~~~~~~~\mathcal D~~~~~~~~~~~~~~\mathcal E\\~~~~~~~~~~~~~~~~~~~~~~~A\vdash A~~~~~~B\vdash B\\~~~~~\mathcal F~~~~~~~~~~~~~~~\mathcal D'~~~~~~~~~~~~~\mathcal E'\\\stackrel{tr.}{\Longrightarrow}\cfrac{\vdash A\lor B~~~~~~A\vdash C~~~~~~B\vdash C}{\vdash C}\small{\lor E}\normalsize\\~~\mathcal G}$$

$${~~~~~~~\mathcal D~~~~~~\mathcal E\\ ~~~~~~~~~~[A]_m~[B]_n\\~~~~~~~~\mathcal D'~~~~~\mathcal E'\\\cfrac{A\lor B~~~~~~C~~~~~~C}{C}\small{\lor E_{m,n}}\normalsize\\\mathcal G~~~~~~~~~\\\mathcal D~~~~~~~~~~~~~~\mathcal E~~~~~~~~~~\\A\vdash A~~~~~~B\vdash B~~~~~~~~~\\\mathcal D'~~~~~~~~~~~~~\mathcal E'~~~~~~~~~\\\stackrel{tr.}{\Longrightarrow}\cfrac{A\vdash C~~~~~~B\vdash C}{A\lor B\vdash C}\small{\lor L}\normalsize~~~~~~~~~~~~~\\\mathcal G~~~~~~~~~}$$

長くなりすぎました。$${\land}$$除去則にいたっては２通りもわざわざ翻訳しました。本当はシークエントに除去則を定義したくありませんでしたが，翻訳のためなら仕方ありません。シークエントから自然演繹への翻訳はできるのかわかりませんが，機会があればやってみます。説明をかなり省いた部分がありますが，続きの記事で書くかもしれませんが，LaTeXが大変すぎるのでわかりません。

おまけ

直観主義論理に限定すると書きましたので，矛盾律(爆発律，否定除去)を翻訳しなければなりませんでした。

$${\mathcal D~~~~~~~~~~~~~~~~~\mathcal D~~~~~~~\\\cfrac{\bot}{A}\small{\bot E}\normalsize\stackrel{tr.}{\Longrightarrow}\cfrac{\vdash \bot}{\vdash A}\small{\bot E}}$$

こんな感じに翻訳できますが，やはり矛盾律は気持ち悪い。せめてシークエント側の「矛盾が証明される」部分は解消しておきます。↓シークエント

$${\overline{\bot \vdash A}^{Ax}}$$

一応$${Ax}$$なのは公理という意味です。といっても$${\bot}$$の導入則ではあるんですがね。