シーケント計算に対応する計算体系を考えてみる

「直観主義論理のカリー・ハワード対応」(と続く文章)に書いたように、自然演繹とラムダ計算との間に対応関係があった。一方、「直観主義論理の「自然さ」(2)」「(3)」にあるように、自然演繹とシーケント計算はおおむね対応していた。
ということは、シーケント計算に対応するような計算体系も作ることができそうに思える。実際、調べてみるとそういう体系としてPhilip Wadlerのdual calculusがあった。

しかし、dual calculusは何か面倒に見えて(term、coterm,statementの区別があったりして面倒。ちゃんと理解していない)どうも好みではないので、別の体系を作ってみる。

カット

シーケント計算では、カット規則によって論理式が消える。
$\frac{\large{\cdots \Rightarrow A \qquad A, \cdots \Rightarrow B}}{\large{\cdots \Rightarrow B}}$
でも計算体系の場合、カットによって項が消えてしまうと都合が悪いので、カットを適用した項を $\bullet$ で繋げて残しておく。これが何を意味するのかは、あとから考える。

$\frac{\large{\cdots \Rightarrow s \; :A \qquad t \; :A, \, \cdots \Rightarrow u \, : B}}{\large{\cdots \Rightarrow s \bullet t, \qquad u\, :B \cdots}}$

論理積、直積型

シーケント計算の∧右規則と自然演繹の∧導入規則はそのまま対応していたので、新しい計算体系でもラムダ計算の規則をそのまま流用する。

$\frac{\large{\cdots \Rightarrow s \quad : A \qquad \cdots \Rightarrow t \quad : B}}{\large{\cdots \Rightarrow (s,t) \quad : A \wedge B}}$

問題は、∧左規則。
$\frac{\large{\cdots, \: s \, :A \Rightarrow \cdots}}{\large{\cdots, \: ? \, :A \wedge B \Rightarrow \cdots}} \qquad \qquad \frac{\large{\cdots, \: t \, :B \Rightarrow \cdots}}{\large{\cdots, \: ? \, :A \wedge B \Rightarrow \cdots}}$
この?の部分をうまく決める必要があるのだけど、これは次のようにする。

$\frac{\large{\cdots, \: s \, :A \Rightarrow \cdots}}{\large{\cdots, \: (s, -) \, :A \wedge B \Rightarrow \cdots}}\qquad \qquad \frac{\large{\cdots, \: t \, :B \Rightarrow \cdots}}{\large{\cdots, \: (-, t) \, :A \wedge B \Rightarrow \cdots}}$

ここの(s,-)と(-,t)が何を表しているかを考える。ラムダ計算で次のように項を作ったとする。
$\frac{\frac{\large{s \, : A \qquad t \, : B}}{\large{(s,t) \, : A \wedge B}}}{\large{{\rm fst}\, (s,t) \, : A}}$
簡約すると計算結果はsになる。
これをシーケント計算に移すと次のようになる。
$\frac{\frac{\large{ \Rightarrow s \, :A \qquad \Rightarrow t \, :B}}{\large{\Rightarrow (s,t) \, : A \wedge B}} \qquad \frac{\large{x \, :A \Rightarrow x \, :A}}{\large{(x,-) \, :A \wedge B \Rightarrow x \, :A}}}{\large{\Rightarrow (s,t)\bullet (x,-) \qquad x \, :A}}$
さらに、カットの位置を移動して簡約してやると、
$\frac{\large{ \Rightarrow s \, :A \qquad x \, :A \Rightarrow x \, :A}}{\large{\Rightarrow s \bullet x \qquad x \, : A }}$
となる。
この証明図とラムダ計算の結果と比較すると、 $\bullet$ は左辺と右辺とをパターンマッチ(とかユニフィケーション)のようなことをしていると考えられる。(s,t)と(x,-)をパターンマッチさせるとs=xとなり、この値がこの場合の最終結果となっている。

含意、関数

自然演繹／ラムダ計算では、→の導入が関数抽象に対応していた。シーケント計算でも同じように考えられるのだけど、λの引数が変数とは限らないところが違う。

