- 378 名前:132人目の素数さん mailto:sage [2013/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ずつ引き続けるプログラムなんか 出されても何の説明にもなってません。
|

|