「含意の定義の正当性」の問題を排中律を使用しない問題として書き直す

Fixes #703

Examples/Solution/ImpDefValidness.lean

@@ -2,24 +2,17 @@
 
 ## イントロダクション
 
-論理学を学び始めた初心者がよく抱く疑問の一つに、「『ならば』の定義に納得がいかない」というのがあります。「P ならば Q」は論理学では P が偽ならば Q が何であっても真であるものとして定義しますが、それが直観に反するという疑問です。
+論理学を学び始めた初心者がよく抱く疑問の一つに、「『ならば』の定義に納得がいかない」というのがあります。「P ならば Q」は論理学や Lean では P が偽ならば Q が何であっても真であるものとして定義しますが、それが直観に反するという疑問です。
 
 自然言語における「ならば」は、あまりこのような使い方をしませんので、確かに違和感がありますね。たとえば、「意味が分かると怖い話」の中にただただ意味不明なだけの話は普通含まれませんよね！
 
 この演習問題では、この疑問に対する一つの答えを提示します。つまり、含意が満たしていて欲しい最低限の性質をいくつか列挙し、それを満たす「何か」の定義はただ一つしかないということを確認します。
 
-```admonish info title="関数として定義するという制約"
-自然言語における「ならば」と論理学における含意の間には埋めがたい溝もあります。たとえば「`1 = 1` ならば、すべての実数 `x` に対して `x ^ 2 ≥ 0` である」という命題は正しいですが、自然言語としてはかなり違和感があります。ここでの前提と結論の間には何も意味上の関係がないように見えるからです。
-
-しかし、命題から命題への関数として含意を定義しようとしている以上、同値な命題同士を入れ替えても真偽が変わってはいけないので、意味上の関連を持たせることは不可能です。つまり、関数で自然言語の「ならば」を再現することはできないのです。
-
-したがって、ここで私たちが主張できることは、あくまで「関数で自然言語の『ならば』を近似しようとするならば、現行の論理学における定義が最も近い」ということであって、決して「自然言語の『ならば』と論理学における含意に実質的な違いがない」ということではありません。
-```
-
 ## 含意が満たしていて欲しい性質
 
 まずは、含意に相当する「何か」を定義しましょう。それは、命題から命題への2引数関数になっているはずです。ここではその何かに `Imp` という名前をつけ、`→ᵥ` という記号で表すことにします。
 -/
+import Lean --#
 set_option autoImplicit false --#
 -- 含意が満たすべき性質を満たす「何か」
 opaque Imp (P Q : Prop) : Prop
@@ -28,54 +21,102 @@ opaque Imp (P Q : Prop) : Prop
 -- `v` は `virtual` の略
 infixr:40 " →ᵥ " => Imp
 
-/- これだけだと型があるだけのノッペラボーなので、性質を与えていきましょう。含意が満たしているべき性質とはなんでしょうか？
+/- これだけだと型があるだけのノッペラボーなので、性質を与えていきましょう。含意が満たしているべき性質とはなんでしょうか？ `P →ᵥ Q` がおおよそ「`P` を仮定すると `Q` が示せる」という意味になるようにしたいと考えると、次のようなものが考えられるでしょう。 -/
+namespace Imp --#
 
-含意は、直観的には「～を前提とすれば…が成り立つ」ということを意味しています。ですから、特に前提と結論が同じであれば必ず成り立つはずですね。したがって反射性を要請することは妥当に思えます。 -/
+variable {P Q R : Prop}
 
 /-- 含意は反射的。前提 P が真だろうと偽だろうと「P ならば P」は正しい。 -/
-axiom imp_reflexive {P : Prop} : P →ᵥ P
+axiom imp_reflexive : P →ᵥ P
 
-/- また、「～を前提とすれば…が成り立つ」という解釈から、`P →ᵥ Q` と `P` が両方成り立っていたら結論の `Q` が成り立っているべきであることも要請できそうです。 -/
+/-- 含意は推移的 -/
+axiom imp_transitive (hpq : P →ᵥ Q) (hqr : Q →ᵥ R) : P →ᵥ R
 
 /-- モーダスポネンス。「P ならば Q」は、P が正しければ Q が成り立つことを意味する。 -/
-axiom modus_ponens {P Q : Prop} (hpq : P →ᵥ Q) (hP : P) : Q
-
-/- さらに、ある推論で `Q` が結論できるなら、前提を増やしても同じ結論が得られるはずですね。このことにより、結論 `Q` が前提なしで真ならば、任意の `P` に対して `P →ᵥ Q` が成り立っているべきだということが要請できます。 -/
+axiom imp_elim (hpq : P →ᵥ Q) (hP : P) : Q
 
 /-- 結論が無条件に正しいなら、仮定をつけても正しい -/
