1 シークエント形式の概要
1.1 基本的な考え方
シークエント形式は、論理式の集合を「前提（仮定）」として、別の論理式（または式の条件）を「結論（目標）」として同時に記述し、その間に成立する推論関係を規則として扱う体系的な枠組みである。自然言語の推論で言えば、「これらを仮定したとき、これが言える」という構造を、記号化して操作対象にする。
この形式では、証明を単に“真偽の到達”としてではなく、前提と目標の間にある導出手続きとして捉える点が中心にある。導出は、シークエントを単位として規則を適用することで進み、証明の過程は明示的な段階列として表される。その結果、証明理論や計算論理が扱う性質（正当性、変換可能性、正規化など）を、形式のレベルで解析しやすくなる。
1.2 シークエントの表記
1.2.1 前提（左辺）の扱い
シークエントは通常、前提側（左側）と結論側（右側）に分かれて書かれる。前提側は論理式の集まりとして表現され、体系によっては順序や重複が意味をもつかどうかが異なる。一般的な読み方としては、左辺にある式すべてを同時に仮定した状況を表す。
このとき、前提側が「集合」なのか「列」なのかは重要である。前提の順序を区別しない体系では、左辺の並び替えは同値変換として扱われる。一方、順序を区別する体系では、推論規則の適用可能性や証明探索の挙動が、配列としての構造に依存することがある。
1.2.2 結論（右辺）の扱い
結論側は論理式、あるいは場合によっては複数の式の条件として表現される。古典論理を扱う代表的な体系では右辺に複数の候補を置けるが、直観主義的な体系では右辺の形が制約されやすい。特に直観主義では、結論を「1つの主張」として明確に対応づけることが多く、右辺の単一性が制約条件として現れる。
読みとしては、右辺に書かれた条件のいずれか、または右辺全体が成り立つことを目標にする、という形で理解される。どの意味が採られているかは、体系の規則設計に依存する。
1.3 推論規則との対応
シークエント形式の核心は、論理結合子や量化に対応する推論規則が、シークエントの形（前提・結論の側の式配置）に直接結び付けられている点にある。たとえば否定、含意、論理積、論理和などの各結合子について、導出可能性が保たれるような導入規則と除去規則に類するものが与えられる。
規則適用の単位がシークエントであるため、証明の“どの段で何を仮定し、どう目標を分解したか”が見える。さらに、証明変換（たとえば特定の推論段を削る、別の形に組み替える）も、シークエント上での変形として定義できる。このため、形式のメタ理論（健全性、完全性、カット除去など）の議論に向いている。
2 数理論理における位置づけ
2.1 自然演繹との違い
2.1.1 証明の形の比較
自然演繹は「仮定を導入し、それを用いて結論へ進む」流れを中心に証明を組み立てるのが一般的であり、サブ証明の入れ子構造や仮定の局所性が目立つ。一方、シークエント形式は、前提集合と結論目標を同時に扱い、推論を段階的に写像する設計になっている。
両者の差は、証明の見た目だけでなく、証明変換のやりやすさにも現れる。シークエント形式ではカットと呼ばれる中間結果の“接続”が明確に記述され、カット除去による正規形への変換が体系的に研究されてきた。自然演繹でも正規化に相当する話題はあるが、シークエントでは前提・結論の配置が機械的に操作できるため、論理結合子ごとの規則の相互作用が追跡しやすい。
2.2 ヒルベルト式との違い
ヒルベルト式は、いくつかの公理（axiom）と推論規則（多くの場合は1つの推論規則、例として変項を含む修正された様式の置換や、含意の推論など）により証明を組み立てる方式である。証明全体が“公理からの連鎖”として表現され、途中での論理構造の分解が見えにくい傾向がある。
これに対してシークエント形式では、各論理記号の振る舞いが規則の形として直接反映される。したがって、どの論理演算がどの導出段で使われたかが追いやすく、証明の局所的な構造解析（例：特定の規則を削る変換）が目的にしやすい。
2.3 証明理論での役割
証明理論の観点では、シークエント形式はメタ理論的性質を取り出すための“制御された舞台”を提供する。とくに、導出規則を明示し、証明をシークエントの列として扱えるため、カット（中間命題の利用）や正規化に相当する性質を形式的に定義できる。
また、証明理論の研究対象である「証明の長さ」「構造的性質」「計算的解釈」といった観点も、シークエントの設計（前提の扱い、構造規則の有無など）と結び付けて解析できる。結果として、論理の強さや計算原理との対応関係を、精密に比較するための共通基盤として使われることが多い。
3 代表的な体系
3.1 LK（古典論理）系
3.1.1 規則の直観的意味
LKは古典論理に対応する代表的なシークエント体系として知られ、前提側と結論側を柔軟に扱いながら、古典的な推論を導出可能にする設計をもつ。規則は、論理結合子に関する導入・除去に相当する形で与えられ、たとえば含意の扱いでは「前提を追加して目標を達成する」方向と、「結論側の目標に対して前提の仮定をどう使うか」という方向が規則として対応づけられる。
また、古典性の特徴は、否定や中間命題の扱いに関する規則群の設計に現れる。直観主義と異なり、右辺の形が厳密に制約されない体系が多く、そこにより古典的等式や双対性が導出として表現される。
3.2 LJ（直観主義論理）系
3.2.1 右辺の単一性の意味
LJは直観主義論理のための代表的なシークエント体系で、右辺が通常単一の式になるように設計される。この「右辺の単一性」は、直観主義が要求する証明の形—つまり結論を1つの主張として扱い、その主張の成立を直接目標に据える—と整合する。
直観主義では、ある主張を導くとは、その主張を実際に構成できることに対応するという解釈が背後にある。そのため、目標を“複数候補の中から選ぶ”ような形にせず、1つの式として固定することで、導出規則の性格が直観主義的意味論と結び付きやすくなる。
さらに、構造規則の扱いにも体系差が現れうる。たとえば前提側の弱めや置換の自由度は、直観主義の枠組みでの証明変換や意味論的解釈に関係するため、LJはその整合性を確保するように規則を調整する。
3.3 変種と拡張
3.3.1 多値・多形式への一般化
シークエント形式は、古典・直観主義の2値論理に限られず、多値論理や、より広い種類の導出関係に拡張されてきた。多値論理では、真理の次数が複数になるため、シークエントにおける結論側の意味や、前提からの到達が“どの値に対して成立するか”として組み直されることがある。
また、多形式（複数の論理構造や複数の結合演算）へ一般化する試みでは、シークエントを構成する部品（前提の型、結論の型、構造規則の有無）を調整し、特定の性質が保たれるようにした体系が設計される。これにより、論理的推論を抽象化した枠組みとして、証明理論・形式言語理論・型理論の周辺領域と結びつけやすくなる。
4 基本性質と代表的結果
4.1 健全性と完全性
4.1.1 導出可能性の対応
健全性と完全性は、シークエント形式が意図した意味論に対して正しく振る舞うかを示す中心的な指標である。健全性は、「シークエントが導出できるなら、その意味での妥当性（真であること、充足されることなど）が成り立つ」ことを述べる。完全性は逆に、「意味での妥当性が成り立つなら、対応するシークエントが導出できる」ことを保証する。
導出可能性と意味論的真理の橋渡しが確立されることで、形式体系は“証明が意味を保存している”だけでなく、“意味が形式で表現し尽くせる”ことも分かる。体系ごとに意味論（古典的、直観主義的、あるいはそれ以外の評価方式）が異なるため、健全性・完全性の証明方法や、必要となる前提（構造規則の範囲など）も変わりうる。
4.2 カット（切断）とその意義
4.2.1 カット除去の考え方
カットは、途中で得た中間結果を別の導出の途中に接続するための仕組みとして現れる。直観的には、「まず補題を証明し、その補題を使って最終目標へ進む」という形を、体系の規則として明示する操作である。カットが許されると、証明が短く見える場合もあるが、その構造は中間命題の依存関係を通じて複雑になることがある。
カット除去は、「カットを含む証明が存在するなら、同じ結論をカットなしで達成できる」ことを目指す考え方である。これは証明の構造を整理し、無駄な中間接続を取り除く方向の正規化として理解できる。カットが除去できれば、証明はより“直接的”で、論理結合子に対応する規則の組み合わせが見える形になる。
さらにカット除去の性質は、証明探索の指針にもなる。中間結果を多用しない方向へ証明が変換されるため、証明の上限や計算的含意の解析が進めやすくなる。
4.3 正規形・証明変換
4.3.1 証明探索への影響
正規形（normal form）や証明変換は、同じ結論を与える証明のうち、特定の“簡潔で標準化された形”を目指す操作である。シークエント形式では、カット除去や特定の規則の並べ替えといった変換が規則系として定義されるため、証明を一種の正規化手続きにより追い込むことができる。
これにより、証明探索の観点では探索空間が整理される。たとえば、変換により同値な証明がまとめられることで、同じ目的に対して冗長な枝分かれが減りうる。また、正規形が存在するなら、導出の検索は“正規形に到達するまで”の問題として捉え直せるため、アルゴリズム設計や計算量の見積もりにも影響が出る。
正規形への変換が必ずしも一意とは限らない場合でも、変換の停止性や、どの程度の簡約が保証されるかが重要な情報になる。結果として、形式的推論を設計・検証する際の指針として、シークエント体系の変換論が役立つ。