読者です 読者をやめる 読者になる 読者になる

Skinerrian's blog

論理学・哲学・科学史・社会学などに興味があるので、その方面のことを書きます。更新は不定期。

ロビンソン算術

ロビンソン算術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 は存在しない。間違ってたらごめんなさい。

関連記事

*1:Schoenfieldの有名な教科書(p.22)でも同じ公理系が提示されている。

*2:フランセーンが提示している公理系の式はすべてΠ1論理式だが、x ≠ 0 → ∃y(Sy = x) はΠ2論理式である。

*3:戸田山『論理学をつくる』を参考にした。