>>12953371Mhm, not sure if I agree with this language. I'd say "the not accept LEM" just means to not allow oneself to use LEM as an axiom schema. The semantics ("knowing", in my example) is not necessary in proving.
>>12953783If R is an abelian ring with multiplication,
you can define extension * of this in R^2 via
Now squaring a point by (x,y) by itself with this new multiplication
and with the norm down to R this identity reads
Really, this is just what you get by thinking of what the difference term between (x^2 + y^2)^2 and (x^2 - y^2)^2 + (2xy)^2.
Sidenote: Of course, you know * from going from the real to the complex numbers.
But generally, the * multiplication and it has a bunch of nice properties you may verify yourself, like
.
In particular, in Z, you can use this to keep on generating solutions of equations involving a multiplicative function f(v·u)=f(u)·f(v). Which is what ends up being the Euclidean algorithm for finding Pytagorean triples when using the 2-norm for f, see below. But you can also see that in a straight forward manner, pic related.
Coming back, consider the points
in R^2, which have norm 1 by construction. You take an (x,y), 2-norm-project them onto the circle (and square the result)
But this "rational parametrization" has
p(k·x, k·y) = p(x, y).
And if y/x is a valid in a field of fractions, then this also means that the value of p(x, y) is always the same as
p(1, y/x).
If R are taken from the Integers, and t=y/x are rational numbers, then p(1, t) are dense points on a circle in Q^2, a.k.a.
SO(2, Q) ? U(1).
