雑に言えば、ペアノの公理に加法と乗法の公理を加えたもの

ペアノの公理の時点では、「+」のような記号が使えなかったことに注意する

以下の公理を持つ体型をペアノ算術と言う

言語

\{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)]

これはなんだ？

上述した加算の公理を導出木を用いて以下のように書き直せる

\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で再帰関数を書くときの定義のようだね

ちょっとちがうか

乗算も同様

\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}

用語の区別

この辺の用語の整理ができていない

ペアノの公理

ペアノ算術の公理

ペアノ算術

ペアノの公理を起点に見れば

ペアノ算術は「ペアノ公理から導かれる定理の集合」と言えるし

ペアノ算術を起点に見れば、

ペアノの公理は「ペアノ算術の公理」と言える

というような解釈をしている

しかしこの記事を読むとこんがらがる

この区別とか用語って合ってるのか？

たぶん合ってるけど、用語が粗いので不安になる

序盤にこの記事を読んだので理解がバグった

参考

『数学ガール 3 ゲーデルの不完全性定理』