構造規則

証明論の論理学の分野では、構造規則とは、論理結合子を参照せず、シーケントに直接作用するシーケント計算の推論規則である。 ^{[ 1 ] [ 2 ]}構造規則は、論理の意図されたメタ理論的性質を模倣することが多い。構造規則の 1 つ以上を否定する論理は、部分構造論理に分類される。

3つの一般的な構造ルールは次のとおりです。^{[ 3 ]}

• 弱化とは、一連の仮説または結論に、追加の要素を追加して拡張できることを意味します。弱化ルールは、記号形式で次のように記述できます。${\displaystyle {\frac {\Gamma \vdash \Sigma }{\Gamma ,A\vdash \Sigma }}}$改札口の左側、そして${\displaystyle {\frac {\Gamma \vdash \Sigma }{\Gamma \vdash \Sigma ,A}}}$右側。古典論理では、含意の単調性として知られている。
• 縮約とは、シーケントの同じ側にある2つの等しい（または統合可能な）要素を、1つの要素（または共通のインスタンス）に置き換えることを指します。記号で表すと次のようになります。${\displaystyle {\frac {\Gamma ,A,A\vdash \Sigma }{\Gamma ,A\vdash \Sigma }}}$そして${\displaystyle {\frac {\Gamma \vdash A,A,\Sigma }{\Gamma \vdash A,\Sigma }}}$自動定理証明システムにおける分解法を用いた因数分解とも呼ばれる。古典論理では含意の冪等性として知られている。
• 交換とは、シーケントの同じ側にある2つの要素を交換できる操作です。記号で表すと次のようになります。${\displaystyle {\frac {\Gamma _{1},A,\Gamma _{2},B,\Gamma _{3}\vdash \Sigma }{\Gamma _{1},B,\Gamma _{2},A,\Gamma _{3}\vdash \Sigma }}}$そして${\displaystyle {\frac {\Gamma \vdash \Sigma _{1},A,\Sigma _{2},B,\Sigma _{3}}{\Gamma \vdash \Sigma _{1},B,\Sigma _{2},A,\Sigma _{3}}}}$（これは順列の法則とも呼ばれます。）

上記の構造規則を一切持たない論理では、シーケントの辺は純粋なシーケンスとして解釈されます。交換がある場合は、多重集合とみなすことができます。縮約と交換の両方がある場合は、集合とみなすことができます。

これらは可能な構造規則のすべてではありません。有名な構造規則はカットとして知られています。^{[ 1 ]}証明論者は、さまざまな論理においてカット規則が不要であることを示すためにかなりの努力を払っています。より正確には、カットは（ある意味で）証明を省略するためのツールにすぎず、証明できる定理を増やすものではないことが示されています。カット規則の「除去」に成功したことは、カット除去として知られており、正規化としての計算の哲学に直接関係しています（カリーとハワードの対応を参照）。これは、与えられた論理を決定する複雑さの良い指標となることがよくあります。

• アフィン論理– 各仮定を最大1回しか使用できないリソース重視の論理 
• 線形論理– リソースを考慮した論理システム 
• 順序付き論理（線形論理）– 線形論理の拡張リダイレクト先の簡単な説明を表示するページ 
• 関連性論理― 非古典論理の一種 
• 分離論理– コンピュータサイエンスにおける概念