From c9fefe07ca41b81fd240c736b367e4710fab8eff Mon Sep 17 00:00:00 2001 From: Seasawher Date: Fri, 16 Aug 2024 19:01:25 +0900 Subject: [PATCH 1/8] =?UTF-8?q?=E5=BA=8A=E5=B1=8B=E3=81=AE=E3=83=91?= =?UTF-8?q?=E3=83=A9=E3=83=89=E3=83=83=E3=82=AF=E3=82=B9=E3=82=92=E8=BF=BD?= =?UTF-8?q?=E5=8A=A0?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- Examples/Exercise/BarberParadox.lean | 35 +++++++++++++++++++++++++ Examples/Exercise/README.lean | 1 + Examples/Solution/BarberParadox.lean | 38 ++++++++++++++++++++++++++++ Examples/Solution/README.lean | 1 + lake-manifest.json | 16 +++++++++--- lakefile.lean | 4 +++ src/SUMMARY.md | 7 +++++ 7 files changed, 99 insertions(+), 3 deletions(-) create mode 100644 Examples/Exercise/BarberParadox.lean create mode 100644 Examples/Exercise/README.lean create mode 100644 Examples/Solution/BarberParadox.lean create mode 100644 Examples/Solution/README.lean diff --git a/Examples/Exercise/BarberParadox.lean b/Examples/Exercise/BarberParadox.lean new file mode 100644 index 00000000..60203004 --- /dev/null +++ b/Examples/Exercise/BarberParadox.lean @@ -0,0 +1,35 @@ +/- # 床屋のパラドックス +集合論が提唱された当初、任意の述語 `P` に対して `P` を満たす要素の集合 `{ x | P x }` が存在するとされていました。このルールを内包公理と呼びます。`P` が成り立つ要素を集めてくることができると主張しているわけで、直観的で受け入れやすいと思われます。しかし、特に述語 `P` として「自分自身を含まない」という述語を採用すると、矛盾が生じることが知られています。これは Russel のパラドックスと呼ばれています。 + +この問題を回避する方法は複数ありえますが、現在広く採用されている ZFC 集合論では、内包公理の適用範囲を部分集合に限定して主張を弱めることで Russel のパラドックスを回避しています。 + +以上が Russel のパラドックスの概要です。床屋のパラドックスとは、Russel のパラドックスの内容をわかりやすく説明するために考えられた比喩です。 + +その内容は自然言語では次のように説明できます。 + +> ある村に床屋がいます。その床屋は、自分で髭を剃る村人の髭は剃らず、自分で髭を剃らない村人の髭を剃るという信念を持っています。このとき、その床屋は自分の髭を剃るでしょうか？ +> +> 仮に剃るとしたら、その床屋はまさに「自分で自分の髭を剃っている」ので剃ってはならないはずで、矛盾が生じます。逆に剃らないとすると、その床屋はまさに「自分で自分の髭を剃らない」ので自分の髭を剃らなければならないことになり、矛盾が生じます。 +> +> いずれにせよ矛盾が生じてしまいます。 + +この内容を Lean で表現してみましょう。演習問題として、`sorry` の部分を埋めてみてください。 +-/ +namespace Barber + +/-- 全体集合となる人々の集合 -/ +opaque Person : Type + +/-- p さんが q さんの髭を剃るという述語 -/ +opaque shave (p q : Person) : Prop + +-- 床屋が存在するという仮定 +variable (barber : Person) + +-- 床屋の信念を仮定として表現したもの +variable (policy : ∀ p : Person, shave barber p ↔ ¬ shave p p) + +example : False := by + sorry + +end Barber diff --git a/Examples/Exercise/README.lean b/Examples/Exercise/README.lean new file mode 100644 index 00000000..17557cf6 --- /dev/null +++ b/Examples/Exercise/README.lean @@ -0,0 +1 @@ +/- # 演習問題 -/ diff --git a/Examples/Solution/BarberParadox.lean b/Examples/Solution/BarberParadox.lean new file mode 100644 index 00000000..a8ec5b72 --- /dev/null +++ b/Examples/Solution/BarberParadox.lean @@ -0,0 +1,38 @@ +/- # 床屋のパラドックス +集合論が提唱された当初、任意の述語 `P` に対して `P` を満たす要素の集合 `{ x | P x }` が存在するとされていました。このルールを内包公理と呼びます。`P` が成り立つ要素を集めてくることができると主張しているわけで、直観的で受け入れやすいと思われます。しかし、特に述語 `P` として「自分自身を含まない」という述語を採用すると、矛盾が生じることが知られています。これは Russel のパラドックスと呼ばれています。 + +この問題を回避する方法は複数ありえますが、現在広く採用されている ZFC 集合論では、内包公理の適用範囲を部分集合に限定して主張を弱めることで Russel のパラドックスを回避しています。 + +以上が Russel のパラドックスの概要です。床屋のパラドックスとは、Russel のパラドックスの内容をわかりやすく説明するために考えられた比喩です。 + +その内容は自然言語では次のように説明できます。 + +> ある村に床屋がいます。その床屋は、自分で髭を剃る村人の髭は剃らず、自分で髭を剃らない村人の髭を剃るという信念を持っています。このとき、その床屋は自分の髭を剃るでしょうか？ +> +> 仮に剃るとしたら、その床屋はまさに「自分で自分の髭を剃っている」ので剃ってはならないはずで、矛盾が生じます。逆に剃らないとすると、その床屋はまさに「自分で自分の髭を剃らない」ので自分の髭を剃らなければならないことになり、矛盾が生じます。 +> +> いずれにせよ矛盾が生じてしまいます。 + +この内容を Lean で表現してみましょう。演習問題として、`sorry` の部分を埋めてみてください。 +-/ +namespace Barber + +/-- 全体集合となる人々の集合 -/ +opaque Person : Type + +/-- p さんが q さんの髭を剃るという述語 -/ +opaque shave (p q : Person) : Prop + +-- 床屋が存在するという仮定 +variable (barber : Person) + +-- 床屋の信念を仮定として表現したもの +variable (policy : ∀ p : Person, shave barber p ↔ ¬ shave p p) + +example : False := by + -- sorry + replace policy := policy barber + simp [iff_not_self] at policy + -- sorry + +end Barber diff --git a/Examples/Solution/README.lean b/Examples/Solution/README.lean new file mode 100644 index 00000000..17557cf6 --- /dev/null +++ b/Examples/Solution/README.lean @@ -0,0 +1 @@ +/- # 演習問題 -/ diff --git a/lake-manifest.json b/lake-manifest.json index 6839f5d8..34646109 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -1,11 +1,21 @@ {"version": "1.1.0", "packagesDir": ".lake/packages", "packages": - [{"url": "https://github.com/Seasawher/mdgen", + [{"url": "https://github.com/Seasawher/mk-exercise.git", "type": "git", "subDir": null, "scope": "", - "rev": "bddd1ec2c02d86e4d5fecb0259471bf282df6a0a", + "rev": "f306b57fcd9c40621a6c41ceecf2969b166dfbcf", + "name": "«mk-exercise»", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": false, + "configFile": "lakefile.lean"}, + {"url": "https://github.com/Seasawher/mdgen", + "type": "git", + "subDir": null, + "scope": "", + "rev": "6d86fc91c6ed2b173b6d0b31a6d7b7c9af41d366", "name": "mdgen", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -75,7 +85,7 @@ "type": "git", "subDir": null, "scope": "", - "rev": "08ecf4c7e62daf335fa2f9e42d6ad90574211eb5", + "rev": "07a0ae9126dff1d2838a59b03ac6763e22ed6cb4", "name": "mathlib", "manifestFile": "lake-manifest.json", "inputRev": "master", diff --git a/lakefile.lean b/lakefile.lean index 0d52bd8b..e0a98599 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -7,6 +7,9 @@ package «Lean by Example» where ⟨`relaxedAutoImplicit, false⟩ ] +require «mk-exercise» from git + "https://github.com/Seasawher/mk-exercise.git" @ "main" + require mdgen from git "https://github.com/Seasawher/mdgen" @ "main" @@ -28,6 +31,7 @@ def runCmd (cmd : String) (args : Array String) : ScriptM Bool := do return hasError script build do + if ← runCmd "lake" #["exe", "mk_exercise", "Examples/Solution", "Examples/Exercise"] then return 1 if ← runCmd "lake" #["exe", "mdgen", "Examples", "src"] then return 1 if ← runCmd "mdbook" #["build"] then return 1 return 0 diff --git a/src/SUMMARY.md b/src/SUMMARY.md index 28d22d0f..b533fc7d 100644 --- a/src/SUMMARY.md +++ b/src/SUMMARY.md @@ -6,6 +6,8 @@ --- +# リファレンス + - [コマンド](./Command/README.md) - [対話的コマンド](./Command/Diagnostic/README.md) - [#check_failure: 意図的なエラー](./Command/Diagnostic/CheckFailure.md) @@ -154,3 +156,8 @@ - [型](./Term/Type/README.md) - [Prop: 命題全体](./Term/Type/Prop.md) - [Type: 型全体](./Term/Type/Type.md) + +# ガイド + +- [演習問題](./Exercise/README.md) + - [床屋のパラドクス](./Exercise/BarberParadox.md) From a729b76f26e04df47a176f1a6e6dc60f3c3aa0e4 Mon Sep 17 00:00:00 2001 From: Seasawher Date: Fri, 16 Aug 2024 19:01:25 +0900 Subject: [PATCH 2/8] =?UTF-8?q?=E5=BA=8A=E5=B1=8B=E3=81=AE=E3=83=91?= =?UTF-8?q?=E3=83=A9=E3=83=89=E3=83=83=E3=82=AF=E3=82=B9=E3=82=92=E8=BF=BD?= =?UTF-8?q?=E5=8A=A0?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- Examples/Exercise/BarberParadox.lean | 35 +++++++++++++++++++++++++ Examples/Exercise/README.lean | 1 + Examples/Solution/BarberParadox.lean | 38 ++++++++++++++++++++++++++++ Examples/Solution/README.lean | 1 + lake-manifest.json | 16 +++++++++--- lakefile.lean | 3 +++ src/SUMMARY.md | 7 +++++ 7 files changed, 98 insertions(+), 3 deletions(-) create mode 100644 Examples/Exercise/BarberParadox.lean create mode 100644 Examples/Exercise/README.lean create mode 100644 Examples/Solution/BarberParadox.lean create mode 100644 Examples/Solution/README.lean diff --git a/Examples/Exercise/BarberParadox.lean b/Examples/Exercise/BarberParadox.lean new file mode 100644 index 00000000..60203004 --- /dev/null +++ b/Examples/Exercise/BarberParadox.lean @@ -0,0 +1,35 @@ +/- # 床屋のパラドックス +集合論が提唱された当初、任意の述語 `P` に対して `P` を満たす要素の集合 `{ x | P x }` が存在するとされていました。このルールを内包公理と呼びます。`P` が成り立つ要素を集めてくることができると主張しているわけで、直観的で受け入れやすいと思われます。しかし、特に述語 `P` として「自分自身を含まない」という述語を採用すると、矛盾が生じることが知られています。これは Russel のパラドックスと呼ばれています。 + +この問題を回避する方法は複数ありえますが、現在広く採用されている ZFC 集合論では、内包公理の適用範囲を部分集合に限定して主張を弱めることで Russel のパラドックスを回避しています。 + +以上が Russel のパラドックスの概要です。床屋のパラドックスとは、Russel のパラドックスの内容をわかりやすく説明するために考えられた比喩です。 + +その内容は自然言語では次のように説明できます。 + +> ある村に床屋がいます。その床屋は、自分で髭を剃る村人の髭は剃らず、自分で髭を剃らない村人の髭を剃るという信念を持っています。このとき、その床屋は自分の髭を剃るでしょうか？ +> +> 仮に剃るとしたら、その床屋はまさに「自分で自分の髭を剃っている」ので剃ってはならないはずで、矛盾が生じます。逆に剃らないとすると、その床屋はまさに「自分で自分の髭を剃らない」ので自分の髭を剃らなければならないことになり、矛盾が生じます。 +> +> いずれにせよ矛盾が生じてしまいます。 + +この内容を Lean で表現してみましょう。演習問題として、`sorry` の部分を埋めてみてください。 +-/ +namespace Barber + +/-- 全体集合となる人々の集合 -/ +opaque Person : Type + +/-- p さんが q さんの髭を剃るという述語 -/ +opaque shave (p q : Person) : Prop + +-- 床屋が存在するという仮定 +variable (barber : Person) + +-- 床屋の信念を仮定として表現したもの +variable (policy : ∀ p : Person, shave barber p ↔ ¬ shave p p) + +example : False := by + sorry + +end Barber diff --git a/Examples/Exercise/README.lean b/Examples/Exercise/README.lean new file mode 100644 index 00000000..17557cf6 --- /dev/null +++ b/Examples/Exercise/README.lean @@ -0,0 +1 @@ +/- # 演習問題 -/ diff --git a/Examples/Solution/BarberParadox.lean b/Examples/Solution/BarberParadox.lean new file mode 100644 index 00000000..a8ec5b72 --- /dev/null +++ b/Examples/Solution/BarberParadox.lean @@ -0,0 +1,38 @@ +/- # 床屋のパラドックス +集合論が提唱された当初、任意の述語 `P` に対して `P` を満たす要素の集合 `{ x | P x }` が存在するとされていました。このルールを内包公理と呼びます。`P` が成り立つ要素を集めてくることができると主張しているわけで、直観的で受け入れやすいと思われます。しかし、特に述語 `P` として「自分自身を含まない」という述語を採用すると、矛盾が生じることが知られています。これは Russel のパラドックスと呼ばれています。 + +この問題を回避する方法は複数ありえますが、現在広く採用されている ZFC 集合論では、内包公理の適用範囲を部分集合に限定して主張を弱めることで Russel のパラドックスを回避しています。 + +以上が Russel のパラドックスの概要です。床屋のパラドックスとは、Russel のパラドックスの内容をわかりやすく説明するために考えられた比喩です。 + +その内容は自然言語では次のように説明できます。 + +> ある村に床屋がいます。その床屋は、自分で髭を剃る村人の髭は剃らず、自分で髭を剃らない村人の髭を剃るという信念を持っています。このとき、その床屋は自分の髭を剃るでしょうか？ +> +> 仮に剃るとしたら、その床屋はまさに「自分で自分の髭を剃っている」ので剃ってはならないはずで、矛盾が生じます。逆に剃らないとすると、その床屋はまさに「自分で自分の髭を剃らない」ので自分の髭を剃らなければならないことになり、矛盾が生じます。 +> +> いずれにせよ矛盾が生じてしまいます。 + +この内容を Lean で表現してみましょう。演習問題として、`sorry` の部分を埋めてみてください。 +-/ +namespace Barber + +/-- 全体集合となる人々の集合 -/ +opaque Person : Type + +/-- p さんが q さんの髭を剃るという述語 -/ +opaque shave (p q : Person) : Prop + +-- 床屋が存在するという仮定 +variable (barber : Person) + +-- 床屋の信念を仮定として表現したもの +variable (policy : ∀ p : Person, shave barber p ↔ ¬ shave p p) + +example : False := by + -- sorry + replace policy := policy barber + simp [iff_not_self] at policy + -- sorry + +end Barber diff --git a/Examples/Solution/README.lean b/Examples/Solution/README.lean new file mode 100644 index 00000000..17557cf6 --- /dev/null +++ b/Examples/Solution/README.lean @@ -0,0 +1 @@ +/- # 演習問題 -/ diff --git a/lake-manifest.json b/lake-manifest.json index 6839f5d8..34646109 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -1,11 +1,21 @@ {"version": "1.1.0", "packagesDir": ".lake/packages", "packages": - [{"url": "https://github.com/Seasawher/mdgen", + [{"url": "https://github.com/Seasawher/mk-exercise.git", "type": "git", "subDir": null, "scope": "", - "rev": "bddd1ec2c02d86e4d5fecb0259471bf282df6a0a", + "rev": "f306b57fcd9c40621a6c41ceecf2969b166dfbcf", + "name": "«mk-exercise»", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": false, + "configFile": "lakefile.lean"}, + {"url": "https://github.com/Seasawher/mdgen", + "type": "git", + "subDir": null, + "scope": "", + "rev": "6d86fc91c6ed2b173b6d0b31a6d7b7c9af41d366", "name": "mdgen", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -75,7 +85,7 @@ "type": "git", "subDir": null, "scope": "", - "rev": "08ecf4c7e62daf335fa2f9e42d6ad90574211eb5", + "rev": "07a0ae9126dff1d2838a59b03ac6763e22ed6cb4", "name": "mathlib", "manifestFile": "lake-manifest.json", "inputRev": "master", diff --git a/lakefile.lean b/lakefile.lean index 2ce7f778..83732b00 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -7,6 +7,8 @@ package «Lean by Example» where ⟨`relaxedAutoImplicit, false⟩ ] +require "Seasawher" / «mk-exercise» + require "Seasawher" / "mdgen" require "leanprover-community" / "mathlib" @@ -26,6 +28,7 @@ def runCmd (cmd : String) (args : Array String) : ScriptM Bool := do return hasError script build do + if ← runCmd "lake" #["exe", "mk_exercise", "Examples/Solution", "Examples/Exercise"] then return 1 if ← runCmd "lake" #["exe", "mdgen", "Examples", "src"] then return 1 if ← runCmd "mdbook" #["build"] then return 1 return 0 diff --git a/src/SUMMARY.md b/src/SUMMARY.md index 28d22d0f..b533fc7d 100644 --- a/src/SUMMARY.md +++ b/src/SUMMARY.md @@ -6,6 +6,8 @@ --- +# リファレンス + - [コマンド](./Command/README.md) - [対話的コマンド](./Command/Diagnostic/README.md) - [#check_failure: 意図的なエラー](./Command/Diagnostic/CheckFailure.md) @@ -154,3 +156,8 @@ - [型](./Term/Type/README.md) - [Prop: 命題全体](./Term/Type/Prop.md) - [Type: 型全体](./Term/Type/Type.md) + +# ガイド + +- [演習問題](./Exercise/README.md) + - [床屋のパラドクス](./Exercise/BarberParadox.md) From 5d7a571326f052c289a8a459fb1cd8f2e7e374f1 Mon Sep 17 00:00:00 2001 From: Seasawher Date: Sat, 17 Aug 2024 05:34:35 +0900 Subject: [PATCH 3/8] =?UTF-8?q?=E3=83=89=E3=83=A2=E3=83=AB=E3=82=AC?= =?UTF-8?q?=E3=83=B3=E3=81=AE=E6=BC=94=E7=BF=92=E3=81=AE=E8=AA=AC=E6=98=8E?= =?UTF-8?q?=E6=96=87=E3=81=AE=E6=9B=B4=E6=96=B0?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- Examples/Exercise/DeMorgan.lean | 12 ++++++------ Examples/Solution/DeMorgan.lean | 10 +++++----- 2 files changed, 11 insertions(+), 11 deletions(-) diff --git a/Examples/Exercise/DeMorgan.lean b/Examples/Exercise/DeMorgan.lean index 91f449f3..019fe291 100644 --- a/Examples/Exercise/DeMorgan.lean +++ b/Examples/Exercise/DeMorgan.lean @@ -37,15 +37,15 @@ theorem not_and_mpr (P Q : Prop) : ¬ P ∨ ¬ Q → ¬ (P ∧ Q) := by /- ## 問3 問1の命題は、排中律を使わずに示すことができます。問2も、`not_and_mpr` の方は排中律なしで証明できます。 -排中律を使うと `Classical.choice` という公理が使用されることを覚えておきましょう。自身の証明で使用した公理を [`#print`](../Command/Diagnostic/Print.md) コマンドで確認して、排中律をもし使っていたら使わない証明に書き換えてみてください。 -/ +証明で使用した公理を [`#print`](../Command/Diagnostic/Print.md) コマンドで確認してみましょう。排中律を使うと `Classical.choice` という公理が使用されるので、この公理が使われていなければ排中律は使っていません。 +ここまでの `not_and_mp` 以外の3つの命題について、排中律をもし使っていたら使わない証明に書き換えてみてください。 -/ -/- ## 問4 -4つの中で唯一排中律が必要だったのは `not_and_mp` ですね。実はこの命題は、直観主義論理において弱い排中律 `¬ P ∨ ¬ ¬ P` と同値になることが知られています。 -これを Lean で証明してみましょう。Lean はデフォルトで直観主義論理を採用しているため、Lean で証明をするのは紙とペンで証明するよりも簡単かもしれません。 +/- ## 問4 +4つの中で唯一排中律が必要だったのは `not_and_mp` です。実はこの命題は、直観主義論理において弱い排中律 `¬ P ∨ ¬ ¬ P` と同値になることが知られています。 -以下の `sorry` の部分を埋めてください。証明が終わったら、証明が排中律に依存していないことを `#print` コマンドで確認することをお忘れなく。 +これを Lean で証明してみましょう。以下の `sorry` の部分を埋めてください。証明が終わったら、証明が排中律に依存していないことを `#print` コマンドで確認することをお忘れなく。 -/ namespace Playground @@ -55,7 +55,7 @@ def not_and_mp := ∀ (P Q : Prop), ¬ (P ∧ Q) → ¬ P ∨ ¬ Q /-- 弱い排中律 -/ def weak_em := ∀ (P : Prop), ¬ P ∨ ¬ ¬ P -/-- カリー化。証明の中で役に立つかも？ -/ +/-- カリー化の特殊な場合。証明の中で役に立つかも？ -/ theorem currying (P Q : Prop) : ¬ (P ∧ Q) ↔ (P → ¬ Q) := by sorry diff --git a/Examples/Solution/DeMorgan.lean b/Examples/Solution/DeMorgan.lean index fb9fe75c..df39b7c4 100644 --- a/Examples/Solution/DeMorgan.lean +++ b/Examples/Solution/DeMorgan.lean @@ -130,7 +130,9 @@ example (P Q : Prop) : ¬ P ∨ ¬ Q → ¬ (P ∧ Q) := by /- ## 問3 問1の命題は、排中律を使わずに示すことができます。問2も、`not_and_mpr` の方は排中律なしで証明できます。 -排中律を使うと `Classical.choice` という公理が使用されることを覚えておきましょう。自身の証明で使用した公理を [`#print`](../Command/Diagnostic/Print.md) コマンドで確認して、排中律をもし使っていたら使わない証明に書き換えてみてください。 -/ +証明で使用した公理を [`#print`](../Command/Diagnostic/Print.md) コマンドで確認してみましょう。排中律を使うと `Classical.choice` という公理が使用されるので、この公理が使われていなければ排中律は使っていません。 + +ここまでの `not_and_mp` 以外の3つの命題について、排中律をもし使っていたら使わない証明に書き換えてみてください。 -/ --##-- -- この模範解答では、不必要な公理を使用しない方法を紹介している。 @@ -151,9 +153,7 @@ example (P Q : Prop) : ¬ P ∨ ¬ Q → ¬ (P ∧ Q) := by /- ## 問4 4つの中で唯一排中律が必要だったのは `not_and_mp` です。実はこの命題は、直観主義論理において弱い排中律 `¬ P ∨ ¬ ¬ P` と同値になることが知られています。 -これを Lean で証明してみましょう。Lean はデフォルトで直観主義論理を採用しているため、Lean で証明をするのは紙とペンで証明するよりも簡単かもしれません。 - -以下の `sorry` の部分を埋めてください。証明が終わったら、証明が排中律に依存していないことを `#print` コマンドで確認することをお忘れなく。 +これを Lean で証明してみましょう。以下の `sorry` の部分を埋めてください。証明が終わったら、証明が排中律に依存していないことを `#print` コマンドで確認することをお忘れなく。 -/ namespace Playground @@ -163,7 +163,7 @@ def not_and_mp := ∀ (P Q : Prop), ¬ (P ∧ Q) → ¬ P ∨ ¬ Q /-- 弱い排中律 -/ def weak_em := ∀ (P : Prop), ¬ P ∨ ¬ ¬ P -/-- カリー化。証明の中で役に立つかも？ -/ +/-- カリー化の特殊な場合。証明の中で役に立つかも？ -/ theorem currying (P Q : Prop) : ¬ (P ∧ Q) ↔ (P → ¬ Q) := by -- sorry have := @not_and P Q From 9b689ad8d52a234a3af97fa52a3a7855c56fc9d8 Mon Sep 17 00:00:00 2001 From: Seasawher Date: Sun, 18 Aug 2024 13:01:26 +0900 Subject: [PATCH 4/8] =?UTF-8?q?=E5=90=AB=E6=84=8F=E3=81=AE=E5=AE=9A?= =?UTF-8?q?=E7=BE=A9=E3=81=AE=E6=AD=A3=E5=BD=93=E6=80=A7=E3=81=AB=E3=81=A4?= =?UTF-8?q?=E3=81=84=E3=81=A6=E3=81=AE=E6=BC=94=E7=BF=92=E5=95=8F=E9=A1=8C?= =?UTF-8?q?=E3=82=92=E8=BF=BD=E5=8A=A0?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- Examples/Exercise/Implication.lean | 70 ++++++++++++++++++++++++ Examples/Solution/Implication.lean | 87 ++++++++++++++++++++++++++++++ src/SUMMARY.md | 1 + 3 files changed, 158 insertions(+) create mode 100644 Examples/Exercise/Implication.lean create mode 100644 Examples/Solution/Implication.lean diff --git a/Examples/Exercise/Implication.lean b/Examples/Exercise/Implication.lean new file mode 100644 index 00000000..bf2957ac --- /dev/null +++ b/Examples/Exercise/Implication.lean @@ -0,0 +1,70 @@ +/- # 含意の定義の正当性 + +## イントロダクション + +論理学を学び始めた初心者がよく抱く疑問の一つに、「『ならば』の定義に納得がいかない」というのがあります。「P ならば Q」は論理学では P が偽ならば Q が何であっても真であるものとして定義しますが、それが直観に反するという疑問です。 + +自然言語における「ならば」は、あまりこのような使い方をしませんので、確かに違和感がありますね。たとえば、「意味が分かると怖い話」の中にただただ意味不明なだけの話は普通含まれませんよね！ + +この演習問題では、この疑問に対する一つの答えを提示します。つまり、含意が満たしていて欲しい最低限の性質をいくつか列挙し、それを満たす「何か」の定義はただ一つしかないということを確認します。 + +> **注意** +> +> 自然言語における「ならば」と論理学における含意の間には埋めがたい溝もあります。たとえば「`1 = 1` ならば、すべての実数 `x` に対して `x ^ 2 ≥ 0` である」という命題は正しいですが、自然言語としてはかなり違和感があります。ここでの前提と結論の間には何も意味上の関係がないように見えるからです。 +> +> しかし、命題から命題への関数として含意を定義しようとしている以上、同値な命題同士を入れ替えても真偽が変わってはいけないので、意味上の関連を持たせることは不可能です。つまり、関数で自然言語の「ならば」を再現することはできないのです。 +> +> したがって、ここで私たちが主張できることは、あくまで「関数で自然言語の『ならば』を近似しようとするならば、現行の論理学における定義が最も近い」ということであって、決して「自然言語の『ならば』と論理学における含意に実質的な違いがない」ということではありません。注意して下さい。 + +## 含意が満たしていて欲しい性質 + +まずは、含意に相当する「何か」を定義しましょう。それは、命題から命題への2引数関数になっているはずです。ここではその何かに `Imp` という名前をつけ、`→ᵥ` という記号で表すことにします。 +-/ +-- 含意が満たすべき性質を満たす「何か」 +opaque Imp (P Q : Prop) : Prop + +-- 含意っぽい記法の導入 +-- `v` は `virtual` の略 +infixr:40 " →ᵥ " => Imp + +/- これだけだと型があるだけのノッペラボーなので、性質を与えていきましょう。含意が満たしているべき性質とはなんでしょうか？ + +含意は、直観的には「～を前提とすれば…が成り立つ」ということを意味しています。ですから、特に前提と結論が同じであれば必ず成り立つはずですね。したがって反射性を要請することは妥当に思えます。 -/ + +/-- 含意は反射的。前提 P が真だろうと偽だろうと「P ならば P」は正しい。 -/ +axiom imp_reflexive {P : Prop} : P →ᵥ P + +/- また、「～を前提とすれば…が成り立つ」という解釈から、`P →ᵥ Q` と `P` が両方成り立っていたら結論の `Q` が成り立っているべきであることも要請できそうです。 -/ + +/-- モーダスポネンス。「P ならば Q」は、P が正しければ Q が成り立つことを意味する。 -/ +axiom modus_ponens {P Q : Prop} (hpq : P →ᵥ Q) (hP : P) : Q + +/- さらに、ある推論で `Q` が結論できるなら、前提を増やしても同じ結論が得られるはずですね。このことにより、結論 `Q` が前提なしで真ならば、任意の `P` に対して `P →ᵥ Q` が成り立っているべきだということが要請できます。 -/ + +/-- 結論が無条件に正しいなら、仮定をつけても正しい -/ +axiom imp_introduce {P Q : Prop} (hQ : Q) : P →ᵥ Q + +/- 最後に、含意による関係は推移的であることを要請できます。つまり `P` から `Q` が結論出来て、`Q` から `R` が結論できるなら `P` から `R` が結論できるはずでしょう。 -/ + +/-- 含意は推移的 -/ +axiom imp_transitive {P Q R : Prop} (hpq : P →ᵥ Q) (hqr : Q →ᵥ R) : P →ᵥ R + +/- ## 問題 +以上の要請のもとで、前提 `P` が偽であるとき `P →ᵥ Q` が `Q` に関係なく真になることが証明できます。以下の注意点に気を付けながら、`sorry` を埋めてみてください。 + +* 排中律は自由に使って構いません。 +* 本文中で課した4つの要請は、全部使う必要はありません。 +-/ + +variable {P Q : Prop} + +/-- 前提が偽であるとき、「P ならば Q」は真 -/ +theorem imp_of_ant_false (nP : ¬ P) : P →ᵥ Q := by + sorry + +/- +## ヒント + +どの要請が絶対に必要なのか考えてみるといいかもしれません。示したい命題 `imp_of_ant_false` は、`→ᵥ` の部分を同値関係 `↔` に読み替えるとともはや正しくありません。つまり、同値関係の話に読み替えたら成り立たなくなるような要請を、どれか一つ必ず使用するはずですね。 + +-/ diff --git a/Examples/Solution/Implication.lean b/Examples/Solution/Implication.lean new file mode 100644 index 00000000..ca6aaded --- /dev/null +++ b/Examples/Solution/Implication.lean @@ -0,0 +1,87 @@ +/- # 含意の定義の正当性 + +## イントロダクション + +論理学を学び始めた初心者がよく抱く疑問の一つに、「『ならば』の定義に納得がいかない」というのがあります。「P ならば Q」は論理学では P が偽ならば Q が何であっても真であるものとして定義しますが、それが直観に反するという疑問です。 + +自然言語における「ならば」は、あまりこのような使い方をしませんので、確かに違和感がありますね。たとえば、「意味が分かると怖い話」の中にただただ意味不明なだけの話は普通含まれませんよね！ + +この演習問題では、この疑問に対する一つの答えを提示します。つまり、含意が満たしていて欲しい最低限の性質をいくつか列挙し、それを満たす「何か」の定義はただ一つしかないということを確認します。 + +> **注意** +> +> 自然言語における「ならば」と論理学における含意の間には埋めがたい溝もあります。たとえば「`1 = 1` ならば、すべての実数 `x` に対して `x ^ 2 ≥ 0` である」という命題は正しいですが、自然言語としてはかなり違和感があります。ここでの前提と結論の間には何も意味上の関係がないように見えるからです。 +> +> しかし、命題から命題への関数として含意を定義しようとしている以上、同値な命題同士を入れ替えても真偽が変わってはいけないので、意味上の関連を持たせることは不可能です。つまり、関数で自然言語の「ならば」を再現することはできないのです。 +> +> したがって、ここで私たちが主張できることは、あくまで「関数で自然言語の『ならば』を近似しようとするならば、現行の論理学における定義が最も近い」ということであって、決して「自然言語の『ならば』と論理学における含意に実質的な違いがない」ということではありません。注意して下さい。 + +## 含意が満たしていて欲しい性質 + +まずは、含意に相当する「何か」を定義しましょう。それは、命題から命題への2引数関数になっているはずです。ここではその何かに `Imp` という名前をつけ、`→ᵥ` という記号で表すことにします。 +-/ +-- 含意が満たすべき性質を満たす「何か」 +opaque Imp (P Q : Prop) : Prop + +-- 含意っぽい記法の導入 +-- `v` は `virtual` の略 +infixr:40 " →ᵥ " => Imp + +/- これだけだと型があるだけのノッペラボーなので、性質を与えていきましょう。含意が満たしているべき性質とはなんでしょうか？ + +含意は、直観的には「～を前提とすれば…が成り立つ」ということを意味しています。ですから、特に前提と結論が同じであれば必ず成り立つはずですね。したがって反射性を要請することは妥当に思えます。 -/ + +/-- 含意は反射的。前提 P が真だろうと偽だろうと「P ならば P」は正しい。 -/ +axiom imp_reflexive {P : Prop} : P →ᵥ P + +/- また、「～を前提とすれば…が成り立つ」という解釈から、`P →ᵥ Q` と `P` が両方成り立っていたら結論の `Q` が成り立っているべきであることも要請できそうです。 -/ + +/-- モーダスポネンス。「P ならば Q」は、P が正しければ Q が成り立つことを意味する。 -/ +axiom modus_ponens {P Q : Prop} (hpq : P →ᵥ Q) (hP : P) : Q + +/- さらに、ある推論で `Q` が結論できるなら、前提を増やしても同じ結論が得られるはずですね。このことにより、結論 `Q` が前提なしで真ならば、任意の `P` に対して `P →ᵥ Q` が成り立っているべきだということが要請できます。 -/ + +/-- 結論が無条件に正しいなら、仮定をつけても正しい -/ +axiom imp_introduce {P Q : Prop} (hQ : Q) : P →ᵥ Q + +/- 最後に、含意による関係は推移的であることを要請できます。つまり `P` から `Q` が結論出来て、`Q` から `R` が結論できるなら `P` から `R` が結論できるはずでしょう。 -/ + +/-- 含意は推移的 -/ +axiom imp_transitive {P Q R : Prop} (hpq : P →ᵥ Q) (hqr : Q →ᵥ R) : P →ᵥ R + +/- ## 問題 +以上の要請のもとで、前提 `P` が偽であるとき `P →ᵥ Q` が `Q` に関係なく真になることが証明できます。以下の注意点に気を付けながら、`sorry` を埋めてみてください。 + +* 排中律は自由に使って構いません。 +* 本文中で課した4つの要請は、全部使う必要はありません。 +-/ + +variable {P Q : Prop} + +/-- 前提が偽であるとき、「P ならば Q」は真 -/ +theorem imp_of_ant_false (nP : ¬ P) : 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 + -- sorry + +/- +## ヒント + +どの要請が絶対に必要なのか考えてみるといいかもしれません。示したい命題 `imp_of_ant_false` は、`→ᵥ` の部分を同値関係 `↔` に読み替えるとともはや正しくありません。つまり、同値関係の話に読み替えたら成り立たなくなるような要請を、どれか一つ必ず使用するはずですね。 + +-/ diff --git a/src/SUMMARY.md b/src/SUMMARY.md index 698e1662..4019bdd9 100644 --- a/src/SUMMARY.md +++ b/src/SUMMARY.md @@ -162,3 +162,4 @@ - [演習問題](./Exercise/README.md) - [床屋のパラドクス](./Exercise/BarberParadox.md) - [De Morganの法則と排中律](./Exercise/DeMorgan.md) + - [含意の定義の正当性](./Exercise/Implication.md) From 95873d34333708512350e21517d5ad8a8c91832c Mon Sep 17 00:00:00 2001 From: Seasawher Date: Sun, 18 Aug 2024 13:03:58 +0900 Subject: [PATCH 5/8] =?UTF-8?q?de=20morgan=20=E6=BC=94=E7=BF=92=E5=95=8F?= =?UTF-8?q?=E9=A1=8C=E3=81=AE=E3=83=95=E3=82=A1=E3=82=A4=E3=83=AB=E5=90=8D?= =?UTF-8?q?=E3=82=92=E5=A4=89=E6=9B=B4?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- Examples/Exercise/{DeMorgan.lean => DeMorganAndEm.lean} | 0 Examples/Solution/{DeMorgan.lean => DeMorganAndEm.lean} | 0 src/SUMMARY.md | 2 +- 3 files changed, 1 insertion(+), 1 deletion(-) rename Examples/Exercise/{DeMorgan.lean => DeMorganAndEm.lean} (100%) rename Examples/Solution/{DeMorgan.lean => DeMorganAndEm.lean} (100%) diff --git a/Examples/Exercise/DeMorgan.lean b/Examples/Exercise/DeMorganAndEm.lean similarity index 100% rename from Examples/Exercise/DeMorgan.lean rename to Examples/Exercise/DeMorganAndEm.lean diff --git a/Examples/Solution/DeMorgan.lean b/Examples/Solution/DeMorganAndEm.lean similarity index 100% rename from Examples/Solution/DeMorgan.lean rename to Examples/Solution/DeMorganAndEm.lean diff --git a/src/SUMMARY.md b/src/SUMMARY.md index 4019bdd9..f0c1b99d 100644 --- a/src/SUMMARY.md +++ b/src/SUMMARY.md @@ -161,5 +161,5 @@ - [演習問題](./Exercise/README.md) - [床屋のパラドクス](./Exercise/BarberParadox.md) - - [De Morganの法則と排中律](./Exercise/DeMorgan.md) + - [De Morganの法則と排中律](./Exercise/DeMorganAndEm.md) - [含意の定義の正当性](./Exercise/Implication.md) From 93a0a17a2be9da753f01fb4ed560e8fa5e1d71bd Mon Sep 17 00:00:00 2001 From: Seasawher Date: Sun, 18 Aug 2024 13:06:37 +0900 Subject: [PATCH 6/8] =?UTF-8?q?=E5=90=AB=E6=84=8F=E3=81=AE=E5=AE=9A?= =?UTF-8?q?=E7=BE=A9=E3=81=AE=E6=AD=A3=E5=BD=93=E6=80=A7=E3=81=AE=E5=95=8F?= =?UTF-8?q?=E9=A1=8C=E3=81=AE=E3=83=95=E3=82=A1=E3=82=A4=E3=83=AB=E5=90=8D?= =?UTF-8?q?=E5=A4=89=E6=9B=B4?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit より具体的に --- Examples/Exercise/{Implication.lean => ImpDefValidness.lean} | 0 Examples/Solution/{Implication.lean => ImpDefValidness.lean} | 0 src/SUMMARY.md | 2 +- 3 files changed, 1 insertion(+), 1 deletion(-) rename Examples/Exercise/{Implication.lean => ImpDefValidness.lean} (100%) rename Examples/Solution/{Implication.lean => ImpDefValidness.lean} (100%) diff --git a/Examples/Exercise/Implication.lean b/Examples/Exercise/ImpDefValidness.lean similarity index 100% rename from Examples/Exercise/Implication.lean rename to Examples/Exercise/ImpDefValidness.lean diff --git a/Examples/Solution/Implication.lean b/Examples/Solution/ImpDefValidness.lean similarity index 100% rename from Examples/Solution/Implication.lean rename to Examples/Solution/ImpDefValidness.lean diff --git a/src/SUMMARY.md b/src/SUMMARY.md index f0c1b99d..49302759 100644 --- a/src/SUMMARY.md +++ b/src/SUMMARY.md @@ -162,4 +162,4 @@ - [演習問題](./Exercise/README.md) - [床屋のパラドクス](./Exercise/BarberParadox.md) - [De Morganの法則と排中律](./Exercise/DeMorganAndEm.md) - - [含意の定義の正当性](./Exercise/Implication.md) + - [含意の定義の正当性](./Exercise/ImpDefValidness.md) From 8f66b8edf07423d84212e96d70df9eeda563c888 Mon Sep 17 00:00:00 2001 From: Seasawher Date: Sun, 18 Aug 2024 13:08:03 +0900 Subject: [PATCH 7/8] =?UTF-8?q?=E6=96=87=E8=A8=80=E5=BE=AE=E4=BF=AE?= =?UTF-8?q?=E6=AD=A3?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 何の単語の略かわかるようにする --- Examples/Solution/ImpDefValidness.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Examples/Solution/ImpDefValidness.lean b/Examples/Solution/ImpDefValidness.lean index ca6aaded..03808178 100644 --- a/Examples/Solution/ImpDefValidness.lean +++ b/Examples/Solution/ImpDefValidness.lean @@ -58,7 +58,7 @@ axiom imp_transitive {P Q R : Prop} (hpq : P →ᵥ Q) (hqr : Q →ᵥ R) : P variable {P Q : Prop} -/-- 前提が偽であるとき、「P ならば Q」は真 -/ +/-- 前件(antecedent)が偽であるとき、「P ならば Q」は真 -/ theorem imp_of_ant_false (nP : ¬ P) : P →ᵥ Q := by -- sorry -- Q が成り立つかどうかで場合分けする From 1f49aaac8a55b6b231df9ac522ab430d30517407 Mon Sep 17 00:00:00 2001 From: Seasawher Date: Sun, 18 Aug 2024 13:08:25 +0900 Subject: [PATCH 8/8] =?UTF-8?q?=E3=82=B3=E3=83=9F=E3=83=83=E3=83=88?= =?UTF-8?q?=E5=BF=98=E3=82=8C?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- Examples/Exercise/ImpDefValidness.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Examples/Exercise/ImpDefValidness.lean b/Examples/Exercise/ImpDefValidness.lean index bf2957ac..5f785dc0 100644 --- a/Examples/Exercise/ImpDefValidness.lean +++ b/Examples/Exercise/ImpDefValidness.lean @@ -58,7 +58,7 @@ axiom imp_transitive {P Q R : Prop} (hpq : P →ᵥ Q) (hqr : Q →ᵥ R) : P variable {P Q : Prop} -/-- 前提が偽であるとき、「P ならば Q」は真 -/ +/-- 前件(antecedent)が偽であるとき、「P ならば Q」は真 -/ theorem imp_of_ant_false (nP : ¬ P) : P →ᵥ Q := by sorry