スマートフォン用の表示で見る

ロビンソン算術

一般

ロビンソン算術

ろびんそんさんじゅつ

ロビンソン算術は、言語Lにおいて以下の8つの公理から表現される算術の理論である。

(1)S(x)≠0

(2)S(x)=S(y) → x = y

(3)x≠0 → (∃y)(x = y)

(4)x+0=x

(5)x+S(y)=S(x+y)

(6)x*0=0

(7)x*S(y)=(x*y)+x

(8)x≤y≡(∃z)(z+x=y)

ロビンソン算術に次のinduction schemaを加えたものが通常ペアノ算術と呼ばれる。

(IS)φ(0)&(∀x)(φ(x)→φS(x)). → (∀x)φ(x)

ペアノ算術においては(3)が冗長になる。