-axiom imp_introduce {P Q : Prop} (hQ : Q) : P →ᵥ Q
+axiom imp_intro (hQ : Q) : P →ᵥ Q
 
-/- 最後に、含意による関係は推移的であることを要請できます。つまり `P` から `Q` が結論出来て、`Q` から `R` が結論できるなら `P` から `R` が結論できるはずでしょう。 -/
+/-- ある前提から `Q` と `R` が導出できるなら、`Q ∧ R` も導出できる -/
+axiom intro_and (hpq : P →ᵥ Q) (hpr : P →ᵥ R) : P →ᵥ (Q ∧ R)
 
-/-- 含意は推移的 -/
-axiom imp_transitive {P Q R : Prop} (hpq : P →ᵥ Q) (hqr : Q →ᵥ R) : P →ᵥ R
+/-- ある前提から `Q ∧ R` が導出できるなら、`Q` も導出できる -/
+axiom elim_and_left (h : P →ᵥ (Q ∧ R)) : P →ᵥ Q
+
+/-- ある前提から `Q ∧ R` が導出できるなら、`R` も導出できる -/
+axiom elim_and_right (h : P →ᵥ (Q ∧ R)) : P →ᵥ R
+
+/-- ある前提から `Q` が導出できるなら、`Q ∨ R` が導出できる -/
+axiom intro_or_left (h : P →ᵥ Q) : P →ᵥ (Q ∨ R)
+
+/-- ある前提から `R` が導出できるなら、`Q ∨ R` が導出できる -/
+axiom intro_or_right (h : P →ᵥ R) : P →ᵥ (Q ∨ R)
+
+end Imp --#
 
 /- ## 問題
-以上の要請のもとで、前提 `P` が偽であるとき `P →ᵥ Q` が `Q` に関係なく真になることが証明できます。以下の注意点に気を付けながら、`sorry` を埋めてみてください。
+以上の要請のもとで、`P →ᵥ Q` が `P → Q` に一致することが証明できます。
+
+以下の `sorry` を埋めてみてください。ただし、以下のことに注意してください。
+
+* 仮定した要請を全部使う必要はありません。
+* 古典論理に限った話ではないので、排中律を使わずに証明してみてください。
 
-* 排中律は自由に使って構いません。
-* 本文中で課した4つの要請は、全部使う必要はありません。
 -/
 
 variable {P Q : Prop}
 
-/-- 前件(antecedent)が偽であるとき、「P ならば Q」は真 -/
-theorem imp_of_ant_false (nP : ¬ P) : P →ᵥ Q := by
+open Imp
+
+/-- 上記の要請を満たす `→ᵥ` は通常の含意と一致する -/
+theorem imp_valid {P Q : Prop} : (P →ᵥ Q) ↔ (P → Q) := by
   -- sorry
-  -- Q が成り立つかどうかで場合分けする
-  by_cases hQ : Q
-
-  -- Q が成り立つ場合
-  case pos =>
-    -- 含意の導入から従う
-    apply imp_introduce hQ
-
-  -- Q が成り立たない場合
-  case neg =>
-    -- このとき P も Q も False なので、これらは同値である
-    have : P ↔ Q := by exact (iff_false_right hQ).mpr nP
-    rw [this]
-
-    -- したがって含意が反射的であることから従う
-    exact imp_reflexive
+  -- 同値の両方向を示す
+  constructor <;> intro h
+
+  -- 左から右を示す
+  case mp =>
+    intro hP
+
+    -- モーダスポネンスから従う
+    exact imp_elim h hP
+
+  -- 右から左を示す
+  case mpr =>
+    have : P →ᵥ (P ∧ Q) := by
+      -- 同値な命題は入れ替えても良いので、`P ∧ Q` は `P ∧ (P → Q)` と入れ替えられる
+      rw [show (P ∧ Q) ↔ P ∧ (P → Q) from by simp_all]
+
+      -- よって `intro_and` に帰着できる
+      apply intro_and
+        (show P →ᵥ P from imp_reflexive)
+        (show P →ᵥ (P → Q) from imp_intro h)
+
+    -- 後は `elim_and_right` から従う
+    apply elim_and_right this
   -- sorry
