ろくに物知らないのは事実だが、
二重否定除去則を正式な推論規則として採用すると、
⊥に関する推論規則も除去される。

そんなものNKでもなんでもない。

排中立の証明などと言う意味のない事を考えなければ、
NKで、正規化定理が成り立つって話だけをしてる。