論理学において、部分構造論理とは、弱化、収縮、交換、結合性など、通常の構造規則(古典論理や直観論理など)のいずれかが欠けている論理です。より重要な部分構造論理の 2 つは、関連性論理と線形論理です。
例
シーケント計算では、証明の各行を次のように書きます。
- 。
ここで構造規則とは、Γで示されるシークエントの左辺を書き換える規則であり、当初は命題の列(シーケンス)として考えられていた。この列の標準的な解釈は接続詞である。つまり、次のように読むことが期待される。
の連続表記として
- ( A と B ) はC を意味します 。
ここでは、 RHS Σ を単一の命題C (シークエントの直観主義スタイル) と見なしていますが、すべての操作は回転式記号 の左側で行われるため、すべてが一般的なケースに等しく適用されます。
連言は可換かつ結合的な操作であるため、シークエント理論の形式的な設定には通常、それに応じてシークエントΓを書き直すための構造規則が含まれる。例えば、
から
- 。
推測できる
- 。
また、
任意のBに対して、
- 。
重複した仮説を単一の発生とは異なって「カウント」する線形論理では、これらのルールの両方が除外されますが、関連(または関連性)論理では、 Bが結論とは明らかに無関係である という理由で、後者のルールのみが除外されます。
上記は構造規則の基本的な例です。これらの規則は、従来の命題計算に適用された場合、議論の余地があるわけではありません。これらの規則は証明理論で自然に発生し、そこで初めて認識されました (名前が付けられる前)。
前提構成
前提 (および複数の結論がある場合は結論も) を構成する方法は多数あります。 1 つの方法は、それらを集合に集めることです。 ただし、たとえば {a,a} = {a} であるため、前提が集合である場合は縮約が無料になります。 また、他の特性の中でも、結合性や順列性 (または可換性) も無料で得られます。 部分構造論理では、通常、前提は集合に構成されるのではなく、ツリーや多重集合 (要素の複数の出現を区別する集合)、または式のシーケンスなどのより細かい粒度の構造に構成されます。 たとえば、線形論理では縮約が失敗するため、前提は少なくとも多重集合と同じくらい細かい粒度で構成する必要があります。
歴史
部分構造論理は比較的新しい分野です。このトピックに関する最初の会議は、1990 年 10 月にテュービンゲンで「制限された構造規則を持つ論理」として開催されました。会議中に、Kosta Došen が「部分構造論理」という用語を提案し、これが今日使用されています。
参照
参考文献
- F. Paoli (2002)、「サブ構造論理:入門書」、Kluwer。
- G. Restall (2000) 『サブ構造論理入門』、Routledge。
さらに読む
- Galatos、Nikolaos、Peter Jipsen、Tomasz Kowalski、小野博明 (2007)、Residuated Lattices。 「An Algebraic Glimpse at Substructural Logics」、エルゼビア、ISBN 978-0-444-52141-5。
外部リンク
ウィキメディア・コモンズにおけるサブ構造論理に関連するメディア- レストール、グレッグ。「サブ構造論理」。ザルタ、エドワード N. (編)。スタンフォード哲学百科事典。
