シーケント計算

さまざまな演繹体系を分類する一つの方法は、体系における判断の形式、つまり、（部分）証明の結論としてどのような事柄が現れるかを調べることである。最も単純な判断形式はヒルベルト型の演繹体系で用いられ、判断は次のような形式をとる。

${\displaystyle B}$

どこ${\displaystyle B}$は、一階述語論理（または演繹体系が適用される論理体系、例えば命題論理、高階論理、様相論理など）の任意の式である。定理とは、有効な証明において結論として現れる式のことである。ヒルベルト型の体系では、式と判断を区別する必要はない。ここでは、後述の事例との比較のためにのみ区別を設けている。

ヒルベルト型の体系のシンプルな構文の代償として、完全な形式的証明は非常に長くなりがちである。このような体系における証明に関する具体的な議論は、ほぼ必ず演繹定理に依拠する。このことから、演繹定理を体系内の形式的規則として組み込むという考え方が生じ、それが自然演繹において実現されている。

自然演繹では、判断は次のような形をとる。

${\displaystyle A_{1},A_{2},\ldots ,A_{n}\vdash B}$

どこで${\displaystyle A_{i}}$'s と${\displaystyle B}$再び数式と${\displaystyle n\geq 0}$言い換えれば、判決は回転式改札機のシンボルの左側にある（空である可能性もある）数式のリストで構成される。${\displaystyle \vdash }$「、右辺に単一の式があり、^{[ 8 ] [ 9 ] [ 10 ]} (ただし、${\displaystyle A_{i}}$はしばしば重要ではない）。定理は、${\displaystyle B}$そのため${\displaystyle \vdash B}$（左側が空の場合）は有効な証明の結論です。（自然演繹のいくつかの表現では、${\displaystyle A_{i}}$sと回転式改札機は明示的に記述されず、代わりにそれらを推測できる二次元表記が用いられる。

自然演繹における判断の標準的な意味論は、^{[ 11 ]が成り立つとき、判断が成り立つと主張することである。}${\displaystyle A_{1}}$、${\displaystyle A_{2}}$などはすべて真実です。${\displaystyle B}$判決もまた真実となるだろう。

${\displaystyle A_{1},\ldots ,A_{n}\vdash B}$

そして

${\displaystyle \vdash (A_{1}\land \cdots \land A_{n})\rightarrow B}$

両者は、一方の証明を他方の証明に拡張できるという強い意味で同等である。

最後に、シーケント計算は自然演繹判断の形式を一般化して

${\displaystyle A_{1},\ldots ,A_{n}\vdash B_{1},\ldots ,B_{k},}$

構文オブジェクトはシーケントと呼ばれます。ターンスタイルの左側の式は前件と呼ばれ、右側の式は後件または後件と呼ばれます。これらをまとめて前件またはシーケント式と呼びます。^{[ 12 ]}再び、${\displaystyle A_{i}}$そして${\displaystyle B_{i}}$は数式であり、${\displaystyle n}$そして${\displaystyle k}$は非負整数であり、つまり、左辺または右辺（あるいはどちらも空でなくても、両方でも可）が空であってもよい。自然演繹と同様に、定理は${\displaystyle B}$どこ${\displaystyle \vdash B}$これは有効な証明の結論である。

シーケントの標準的な意味論は、すべての${\displaystyle A_{i}}$少なくとも1つは本当です${\displaystyle B_{i}}$も真になります。^{[ 13 ]}したがって、両方の先行詞が空である空のシーケントは偽です。^{[ 14 ]}これを表現する1つの方法は、ターンスタイルの左側のコンマは「and」と考え、ターンスタイルの右側のコンマは（包括的な）「or」と考えることです。シーケント

${\displaystyle A_{1},\ldots ,A_{n}\vdash B_{1},\ldots ,B_{k}}$

そして

${\displaystyle \vdash (A_{1}\land \cdots \land A_{n})\rightarrow (B_{1}\lor \cdots \lor B_{k})}$

両者は、一方のシーケントの証明を他方のシーケントの証明に拡張できるという強い意味で同等である。

一見すると、この判断形式の拡張は奇妙な複雑さのように見えるかもしれない。それは自然演繹の明らかな欠陥によって動機づけられたものではなく、コンマが改行の両側で全く異なる意味を持つように見えることは、最初は混乱を招く。しかし、古典的な文脈では、シーケントの意味論は（命題的トートロジーによって）次のように表現することもできる。