$\frac{\large{s \, : A \Rightarrow t \, : B}}{\large{\Rightarrow \lambda s . t \, : A \to B}}$

ラムダ計算におけるλx.(fst x)を、シーケント計算に移すと
$\frac{\frac{\large{y \, : A \Rightarrow y \, : A}}{\large{(y,-) \, : A \wedge B \Rightarrow y \, : A}}}{\large{\Rightarrow \lambda (y,-).y \, : A \wedge B \to A}}$
となり、λの引数に変数以外のものが来ている。ただしカットをかまして次のようにすることもできる。

$\frac{\frac{{{\large{x \, :A \Rightarrow x \, :A}}} \qquad \frac{\large{y \, : A \Rightarrow y \, : A}}{\large{(y,-) \, : A \wedge B \Rightarrow y \, : A}}}{\large{x \, :A \Rightarrow x \bullet (y,-) \qquad y \, :A}}}{{\large{ \Rightarrow x \bullet (y,-) \qquad \lambda x .y \, :A}}}$

それから左辺が変数とは限らないために困ることがある。次のような証明図があるとする。
$\frac{\frac{\frac{\large{[x \, : A \wedge B ]{}_{\small{1}}}}{\large{{\rm snd}\, x \, :B}} \qquad \frac{\large{ [ x \, : A \wedge B ]{}_{\small{1}}}}{\large{{\rm fst}\, x \, :A}}}{\large{ ({\rm snd}\, x , {\rm fst} \, x) \, : B \wedge A }}}{\large{\lambda x . ({\rm snd}\, x , {\rm fst} \, x) \, : A \wedge B \to B \wedge A}}{\small{1}}$
これをシーケント計算に移すと、途中までは次のようになる。

$\frac{\frac{\large{z \, :B \Rightarrow z \, :B}}{\large{(-,z) \, : A \wedge B \Rightarrow z \, : B}} \qquad \frac{\large{ y \, : A \Rightarrow y \, : A}}{\large{(y,-) \, : A \wedge B \Rightarrow y \, : A}}}{\large{(y,-) \, : A \wedge B, \quad (-, z) \, : A \wedge B \Rightarrow (z,y) \, : B \wedge A}}$
このあと関数抽象をしたいのだけど、(y,-)と(-,z)の両方を一度に右辺に移動させる必要がある(そうしないと左辺に仮定が残ってしまう)。ひとつのやり方は、上でやったのと同じようにカットをかまして左辺を同一の変数にしてから関数抽象をするというもの。
$\large{\Rightarrow x \bullet (y,-) , \, x \bullet (-,z), \quad \lambda x . (z,y) \, : B \wedge A}$

別のやりかたは、同じ型の項は一つにまとめてもよいという規則を追加すること(シーケント計算のcontraction規則)。こちらのやり方だと上の証明の続きはこうなる。
$\frac{\frac{\large{(y,-) \, : A \wedge B, \quad (-, z) \, : A \wedge B \Rightarrow (z,y) \, : B \wedge A}}{\large{ \{(y,-), \,(-, z) \} \, : A \wedge B \Rightarrow (z,y) \, : B \wedge A}}}{\large{\Rightarrow \lambda \{(y,-), \,(-, z) \}. (z,y) \, : A \wedge B \to B \wedge A}}$
A∧B型の引数を受け取って、それを(y,-)と(-,z)のそれぞれとパターンマッチをおこなって(z,y)を作る。
一方、→左規則は次のようにする。

$\frac{\large{ \cdots \Rightarrow s \, : A \qquad t \, : B , \cdots \Rightarrow \cdots }}{\large{\cdots, \, s @ t \, :A \to B \Rightarrow \cdots }}$

