野矢論理学 4章

直観論理についての概説。排中律が否定されるとともに、古典論理では妥当であったいくつかの定理が成り立たないことを示す。例えば、次のものは直観論理では成立しない：否定除去型の背理法（￢Aを仮定して矛盾を示せば、Aが示せる）、二重否定除去（￢￢AからAを示す）。直観論理とは観念論であり、証明は構成可能性によってしめされるものだという言及。

上記の概説の元、直観命題論理である公理系LIPを紹介。意味論として、クリプキによる意味論を採用し、認識史・知識状態・「 ||- 」を使って意味論を与える。古典論理の真理値分析に対して、認識史分析がある、すなわち決定手続きがあることを示す（具体的に書いてあるが、煩雑なので読むのをあきらめた）。

また、古典論理に関して再度意味論を検討する。すなわち、モデルという概念によって意味論を再解釈した。

直観命題論理は、古典命題論理の部分系であるが、完全である。直観命題論理の妥当式は、古典命題論理の妥当式であるが、その逆は必ずしも成り立たない。

ここで「 ||- 」が出てきた。なるほど、確かに直観論理から借りてきた記号なのか・・・と腹落ちしたのであった