${\displaystyle \vdash \neg A_{1}\lor \neg A_{2}\lor \cdots \lor \neg A_{n}\lor B_{1}\lor B_{2}\lor \cdots \lor B_{k}}$

（Aのうち少なくとも1つは偽、またはBのうち少なくとも1つは真である）

または

${\displaystyle \vdash \neg (A_{1}\land A_{2}\land \cdots \land A_{n}\land \neg B_{1}\land \neg B_{2}\land \cdots \land \neg B_{k})}$

（すべてのAが真であり、すべてのBが偽であるということはあり得ない。）

これらの定式化では、回転式ゲートの両側の式の唯一の違いは、片側が否定されていることです。したがって、シーケントで左と右を入れ替えることは、構成要素となるすべての式を否定することに対応します。これは、意味論レベルで論理否定として現れるド・モルガンの法則のような対称性が、シーケントの左右対称性に直接変換されることを意味します。実際、シーケント計算における論理積（∧）を扱う推論規則は、論理和（∨）を扱う推論規則の鏡像です。

多くの論理学者は、この対称的な表現は、否定の古典的な双対性が規則にそれほど明確ではない他のスタイルの証明システムよりも、論理の構造についてより深い洞察を提供すると考えている。^{[ 15 ] [ 16 ]}

ゲンツェンは、自身の単一出力自然演繹システム（NKとNJ）と、自身の複数出力シーケント計算システム（LKとLJ）との間に明確な区別があると主張した。彼は、直観主義自然演繹システムNJはやや醜いと書いた。^{[ 17 ]}彼は、古典的自然演繹システムNKにおける排中律の特別な役割は、古典的シーケント計算システムLKでは取り除かれていると述べた。^{[ 18 ]}彼は、直観主義論理の場合も古典論理の場合も（LK対NK）、シーケント計算LJは自然演繹NJよりも対称性が高いと述べた。^{[ 19 ]}そして彼は、これらの理由に加えて、複数の後続式を持つシーケント計算は、特に彼の主定理（「Hauptsatz」）のために意図されていると述べた。^{[ 20 ]}

「sequent」という単語は、ゲンツェンの1934年の論文にある「Sequenz」という単語から取られています。^{[ 1 ]}クリーネは英語への翻訳について次のようにコメントしています。「ゲンツェンは『Sequenz』と言っていますが、私たちはそれを『sequent』と訳しています。なぜなら、私たちはすでに『sequence』をあらゆる物の連続に対して使用しており、ドイツ語では『Folge』だからです。」^{[ 21 ]}

ゲンツェンは、さまざまな証明体系を表すために2文字の大文字を使用した。1935年の論文で、彼はLKにおいて、Lは「logische」（論理的）を、Kは「klassische Pradikatenlogik」（古典述語論理）を表すと述べている。LJのJは「 intuitionistische Pradikatenlogik」（直観主義述語論理）を表す。^{[ 1 ] : 177}同様に、NKとNJのNは「natürlichen Schließens」（自然演繹）を表す。彼がどのようにして「intuitionistische」を表すのにJを使用するようになったのかは不明だが、おそらく数字の1とローマ数字のIと区別するために活字上区別するためであろう。他の箇所では、ゲンツェンはLJとNJの代わりにLIとNIを使用している。^{[ 22 ] : 83}

シーケント計算は、解析タブロー法と同様に、命題論理における論理式の証明のためのツールと見なすことができる。これは、論理式の証明問題を、より単純な式に還元していき、最終的に自明な式にたどり着く一連の手順を提供する。^{[ 23 ]}

次の式を考えてみましょう。

${\displaystyle ((p\rightarrow r)\lor (q\rightarrow r))\rightarrow ((p\land q)\rightarrow r)}$

これは次の形式で記述されており、証明すべき命題は回転式改札機のシンボルの右側に示されています。${\displaystyle \vdash }$:

${\displaystyle \vdash ((p\rightarrow r)\lor (q\rightarrow r))\rightarrow ((p\land q)\rightarrow r)}$

さて、これを公理から証明する代わりに、含意の前提を仮定して、その結論を証明しようと試みれば十分である。^{[ 24 ]}したがって、次のシーケントに進む。

${\displaystyle (p\rightarrow r)\lor (q\rightarrow r)\vdash (p\land q)\rightarrow r}$