s@tが何を表しているかを見るために、(λx.s)tに対応する証明をシーケント計算でおこなってみる。
$\frac{\frac{\large{x \, : A \Rightarrow s \, : B}}{\large{\Rightarrow \lambda x . s \, : A \to B}} \qquad \frac{\large{\Rightarrow t \, : A \qquad y \, : B \Rightarrow y \, : B}}{\large{t @ y \, : A \to B \Rightarrow y \, : B}}}{\large{\Rightarrow \lambda x . s \bullet t @ y \qquad y \, : B}}$
この証明図は、カットを移動させて次のように書き換えられる。
$\frac{\frac{\large{\Rightarrow t \, : A \qquad x \, : A \Rightarrow s \, : B}}{\large{ \Rightarrow t \bullet x \qquad s \, : B}}\qquad {\large{y \, : B \Rightarrow y \, : B}}}{\large{\Rightarrow t \bullet x \quad s \bullet y \qquad y \, : B}}$
xにtが代入される。その結果はsにも反映され(つまりs[x←t]となる)、それがyに代入される。
このことから、「f $\bullet$ t@y」は、関数適用(f t)の結果とyとのパターンマッチを表していると考えることができる。

論理和、直和型

∨右規則は、自然演繹／ラムダ計算のものをそのまま流用すればよい。

$\frac{\large{\cdots \Rightarrow s \, : A}}{\large{\cdots \Rightarrow {\rm Left}\, s \, : A \vee B}} \qquad \qquad \frac{\large{\cdots \Rightarrow t \, : B}}{\large{\cdots \Rightarrow {\rm Right}\, t \, : A \vee B}}$

ただし∨左規則との対応を考慮して、次のようにも書くことにする。

$\frac{\large{\cdots \Rightarrow s \, : A}}{\large{\cdots \Rightarrow [s,-] \, : A \vee B}} \qquad \qquad \frac{\large{\cdots \Rightarrow t \, : B}}{\large{\cdots \Rightarrow [-,t] \, : A \vee B}}$

一方、∨左規則は次のようにする。シーケントの右辺は型だけでなく項自体が同じでないといけない。

$\frac{\large{\cdots , \, s \, : A \Rightarrow u \, : C \qquad \cdots , \, t \, : B \Rightarrow u \, : C}}{\large{ [s,t] \, : A \vee B \Rightarrow u \, :C}}$

右辺の項が違っていて∨左規則を使いたい場合は、カットを使って同一の項にする。
$\frac{\frac{\large{\cdots , \, s \, : A \Rightarrow p \, : C \qquad y \, : C \Rightarrow y \, : C}}{\large{\cdots , \, s \, : A \Rightarrow p \bullet y \quad y \, :C}} \qquad \frac{\large{\cdots , \, t \, : B \Rightarrow q \, : C \qquad y \, : C \Rightarrow y \, : C}}{\large{\cdots , \, t \, : B \Rightarrow q \bullet y \quad y \, :C}}}{\large{\cdots , \, [s,t] \, : A \vee B \Rightarrow p \bullet y , \, q \bullet y \quad y \, :C}}$

古典論理への拡張

ここまでの説明で、直観主義論理の範囲での計算体系はほとんど完成している(直観主義論理の範囲では、矛盾や否定に対応する計算はほとんど意味がないから)。そこで古典論理に対応するように拡張することを考える。そうすると、矛盾をどう扱うかが問題になる。
シーケント計算の体系では自然演繹とは違い矛盾記号 $\bot$ が出てこない。これは単に矛盾記号が省略されているだけと考えることも一応できる。そう考えた場合は、矛盾に関する規則は自然演繹の場合と同じでよい。また¬Aは、A→ $\bot$ の略と考えればよい。

$\frac{\large{\cdots \Rightarrow s \, : A}}{\large{\cdots \Rightarrow [\alpha]s \, : \bot \quad \alpha \, : A}}$

$\frac{\large{\cdots \Rightarrow t \, : A \qquad \alpha \, : A}}{\large{\cdots \Rightarrow \mu \, \alpha. t \, :A}}$

これでもよいのだけど、 $\bot$ を使わないような規則を考えてみる。
まず最初の規則を

$\frac{\large{\cdots \Rightarrow s \, : A}}{\large{\cdots \Rightarrow [\alpha]s \, : C \quad \alpha \, : A}}$

