∀x∀y.x+y=y+x,
∀x∀y∀z.(x+y)+z=x+(y+z),
∀x.x+0=x,
∀x∃y.x+y=0,
∀x∀y.x*y=y*x,
∀x∀y∀z.(x*y)*z=x*(y*z),
∀x.x*1=x,
∀x.(¬x=0→∃y.x*y=1),
¬(0=1),
∀x∀y∀z.x*(y+z)=x*y+x*z,
∀x.¬x＜x,
∀x∀y∀z.x＜y∧y∧z→x＜z,
∀x∀y. x＜y∨y＜x∨x=y,
∀x∀y∀z.x＜y→x+z＜y+z,
∀x∀y∀z.x＜y∧0＜z→x*z＜y*z,
N(1),
∀x x＜1→¬N(x),
∀xN(x)→N(x+1),
∀x「N(x)→∀y[(x≦y＜x+1∧N(y))→y=x]」
|-¬(∃x∃n∃m.x*x=2∧n=x*m∧N(n)∧N(m))

とりあえずこんな感じが示せれば良いわけですよね