+
+--#--
+section
+/- ## 選択原理を使用していないことを確認するコマンド -/
+
+open Lean Elab Command
+
+elab "#detect_classical " id:ident : command => do
+  let constName ← liftCoreM <| realizeGlobalConstNoOverload id
+  let axioms ← collectAxioms constName
+  if axioms.isEmpty then
+    logInfo m!"'{constName}' does not depend on any axioms"
+    return ()
+  let caxes := axioms.filter fun nm => Name.isPrefixOf `Classical nm
+  if caxes.isEmpty then
+    logInfo m!"'{constName}' is non-classical and depends on axioms: {axioms.toList}"
+  else
+    throwError m!"'{constName}' depends on classical axioms: {caxes.toList}"
+
+end
+
+-- 選択原理を使用していないことを確認
+#detect_classical imp_valid
+--#--

Exercise/ImpDefValidness.lean

@@ -2,24 +2,17 @@
 
 ## イントロダクション
 
-論理学を学び始めた初心者がよく抱く疑問の一つに、「『ならば』の定義に納得がいかない」というのがあります。「P ならば Q」は論理学では P が偽ならば Q が何であっても真であるものとして定義しますが、それが直観に反するという疑問です。
+論理学を学び始めた初心者がよく抱く疑問の一つに、「『ならば』の定義に納得がいかない」というのがあります。「P ならば Q」は論理学や Lean では P が偽ならば Q が何であっても真であるものとして定義しますが、それが直観に反するという疑問です。
 
 自然言語における「ならば」は、あまりこのような使い方をしませんので、確かに違和感がありますね。たとえば、「意味が分かると怖い話」の中にただただ意味不明なだけの話は普通含まれませんよね！
 
 この演習問題では、この疑問に対する一つの答えを提示します。つまり、含意が満たしていて欲しい最低限の性質をいくつか列挙し、それを満たす「何か」の定義はただ一つしかないということを確認します。
 
-```admonish info title="関数として定義するという制約"
-自然言語における「ならば」と論理学における含意の間には埋めがたい溝もあります。たとえば「`1 = 1` ならば、すべての実数 `x` に対して `x ^ 2 ≥ 0` である」という命題は正しいですが、自然言語としてはかなり違和感があります。ここでの前提と結論の間には何も意味上の関係がないように見えるからです。
-
-しかし、命題から命題への関数として含意を定義しようとしている以上、同値な命題同士を入れ替えても真偽が変わってはいけないので、意味上の関連を持たせることは不可能です。つまり、関数で自然言語の「ならば」を再現することはできないのです。
-
-したがって、ここで私たちが主張できることは、あくまで「関数で自然言語の『ならば』を近似しようとするならば、現行の論理学における定義が最も近い」ということであって、決して「自然言語の『ならば』と論理学における含意に実質的な違いがない」ということではありません。
-```
-
 ## 含意が満たしていて欲しい性質
 
 まずは、含意に相当する「何か」を定義しましょう。それは、命題から命題への2引数関数になっているはずです。ここではその何かに `Imp` という名前をつけ、`→ᵥ` という記号で表すことにします。
 -/
+import Lean --#
 set_option autoImplicit false --#
 -- 含意が満たすべき性質を満たす「何か」
 opaque Imp (P Q : Prop) : Prop
@@ -28,37 +21,78 @@ opaque Imp (P Q : Prop) : Prop
 -- `v` は `virtual` の略
 infixr:40 " →ᵥ " => Imp
 
-/- これだけだと型があるだけのノッペラボーなので、性質を与えていきましょう。含意が満たしているべき性質とはなんでしょうか？
+/- これだけだと型があるだけのノッペラボーなので、性質を与えていきましょう。含意が満たしているべき性質とはなんでしょうか？ `P →ᵥ Q` がおおよそ「`P` を仮定すると `Q` が示せる」という意味になるようにしたいと考えると、次のようなものが考えられるでしょう。 -/
+namespace Imp --#
 
-含意は、直観的には「～を前提とすれば…が成り立つ」ということを意味しています。ですから、特に前提と結論が同じであれば必ず成り立つはずですね。したがって反射性を要請することは妥当に思えます。 -/
+variable {P Q R : Prop}
 
 /-- 含意は反射的。前提 P が真だろうと偽だろうと「P ならば P」は正しい。 -/
-axiom imp_reflexive {P : Prop} : P →ᵥ P
+axiom imp_reflexive : P →ᵥ P
 
-/- また、「～を前提とすれば…が成り立つ」という解釈から、`P →ᵥ Q` と `P` が両方成り立っていたら結論の `Q` が成り立っているべきであることも要請できそうです。 -/
+/-- 含意は推移的 -/
+axiom imp_transitive (hpq : P →ᵥ Q) (hqr : Q →ᵥ R) : P →ᵥ R
 
 /-- モーダスポネンス。「P ならば Q」は、P が正しければ Q が成り立つことを意味する。 -/
-axiom modus_ponens {P Q : Prop} (hpq : P →ᵥ Q) (hP : P) : Q
-
-/- さらに、ある推論で `Q` が結論できるなら、前提を増やしても同じ結論が得られるはずですね。このことにより、結論 `Q` が前提なしで真ならば、任意の `P` に対して `P →ᵥ Q` が成り立っているべきだということが要請できます。 -/
+axiom imp_elim (hpq : P →ᵥ Q) (hP : P) : Q
 
 /-- 結論が無条件に正しいなら、仮定をつけても正しい -/
-axiom imp_introduce {P Q : Prop} (hQ : Q) : P →ᵥ Q
+axiom imp_intro (hQ : Q) : P →ᵥ Q
 
-/- 最後に、含意による関係は推移的であることを要請できます。つまり `P` から `Q` が結論出来て、`Q` から `R` が結論できるなら `P` から `R` が結論できるはずでしょう。 -/
+/-- ある前提から `Q` と `R` が導出できるなら、`Q ∧ R` も導出できる -/
+axiom intro_and (hpq : P →ᵥ Q) (hpr : P →ᵥ R) : P →ᵥ (Q ∧ R)
 
-/-- 含意は推移的 -/
-axiom imp_transitive {P Q R : Prop} (hpq : P →ᵥ Q) (hqr : Q →ᵥ R) : P →ᵥ R
+/-- ある前提から `Q ∧ R` が導出できるなら、`Q` も導出できる -/
+axiom elim_and_left (h : P →ᵥ (Q ∧ R)) : P →ᵥ Q
+
+/-- ある前提から `Q ∧ R` が導出できるなら、`R` も導出できる -/
+axiom elim_and_right (h : P →ᵥ (Q ∧ R)) : P →ᵥ R
+
+/-- ある前提から `Q` が導出できるなら、`Q ∨ R` が導出できる -/
+axiom intro_or_left (h : P →ᵥ Q) : P →ᵥ (Q ∨ R)
+
+/-- ある前提から `R` が導出できるなら、`Q ∨ R` が導出できる -/
+axiom intro_or_right (h : P →ᵥ R) : P →ᵥ (Q ∨ R)
+
+end Imp --#
 
 /- ## 問題
-以上の要請のもとで、前提 `P` が偽であるとき `P →ᵥ Q` が `Q` に関係なく真になることが証明できます。以下の注意点に気を付けながら、`sorry` を埋めてみてください。
+以上の要請のもとで、`P →ᵥ Q` が `P → Q` に一致することが証明できます。
+
+以下の `sorry` を埋めてみてください。ただし、以下のことに注意してください。
+
+* 仮定した要請を全部使う必要はありません。
+* 古典論理に限った話ではないので、排中律を使わずに証明してみてください。
 
-* 排中律は自由に使って構いません。
-* 本文中で課した4つの要請は、全部使う必要はありません。
 -/
 
 variable {P Q : Prop}
 
-/-- 前件(antecedent)が偽であるとき、「P ならば Q」は真 -/
-theorem imp_of_ant_false (nP : ¬ P) : P →ᵥ Q := by
+open Imp
+
+/-- 上記の要請を満たす `→ᵥ` は通常の含意と一致する -/
+theorem imp_valid {P Q : Prop} : (P →ᵥ Q) ↔ (P → Q) := by
   sorry
+
+--#--
+section
+/- ## 選択原理を使用していないことを確認するコマンド -/
+
+open Lean Elab Command
+
+elab "#detect_classical " id:ident : command => do
+  let constName ← liftCoreM <| realizeGlobalConstNoOverload id
+  let axioms ← collectAxioms constName
+  if axioms.isEmpty then
+    logInfo m!"'{constName}' does not depend on any axioms"
+    return ()
+  let caxes := axioms.filter fun nm => Name.isPrefixOf `Classical nm
+  if caxes.isEmpty then
+    logInfo m!"'{constName}' is non-classical and depends on axioms: {axioms.toList}"
+  else
+    throwError m!"'{constName}' depends on classical axioms: {caxes.toList}"
+
+end
+
+-- 選択原理を使用していないことを確認
+#detect_classical imp_valid
+--#--