現代数理論理学序説 p.45 自然推論NJでは、論理記号'⊥'を含まない論理式αに至る正規な証明図に現れる論理式はαの部分論理式だけである これの証明のチャレンジしてみました。 正規な推論図であることの別定義 推論図が正規形であることは、以下で定義される…