13/12/07 19:39:22.13
＞Natの定義がどうマトモでないか
これから定義するべきNat自身を使って
Natを定義しているところ。
整礎関係に対する帰納的定義の場合は、これがきちんと唯一のものを定めているということの
証明が、集合論の教科書にちゃんと書いてあります。
ペアノ算術の場合の、帰納的な関数や述語の定義ができるということの証明は
一階算術の表現能力があまりないのでβ関数とか中国剰余定理とかを
使ってかなりテクニカルな証明をします。たぶんあなたは読んだことないと思います。
>>373
xが群であることをGrp(x)と書くことにすると
>>370に書いたのは
Grp(x) :⇔ ∀y⊆x Grp(y)
ですよ。
「左辺はGrp(x)、右辺はGrp(y)だからちゃんと定義になってます。
見れば分かるでしょ？」とか言われても、
「はぁ？意味不明……」と思いませんか。
Nat(x)の場合との違いが私には分かりません。
それから、私は「逆向きの帰納法」が何を意味するのか分からなくて
私にとっては明らかでも何でもないから
まずあなたが、それが何なのか説明して下さい。
与えられた数から1ずつ引き続けるプログラムなんか
出されても何の説明にもなってません。