ペアノ公理
PA1 1は自然数である。
PA2 どんな自然数nに対しても、succ(n)は自然数である。
PA3 どんな自然数nに対しても、succ(n)≠1が成り立つ
1はどんな数字のsuccでも無い、と言っている
PA4 異なる自然数は異なる後者を持つ：a ≠ b のとき suc(a) ≠ suc(b) となる。
ん、これ数学ガールの記述と違うな
数学ガールは suc(a) ≠ suc(b)ならばa ≠ bって言ってる
合流を防ぐのはどっちもできているなblu3mo.icon
suc(a) ≠ suc(b)ならばa ≠ b と、a ≠ bならばsuc(a) ≠ suc(b) が同値だったりする？
違うわ、数学ガールはsuc(a) = suc(b)ならばa = bって言ってる
理解
PA5 0 がある性質を満たし、a がある性質を満たせばその後者 suc(a) もその性質を満たすとき、すべての自然数はその性質を満たす。
PA5の必要性は数学ガール読んでもいまいちわからず?
PA5で定義されてない場合に数学的帰納法を使っちゃいけないのはなぜ? これは逆。PA5を定義したから数学的帰納法を使えるtakker.icon
$ \text{PA5}\implies\text{mathematical induction}
逆に言うと、PA5が存在しない世界では数学的帰納法を使えるかどうかが定かではない
「使えるかどうか定かでは無い」というのが分からないですblu3mo.icon
数学的帰納法は演繹的推論を繋げているだけなのだから、定義されるまでもなく使って良いのでは..?とblu3mo.icon
数学的帰納法は述語論理の推論規則から演繹できませんtakker.icon
逆にこれができないなら、「1が自然数」（PA1）で、「succ(自然数)は自然数」（PA2）なら「suc(1)やsuc(suc(1))も自然数」とも言えない気がします
そうか、言えないのかblu3mo.icon*6
それこそ自分達はPA1~4を読んで、勝手にsucc(succ(1))も自然数だと推論してしまう
けど、PA5が無い限りsucc(succ(1))は自然数であると言えない、ということか
いや言えますtakker.icon
PA1とPA2を組んで$ \mathrm{succ}(1)\in\Nを導く行為は推論規則上正しいです。
あー、ちょっと説明が悪かったかも。数学的帰納法とPA5は同値だからですtakker.icon
PA5: $ \forall B((1\in B\land\forall n\in B;\mathrm{succ}(n)\in B)\implies B=A)
数学的帰納法:
任意の論理式$ Pについて$ P(1)\land\forall n\in A;(P(n)\implies P(\mathrm{succ}(n)))\implies\forall n\in A;P(n)
PA5$ \iff数学的帰納法
引用にあるPA5の表現だと、同値どころか数学的帰納法と全く同じですね
……blu3mo.iconさんが疑問に思った箇所を認識できていない気がするtakker.icon
質問と回答が噛み合っていないような
なるほど、1のsuccessor以外に自然数がいないよとも言いたいのか
となると、1のsuccessorのみに対して成り立つロジックである数学的帰納法を定義に組み込むことで、それ以外を逆説的に排除している、ってことかな
もっとシンプルに「1のsuccessorやそのsuccessor、〜〜〜以外は自然数じゃないよ」って書いちゃだめなのかな
あ〜でもシンプルな記述を考えたけど再帰的表現は避けられなさそう
そうなると、PA5で推論を定義してもらえないといけない、ということか
ちなみに、PA5の代わりにPA5の否定を導入すると面白いことになりますtakker.icon 面白いblu3mo.icon