13/12/05 23:19:22.76
>>351
>Nat(x)は、xの前者yで、yもNatであるようなものが必ず存在する、
>ということしか言っていませんから、
いいえ、それに加えて、「"いずれ"0に到達できる」ことも言っていると思いますが。
というのは、お分りと思いますが、上記の中の「yもNatである」の部分に対しても
Nat(y) <==> y=0 ∨∃z.(y=z+1 ∧ Nat(z))
が適用されて、さらにそのうちの「zもNatである」の部分に対しても・・・
となりますから。
ですから、0に到達しないωはここのNatには入らないと思うのです。
(ご紹介のスライドは後で勉強してみます）