Eu não sei mais a diferença entre -1 e 1.

Resolvi brincar de axiomatização com um provador de teoremas automático. Coloquei as definições de add e mul no Prover9, e a primeira surpresa é que ele não sabia que 0 é diferente de 1! Na verdade tanto faz, você pode completar essa aritmética dos dois jeitos sem cair em contradição.

Então eu adicionei 0 != 1 como axioma e bola pra frente. Mas aí bati no segundo problema. Se eu tento adicionar raiz quadrada, ele começa a concluir que 1=-1. Usei como definição sqrt(x)=y <=> sqr(y)=x; mas aí ele raciocina que sqrt(1)=1 porque sqr(1)=1, mas sqr(-1)=1 também logo sqrt(1)=-1 e como sqrt(1)=sqrt(1) então 1=-1.

Se eu conserto introduzindo ordem, por exemplo dizendo que (x>0) -> (0>-x) então eu não consigo representar complexos, só reais. Para fazer complexos eu vou precisar de uma definição bem mais complicada de sqrt :(

Aqui meus axiomas até agora:

formulas(sos).
 add(x, 0) = x.
 add(x, minus(x)) = 0.
 add(x, y) = add(y, x).
 add(x, add(y, z)) = add(add(x, y), z).
 mul(x, 1) = x.
 (x != 0) -> (mul(x, inverse(x)) = 1).
 mul(x, y) = mul(y, x).
 mul(x, mul(y, z)) = mul(mul(x, y), z).
 mul(x, add(y, z)) = add(mul(x, y), mul(x, z)).
 1 != 0.
 sqr(x) = mul(x, x).
 (sqrt(x) = y) <-> ((sqr(y) = x)).
end_of_list.

formulas(goals).
 1 = minus(1).
end_of_list.