部分構造論理

部分構造論理（ぶぶんこうぞうろんり、英: Substructural logic）は、通常の命題論理を弱くした論理体系群を指し、数理論理学の中でも証明理論と密接に関連する。部分構造論理は使用可能な構造規則が命題論理よりも少なく、かつ個々の部分構造論理によってその種類が異なる。構造規則の概念は自然演繹の定式化手法よりもシークエント表現に基づく。主な部分構造論理の例として、適切さの論理と線型論理がある^[1]。

シークエント計算では、証明の各行は次のように記される。

${\displaystyle \Gamma \vdash \Sigma }$

ここでの構造規則とは、左辺 ${\displaystyle \Gamma }$ のシークエント（命題を表す文字列）の項書き換え規則である。一般にここの文字列は論理積と解釈される。例えば、命題 ${\displaystyle A,B,C}$ に対して、以下のようなシークエント表現

${\displaystyle {\mathcal {A}},{\mathcal {B}}\vdash {\mathcal {C}}}$

は次のように解釈される。

(${\displaystyle A}$ かつ ${\displaystyle B}$) は ${\displaystyle C}$ を含意する。

ここで、右辺 ${\displaystyle \Sigma }$ が単一の命題 ${\displaystyle C}$ であるとしたが（直観主義的なシークエントのスタイル）、全ての操作はターンスタイル記号の左側で行われるので、一般のケースにも当てはまる。

論理積には交換法則と結合法則が成り立つので、シークエント ${\displaystyle \Gamma }$ を書き換える構造規則にも同じ法則に対応したもの（転置規則）がある。例えば、

${\displaystyle {\mathcal {B}},{\mathcal {A}}\vdash {\mathcal {C}}}$

から

${\displaystyle {\mathcal {A}},{\mathcal {B}}\vdash {\mathcal {C}}}$

を導くことができる。他にも冪等に対応した規則（縮約規則）と単調性に対応した規則（弱化規則）が存在する。

${\displaystyle \Gamma ,{\mathcal {A}},{\mathcal {A}},\Delta \vdash {\mathcal {C}}}$

から、次を導くことができる（縮約規則）。

${\displaystyle \Gamma ,{\mathcal {A}},\Delta \vdash {\mathcal {C}}}$

また

${\displaystyle \Gamma ,{\mathcal {A}},\Delta \vdash {\mathcal {C}}}$

から任意の B を加えて

${\displaystyle \Gamma ,{\mathcal {A}},{\mathcal {B}},\Delta \vdash {\mathcal {C}}}$

を導くこともできる（弱化規則）。

線型論理では、前提が重複する場合は単一のときとは異なった意味を持つので、これらの規則は除外される。適切さの論理では、弱化規則だけを除外する（${\displaystyle B}$ は帰結とは明らかに無関係であるため）。

これらは部分構造論理の基本的な例である。なお、通常の命題論理にこれらの規則を適用することは何ら問題ない。

脚注

[脚注の使い方]

1. 坪井直人『線形論理の拡張体系に対する代数的研究』 北陸先端科学技術大学院大学 情報科学研究科〈修士〉、2004年。hdl:10119/1789。https://hdl.handle.net/10119/1789。

外部リンク

• Article on Substructural logics スタンフォード哲学百科事典