Robinson算術
$ \mathsf{Q}
インフォーマルにはPeano算術から帰納法の公理を落としたものと考えられる． Peano算術の帰納法の公理スキーマというのは強すぎ，そこまで強くなくとも良い，という分析によって生み出された体系である．（歴史的敬意については嘘かも） メモ
Def
$ \mathbf{Q1}\colon \forall_{x,y}.\lbrack S(x) = S(y) \to x = y \rbrack
$ \mathbf{Q2}\colon \forall_x.\lbrack S(x) \neq 0 \rbrack
$ \mathbf{Q3}\colon \forall_{x}.\lbrack x \neq 0 \to\exists_y.\lbrack x = S(y) \rbrack \rbrack
$ \mathbf{Q4}\colon \forall_x.\lbrack x + 0 = x \rbrack
$ \mathbf{Q5}\colon \forall_{x,y}.\lbrack x + S(y) = S(x+y) \rbrack
$ \mathbf{Q6}\colon\forall_x.\lbrack x \times 0 = 0 \rbrack
$ \mathbf{Q7}\colon\forall_{x,y}.\lbrack x \times S(y) = x \times y + x \rbrack