>>644
ツリー状の NK の証明図の帰納的定義を形式化したのがシーケントによる NK だよね。
ツリーを下に伸ばす見方に立てば、右導入規則と右除去規則になるわけだけど、
上に伸ばしていく見方に立てば左導入規則と左除去規則になる。
どちらの見方に立った帰納的定義でも、結果として得られるツリー状の証明図全体は一致するのだから、
右導入規則と右除去規則によるシーケント計算がツリー状の NK の異なる表現に過ぎないというのなら
同様に左導入規則と左除去規則によるシーケント計算だって NK の異なる表現に過ぎないはず。
だから >>631 の「私見」は正しくないと思うな。