部分構造論理

提供: miniwiki
2018/8/19/ (日) 17:27時点におけるAdmin (トーク | 投稿記録)による版 (1版 をインポートしました)
(差分) ← 古い版 | 最新版 (差分) | 新しい版 → (差分)
移動先:案内検索

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

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

[math]\Gamma\vdash\Sigma[/math]

ここでの構造規則とは、右辺 Γ のシークエント(命題を表す文字列)の項書き換え規則である。一般にここの文字列は論理積と解釈され、以下のようなシークエント表現

[math]\mathcal A,\mathcal B \vdash\mathcal C[/math]

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

(A かつ B) は C含意する。

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

論理積には交換法則結合法則が成り立つので、シークエント Γ を書き換える構造規則にも同じ法則に対応したもの(転置規則)がある。例えば、

[math]\mathcal B,\mathcal A\vdash\mathcal C[/math]

から

[math]\mathcal A,\mathcal B\vdash\mathcal C[/math]

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

[math] \Gamma,\mathcal A,\mathcal A,\Delta\vdash\mathcal C[/math]

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

[math] \Gamma,\mathcal A,\Delta\vdash\mathcal C[/math]

また

[math] \Gamma,\mathcal A,\Delta\vdash\mathcal C[/math]

から任意の B を加えて

[math] \Gamma,\mathcal A,\mathcal B,\Delta\vdash\mathcal C[/math]

を導くこともできる(弱化規則)。

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

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

外部リンク