ペアノ公理
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って言ってる
- 合流を防ぐのはどっちもできているな
- 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を定義したから数学的帰納法を使える
- $\text{PA5}\implies\text{mathematical induction}$
- 逆に言うと、PA5が存在しない世界では数学的帰納法を使えるかどうかが定かではない
- 「使えるかどうか定かでは無い」というのが分からないです
- 数学的帰納法は演繹的推論を繋げているだけなのだから、定義されるまでもなく使って良いのでは..?と
- 数学的帰納法は述語論理の推論規則から演繹できません
- 逆にこれができないなら、「1が自然数」(PA1)で、「succ(自然数)は自然数」(PA2)なら「suc(1)やsuc(suc(1))も自然数」とも言えない気がします
- そうか、言えないのか
- それこそ自分達はPA1~4を読んで、勝手にsucc(succ(1))も自然数だと推論してしまう
- けど、PA5が無い限りsucc(succ(1))は自然数であると言えない、ということか
- いや言えます
- PA1とPA2を組んで$\mathrm{succ}(1)\in\N$を導く行為は推論規則上正しいです。
- 数学的帰納法は演繹的推論を繋げているだけなのだから、定義されるまでもなく使って良いのでは..?と
- あー、ちょっと説明が悪かったかも。数学的帰納法とPA5は同値だからです
- 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の表現だと、同値どころか数学的帰納法と全く同じですね
- ……さんが疑問に思った箇所を認識できていない気がする
- 質問と回答が噛み合っていないような
- これは逆。PA5を定義したから数学的帰納法を使える
- PA5で定義されてない場合に数学的帰納法を使っちゃいけないのはなぜ?
- ペアノの公理の一つに数学的帰納法の原理がありますが、では数学的帰納法を用いないと証明できない定理には何があるのでしょうか? - Quora
- なるほど、1のsuccessor以外に自然数がいないよとも言いたいのか
- となると、1のsuccessorのみに対して成り立つロジックである数学的帰納法を定義に組み込むことで、それ以外を逆説的に排除している、ってことかな
- もっとシンプルに「1のsuccessorやそのsuccessor、〜〜〜以外は自然数じゃないよ」って書いちゃだめなのかな
- あ〜でもシンプルな記述を考えたけど再帰的表現は避けられなさそう
- そうなると、PA5で推論を定義してもらえないといけない、ということか
- ちなみに、PA5の代わりにPA5の否定を導入すると 面白いことになります
- PA5の必要性は数学ガール読んでもいまいちわからず?
面白い