なるほどダメだ：シーケント記法

推論のストリング図をテキストで表したものがシーケントだと解釈すると、通常のシーケント記法はダメなことがわかる。シーケント矢印が

• 推論のスパイダーを表す矢印
• ケーブリングを表す矢印

の区別ができないと、ストリング図を書き写すことができない。次のように区別する。

• -○→ 推論のスパイダーを表す矢印
• → ケーブリングを表す矢印

これを使うと、ダイアモンド・リーズニング（リーズニング＝推論に対する演算子）の基本リーズニング図は次のように表される。

  Γ→(x∈X| A -○→ B[x])
 =========================== ◇
  Γ, A -○→ ∀x∈X.B[x]

Γから出る矢印は、コンテキストの外部の仮定がコンテキスト（のスコープボックス）内部に侵入する様を表している。

スクエア・リーズニングの基本リーズニング図は

  Γ→(x∈X| A[x] -○→ B)
 =========================== □
  Γ, ∃x∈X.A[x] -○→ B