ここでも右辺には含意が含まれており、その前提はさらに仮定できるため、結論のみを証明すればよい。

${\displaystyle (p\rightarrow r)\lor (q\rightarrow r),(p\land q)\vdash r}$

左辺の引数は論理積によって関連付けられていると仮定すると、これは次のように置き換えることができます。

${\displaystyle (p\rightarrow r)\lor (q\rightarrow r),p,q\vdash r}$

これは、左側の最初の引数に対する選言の結論を両方のケースで証明することと同等です。したがって、シーケントを2つに分割することができ、それぞれを個別に証明する必要があります。

${\displaystyle p\rightarrow r,p,q\vdash r}$

${\displaystyle q\rightarrow r,p,q\vdash r}$

最初の判決の場合、我々は書き直す${\displaystyle p\rightarrow r}$として${\displaystyle \lnot p\lor r}$そして、シーケントを再度分割して、次の結果を得ます。

${\displaystyle \lnot p,p,q\vdash r}$

${\displaystyle r,p,q\vdash r}$

2番目のシーケントは完了しました。最初のシーケントはさらに次のように簡略化できます。

${\displaystyle p,q\vdash p,r}$

このプロセスは、各辺に原子式だけが含まれるようになるまで常に続けることができます。このプロセスは、右図のように、根付き木でグラフィカルに表現できます。木の根は証明したい式であり、葉は原子式のみで構成されています。この木は還元木として知られています。^{[ 23 ] [ 25 ]}

回転式改札機の左側の項目は論理積で結び付けられ、右側の項目は論理和で結び付けられていると理解される。したがって、両方が原子記号のみで構成されている場合、右側の記号のうち少なくとも1つが左側にも現れる場合に限り、シーケントは公理的に受け入れられる（そして常に真となる）。

ツリーに沿って進む際のルールは以下のとおりです。1 つのシーケントが 2 つに分割されると、ツリーの頂点には 2 つの子頂点が生まれ、ツリーは分岐します。さらに、各側の引数の順序を自由に変更できます。ΓとΔ は、追加可能な引数を表します。^{[ 23 ]}

自然演繹のためのゲンツェン式レイアウトで使用される水平線の一般的な用語は推論線である。^{[ 26 ]}

命題論理の任意の式から始めて、一連の手順を経て、回転式の右側が原子記号のみを含むまで処理されます。次に、左側についても同じことが行われます。すべての論理演算子は上記の規則のいずれかに現れ、規則によって削除されるため、論理演算子が残らなくなった時点で処理は終了します。つまり、式は分解されました。

したがって、木の葉にあるシーケントには原子記号のみが含まれており、右側の記号のいずれかが左側にも現れるかどうかに応じて、公理によって証明可能か否かが決まります。

ツリー内の各ステップは、それらが暗示する論理式の真偽値を保持し、分岐があるたびにツリーの異なるブランチ間で論理積が暗黙的に成立することが容易にわかる。また、公理が証明可能であるのは、原子記号へのすべての真偽値の割り当てに対して公理が真である場合に限ることも明らかである。したがって、この体系は古典命題論理に対して健全かつ完全である。

シーケント計算は、フレーゲの命題計算やヤン・ルカシェヴィチの公理化（それ自体が標準ヒルベルト体系の一部）など、古典的な命題計算の他の公理化と関連しています。これらの体系で証明できるすべての論理式には還元木があります。これは次のように示すことができます。命題計算のすべての証明は、公理と推論規則のみを使用します。公理体系の各使用は真の論理式を生成し、したがってシーケント計算で証明できます。これらの例を以下に示します。上記の体系で唯一の推論規則は、カット規則によって実装されるモーダス・ポネンスです。

以下の表記法を使用します。

• ${\displaystyle \vdash }$回転式改札口として知られるこの装置は、左側の前提と右側の命題を分離する。
• ${\displaystyle A}$そして${\displaystyle B}$一階述語論理の式を表す（命題論理に限定することもできる）。
• ${\displaystyle \Gamma ,\Delta ,\Sigma }$、 そして${\displaystyle \Pi }$は、 有限（空の場合もあり得る）の数式の列（実際には、数式の順序は関係ありません。§構造規則を参照）であり、コンテキストと呼ばれます。
  • 左側にあるとき${\displaystyle \vdash }$一連の式は連言的に考慮される（すべて同時に成り立つと仮定される）。
  • 右側では${\displaystyle \vdash }$式列は選言的に考慮される（変数の任意の割り当てに対して、少なくとも1つの式が成り立つ必要がある）。
