自然演繹の位置づけ

結局、自然演繹とはシーケント計算の簡便な別法ってことかと。

α = (Γ⇒Δ) が定理シーケント、つまり証明できるシーケントのとき、

  Γ
 ----[α]
  Δ

という自然演繹の推論図を使ってイイゾと。また、Γ⇒Δ から Γ'⇒Δ'がシーケント計算で証明できるとき、対応する自然演繹の推論図を書き換えていい、と。

こう考えると、自然演繹の推論図／証明図は、実際には証明過程のスナップショットを表すに過ぎない。状態遷移の状態に過ぎない。ほんとの証明過程は、so-called推論図をスチルとするムービー（アニメーション）となる。

自然演繹が局所性を持たない（スナップショットである証明図の全体を見ないと次の書き換えが分からない）、破壊的な書き換えが存在して、単純に追加描画では済まない、などの特徴は、重複を避けるために図を省略している、カリー化のような操作は破壊的にならざるを得ない、ことで説明が付く。

別な考え方としては、片側シーケントによるシーケント計算が自然演繹だというものがある。だが、これは特殊な場合にしか説明が付かない気がする。

いずれにしても、自然演繹から出発するのは今となっては得策ではなくて、人間にとって扱いやすいように調整した計算系と見るべきだろう。「人間にとって」なので、一意的に決まるわけもなく、理論的に強い根拠があるわけでもない。俺にとって計算しやすい体系を作れば、それは俺流自然演繹系となる。俺流でいいのだ。