と書き換える(Cは任意の型)。これは $\bot$ からは何でも導けるという規則をあらかじめ組み込んだ形にしただけ。次に項を入れ替える。

$\frac{\large{\cdots \Rightarrow s \, : A}}{\large{\cdots \Rightarrow \alpha \, : C \quad [\alpha]s \, : A}}$
このように書き換えると、元は
$\frac{\frac{\large{\cdots \Rightarrow s \, : A}}{\large{\begin{array}{c}\cdots \Rightarrow [\alpha]s \, : C \quad \alpha \, : A \\ \vdots \\ \cdots \Rightarrow E\{[\alpha ] s \} \, :A \quad \alpha \, : A \end{array}}}}{\large{\cdots \Rightarrow \mu \alpha . E\{[\alpha] s \} \, : A}}$
という証明だったものが、
$\frac{\frac{\large{\cdots \Rightarrow s \, : A}}{\large{\begin{array}{c}\cdots \Rightarrow \alpha \, : C \quad [\alpha]s \, : A\\ \vdots \\ \cdots \Rightarrow E\{\alpha \} \, :A \quad [\alpha]s \, : A \end{array}}}}{\large{\cdots \Rightarrow \mu \alpha . E\{[\alpha] s \} \, : A}}$
となる(最後に得られる項は同じ)。
このように書き換えると、例えばμα.(1+2+([α](3+4))+5)という項は、(1+2+α+5)という項と[α](3+4)が別々にあって、それを合体させて作られることになる(元の規則では[α](3+4)は初めから組み込まれている)。そうすると、μα.(1+2+([α](3+4))+5)と書くのではなく、例えば
{(1+2+α+5), [α](3+4)}
のように書くことも考えられる。こうすると(1+2+α+5)という項は型の整合性はあるけれど、αに値が入ることが無いので、具体的な値を持たないことがはっきりする。
(ただしこの書き方をする場合、変数の束縛関係を気を付ける必要があって、{ E{α}, [α]s }とある場合に、sはEの変数束縛の影響を受けている。逆に束縛関係をはっきりするなら、[α]を付ける必要さえなくて、{ E{α}, s}でもよいかもしれない。だめかもしれないけど)
こうすると、仮定を増やす規則

$\frac{\large{\cdots \Rightarrow \cdots}}{\large{y \, :A , \, \cdots \Rightarrow \cdots}}$

との類似性が見えてくる。ここで追加された変数yは右辺には一切出てこない。したがって、yを関数抽象で使ってλy.(…)とした場合、yに束縛された値は捨てられてしまう。つまりyへの入力は捨てられる。
一方、ラベルを与える規則
$\frac{\large{\cdots \Rightarrow s \, : A}}{\large{\cdots \Rightarrow \alpha \, : C \quad [\alpha ]s \, :A}}$
では、左辺にαは登場しない。したがって、αに具体的な値が与えられることはない。つまりαからは何も出力されない。
こうした観察から、とりあえず次のような規則を置くことにする。

$\frac{\large{\cdots \Rightarrow s \, :A}}{\large{\cdots \Rightarrow \alpha \, : C \quad [\alpha]s \, :A}}$

$\frac{\large{ \cdots \Rightarrow E\{\alpha\} \, : A \quad [\alpha ]s \, :A}}{\large{\cdots \Rightarrow \{E\{\alpha\}, \quad [\alpha]s\} \, : A}}$

これは実質的には、自然演繹の場合と同じ規則のはず。本当は、

$\frac{\large{\cdots \Rightarrow s \, :A}}{\large{\cdots \Rightarrow \alpha \, : C \quad s \, :A}}$

$\frac{\large{ \cdots \Rightarrow E\{\alpha\} \, : A \quad s \, :A}}{\large{\cdots \Rightarrow \{E\{\alpha\}, \quad [\alpha]s\} \, : A}}$

とか、あるいはもっと単純にして

$\frac{\large{\cdots \Rightarrow s \, :A}}{\large{\cdots \Rightarrow \alpha \, : C \quad s \, :A}}$

