定理 4.1 の応用
反駁による証明問題を歩いて学ぶ
開発者向け解説
Module 1〜4 で身につけた道具（反駁・スコーレム化・節集合・エルブラン）と Theorem 4.1 を使って、 実際の論理式に 反駁証明 を適用してみる演習。
Theorem 4.1 は単なる定理ではなく、 「節集合が空節を導出した」 という構文的な事実から「元の式が妥当である」 という意味論的結論へ渡るための唯一の橋。 この橋がなぜ必要で、どこで使われるのかを 8 ステップで体感する。
題材は古典的な含意：「誰かが全員を愛しているなら、全員はそれぞれ誰かに愛されている」。 ∃ と ∀ の両方が混ざった、Theorem 4.1 の真価が現れる典型例。
例題：「愛されているか？」（古典）
前提と結論を 8 ステップで反駁する。各ステップは「次へ」で順に開く。
進捗 1 / 9
- Step 0｜証明したい命題目的：意味論ではなく構文だけで反駁を導く
「誰か が全員 を愛している」が真ならば、 「全員 は誰か に愛されている」も真である、 と直感的には当たり前のこの含意を機械的に証明する。
なぜ Theorem 4.1 が必要なのか — 一行のまとめ
反駁手続きは「節集合 から空節 を導く」という純粋に構文的な操作しかしない。 一方、証明したい命題は「元の式 が妥当」という意味論的な主張。 この二つを結ぶ唯一の論理的橋が 、 すなわち Theorem 4.1 である。