第9章 シークエント計算とカット除去

証明そのものを、数学の対象にする

ここまで「$\vdash$」を「導ける／導けない」という有無で使ってきました。証明論はもう一歩踏み込み、 証明の形そのものを数学的対象として解析します。証明はどんな構造をもつのか、余計な回り道を 削れるのか、削るとどんな良いことが起きるのか。

その舞台がゲンツェンのシークエント計算 LK です。自然演繹（第2章）が「仮定を立てて解消する」木だったのに対し、 LK は「$\Gamma\vdash\Delta$（前提の並びから結論の並びへ）」というシークエントを書き換えていく、非常に対称的な体系です。 そして LK の心臓がカット規則——補題を使う推論の形式化——と、その驚くべき除去可能性（カット除去定理）。 カットが消せるという一事から、無矛盾性・部分論理式性・決定可能性が次々に流れ出ます。ゲンツェンが 算術の無矛盾性を証明した道具でもあり、証明論の背骨です。

シークエント計算は証明を対称的な書き換えとして扱う。カット除去が、無矛盾性など深い帰結を生む。

シークエントと LK の規則

LK の規則は、公理・構造規則・論理規則・カットの4種。各結合子に左規則（前件に導入）と右規則（後件に導入）が対で付きます。

カット規則の意味は「補題 $A$ を、片方で示し（$\vdash A$）、もう片方で使う（$A\vdash$）と、$A$ を消して繋げられる」。 数学者が「補題 $A$ を経由して」証明するのを形式化したものです。論理規則が結合子を組み立てるだけなのに対し、 カットだけが「途中で現れて消える式 $A$」を許す——これがカットの特別さであり、除去の対象になる理由です。 例として $\vdash(A\land B)\to(B\land A)$ を、カットを使わずに導きます。

下から読むと、$\to$ を後件に作り（→R）、$\land$ を後件に作り（∧R）、前件の $\land$ を分解（∧L）して公理に至る。 各段で扱う論理式は、下の結論の“部分”になっている——この性質（部分論理式性）が、カットの無い証明の際立った特徴です。

カット除去定理

証明は「カットを木の上へ押し上げ、より単純なカットに分解して消す」という二重帰納法です。全ケースは膨大なので、 帰納の骨格と鍵となる簡約を示します。

証明の“エンジン”は、主要カットがカット式の部分論理式に関する小さいカットへ分解されること。 $B\land C$ のカットが $B$（または $C$）のカットに落ちる——結合子が1つ減る。この降下が停止性を保証します （ただし、証明の大きさは超指数的に爆発しうる。効率と可能性は別問題）。

カット除去の帰結

カットが消せると、証明が「部分論理式だけで組み上がる」形に正規化され、深い系が一気に出ます。

無矛盾性の証明が「空シークエントはどの規則の結論にもならない」というほとんど目視で分かる議論に落ちるのが、 カット除去の威力です。意味論（健全性）を経由せず、証明の構文的構造だけから無矛盾性が出る——この“純構文的な 無矛盾性証明”の路線が、第13章のゲンツェンによる算術の無矛盾性証明（$\varepsilon_0$ までの超限帰納法）へ発展します。

つまずきポイント

この章のまとめ

• シークエント計算 LK は $\Gamma\vdash\Delta$ を書き換える対称的な体系。各結合子に左右の規則があり、カット規則が「補題を経由する推論」を担う。
• カット除去定理：カットは常に除去できる。証明は $(\text{次数},\text{階数})$ の二重帰納法で、主要カットを部分論理式の小さいカットへ分解するのがエンジン。
• 帰結：部分論理式性・無矛盾性（空シークエントは導けない）・命題論理の決定可能性・クレイグ補間。純構文的な無矛盾性証明はゲンツェンの算術無矛盾性へ繋がる。

次章は、これまでの古典論理を相対化します。直観主義論理・様相論理・高階論理という非古典・高階の論理へ進みます。