$\frac{\large{ \cdots \Rightarrow E\{\alpha\} \, : A \quad s \, :A}}{\large{\cdots \Rightarrow \{E\{\alpha\}, \quad s\} \, : A}}$

と書きたいのだけど、こうすると束縛関係が曖昧になってしまうかもしれない
(追記: この心配はしなくても良い気がする。というか少なくとも以下に書いたような自然演繹での表記を持ち込むのはおかしい。[α]sを含む項が左辺に移動している可能性もあるので。そのうち書き直すかもしれない)。
ただ、最後の書き方をすると、左辺についての、任意の仮定を追加してよいという規則、同じ型の項をひとまとめにしてよいという規則との対応関係がわかりやすい。

$\frac{\large{\cdots \Rightarrow \cdots}}{\large{y \, : A , \, \cdots \Rightarrow \cdots}}$

$\frac{\large{s \, : A \quad t \, : A \Rightarrow \cdots}}{\large{ \{s, t\} \, : A , \, \cdots \Rightarrow \cdots}}$

カリー・ハワード対応と直観主義論理の関係について

古典論理では、命題を左辺に追加してよいという規則と右辺に命題を追加してよいという規則が対応している。この対応関係を観察していると、なぜカリー・ハワード対応がもともとは直観主義論理との対応に限られていたのかについての理屈が思いつく。

左辺に命題を追加してよいという規則

$\frac{\large{\cdots \Rightarrow \cdots}}{\large{y \, : A , \, \cdots \Rightarrow \cdots}}$

で現れた変数yは右辺には出てこないので、yに代入される値はすべて捨てられる。これは無駄だけど計算としては意味がある。
逆に、右辺に命題を追加してよいという規則

$\frac{\large{\cdots \Rightarrow s \, :A}}{\large{\cdots \Rightarrow \alpha \, : C \quad s \, :A}}$

で新しく現れた変数αは左辺に出てこない。なので変数αに具体的な値が入ることはない。そうするとこの変数αを含んだ項も値は決まらないから項の意味づけも与えづらい。つまり右辺に命題を追加する規則は、何を表しているのか不明な項を右辺に追加する役割しか果たしていないように見える。

そもそも、右辺に複数の項があるというのがどういうことなのかもよくわからない。しかも、一つの項を除いてあとの項は左辺に出てこない変数を含んでいる。

というように、カリー・ハワード対応を古典論理に拡張するためには、こういったことに意味づけを与える必要がある。シーケント計算と自然演繹は兄弟のようなものだから、シーケント計算で発生する問題は自然演繹にもついてまわる。
しかも自然演繹はシーケント計算と比べると仮定と結論の扱い方に偏りがある(演繹規則は結論の命題だけをいじる)ために、ラムダ計算を古典論理に拡張する動機があまりない。あるいは、古典論理は仮定と結論を対称的に扱うけど、計算に関しても同じように対称に扱うのはコストがかかると言い換えてもよいかもしれない。
これがカリー・ハワード対応が直観主義論理と相性よく見える理由のひとつじゃないかと思う。

古典論理への拡張の解釈

では、何も知らないまま古典論理に合わせるように計算体系を拡張した場合、どういう解釈を与えることになるか。
「右辺に出てくる項はひとつを除いてあとは左辺に無い変数を含んでいるから、そうした項は意味のないダミー項だと思って気にしない」と思えばよさそうだけど、もう少し考える必要がある。
右辺にしかない変数αを含んだ項E{α}に→右規則を適用してみる。

$\frac{\large{\cdots \Rightarrow E\{ \alpha \} , \, s}}{\large{\cdots \Rightarrow \lambda x . E\{\alpha\} , \, s}}$
ここで項sが変数xを含んでいる場合、λx.E{α}を無視するわけにはいかなくなる。無視してしまうと、sに含まれているxは左辺には登場しない無意味な変数になってしまう。それを避けるためには、このときsに含まれているxは、λx.E{α}のxによって束縛されているとみなせばよい。この束縛関係は、λx.E{α(s)}みたいにsがαの位置にあるかのようにみなせば成立する(変数αを右辺に複数追加する場合でも、後から追加したαがスコープで外側にあるとみなせばよい)。
そうすると、右辺に同じ型の項がある場合はひとつにまとめてよいという規則は、右辺にある複数の項を実際にスコープの入れ子を考慮した上でひとつにまとめる規則だと考えられる。これを明示するために

