ペアノ算術(PA)
Peano arithmetic
ペアノの公理の時点では、「+」のような記号が使えなかったことに注意する 以下の公理を持つ体型をペアノ算術と言う
言語
$ \{0,S,+,\times,=\}
公理
①$ \forall n(S(n)\ne 0)
②$ \forall m\forall n(S(m)=S(n)\Rightarrow m=n)
加算
③$ \forall n(n+0=0)
④$ \forall (m\forall n\; m+S(n)=S(m+n))
乗算
⑤$ \forall n(n\times0=0)
⑥$ \forall m\forall n (m\times S(n)=(m\times n)+m)
⑦Pを算術の論理式とする
Pの自由変数を$ n,w_0,\cdots,w_{i-1}とする
$ \left.\forall w_{0} \ldots \forall w_{i-1}((P(0) \wedge(\forall n)(P(n) \Rightarrow P(S(n))))) \Rightarrow \forall n P(n)\right)
不等号の公理
$ \forall n \in \mathbb { N } [ \neg ( n < 1 )]
$ \forall m \in \mathbb { N } \quad \forall n \in \mathbb { N }[ \left( m < n ^ { \prime } \right) \Longleftrightarrow \left( m < n \vee m = n \right)]
これはなんだ？mrsekut.icon
上述した加算の公理を導出木を用いて以下のように書き直せる $ \frac{}{Z \, \mathrm{plus}\, n\, \mathrm{is} \, n}
$ \frac{n_1\,\mathrm{plus}\,n_2\,\mathrm{is}\,n}{S(n_1)\,\mathrm{plus}\,n_2\,\mathrm{is}\,S(n)}
こうやってみるとHaskellで再帰関数を書くときの定義のようだね
ちょっとちがうかmrsekut.icon
乗算も同様
$ \frac{}{Z \,\mathrm{times}\,n\,\mathrm{is}\,Z}
$ \frac{n_1\,\mathrm{times}\,n_2\,\mathrm{is}\,n_3\quad n_2\,\mathrm{plus}\,n_3\,\mathrm{is}\,n_4}{S(n_1)\,\mathrm{times}\,n_2\,\mathrm{is}\,n_4}
用語の区別
この辺の用語の整理ができていないmrsekut.icon
ペアノの公理
ペアノ算術の公理
ペアノ算術
ペアノの公理を起点に見れば
ペアノ算術は「ペアノ公理から導かれる定理の集合」と言えるし
ペアノ算術を起点に見れば、
ペアノの公理は「ペアノ算術の公理」と言える
というような解釈をしているmrsekut.icon
この区別とか用語って合ってるのか？
たぶん合ってるけど、用語が粗いので不安になる
序盤にこの記事を読んだので理解がバグった
参考