• ${\displaystyle t}$は任意の項を表し、
• ${\displaystyle x}$そして${\displaystyle y}$変数を表す。
• 式の中で変数が自由変数であるとは、その変数が量化子によって束縛されていない場合をいう。${\displaystyle \forall }$または${\displaystyle \exists }$。
• ${\displaystyle A[t/x]}$は、項を代入して得られる式を表します。${\displaystyle t}$変数の自由出現ごとに${\displaystyle x}$式の中で${\displaystyle A}$用語の制限付き${\displaystyle t}$変数は自由でなければならない${\displaystyle x}$で${\displaystyle A}$（つまり、変数の出現がない）${\displaystyle t}$束縛される${\displaystyle A[t/x]}$)
• ${\displaystyle WL}$、${\displaystyle WR}$、${\displaystyle CL}$、${\displaystyle CR}$、${\displaystyle PL}$、${\displaystyle PR}$: これら 6 は、3 つの構造規則のそれぞれ 2 つのバージョンを表しています。1 つは左側 (「L」) で使用するものです。${\displaystyle \vdash }$、そしてその右側のもう一方（「R」）。ルールは、弱化（左/右）の場合は「W」、収縮の場合は「C」、順列の場合は「P」と略記される。

なお、上記で示した還元ツリーに沿って進むための規則とは異なり、以下の規則は公理から定理へと逆方向に進むためのものです。したがって、これらは上記の規則と完全に鏡像の関係にありますが、ここでは暗黙のうちに対称性が仮定されておらず、量化に関する規則が追加されています。

以下の表では、${\displaystyle A\setminus B}$の相対補数を表す${\displaystyle B}$で${\displaystyle A}$。

制限事項：(†)でマークされたルールでは、${\displaystyle ({\forall }R)}$そして${\displaystyle ({\exists }L)}$変数${\displaystyle y}$それぞれの下位シーケント内のどこにも、自由に出現してはならない。

上記のルールは、論理ルールと構造ルールの2つの主要なグループに分けられます。論理ルールはそれぞれ、回転式改札機の左側または右側に新しい論理式を導入します。${\displaystyle \vdash }$対照的に、構造規則はシーケントの構造に作用し、式の正確な形状は無視します。この一般的なスキームの2つの例外は、恒等公理（I）と（カット）規則です。

上記の規則は形式的に述べられているものの、古典論理の観点から非常に直感的に理解できる。例えば、次の規則を考えてみよう。${\displaystyle ({\land }L_{1})}$。それは、証明できるときはいつでも${\displaystyle \Delta }$を含む一連の式から結論付けることができる${\displaystyle A}$そうすれば、次のように結論づけることもできる。${\displaystyle \Delta }$（より強い）仮定から${\displaystyle A\land B}$成り立つ。同様に、ルールは${\displaystyle ({\neg }R)}$もし${\displaystyle \Gamma }$そして${\displaystyle A}$結論として十分である${\displaystyle \Delta }$それから${\displaystyle \Gamma }$一人ではまだ結論を出すことができる${\displaystyle \Delta }$あるいはそれ${\displaystyle A}$偽でなければならない、つまり${\displaystyle {\neg }A}$成立する。すべての規則はこのように解釈できる。

量化子規則についての直感的な理解のために、次の規則を考えてみましょう。${\displaystyle ({\forall }R)}$もちろん、${\displaystyle \forall {x}A}$事実から${\displaystyle A[y/x]}$が真であることは、一般には不可能である。ただし、変数yが他の場所で言及されていない場合（つまり、他の式に影響を与えることなく自由に選択できる場合）、次のことが成り立つと仮定できる。${\displaystyle A[y/x]}$これはyの任意の値に対して成り立つ。他のルールは、その後は非常に分かりやすいはずだ。