$\frac{\large{ \cdots \Rightarrow E\{\alpha\} \, : A \quad s \, :A}}{\large{\cdots \Rightarrow \{E\{\alpha\}, \quad s\} \, : A}}$

を

$\frac{\large{ \cdots \Rightarrow E\{\alpha\} \, : A \quad s \, :A}}{\large{\cdots \Rightarrow \mu \alpha . E\{[\alpha]s\} \, : A}}$

と書いてみる。項sをEの内側に置くことでスコープ上の関係が示されている。[α]は型の変換のような役割も持つ。「μα」は、この位置でαを含んだ項をまとめたことを示す印。
これで右辺の意味がいくらか定まってきた。さらに解釈を与えるには、証明図の書き換えが計算のやり方(簡約の仕方)に対応するという考えを使う。
μα.E{[α]s}という項は、まず「無意味な変数」αを導入して、それに演繹規則を適用しE{α}としてから、sとひとつにまとめている。ここでE{α}とsは型が一致している。そうすると、→右規則を使っていない場合は、αの導入からE{α}に至るまでの証明を削って直観主義論理の範囲の証明に書き換えることができる。このとき項μα.E{[α]s}は、sに置き換わる。
これは[α]の位置からμαの位置までジャンプしたと解釈することができる(「→右規則を使っていない」という条件はsがEの中のλによって束縛されていないということなので、ジャンプをする場合は成り立っている必要がある)。また、このような証明図の書き換えは項の外側に影響を与えることになる。項の外側というのは、計算でいうと文脈・継続にあたる。
と、このようにカリー・ハワード対応を古典論理に拡張しようとすると、ジャンプや継続を扱う必要が出てくることになる。

否定

