排他的選言の推論規則

日常言語での接続詞の用法や真理値表では通常の選言(両立的選言)の他に両方の選言肢の両方が真である場合に全体が偽になるという排他的選言が紹介されることがある。

形式的証明体系であるシーケント計算や自然演繹で現れる選言の規則は両立的選言である。

それでは排他的選言はどのような推論規則になるのだろうか？

排他的選言は両立的選言の場合とは異なり大多数の人々が認めるような推論規則を持たないが、いくつかの推論規則を構成する方法がある。これらの方法は排他的選言に限らず真理値が知られていれば用いることができる。私見での大まかなメリットとデメリットも述べる。

1. 真理値で同値な論理式を分解して推論規則を得る。

例えば同値の論理結合子 ( $A\Leftrightarrow B$ ) の推論規則を考える場合は真理値が同じになる $(A\to B)\land (B\to A)$ の中に現れる論理結合子がなくなるまで規則を逆適用していき、推論規則を得る。その際に適当なコンテクストを追加して考える。結論である $\Gamma\vdash (A\to B)\land (B\to A),\Delta$ を分解して前提( $\Gamma, A\vdash B,\Delta$ ), ( $\Gamma, B\vdash A,\Delta$ ) を得る。

メリット

どのような体系でも考えることができる。
論理式によっては面白い前提の形をした推論規則が得られることもある。

デメリット

真理値が同値な論理式は複数あるのでどれを選ぶのかには恣意性がある。
カット除去や正規化は一般には成り立たない。

2. Generalized natural deductionを使う。

以下の文献の方法で真理値表から推論規則を構成することができる。

Geuvers and T. Hurkens. Deriving Natural Deduction Rules from Truth Tables. In ICLA, volume 10119 of Lecture Notes in Computer Science, pages 123–138. Springer, 2017.

以下で読むことができる。

http://www.cs.ru.nl/~herman/PUBS/NatDedTruthTables_Extended.pdf

カリー・ハワード対応も考えることができる。

https://drops.dagstuhl.de/opus/volltexte/2018/10051/pdf/LIPIcs-TYPES-2017-3.pdf

排他的選言(xor)の具体的な推論規則については以下を参照

http://www.sqlab.i.is.nagoya-u.ac.jp/~nakazawa/papers/ppl2020.pdf

メリット

体系の強正規化定理がメタ定理として示されている。つまりこの方法で作られた推論規則は一律に証明論的に良い性質を持つ。クリプキモデルがある。

デメリット

道具立てが大掛かりである。

3. 公理として追加する

この方法は以下の論文を参照。

S.Bobzien, R. Dyckhoff, Analyticity, Balance and Non-admissibility of Cut in Stoic Logic, Studia Logica, 2019, pp.375-397

排他的選言の場合は( $A+B, A \Rightarrow \neg B$ ), ( $A+B, B \Rightarrow \neg A$ ), ( $A+B, \neg A \Rightarrow B$ ), ( $A+B, \neg B \Rightarrow A$ )の四つを公理に追加する。計算は論理プログラミングのようにカット規則によって行う。