√素数が有理数でないこと(その3)

同じ内容をどこかに書いた気もするのですが,等号の話が出た流れで.かなり以前の「√素数有理数でないこと」http://ehito.hatenablog.com/entry/20130419/1366333894 の続編です.

定数記号c,2項関数記号f,gをもつ言語に,前回のように等号の公理を導入して,理論

{∀x(fcx=x),∀x(gxx=x),∀x∀y∀z(g(fxy)z=c \leftrightarrow gxz=c∧gyz=c)}

をTとおくと,domain が自然数全体,c,f,gの解釈がそれぞれ1,乗算,最大公約数を与える関数である任意の構造Mは,Tのモデルですが,論理式

∀p(p≠c∧∀x∀y(fxy=p→x=c∨y=c)→ ¬(∃x∃y(gxy=c∧fxx=f(fyy)p)))

は,Tから証明可能なので,(健全性により)Mにおいて valid です.

# (UNDISCH_ALL o SPEC_ALL) (METIS [] 
`!f g:a->a->a. (!x. f c x = x) ==> (!x. g x x = x) 
==> (!x y z. g (f x y) z = z <=> g x z = c /\ g y z = c) 
==> (!p. ~(p = c) /\ (!x y. f x y = p ==> x = c \/ y = c) ==> ~(?x y. g x y = c /\ f x x = f (f y y) p))`
);;
val it : thm = !x y z. g (f x y) z = z <=> g x z = c /\ g y z = c,
  !x. f c x = x, !x. g x x = x
  |- !p. ~(p = c) /\ (!x y. f x y = p ==> x = c \/ y = c)
         ==> ~(?x y. g x y = c /\ f x x = f (f y y) p)