直観主義論理と言うよりも構成的数学かもしれませんが、

任意の論理式ψが、古典論理において妥当式であり、
直観主義論理で証明不可能であることは、どのように
証明もしくは定義できるのでしょうか?

たとえば、任意の論理式ψの全ての演繹を定義できるので
あれば、それら演繹の中に証明であるものが存在しない事を
証明すればいいと思います。

しかし、古典論理において論理式ψが妥当式であれば、
論理式ψがたとえ有限であっても、背理法などを考えれば、
その演繹は無限に存在するように思います。

任意の論理式ψについて、直観主義論理の範囲で有効な演繹は
論理式ψが有限であれば、有限個しかないのでしょうか?

結局何が言いたいかと言うと、直観主義論理において
証明不可能であることを証明する自動証明アルゴリズムは
存在するのでしょうか？