>>652
その線で行くと、正規なNK/NJの証明図はLK/LJそのものになる。
除去規則は上に伸ばす方向で、導入規則は下に伸ばす方向で
木状のNK/NJ証明図を構成すると、正規形が出来る。
これは正規な証明図の再帰的定義の一つであり、
この再帰に基づいてシーケント表現すれば
各論理記号ごとに左導入規則と右導入規則を持つ体系になる。
NJの場合、これはLJ-Cutそのもの。
（NKの場合、排中律か二重否定除去則かその替わりになるもの次第。）
NJとLJの正規形同士が綺麗に対応するとかじゃなくて、
そもそも両者を区別する術がなく完全に同じものってことになってしまうんだが
それでもいいのだろうか？