否定をどう扱えばよいのかは、まだよくわからない。¬Aを(A→ $\bot$ の略だと考えると、次のような規則になる。

$\frac{\frac{\large{s \, : A \Rightarrow \cdots }}{\large{s \, : A \Rightarrow \alpha \: \bot \quad \cdots}}}{\large{\Rightarrow \lambda s . \alpha \, : \neg A \quad \cdots}}$

$\frac{\large{\Rightarrow t \, : A \qquad z \, : \bot \Rightarrow z \, : \bot}}{\large{ t@ z \, : \neg A \Rightarrow z \, : \bot}}$

とりあえず¬右規則は

$\frac{\large{s \, : A \Rightarrow \cdots}}{\large{\Rightarrow {\rm not}\,(s,\alpha) \, : \neg A}}$

と書くことにしてみる。ラベルαが邪魔な感じだけど残しておく(無しでも規則次第でどうにかなる気もするけど)。
一方、¬左規則に出てくるzについては、型が $\bot$ なので、zに具体的な値が入ることはないはず。ということは、省略しても問題ない気がする。そこでzに関することを省略すると、¬左規則は次のように書けることになる。

$\frac{\large{\Rightarrow t \, : A }}{\large{ {\rm not}\, t \, : \neg A \Rightarrow }}$

でも本当にこうしてよいのか、ちょっとわからない。
not(s,α) (=λs.α)とt@zについてカット規則を使うと、
$\frac{{\frac{\large{s \, : A \Rightarrow \cdots }}{\large{ \Rightarrow {\rm not}(s,\alpha) \, : \neg A \quad \cdots}}} \qquad \frac{\large{\Rightarrow t \, : A \qquad z \, : \bot \Rightarrow z \, : \bot}}{\large{ t@ z \, : \neg A \Rightarrow z \, : \bot}}}{\large{\Rightarrow {\rm not}( s , \alpha) \bullet t @ z \qquad z \, : \bot, \, \cdots}}$

となるけど、zを省略すると
$\frac{{\frac{\large{s \, : A \Rightarrow \cdots }}{\large{ \Rightarrow {\rm not}(s,\alpha) \, : \neg A \quad \cdots}}} \qquad \frac{\large{\Rightarrow t \, : A}}{\large{{\rm not}\, t \, : \neg A \Rightarrow }}}{\large{\Rightarrow {\rm not}( s , \alpha) \bullet {\rm not}\,t \, \cdots}}$
となり、何となくよいような気もする。カットの位置をずらして簡単化すると、
$\frac{\large{\Rightarrow t \, : a \qquad s \, : A \Rightarrow \cdots}}{\large{\Rightarrow t \bullet s \quad \cdots}}$
となることとも整合性はある感じがするけど、じゃあラベルαは何の役に立っているのかと考えるとよくわからなくなる。

まとめ

推論規則をまとめておく(いくつかの規則は右辺に式が一つしか置けないみたいな書き方がしてあるけど、古典論理の場合は適当に読み替える)。
ただし、weakening右、contraction右、¬右、¬左は暫定的なもの。

(カット)
$\frac{\large{\cdots \Rightarrow s \; :A \qquad t \; :A, \, \cdots \Rightarrow \cdots }}{\large{\cdots \Rightarrow s \bullet t, \qquad \cdots}}$

(∧右)
$\frac{\large{\cdots \Rightarrow s \quad : A \qquad \cdots \Rightarrow t \quad : B}}{\large{\cdots \Rightarrow (s,t) \quad : A \wedge B}}$

(∧左)
$\frac{\large{\cdots, \: s \, :A \Rightarrow \cdots}}{\large{\cdots, \: (s, -) \, :A \wedge B \Rightarrow \cdots}}\qquad \qquad \frac{\large{\cdots, \: t \, :B \Rightarrow \cdots}}{\large{\cdots, \: (-, t) \, :A \wedge B \Rightarrow \cdots}}$

(∨右)
$\frac{\large{\cdots \Rightarrow s \, : A}}{\large{\cdots \Rightarrow [s,-] \, : A \vee B}} \qquad \qquad \frac{\large{\cdots \Rightarrow t \, : B}}{\large{\cdots \Rightarrow [-,t] \, : A \vee B}}$

(∨左)
$\frac{\large{\cdots , \, s \, : A \Rightarrow u \, : C \qquad \cdots , \, t \, : B \Rightarrow u \, : C}}{\large{ [s,t] \, : A \vee B \Rightarrow u \, :C}}$

(→右)
$\frac{\large{s \, : A \Rightarrow t \, : B}}{\large{\Rightarrow \lambda s . t \, : A \to B}}$

(→左)
$\frac{\large{ \cdots \Rightarrow s \, : A \qquad t \, : B , \cdots \Rightarrow \cdots }}{\large{\cdots, \, s @ t \, :A \wedge B \Rightarrow \cdots }}$

(weakening左)
$\frac{\large{\cdots \Rightarrow \cdots}}{\large{x \, : A \, , \cdots \Rightarrow \cdots}}$

(contraction左)
$\frac{\large{s \, : A , \quad t \, : A \, , \quad \cdots \Rightarrow \cdots}}{\large{ \{ s, t\} \, : A \, , \quad \cdots \Rightarrow \cdots}}$

(weakening右) (古典論理)
$\frac{\large{\cdots \Rightarrow \cdots}}{\large{\cdots \Rightarrow \alpha \, : A \, , \cdots}}$

(contraction右) (古典論理)
$\frac{\large{\cdots \Rightarrow E \{\alpha\} \, : A , \, s \, : A}}{\large{\cdots \Rightarrow \{ E\{\alpha\}, [\alpha ]s\} \, : A}} \qquad \qquad \qquad$ または、 $\frac{\large{\cdots \Rightarrow E \{\alpha\} \, : A , \, s \, : A}}{\large{\cdots \Rightarrow \mu \alpha . E\{[\alpha]s\} \, : A}}$