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.