ロビンソン算術Qは以下7つの式（の全称閉包）を公理にもつ。
- Sx ≠ 0
- Sx = Sy → x = y
- x ≠ 0 → ∃y(Sy = x)
- x+0 = x
- x+Sy = S(x+y)
- x・0 = 0
- x・Sy = (x・y)+x
不等号は次の定義によって導入する。
- x < y ≡ ∃z(x+Sz = y)
フランセーン『ゲーデルの定理』はよく似ている公理系を提示している*1。これは、上の3番目の公理の代わりに、不等号に関する3つの公理をおく。
- (x = y v x < y) v y < x
- ￢(Sx < 0)
- x < Sy ≡ (x = y v x < y)
こちらの公理系は存在量化子を使わないぶんエレガントに思える*2。
しかし、二つの公理系は同値ではなさそうだ。例えば、Qから (x = y v x < y) v y < x を導出できないことを示す反例モデルとして、以下を考えてみた*3。モデルのドメインは自然数に加えて、i, j, k という三つの余分なエレメントからなる。Si = i, Sj = j, Sk = kであり、任意の自然数nについて、n+i = i+n = i, n+j = j+n = j, n+k = k+n = k。そして、i+i = i, j+j = j, k+k = k, i+j = j+i = k, i+k = k+i = j+k = k+j = kとする。このモデルでは i と j の順序関係が決まらないと思う。i ≠ jだし、i+Sz = j となるようなz, j+Sz = i となるようなz は存在しない。間違ってたらごめんなさい。