規則を述語論理における合法的な導出の説明とみなす代わりに、与えられた命題の証明を構築するための指示とみなすこともできる。この場合、規則は下から上に読むことができる。例えば、${\displaystyle ({\land }R)}$それは、${\displaystyle A\land B}$仮定から導かれる${\displaystyle \Gamma }$そして${\displaystyle \Sigma }$証明すれば十分である${\displaystyle A}$から結論付けられる${\displaystyle \Gamma }$そして${\displaystyle B}$から結論付けられる${\displaystyle \Sigma }$それぞれ。ただし、何らかの前件が与えられた場合、これをどのように分割するかは明らかではないことに注意してください。${\displaystyle \Gamma }$そして${\displaystyle \Sigma }$しかし、仮定による前件が有限であるため、検証できる可能性は有限個しかありません。これはまた、証明論が証明に対して組み合わせ論的な方法で作用していると考えることができることを示しています。${\displaystyle A}$そして${\displaystyle B}$証明を構築することができる${\displaystyle A\land B}$。

証明を探すとき、ほとんどのルールは、その方法を多かれ少なかれ直接的に示しています。カットのルールは異なります。それは、数式が${\displaystyle A}$結論を導き出すことができ、この式は他の命題を結論付けるための前提としても機能する可能性がある。${\displaystyle A}$「切り離す」ことができ、それぞれの導出が結合されます。ボトムアップで証明を構築する場合、これは推測の問題を生み出します。${\displaystyle A}$（以下には全く現れないため）。したがって、カット除去定理は、自動演繹におけるシーケント計算の応用にとって極めて重要である。この定理は、証明からカット規則のすべての使用を排除できることを示しており、証明可能なシーケントにはカットフリーの証明を与えることができることを意味する。

やや特殊な2つ目の規則は、同一性の公理（I）です。直感的に理解すれば、すべての論理式はそれ自身を証明できることがわかります。カット規則と同様に、同一性の公理もやや冗長です。原子的な初期シーケントの完全性から、この規則は証明可能性を損なうことなく原子的な論理式に限定できることがわかります。

非標準的な接続詞 \ を無視すれば、含意に関するものを除いて、すべての規則に鏡像関係が存在することに注目してください。これは、一階述語論理の通常の言語には「含意されない」という接続詞が含まれていないことを反映しています。${\displaystyle \not \leftarrow }$それは含意のド・モルガン双対となる。このような結合子とその自然な規則を加えることで、微積分は完全に左右対称になる。

ここに「${\displaystyle \vdash A\lor \lnot A}$これは排中律（ラテン語でtertium non datur）として知られています。

次に、量化子に関する単純な事実の証明を示します。逆は真ではないことに注意してください。また、既存の自由変数を規則の代入に使用できないため、ボトムアップで導出しようとすると、その偽りがわかります。${\displaystyle (\forall R)}$そして${\displaystyle (\exists L)}$。

さらに興味深いことを証明します${\displaystyle {\left(\left(A\rightarrow \left(B\lor C\right)\right)\rightarrow \left(\left(\left(B\rightarrow \lnot A\right)\land \lnot C\right)\rightarrow \lnot A\right)\right)}}$導出過程を見つけるのは簡単であり、これは自動証明におけるLKの有用性を示す好例である。

これらの導出は、シーケント計算の厳密な形式的構造も強調している。例えば、上述の論理規則は常にターンスタイルに隣接する式に作用するため、置換規則が必要となる。ただし、これはゲンツェンの原文のスタイルによる表現上のアーティファクトでもあることに注意が必要である。一般的な簡略化としては、シーケントの解釈において、数列ではなく式の多重集合を用いることで、明示的な置換規則を不要にする方法がある。これは、仮定と導出の可換性をシーケント計算の外部に移すことに相当するが、LKではそれをシステム自体に組み込んでいる。

シーケント計算の特定の形式（つまり変種）では、そのような計算における証明は、上下逆の閉じた解析タブローと同型である。^{[ 28 ]}

構造上の規則については、さらに議論の余地がある。

弱化（W）は、任意の要素を数列に追加することを可能にします。直感的に言えば、これは前件部では常に証明の範囲を限定できるため（すべての車に車輪が付いている場合、すべての黒い車に車輪が付いていると断言しても差し支えない）、また後件部では常に別の結論を許容できるため（すべての車に車輪が付いている場合、すべての車に車輪か翼のどちらかが付いていると断言しても差し支えない）に許容されます。

縮約 (C) と順列 (P) により、シーケンスの要素の順序 (P) も出現の多重度 (C) も関係ないことが保証されます。したがって、シーケンスの代わりに集合を考えることもできます。

しかし、シーケンスを用いるという余分な労力は、構造規則の一部または全部を省略できるため正当化される。そうすることで、いわゆる部分構造論理が得られる。

