定理証明手習い (41)

Defun帰納法はかなり適用範囲が広そうなやり方です

Defun帰納法は、自分たちで書くどんな関数でも使えるのでしょうか？
帰納的な主張を構成する方法にしろ、全域性の主張を構成する方法にしろ、どんな関数に対しても構成はできます。

ifの位置にもよるけど持ち上げればOK、とのこと

ということは、あらゆる全域的な関数に対し、全域性の主張と帰納的な主張を書けるんですね。
いいえ、あらゆる全域的な関数と言うわけにはいきません。

主張を書けたからといって必ずしも証明できるものではないと思うんですけど
主張すら書けないこともあるってことか

全域だけれども全域であることが証明できない or
全域だけれども全域であることの主張すら書けない、って
不完全性定理みたいな話？
それほど大げさな話ではない？

どんな関数だとダメなんだろうか
たとえば・・・
わからん

コラッツの関数みたいなのだと証明はできないかもしれないけど
あれはそもそも全域かどうかわからないってやつだったし

関数によっては、全域的であっても自然数の尺度を持たないものがあります。 順序数を使えば、もっと多くの関数の全域性が証明可能になるでしょう。

超限帰納法ってやつかな（よく知らない
超限帰納法って響きはなんか必殺技感があって好きです

順序数を使うともっと多くの関数の全域性が証明できるけれども
やっぱり全部ってわけではないという書きっぷり

そろそろ証明に戻りましょうよ！

そうですね最近J-Bob書いてませんから