Bluemo's Brain

Search

Search IconIcon to open search

ペアノ公理

Last updated Unknown Edit Source

    • 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.iconblu3mo.iconblu3mo.iconblu3mo.iconblu3mo.iconblu3mo.icon
                • それこそ自分達は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
            • 質問と回答が噛み合っていないような
      • ペアノの公理の一つに数学的帰納法の原理がありますが、では数学的帰納法を用いないと証明できない定理には何があるのでしょうか? - Quora
        • なるほど、1のsuccessor以外に自然数がいないよとも言いたいのか
        • となると、1のsuccessorのみに対して成り立つロジックである数学的帰納法を定義に組み込むことで、それ以外を逆説的に排除している、ってことかな
        • もっとシンプルに「1のsuccessorやそのsuccessor、〜〜〜以外は自然数じゃないよ」って書いちゃだめなのかな
          • あ〜でもシンプルな記述を考えたけど再帰的表現は避けられなさそう
          • そうなると、PA5で推論を定義してもらえないといけない、ということか
      • ちなみに、PA5の代わりにPA5の否定を導入すると 面白いことになりますtakker.icon
    • 面白いblu3mo.icon