この規則体系は、一階述語論理、すなわち命題に関して健全かつ完全であることが示せる。${\displaystyle A}$意味的に一連の前提から導かれる${\displaystyle \Gamma }$${\displaystyle (\Gamma \vDash A)}$後続の${\displaystyle \Gamma \vdash A}$上記の規則から導き出すことができる。^{[ 29 ]}

シーケント計算では、カットルールは許容される。この結果は、ゲンツェンの主定理（「主定理」）とも呼ばれる。 ^{[ 2 ] [ 3 ]}

システムが導出するシーケントを変更することなく、シーケントと構造規則をどのように形式化するかという技術的な詳細については、ある程度の選択の自由度がある。

まず、前述のように、シーケントは集合または多重集合から構成されると考えることができます。この場合、順列の規則や（集合を使用する場合の）縮約式は不要です。

弱化規則は、公理（I）が次の形式の任意のシーケントを導出するように変更された場合に許容される。${\displaystyle \Gamma ,A\vdash A,\Delta }$導出過程に現れる弱化は、証明の冒頭に移動させることができる。これは、ボトムアップ方式で証明を構築する際に便利な変更となる場合がある。

複数の前提を持つルールが、それぞれの前提に対して同じコンテキストを共有するか、あるいはそれらのコンテキストを分割するかを変更することもできます。たとえば、${\displaystyle ({\lor }L)}$代わりに次のように定式化できる

${\displaystyle {\cfrac {\Gamma ,A\vdash \Delta \qquad \Sigma ,B\vdash \Pi }{\Gamma ,\Sigma ,A\lor B\vdash \Delta ,\Pi }}.}$

縮約と弱化により、このバージョンの規則は上記のバージョンと相互に導出可能になりますが、線形論理のようにこれらがない場合、これらの規則は異なる結合子を定義します。

紹介することができます${\displaystyle \bot }$偽を表す不条理定数、公理：

${\displaystyle {\cfrac {}{\bot \vdash \quad }}}$

あるいは、上記のように弱化が許容される規則であるならば、次の公理が成り立つ。

${\displaystyle {\cfrac {}{\Gamma ,\bot \vdash \Delta }}}$

と${\displaystyle \bot }$否定は、定義により含意の特殊なケースとして包含される。${\displaystyle (\neg A)\iff (A\to \bot )}$。

あるいは、構造規則の一部の使用を制限または禁止することもできる。これにより、さまざまな部分構造論理システムが得られる。これらは一般的にLKよりも弱く（つまり、定理の数が少ない）、したがって一階述語論理の標準的な意味論に関しては完全ではない。しかし、理論計算機科学や人工知能への応用につながる、その他の興味深い特性を持っている。

驚くべきことに、LK の規則に少し変更を加えるだけで、直観主義論理の証明システムに変えることができる。^{[ 30 ]}この目的のために、右辺に最大 1 つの式を持つシーケントに制限し、^{[ 31 ]}この不変条件を維持するように規則を修正する必要がある。例えば、${\displaystyle ({\lor }L)}$以下のように再定式化される（Cは任意の式である）。

${\displaystyle {\cfrac {\Gamma ,A\vdash C\qquad \Gamma ,B\vdash C}{\Gamma ,A\lor B\vdash C}}\quad ({\lor }L)}$

結果として得られる体系はLJと呼ばれる。直観主義論理に関して健全かつ完全であり、同様のカット除去証明が可能である。これは、選言性質や存在性質の証明に利用できる。

実際、LKにおいて単一式の帰結に限定する必要がある規則は、${\displaystyle ({\to }R)}$、${\displaystyle (\neg R)}$（これは、${\displaystyle {\to }R}$（上記のとおり）${\displaystyle ({\forall }R)}$多重論理式の帰結が選言として解釈される場合、LK の他のすべての推論規則は LJ で導出可能であり、規則は${\displaystyle ({\to }R)}$そして${\displaystyle ({\forall }R)}$なる

${\displaystyle {\cfrac {\Gamma ,A\vdash B\lor C}{\Gamma \vdash (A\to B)\lor C}}}$

そして（${\displaystyle y}$（下部の次の行では自由に発生しない）

${\displaystyle {\cfrac {\Gamma \vdash A[y/x]\lor C}{\Gamma \vdash (\forall xA)\lor C}}.}$

これら二つの規則は、直観的に妥当ではない。