- 215 名前：１３２人目の素数さん mailto:sage [2012/04/20(金) 21:11:59.82 ]
- 直観主義論理と言うよりも構成的数学かもしれませんが、
任意の論理式ψが、古典論理において妥当式であり、
直観主義論理で証明不可能であることは、どのように
証明もしくは定義できるのでしょうか?
たとえば、任意の論理式ψの全ての演繹を定義できるので
あれば、それら演繹の中に証明であるものが存在しない事を
証明すればいいと思います。
しかし、古典論理において論理式ψが妥当式であれば、
論理式ψがたとえ有限であっても、背理法などを考えれば、
その演繹は無限に存在するように思います。
任意の論理式ψについて、直観主義論理の範囲で有効な演繹は
論理式ψが有限であれば、有限個しかないのでしょうか?
結局何が言いたいかと言うと、直観主義論理において
証明不可能であることを証明する自動証明アルゴリズムは
存在するのでしょうか？
