（１） ⊢ ∃x∀yRxy → ∀y∃xRxy ⊢ ∃x∀yRxy → ∀y∃xRxy ことばにすると、 ∃x∀yRxy ならば ∀y∃xRxy ならばの前件∃x∀yRxyは前提とみなせますから、 ∃x∀yRxy ⊢ ∀y∃xRxy のつもりで証明したらいいです。私はこのとき仮定という言葉を使い、もともとある前提とは区別しておきます。というのは前提は開いたままでいいけれど、自分が仮定としたものは後始末しなければならないからです。 自然演繹法で証明します。 (証明) 1. ⊢ ∃x∀yRxy 仮定1* 2. ⊢ ∀yRay 仮定2* 3. ⊢ Rab ∀除去 4. ⊢ ∃xRxb ∃導入 5. ⊢ ∀y∃xRxy ∀導入(yは変数条件を満たす) 6. ⊢ ∀y∃xRxy ∃除去,2*(xは変数条件を満たす) 7. ⊢ ∃x∀yRxy → ∀y∃xRxy 1,6→導入,1* (証明終わり) 自然演繹法は∨除去規則と∃除去規則が面倒くさいです。その点タブロー法は簡単です。D規則(∃の除去、¬∀の除去)のパラメータを新たな文字にとるだけで、上手く矛盾が導かれるよう優先的にD規則を使うだけです。C規則のパラメータは使ったものに合わせて良い。 タブロー法の略式で証明します。 (証明) 1. ¬(∃x∀yRxy → ∀y∃xRxy) 反証式 2. (∃x∀yRxy)¬(∀y∃xRxy) ¬→除去 3. (∀yRay)¬(∀y∃xRxy) ∃除去 4. (∀yRay)¬(∃xRxb) ¬∀除去 5. Rab¬(∃xRxb) ∀除去 6. Rab¬Rab ¬∃除去 (証明終わり) 正式なタブローはリンク先で作成できます。 https://www.umsu.de/trees/ タブロー法は分解ばかりしますが逆に合成ばかりするタイプのシーケント計算で証明します。 (証明) ───── Ax Rab ⊢ Rab ────── ∃R Rab ⊢ ∃xRxb ─────── ∀L ∀yRay ⊢ ∃xRxb ──────── ∀R (yは非自由出現) ∀yRay ⊢ ∀y∃xRxy ───────── ∃L(xは非自由出現) ∃x∀yRxy ⊢ ∀y∃xRxy ────────── →R ⊢ ∃x∀yRxy → ∀y∃xRxy (証明終わり) タブロー法とは逆行して証明していますね。こちらが直接証明、背理法を使うタブロー法の方が間接証明とされているようです。