構成的な証明とは何か｜直観主義論理入門 - 記号論理学

直観主義論理（intuitionistic logic）は、古典論理とは異なる基盤に立つ論理体系です。「構成的な証明」を重視し、排中律を認めないという特徴を持ちます。数学の基礎論や計算機科学で重要な役割を果たしています。

直観主義の哲学的背景

直観主義は、20世紀初頭にオランダの数学者ブラウワーが提唱した数学哲学です。

ブラウワーは、数学的対象は人間の精神によって構成されるものであり、存在証明には具体的な構成方法が必要だと主張しました。単に「存在しないと矛盾する」という背理法による存在証明は認めないのです。

排中律の拒否

古典論理では、任意の命題 φ について φ ∨ ¬φ（排中律）が成り立ちます。

直観主義論理では、排中律を公理として認めません。φ ∨ ¬φ を主張するには、φ の証明か ¬φ の証明のどちらかを実際に構成する必要があります。

たとえば「すべての偶数より大きい偶数は2つの素数の和である」（ゴールドバッハ予想）は、証明も反証もされていません。古典論理では「真か偽か」のどちらかですが、直観主義では決定するには具体的な証明が必要です。

BHK 解釈

直観主義論理の意味論は、BHK（ブラウワー・ハイティング・コルモゴロフ）解釈で与えられます。

φ の証明とは何かを、再帰的に定義します。

φ ∧ ψ の証明は、φ の証明と ψ の証明の対。

φ ∨ ψ の証明は、φ の証明か ψ の証明のどちらかと、どちらかを示すタグ。

φ → ψ の証明は、φ の証明を受け取って ψ の証明を返す方法（関数）。

¬φ の証明は、φ の証明から矛盾を導く方法。

直観主義論理の推論規則

直観主義の自然演繹は、古典論理から二重否定除去を除いたものです。

ほとんどの規則は同じですが、背理法の使い方が制限されます。¬φ を仮定して矛盾を導いても、φ を直接結論することはできません（ただし ¬¬φ は結論できます）。

古典論理の定理の多くは直観主義でも成り立ちますが、排中律、二重否定除去、対偶の一方向（¬¬φ → φ）、ド・モルガンの一部などは成り立ちません。

カリー・ハワード対応

直観主義論理は、型付きラムダ計算と深い対応関係にあります。これをカリー・ハワード対応（命題＝型対応）といいます。

命題は型に、証明はプログラムに対応します。φ → ψ の証明は、φ 型の値を受け取って ψ 型の値を返す関数です。

この対応により、プログラムの正しさの証明と論理の証明が同一視できます。直観主義論理は、計算機科学の型理論と自然に結びつくのです。

直観主義と古典論理の関係

直観主義論理で証明可能なことは、古典論理でも証明可能です。直観主義は古典論理の「部分」です。

逆に、古典論理の定理を直観主義に「翻訳」する方法（ゲーデル・ゲンツェン翻訳など）があります。古典論理の ¬¬ を挿入することで、直観主義で証明可能になります。

直観主義の現代的意義

直観主義論理は、構成的数学と証明支援系の基礎となっています。

Coq や Agda といった証明支援系は、直観主義論理（またはその拡張）に基づいています。証明はプログラムとして抽出でき、正しさが保証されたソフトウェアを開発できます。

このように、直観主義論理は純粋な哲学的興味を超えて、実用的な応用を持つ論理体系として重要性を増しています。