シークエント計算
概要
シークエント計算（sequent calculus）とは、論理式の有限列の組 $\Gamma\Rightarrow\Delta$（「$\Gamma$ がすべて成り立つなら $\Delta$ のどれかが成り立つ」と読む）を、始シークエント $A\Rightarrow A$ から構造規則・カット・論理記号ごとの左右の規則で導出する証明体系で、Gentzen が古典論理の体系 LK と直観主義論理の体系 LJ として導入した。導出できるシークエントは妥当であり、Gentzen の基本定理によりカットを使わずに導出できる。カットのない導出には結論の部分論理式しか現れないので、空のシークエントが導出できないこと（無矛盾性）や、LJ で $A\lor B$ が導出できれば $A$ か $B$ が導出できることが、導出の形から分かる。
シークエント計算（sequent calculus、シーケント計算）は、Gentzen が 1930 年代に導入した証明体系である（Zac25 §9.2、p. 155）。扱う対象は論理式そのものではなく、論理式の有限列の組 $\Gamma\Rightarrow\Delta$（シークエント）で、「$\Gamma$ がすべて成り立つなら、$\Delta$ のどれかが成り立つ」と読む。推論規則は、論理記号ごとに「左辺に導入する規則」と「右辺に導入する規則」が対になって並び、ほかに列を整える構造規則と、補題を使う推論にあたる カット がある。
シークエント計算の中心にあるのは Gentzen の 基本定理（Hauptsatz、カット除去定理）である。導出できるシークエントはカットを使わずに導出でき、カットのない導出には、結論に現れる論理式の部分論理式しか現れない。この性質から、体系の無矛盾性や直観主義論理の選言の性質が、導出の形を調べるだけで分かる。この記事では、古典論理の体系 $\mathbf{LK}$ を定義し、健全性、命題論理での基本定理、部分論理式性とその帰結を証明し、直観主義論理の体系 $\mathbf{LJ}$ との違いを説明する。
定義
シークエント
一階言語 $L$ を固定する。この記事では等号を扱わず、論理記号は $\lnot,\land,\lor,\to,\forall,\exists$ とする。固有変数（後述）に使うため、$L$ は無限に多くの定数記号をもつとする。シークエントに並べるのは文（自由変数のない論理式）である。$A(x)$ は自由変数が高々 $x$ の論理式を表し、項 $t$ について $A(t)$ は $x$ に $t$ を代入した文を表す。
文の有限列（空でもよい）$\Gamma,\Delta$ の組を $\Gamma\Rightarrow\Delta$ と書き、シークエント（sequent）という。$\Gamma$ を 前件、$\Delta$ を 後件 という。$L$ 構造 $\mathcal M$ が $\Gamma\Rightarrow\Delta$ を 満たす とは、$\Gamma$ のある元が $\mathcal M$ で偽であるか、$\Delta$ のある元が $\mathcal M$ で真であることをいう。すべての $L$ 構造が満たすシークエントを 妥当 という。
$\Gamma=A_1,\dots,A_m$、$\Delta=B_1,\dots,B_n$ なら、$\Gamma\Rightarrow\Delta$ が妥当であることは、文 $A_1\land\cdots\land A_m\to B_1\lor\cdots\lor B_n$ が妥当であることと同じである。前件が空のシークエント $\Rightarrow\Delta$ は「$\Delta$ のどれかが真」、後件が空のシークエント $\Gamma\Rightarrow$ は「$\Gamma$ のどれかが偽」を表す。両辺が空のシークエント $\Rightarrow$ はどの構造も満たさない。$\Gamma,A$ は列 $\Gamma$ の右端に $A$ を付け加えた列、$\Gamma,\Pi$ は列の連結を表す。
体系 LK
始シークエント は $A\Rightarrow A$（$A$ は任意の文）の形のシークエントである。推論規則は次のとおりで、横線の上が前提、下が結論である。$\Gamma,\Delta,\Pi,\Lambda$ は文の任意の有限列、$A,B$ は任意の文を表す。
構造規則（弱化 W・縮約 C・交換 X）：
$$
\frac{\Gamma\Rightarrow\Delta}{A,\Gamma\Rightarrow\Delta}\,\mathrm{WL}\qquad
\frac{\Gamma\Rightarrow\Delta}{\Gamma\Rightarrow\Delta,A}\,\mathrm{WR}\qquad
\frac{A,A,\Gamma\Rightarrow\Delta}{A,\Gamma\Rightarrow\Delta}\,\mathrm{CL}\qquad
\frac{\Gamma\Rightarrow\Delta,A,A}{\Gamma\Rightarrow\Delta,A}\,\mathrm{CR}
$$
$$
\frac{\Gamma,A,B,\Pi\Rightarrow\Delta}{\Gamma,B,A,\Pi\Rightarrow\Delta}\,\mathrm{XL}\qquad
\frac{\Gamma\Rightarrow\Delta,A,B,\Lambda}{\Gamma\Rightarrow\Delta,B,A,\Lambda}\,\mathrm{XR}\qquad
\frac{\Gamma\Rightarrow\Delta,A\quad A,\Pi\Rightarrow\Lambda}{\Gamma,\Pi\Rightarrow\Delta,\Lambda}\,\mathrm{Cut}
$$
論理規則：
$$
\frac{\Gamma\Rightarrow\Delta,A}{\lnot A,\Gamma\Rightarrow\Delta}\,\lnot\mathrm{L}\qquad
\frac{A,\Gamma\Rightarrow\Delta}{\Gamma\Rightarrow\Delta,\lnot A}\,\lnot\mathrm{R}\qquad
\frac{A,\Gamma\Rightarrow\Delta}{A\land B,\Gamma\Rightarrow\Delta}\qquad
\frac{B,\Gamma\Rightarrow\Delta}{A\land B,\Gamma\Rightarrow\Delta}\,\land\mathrm{L}\qquad
\frac{\Gamma\Rightarrow\Delta,A\quad\Gamma\Rightarrow\Delta,B}{\Gamma\Rightarrow\Delta,A\land B}\,\land\mathrm{R}
$$
$$
\frac{A,\Gamma\Rightarrow\Delta\quad B,\Gamma\Rightarrow\Delta}{A\lor B,\Gamma\Rightarrow\Delta}\,\lor\mathrm{L}\qquad
\frac{\Gamma\Rightarrow\Delta,A}{\Gamma\Rightarrow\Delta,A\lor B}\qquad
\frac{\Gamma\Rightarrow\Delta,B}{\Gamma\Rightarrow\Delta,A\lor B}\,\lor\mathrm{R}
$$
$$
\frac{\Gamma\Rightarrow\Delta,A\quad B,\Pi\Rightarrow\Lambda}{A\to B,\Gamma,\Pi\Rightarrow\Delta,\Lambda}\,{\to}\mathrm{L}\qquad
\frac{A,\Gamma\Rightarrow\Delta,B}{\Gamma\Rightarrow\Delta,A\to B}\,{\to}\mathrm{R}
$$
$$
\frac{A(t),\Gamma\Rightarrow\Delta}{\forall x\,A(x),\Gamma\Rightarrow\Delta}\,\forall\mathrm{L}\qquad
\frac{\Gamma\Rightarrow\Delta,A(a)}{\Gamma\Rightarrow\Delta,\forall x\,A(x)}\,\forall\mathrm{R}\qquad
\frac{A(a),\Gamma\Rightarrow\Delta}{\exists x\,A(x),\Gamma\Rightarrow\Delta}\,\exists\mathrm{L}\qquad
\frac{\Gamma\Rightarrow\Delta,A(t)}{\Gamma\Rightarrow\Delta,\exists x\,A(x)}\,\exists\mathrm{R}
$$
$\forall\mathrm{L}$ と $\exists\mathrm{R}$ の $t$ は任意の閉項である。$\forall\mathrm{R}$ と $\exists\mathrm{L}$ の $a$ は定数記号で、その規則の結論のシークエントに現れてはならない（固有変数の条件）。この $a$ を 固有変数（eigenvariable）という。
導出 とは、シークエントを頂点とする有限の木で、一番上のシークエントがすべて始シークエントであり、それ以外の各シークエントがすぐ上のシークエントから 1 つの規則で得られるものをいう。一番下のシークエントが $\Gamma\Rightarrow\Delta$ である導出があるとき、$\Gamma\Rightarrow\Delta$ は $\mathbf{LK}$ で 導出可能 であるといい、$\mathbf{LK}\vdash\Gamma\Rightarrow\Delta$ と書く。カットを使わない導出を カットなしの導出 という。
この体系は Zac25 §10.1〜10.5（pp. 162–167）のものと同じである（同書は始シークエントに $\bot\Rightarrow$ も加えている）。論理規則で結論に新しく現れる論理式を 主論理式、前提でそれのもとになった $A,B,A(t),A(a)$ を 副論理式 という。命題変数から $\lnot,\land,\lor,\to$ で作った論理式だけを扱い、量化記号の規則を除いた体系を、命題論理の $\mathbf{LK}$ という。このとき「妥当」は、すべての付値で満たされることとする（命題論理 の記事の定義「付値と真理値」）。
直感
規則を下から上へ読むと、シークエントを偽にする構造を探す手順になる。右辺の $A\land B$ を偽にするには $A$ か $B$ を偽にすればよいので、$\land\mathrm R$ の前提は 2 つに分かれる。左辺の $\forall x\,A(x)$ を真にするには、すべての $t$ で $A(t)$ が真でなければならないので、$\forall\mathrm L$ はどの $t$ を選んでもよい。右辺の $\forall x\,A(x)$ を偽にするには、どこかに反例があればよい。その反例は何についても仮定されていない新しい名前 $a$ で表さなければならない。これが固有変数の条件である。カットは「補題 $A$ を証明し、それを使って結論を導く」推論で、カットの論理式 $A$ は結論から消えてしまう。基本定理は、この補題を使う推論を省いても導出できるものは変わらないと主張する。
導出の例
命題変数 $p$ について、$\Rightarrow p\lor\lnot p$ は次のように導出できる。
$$
\begin{prooftree}
\AxiomC{$p\Rightarrow p$}
\RightLabel{$\lnot\mathrm R$}
\UnaryInfC{$\Rightarrow p,\lnot p$}
\RightLabel{$\lor\mathrm R$}
\UnaryInfC{$\Rightarrow p,\ p\lor\lnot p$}
\RightLabel{$\mathrm{XR}$}
\UnaryInfC{$\Rightarrow p\lor\lnot p,\ p$}
\RightLabel{$\lor\mathrm R$}
\UnaryInfC{$\Rightarrow p\lor\lnot p,\ p\lor\lnot p$}
\RightLabel{$\mathrm{CR}$}
\UnaryInfC{$\Rightarrow p\lor\lnot p$}
\end{prooftree}
$$
途中で右辺に 2 つの論理式が並び、最後に右の縮約で 1 つにまとめている。この 2 つの点が、後で見るように古典論理に特有である。
2 項関係記号 $R$ について、$\exists x\,\forall y\,R(x,y)\Rightarrow\forall y\,\exists x\,R(x,y)$ は次のように導出できる（$a,b$ は定数記号）。
$$
\begin{prooftree}
\AxiomC{$R(a,b)\Rightarrow R(a,b)$}
\RightLabel{$\forall\mathrm L$}
\UnaryInfC{$\forall y\,R(a,y)\Rightarrow R(a,b)$}
\RightLabel{$\exists\mathrm R$}
\UnaryInfC{$\forall y\,R(a,y)\Rightarrow\exists x\,R(x,b)$}
\RightLabel{$\forall\mathrm R$}
\UnaryInfC{$\forall y\,R(a,y)\Rightarrow\forall y\,\exists x\,R(x,y)$}
\RightLabel{$\exists\mathrm L$}
\UnaryInfC{$\exists x\,\forall y\,R(x,y)\Rightarrow\forall y\,\exists x\,R(x,y)$}
\end{prooftree}
$$
$\forall\mathrm R$ の固有変数 $b$ は結論 $\forall y\,R(a,y)\Rightarrow\forall y\,\exists x\,R(x,y)$ に現れず、$\exists\mathrm L$ の固有変数 $a$ も最後のシークエントに現れないので、条件は満たされている。順番を変えて $\exists\mathrm L$ を先に使おうとすると、その結論 $\exists x\,\forall y\,R(x,y)\Rightarrow R(a,b)$ に固有変数 $a$ が残って条件を破る。逆向きの $\forall y\,\exists x\,R(x,y)\Rightarrow\exists x\,\forall y\,R(x,y)$ は妥当でない（$\mathbb N$ で $R$ を $>$ と解釈すると左辺は真、右辺は偽）ので、後の thm-sc-soundness により導出できない。
健全性
$\mathbf{LK}$ で導出可能なシークエントは妥当である。命題論理の $\mathbf{LK}$ で導出可能なシークエントは、すべての付値で満たされる。
導出に関する帰納法により、始シークエントが妥当であることと、各規則について前提がすべて妥当なら結論も妥当であることを示せばよい。始シークエント $A\Rightarrow A$ は、$A$ が偽なら左辺が偽、真なら右辺が真なので妥当である。
量化記号の規則以外は、もっと強く、1 つの構造 $\mathcal M$（命題論理では 1 つの付値）について「$\mathcal M$ が前提をすべて満たすなら結論も満たす」が成り立つ。カットで確かめる。$\mathcal M$ が $\Gamma\Rightarrow\Delta,A$ と $A,\Pi\Rightarrow\Lambda$ を満たし、$\Gamma,\Pi$ がすべて真、$\Delta,\Lambda$ がすべて偽だとすると、1 つ目から $A$ は真、2 つ目から $A$ は偽になって矛盾する。よって $\mathcal M$ は $\Gamma,\Pi\Rightarrow\Delta,\Lambda$ を満たす。
ほかの命題の規則と構造規則を開く
どの規則でも、結論の文脈（$\Gamma,\Delta,\Pi,\Lambda$）のある元が「左辺で偽」か「右辺で真」なら、結論はそれだけで満たされる。そこで文脈の左辺がすべて真、右辺がすべて偽の場合を調べればよい。弱化・縮約・交換は、列に現れる文の集合を変えないか、文を付け加えるだけなので、満たされることを保つ。$\lnot\mathrm L$：前提から $A$ が真なので $\lnot A$ は偽で、結論の左辺に偽の文がある。$\lnot\mathrm R$：前提から $A$ が偽なので $\lnot A$ は真。$\land\mathrm L$：前提から $A$（または $B$）が偽なので $A\land B$ は偽。$\land\mathrm R$：前提から $A,B$ がともに真。$\lor\mathrm L$：前提から $A,B$ がともに偽なので $A\lor B$ は偽。$\lor\mathrm R$：前提から $A$（または $B$）が真。${\to}\mathrm L$：前提から $A$ は真、$B$ は偽なので $A\to B$ は偽。${\to}\mathrm R$：前提から $A$ が偽か $B$ が真なので $A\to B$ は真。
量化記号の規則を確かめる。$\forall\mathrm L$：$\mathcal M$ が前提を満たし、$\forall x\,A(x)$ と $\Gamma$ が真、$\Delta$ が偽とする。$\forall x\,A(x)$ が真なので閉項 $t$ について $A(t)$ も真であり（一階述語論理 の記事の補題「代入補題」）、前提を満たすことに反する。$\exists\mathrm R$ も同様である。
$\forall\mathrm R$：前提 $\Gamma\Rightarrow\Delta,A(a)$ が妥当で、$a$ は $\Gamma,\Delta,\forall x\,A(x)$ に現れないとする。構造 $\mathcal M$ で $\Gamma$ が真、$\Delta$ が偽だとし、$\mathcal M\models\forall x\,A(x)$ を示す。元 $m\in M$ を任意にとり、$\mathcal M$ の $a$ の解釈だけを $m$ に替えた構造を $\mathcal M'$ とする。文の真偽はその文に現れる記号の解釈だけで決まる（論理式の組み立てに沿った帰納法で分かる）ので、$\mathcal M'$ でも $\Gamma$ は真、$\Delta$ は偽である。前提は妥当なので $\mathcal M'\models A(a)$ であり、代入補題により $A(x)$ は $\mathcal M'$ で $x$ に $m$ を割り当てると真になる。$A(x)$ に $a$ は現れないので、$\mathcal M$ でも同じである。$m$ は任意なので $\mathcal M\models\forall x\,A(x)$ である。$\exists\mathrm L$ も同様である。$\square$
$\forall\mathrm R$ と $\exists\mathrm L$ だけは、1 つの構造ごとの議論では済まず、前提が すべての 構造で満たされること（妥当性）を使っている。固有変数 $a$ の解釈を自由に動かせることが、$a$ を「任意の元」の名前として使える理由であり、固有変数の条件はそのために必要である（後の反例の表の 1 行目）。この定理は Zac25 Theorem 10.28（p. 183）、Bus98 §2.3.6（p. 33）にある。
健全性から、両辺が空のシークエント $\Rightarrow$ は導出できない。どの構造も満たさないからである。
基本定理
$\mathbf{LK}$ で導出可能なシークエントは、カットなしで導出可能である。
一階の $\mathbf{LK}$ についてのこの定理は、この記事では証明しない。Gentzen の元の証明は、導出の中のカットを、カット論理式の複雑さなどに関する帰納法で上へ押し上げて消していく構文的なものである。Bus98 §2.4.2（Cut-Elimination Theorem、p. 37。証明は pp. 37–41）は、この流れの証明と、カットのない導出の大きさの上界を与えている。一方、カットのない導出だけで完全であること（妥当なシークエントはカットなしで導出できること）を直接示し、健全性と合わせて基本定理を導く方法もある（Bus98 §2.3.7、pp. 33–36、Gal15 Theorem 6.2.1 と系、pp. 249–250）。これらの文献の体系は固有変数に自由変数を使うなど細部の流儀が違うが、同じ結論が成り立つ。
命題論理では、後者の方法が 命題論理 の記事の結果からすぐに実行できる。そこで扱われているシーケント計算は、$\Gamma,\Delta$ を有限 集合 とし、共通の論理式をもつ $\Gamma\Rightarrow\Delta$ を始シーケントにした、構造規則のない体系である（同記事の定義「シーケント計算」）。以下、それを集合版とよぶ。まず、$\mathbf{LK}$ の構造規則で列を自由に整えられることを確かめる。
$\Gamma\Rightarrow\Delta$ がカットなしで導出可能で、$\Gamma$ に現れる文がすべて $\Gamma'$ に、$\Delta$ に現れる文がすべて $\Delta'$ に現れるならば、$\Gamma'\Rightarrow\Delta'$ もカットなしで導出可能である。
$\Gamma\Rightarrow\Delta$ に $\mathrm{WL}$ で $\Gamma'$ の文を、$\mathrm{WR}$ で $\Delta'$ の文を 1 つずつ付け加えると、$\Gamma'',\Gamma\Rightarrow\Delta,\Delta''$ の形（$\Gamma''$ は $\Gamma'$ の文を逆順に並べた列、$\Delta''$ は $\Delta'$ と同じ列）のシークエントが得られる。左辺の $\Gamma$ の部分の各文 $C$ は $\Gamma''$ にも現れるので、交換で 2 つの $C$ を左端に隣り合わせて $\mathrm{CL}$ で 1 つにできる。これを繰り返すと左辺は $\Gamma''$ になり、さらに交換で $\Gamma'$ の順に並べ替えられる。右辺も同様にして $\Delta'$ にできる。どの段階でもカットは使っていない。$\square$
命題論理のシークエント $\Gamma\Rightarrow\Delta$ について、次の 3 つは同値である。
- 命題論理の $\mathbf{LK}$ で導出可能である。
- 命題論理の $\mathbf{LK}$ でカットなしで導出可能である。
- すべての付値で満たされる。
2 ⇒ 1 は明らかで、1 ⇒ 3 は thm-sc-soundness である。3 ⇒ 2 を示す。$\Gamma,\Delta$ に現れる論理式の集合を $\Gamma_0,\Delta_0$ とすると、集合版のシーケント $\Gamma_0\Rightarrow\Delta_0$ はすべての付値で満たされるので、命題論理 の記事の定理「健全性と完全性」により集合版で導出できる。そこで、集合版の導出の長さに関する帰納法で、次の主張を示す。
（主張）集合版で $\Gamma_0\Rightarrow\Delta_0$ が導出できるなら、$\Gamma_0,\Delta_0$ の元を並べた（重複も許す）任意の列 $\Gamma,\Delta$ について、$\Gamma\Rightarrow\Delta$ は $\mathbf{LK}$ でカットなしで導出できる。
lem-sc-structural により、$\Gamma_0,\Delta_0$ の元を 1 回ずつ並べた列 $\Gamma_1,\Delta_1$ について $\Gamma_1\Rightarrow\Delta_1$ を導出すれば十分である。
始シーケント：$\Gamma_0,\Delta_0$ に共通の $A$ があれば、$A\Rightarrow A$ から lem-sc-structural で得られる。
$\land$ の左規則：集合版の結論が $\Gamma_0\cup\{A\land B\}\Rightarrow\Delta_0$、前提が $\Gamma_0\cup\{A,B\}\Rightarrow\Delta_0$ のとき、帰納法の仮定から $A,B,\Gamma_1\Rightarrow\Delta_1$ がカットなしで導出でき、次のように続ければよい。
$$
\begin{prooftree}
\AxiomC{$A,B,\Gamma_1\Rightarrow\Delta_1$}
\RightLabel{$\land\mathrm L$}
\UnaryInfC{$A\land B,B,\Gamma_1\Rightarrow\Delta_1$}
\RightLabel{$\mathrm{XL}$}
\UnaryInfC{$B,A\land B,\Gamma_1\Rightarrow\Delta_1$}
\RightLabel{$\land\mathrm L$}
\UnaryInfC{$A\land B,A\land B,\Gamma_1\Rightarrow\Delta_1$}
\RightLabel{$\mathrm{CL}$}
\UnaryInfC{$A\land B,\Gamma_1\Rightarrow\Delta_1$}
\end{prooftree}
$$
最後のシークエントの左辺に現れる論理式の集合は $\Gamma_0\cup\{A\land B\}$ である。
ほかの規則を開く
$\lnot$ の左右の規則、$\land$ の右規則、$\lor$ の左規則、$\to$ の右規則は、帰納法の仮定で得た列のシークエントに $\mathbf{LK}$ の同じ名前の規則をそのまま使えばよい（集合版の規則と形が同じである）。$\lor$ の右規則（集合版の前提 $\Gamma_0\Rightarrow\Delta_0\cup\{A,B\}$）は、$\Gamma_1\Rightarrow\Delta_1,A,B$ から $\lor\mathrm R$ で $\Gamma_1\Rightarrow\Delta_1,A,A\lor B$、$\mathrm{XR}$ で $\Gamma_1\Rightarrow\Delta_1,A\lor B,A$、$\lor\mathrm R$ で $\Gamma_1\Rightarrow\Delta_1,A\lor B,A\lor B$、$\mathrm{CR}$ で $\Gamma_1\Rightarrow\Delta_1,A\lor B$ とすればよい。$\to$ の左規則（集合版の前提 $\Gamma_0\Rightarrow\Delta_0\cup\{A\}$ と $\Gamma_0\cup\{B\}\Rightarrow\Delta_0$）は、$\Gamma_1\Rightarrow\Delta_1,A$ と $B,\Gamma_1\Rightarrow\Delta_1$ に ${\to}\mathrm L$ を使って $A\to B,\Gamma_1,\Gamma_1\Rightarrow\Delta_1,\Delta_1$ を得て、lem-sc-structural で重複を除けばよい。どの場合も、得られた列に現れる論理式の集合は集合版の結論の集合と一致し、カットは使っていない。$\square$
この証明は、カットを含む導出からカットのない導出を「作り変える」のではなく、妥当性を経由して作り直している。Gal15 Theorem 3.6.1 とその系（pp. 108–109）も同じ方法をとる。
部分論理式性とその帰結
文の 部分論理式 を次のように定める。$A$ 自身は $A$ の部分論理式である。$\lnot B$ の部分論理式には $B$ の部分論理式が、$B\land C$、$B\lor C$、$B\to C$ の部分論理式には $B$ と $C$ の部分論理式が含まれる。$\forall x\,B(x)$ と $\exists x\,B(x)$ の部分論理式には、すべての閉項 $t$ についての $B(t)$ の部分論理式が含まれる。
カットなしの導出に現れる文は、どれもその導出の最後のシークエントに現れるある文の部分論理式である。
カット以外の各規則について、前提に現れる文はどれも結論に現れるある文の部分論理式であることを確かめる。構造規則では、前提の文はすべて結論にも現れる（弱化は結論に文を加え、縮約と交換は現れる文の種類を変えない）。論理規則では、前提の文脈 $\Gamma,\Delta,\Pi,\Lambda$ の文は結論にも現れ、副論理式 $A,B$ は主論理式 $\lnot A$、$A\land B$、$A\lor B$、$A\to B$ の部分論理式であり、$A(t)$、$A(a)$ は $\forall x\,A(x)$、$\exists x\,A(x)$ の部分論理式である。部分論理式の部分論理式は部分論理式なので、導出の木を最後のシークエントから上へたどる帰納法により結論を得る。$\square$
カットの規則だけはこの性質をもたない。カット論理式 $A$ は前提に現れるが、結論には現れないからである。命題論理の体系についての部分論理式性は Bus98 §1.2.4（Proposition、p. 13）にあり、量化記号の規則を含む場合も上の証明のとおり成り立つ。
両辺が空のシークエント $\Rightarrow$ は $\mathbf{LK}$ で導出できない。
導出できたとすると、thm-sc-hauptsatz によりカットなしの導出がある。prop-sc-subformula により、その導出に現れる文はどれも最後のシークエント $\Rightarrow$ に現れる文の部分論理式だが、そのような文はないので、導出には文が 1 つも現れない。しかし導出の一番上は始シークエント $A\Rightarrow A$ で、文 $A$ を含む。これは矛盾である。$\square$
健全性からも同じ結論は得られるが（thm-sc-soundness の後の段落）、この証明は構造や真偽を一切使わず、導出の形だけを見ている。文の集合 $\Gamma$ が矛盾することは、$\Gamma$ のある有限部分集合の元を並べた列 $\Gamma_0$ について $\Gamma_0\Rightarrow$ が導出できることと定義でき（Zac25 Definition 10.12、p. 176）、無矛盾性 の記事の体系での定義と同じ概念になる。
直観主義の体系 LJ
論理記号 $\lnot$ の代わりに、常に偽である命題定数 $\bot$ を使い、$\lnot A$ を $A\to\bot$ の略記とする。$\mathbf{LK}$ から $\lnot$ の規則を除き、始シークエント $\bot\Rightarrow$ を加え、さらに すべてのシークエントの後件の文を高々 1 個に制限した 体系を $\mathbf{LJ}$ という。
これは Bus98 §3.1（pp. 64–65）の $\mathbf{LJ}$ と同じ考え方（$\lnot$ を $\bot$ で置き換え、後件を高々 1 個に制限する）による。同書の体系は、始シークエントを原子論理式 $A$ の $A\Rightarrow A$ に限ること、$\land\mathrm L$ が $A,B,\Gamma\Rightarrow\Delta$ から $A\land B,\Gamma\Rightarrow\Delta$ を導く 1 本の規則であること、${\to}\mathrm L$ が $\Gamma\Rightarrow A$ と $B,\Gamma\Rightarrow\Delta$ から $A\to B,\Gamma\Rightarrow\Delta$ を導き、カットが $\Gamma\Rightarrow A$ と $A,\Gamma\Rightarrow\Delta$ から $\Gamma\Rightarrow\Delta$ を導くこと（2 つの前提が前件を共有する）、固有変数に自由変数を使うことが、この記事の $\mathbf{LJ}$ と違う。しかし、一般の $A\Rightarrow A$ は原子論理式の始シークエントから $A$ の組み立てに沿ってカットなしで導出でき、規則の形の違いは弱化・縮約・交換で埋められ、自由変数と固有変数の定数記号は導出に現れない別の定数記号・自由変数に付け替えられるので、導出を互いに移せる。この移し方は新しいカットを使わないので、文だけからなるシークエントについて、導出できるもの、カットなしで導出できるものは 2 つの体系で同じである。後件が高々 1 個なので、$\mathbf{LJ}$ では右の縮約と右の交換は使い道がなく、${\to}\mathrm L$ では左の前提の後件 $\Delta$ が空になる。$\mathbf{LJ}$ の導出は、$\bot$ を常に偽と解釈すれば $\mathbf{LK}$ と同じ形の規則の組み合わせであり、$\bot\Rightarrow$ はどの構造でも満たされるので、thm-sc-soundness の証明は $\mathbf{LJ}$ にもそのまま当てはまる。後件がちょうど 1 個の文であるシークエントについて、$\mathbf{LJ}$ でも基本定理が成り立つ（Bus98 §3.1.1、p. 65。この記事では証明しない）。そこから次の性質が導出の形だけで分かる。
$\mathbf{LJ}$ で $\Rightarrow A\lor B$ が導出可能ならば、$\Rightarrow A$ と $\Rightarrow B$ の少なくとも一方が $\mathbf{LJ}$ で導出可能である。
$\mathbf{LJ}$ の基本定理により、$\Rightarrow A\lor B$ のカットなしの導出がある。その最後の規則を調べる。前件が空なので、左の規則（$\mathrm{WL}$、$\mathrm{CL}$、$\mathrm{XL}$ と論理記号の左規則）の結論にはなりえず、始シークエント（$A\Rightarrow A$ や $\bot\Rightarrow$）でもない。$\mathrm{CR}$ は前提の後件が 2 個になるので $\mathbf{LJ}$ には現れず、$\mathrm{XR}$ は結論の後件が 2 個以上なので当たらない。$\mathrm{WR}$ の結論なら前提は $\Rightarrow$ だが、これは健全性により導出できない。右の論理規則のうち結論の主論理式が $A\lor B$ になるのは $\lor\mathrm R$ だけである。したがって最後の規則は $\lor\mathrm R$ で、その前提 $\Rightarrow A$ か $\Rightarrow B$ が導出されている。$\square$
$\mathbf{LK}$ では ex-sc-excluded-middle のとおり $\Rightarrow p\lor\lnot p$ が導出できるが、$\mathbf{LJ}$ ではできない。できたとすると thm-sc-disjunction により $\Rightarrow p$ か $\Rightarrow\lnot p$ が導出でき、健全性によりそれが妥当になるが、$p$ を偽にする付値は前者を、$p$ を真にする付値は後者を満たさないからである。ex-sc-excluded-middle の導出が、右辺に 2 つの文を並べる段階を通ることが、この違いの源である。Bus98 §3.1.3（p. 66）は、選言の性質を Harrop 論理式の前提がある場合に広げた Harrop の定理を、カットのない導出についての帰納法で示せると述べている。
反例：条件を外すと成り立たない
| 外す条件 | 反例 | 成り立たなくなること |
|---|---|---|
| $\forall\mathrm R$ の固有変数の条件 | $A(a)\Rightarrow A(a)$ から $\forall\mathrm R$、$\exists\mathrm L$ で $\exists x\,A(x)\Rightarrow\forall x\,A(x)$ | 健全性 |
| カットなしの体系の右の縮約 $\mathrm{CR}$ | $\Rightarrow p\lor\lnot p$ | 妥当なシークエントをカットなしで導出できること |
| 後件に 2 個以上の文を並べてよいこと（$\mathbf{LJ}$ の制限） | $\Rightarrow p\lor\lnot p$ | 妥当なシークエントを導出できること |
| prop-sc-subformula の「カットを使わない」 | カット論理式 $q$ を使う $p\Rightarrow p$ の導出 | 部分論理式性 |
1 行目：$\forall\mathrm R$ で $A(a)\Rightarrow\forall x\,A(x)$ を得るとき、結論の左辺に固有変数 $a$ が残っているので条件を破る。条件を無視して続け、$\exists\mathrm L$（結論 $\exists x\,A(x)\Rightarrow\forall x\,A(x)$ に $a$ は現れない）を使うと、妥当でないシークエントが得られる。台集合 $\{0,1\}$ で $A(x)$ が $x=0$ のときだけ真になるように解釈すれば、左辺は真で右辺は偽である（Zac25 p. 165 も同じ例を挙げている）。
2 行目：$\mathrm{CR}$ を除いたカットなしの体系で $\Rightarrow p\lor\lnot p$ の導出があったとする。前件が空なので最後の規則は左の規則ではなく、後件が 1 個なので $\mathrm{XR}$ でもない。$\mathrm{WR}$ なら前提 $\Rightarrow$ は健全性で導出できない。残るのは $\lor\mathrm R$ で、前提は $\Rightarrow p$ か $\Rightarrow\lnot p$ だが、どちらも妥当でないので導出できない。よって導出はない。一方、$\Rightarrow p\lor\lnot p$ は妥当である。
3 行目：thm-sc-disjunction の後の段落で確かめた。
4 行目：次の導出には、結論 $p\Rightarrow p$ の部分論理式でない $q$ が現れる。
$$
\begin{prooftree}
\AxiomC{$p\Rightarrow p$}
\RightLabel{$\mathrm{WR}$}
\UnaryInfC{$p\Rightarrow p,q$}
\AxiomC{$p\Rightarrow p$}
\RightLabel{$\mathrm{WL}$}
\UnaryInfC{$q,p\Rightarrow p$}
\RightLabel{$\mathrm{Cut}$}
\BinaryInfC{$p,p\Rightarrow p,p$}
\RightLabel{$\mathrm{CL},\mathrm{CR}$}
\UnaryInfC{$p\Rightarrow p$}
\end{prooftree}
$$
補足
カットのない導出は部分論理式しか含まないので、与えられたシークエントの導出を下から上へ探すとき、試すべき規則が限られる。命題論理ではこの探索は必ず止まり、導出が見つからなければ反例の付値が得られる（命題論理 の記事の定理「健全性と完全性」の後の段落）。一階論理では $\forall\mathrm L$・$\exists\mathrm R$ の閉項 $t$ の選び方が無限にあるので探索は止まるとは限らないが、カットのない導出の形を調べることで、Craig の補間定理や Herbrand の定理が導かれる（Gal15 §6.5（pp. 275–282）と第 7 章、Bus98 §2.5（pp. 48–59））。一方、カットを除くと導出が非常に長くなることがあり、Bus98 §2.4.2 の上界は、指数関数を何重にも重ねた形になっている。
関連項目
- 前提: 命題論理, 一階述語論理, 一階論理の証明体系
- 比較: 自然演繹, Hilbert流の証明体系, 直観主義論理
- 直後に読む: カット除去定理, 無矛盾性, Herbrandの定理
- 発展: Craigの補間定理, Gentzenの無矛盾性証明, 線形論理
参考文献
Mathpediaは寄付と、参考文献の書籍リンク（Amazonアソシエイト）の紹介料で運営されています。 支援について ／ 寄付する
