>>507
NKの場合、単純な意味での部分論理式原理は成り立たない。
例：排中律 p∨¬p の証明図中には部分論理式ではない ¬¬(p∨¬p) の登場が必要。