部分関数禁止の理由にカリー・ハワード同型対応の観点からの補足を追加

LeanByExample/Modifier/DecreasingBy.lean

@@ -36,7 +36,7 @@ def Nat.toListNat (n : Nat) : List Nat :=
     Nat.toListNat (n / 10) ++ [(n % 10)]
 
 end Hidden --#
-/- `decreasing_by` に続けて停止することの証明を与えれば Lean に受け入れられるようになります。再帰のたびに引数が真に減少し、無限に減少し続けないことを示せば十分です。 -/
+/- `decreasing_by` に続けて停止することの証明を与えれば Lean に受け入れられるようになります。再帰のたびに(無限には減少できない)引数が真に減少することを示せば十分です。 -/
 
 def Nat.toListNat (n : Nat) : List Nat :=
   if n == 0 then
@@ -68,11 +68,21 @@ end Have --#
 
 そもそもなぜ Lean では関数の停止性を示す必要があるのでしょうか？それは、Lean の論理体系の健全性を保つためです。[^recursive]
 
-例として、停止する保証がない関数を定義してみましょう。以下の関数は引数の数列の `f` がいつか `some` になる保証がないので、無限に計算が終わらない可能性があります。
+[カリー・ハワード同型対応](#{root}/Type/Prop.md#CH)によれば「帰納法は再帰」なので、停止しない再帰を許すことは直接的に「終了しない帰納法」を許すことに繋がり、矛盾をもたらすことになってしまいます。
+-/
+
+-- unsafe を使うと終わらない帰納法が使えるので、何でも証明できる
+unsafe def loop_thm (P : Prop) : P :=
+  loop_thm P
+
+unsafe example : False := loop_thm False
+
+/-
+定理ではなくて通常の関数の場合も、停止しない関数を野放図に許すと矛盾を導くことができます。例として、以下の「`Option` 値の点列から `some` であるようなものを探す関数」を考えてみましょう。この関数は引数の点列の `f` がいつか `some` になる保証がないので、無限に計算が終わらない可能性があります。
 -/
 variable {α : Type}
 
-/-- 数列 `f : Nat → Option α` が `some` を返すような最初の `f n` を返す -/
+/-- 点列 `f : Nat → Option α` が `some` を返すような最初の `f n` を返す -/
 unsafe def search (f : Nat → Option α) (start : Nat) : α :=
   match f start with
   | .some x => x