論理学において、部分構造論理とは、弱化、縮約、交換、結合性といった、古典論理や直観主義論理などの通常の構造規則のいずれかを欠いた論理のことである。より重要な部分構造論理の例として、関連性論理と線形論理が挙げられる。
シーケント計算では、証明の各行を次のように記述します。
ここで構造規則とは、当初は命題の有限列(シーケンス)として考えられていたシーケントの左辺(Γで表される)を書き換えるための規則である。この列の標準的な解釈は論理積であり、次のように読むことが期待される。
シーケント表記として
ここでは、右辺のΣを単一の命題C(直観主義的なシーケントのスタイル)とみなしていますが、すべての操作がターンスタイル記号の左側で行われるため、すべては一般の場合にも同様に当てはまります。。
論理積は可換かつ結合的な演算であるため、シーケント理論の形式的な設定には通常、シーケントΓを適切に書き換えるための構造規則が含まれる。例えば、演繹のために。
から
推測できる
また、
任意のBに対して、
線形論理では、重複する仮説は単一の仮説とは異なる扱いを受けるため、これらの規則は両方とも除外されますが、関連性(または関連性)論理では、 Bが結論に明らかに無関係であるという理由で、後者の規則のみが除外されます。
上記は構造規則の基本的な例である。これらの規則は、従来の命題論理に適用する際に議論の余地があるわけではない。これらは証明論において自然に現れるものであり、最初に注目されたのは(名称が付けられる以前から)証明論においてであった。
前提(そして複数の結論がある場合は結論も)を構成する方法は数多くあります。一つの方法は、それらを集合にまとめることです。しかし、例えば {a,a} = {a} なので、前提が集合であれば縮約は自動的に成り立ちます。また、結合法則や順列(または可換性)も自動的に成り立ちます。部分構造論理では、通常、前提は集合ではなく、木や多重集合(要素の複数回の出現を区別する集合)、あるいは式の列といった、より細かい構造に構成されます。例えば、線形論理では縮約が成り立たないため、前提は少なくとも多重集合と同じくらい細かい構造で構成されなければなりません。
部分構造論理は比較的新しい分野である。このテーマに関する最初の会議は、1990年10月にテュービンゲンで「制限付き構造規則を持つ論理」というタイトルで開催された。この会議で、コスタ・ドシェンが「部分構造論理」という用語を提唱し、現在ではこの用語が広く用いられている。