16/11/06 03:52:38.87 vZo58XwI.net
>>633
> 直観論理の ¬A すなわち A ⊃ f はAを確認する方法が与えられたと仮定して、その方法に基づくと矛盾する、という意味ですよね?
違う
構成主義的な説明(BHK解釈)が一番理解しやすいと思うので、そのスタイルで直観主義論理の含意命題の意味を述べると次のようになる
Aの証明が任意に与えられた時、それを元にしてBの証明を組み上げる手続き(Aの証明木からBを結論とする証明木への変換手続き)を具体的に構成できる、
というの