ハイパーシエント

数理論理学において、ハイパーシーケントフレームワークは、構造証明論で使用されるシーケント計算の証明論的フレームワークを拡張したものであり、シーケントフレームワークでは捉えられない論理体系に対して解析的計算を提供する。ハイパーシーケントは通常、通常のシーケントの有限多重集合として扱われ、次のように表記される。

$\displaystyle \Gamma _{1}\Rightarrow \Delta _{1}\mid \cdots \mid \Gamma _{n}\Rightarrow \Delta _{n}}$

ハイパーシーケントを構成するシーケントはコンポーネントと呼ばれます。ハイパーシーケントフレームワークの表現力の向上は、中間論理LC（ゲーデル・ダメット論理）の通信規則など、さまざまなコンポーネントを操作する規則によって実現されます。

${\displaystyle {\frac {\Gamma _{1}\Rightarrow \Delta _{1}\mid \dots \mid \Gamma _{n}\Rightarrow \Delta _{n}\mid \Sigma \Rightarrow A\qquad \Omega _{1}\Rightarrow \Theta _{1}\mid \dots \mid \Omega _{m}\Rightarrow \Theta _{m}\mid \Pi \Rightarrow B}{\Gamma _{1}\Rightarrow \Delta _{1}\mid \dots \mid \Gamma _{n}\Rightarrow \Delta _{n}\mid \Omega _{1}\Rightarrow \Theta _{1}\mid \dots \mid \Omega _{m}\Rightarrow \Theta _{m}\mid \Sigma \Rightarrow B\mid \Pi \Rightarrow A}}}$

または様相論理S5の様相分割規則：^{[ 1 ]}

${\displaystyle {\frac {\Gamma _{1}\Rightarrow \Delta _{1}\mid \dots \mid \Gamma _{n}\Rightarrow \Delta _{n}\mid \Box \Sigma ,\Theta \Rightarrow \Box \Pi ,\Omega }{\Gamma _{1}\Rightarrow \Delta _{1}\mid \dots \mid \Gamma _{n}\Rightarrow \Delta _{n}\mid \Box \Sigma \Rightarrow \Box \Pi \mid \Theta \Rightarrow \Omega }}}$

ハイパーシーケント計算は、様相論理、中間論理、部分構造論理を扱うために用いられてきた。ハイパーシーケントは通常、論理式解釈を持ち、すなわち、対象言語の論理式によって解釈される。その論理式は、ほぼ常に何らかの選言として解釈される。正確な論理式解釈は、対象となる論理によって異なる。

形式的には、ハイパーシーケントは通常、通常のシーケントの有限多重集合として扱われ、次のように表記される。

$\displaystyle \Gamma _{1}\Rightarrow \Delta _{1}\mid \dots \mid \Gamma _{n}\Rightarrow \Delta _{n}}$

ハイパーシーケントを構成するシーケントは、論理式の多重集合のペアからなり、ハイパーシーケントのコンポーネントと呼ばれます。多重集合の代わりに集合またはリストを使用してハイパーシーケントとシーケントを定義するバリアントも考慮され、考慮される論理に応じて、シーケントは古典的または直観主義的になります。命題結合子の規則は通常、対応する標準シーケント規則の適応であり、ハイパーシーケントコンテキストとも呼ばれる追加のサイドハイパーシーケントがあります。たとえば、機能的に完全な結合子の集合に対する共通の規則セット。${\displaystyle \{\bot ,\to \}}$古典命題論理は、以下の4つの規則によって規定される。

${\displaystyle {\frac {}{{\mathcal {G}}\mid \Gamma ,p\Rightarrow p,\Delta }}}$

${\displaystyle {\frac {}{{\mathcal {G}}\mid \Gamma ,\bot \Rightarrow \Delta }}}$

${\displaystyle {\frac {{\mathcal {G}}\mid \Gamma ,B\Rightarrow \Delta \qquad {\mathcal {G}}\mid \Gamma \Rightarrow A,\Delta }{{\mathcal {G}}\mid \Gamma ,A\to B\Rightarrow \Delta }}}$

${\displaystyle {\frac {{\mathcal {G}}\mid \Gamma ,A\Rightarrow B,\Delta }{{\mathcal {G}}\mid \Gamma \Rightarrow A\to B,\Delta }}}$

ハイパーシーケント設定における追加構造のため、構造規則は内部および外部のバリアントで検討されます。内部弱化規則と内部収縮規則は、ハイパーシーケントのコンテキストを追加した対応するシーケント規則の適応です。

${\displaystyle {\frac {{\mathcal {G}}\mid \Gamma \Rightarrow \Delta }{{\mathcal {G}}\mid \Gamma ,\Sigma \Rightarrow \Delta ,\Pi }}}$

${\displaystyle {\frac {{\mathcal {G}}\mid \Gamma ,A,A\Rightarrow \Delta }{{\mathcal {G}}\mid \Gamma ,A\Rightarrow \Delta }}}$

${\displaystyle {\frac {{\mathcal {G}}\mid \Gamma \Rightarrow A,A,\Delta }{{\mathcal {G}}\mid \Gamma \Rightarrow A,\Delta }}}$

外部弱化ルールと外部収縮ルールは、数式ではなく、ハイパーシーケントコンポーネントのレベルにおける対応するルールである。

${\displaystyle {\frac {\mathcal {G}}{{\mathcal {G}}\mid \Gamma \Rightarrow \Delta }}}$

${\displaystyle {\frac {{\mathcal {G}}\mid \Gamma \Rightarrow \Delta \mid \Gamma \Rightarrow \Delta }{{\mathcal {G}}\mid \Gamma \Rightarrow \Delta }}}$

これらの規則の妥当性は、ハイパーシーケント構造の論理式解釈と密接に関係しており、ほとんどの場合、何らかの形式の選言として解釈されます。正確な論理式解釈は、考慮される論理によって異なります。いくつかの例については、以下を参照してください。

ハイパーシーケント構造は、様相論理S5の計算体系を得るために^{[ 2 ]}でcortegeという名前で最初に登場したようです。これは、様相論理を扱うために^{[ 3 ]}でも独立して開発されたようで、また、様相論理、中間論理、部分構造論理の計算体系が検討され、ハイパーシーケントという用語が導入された影響力のある^{[ 1 ]}でも開発されました。