If I construct points in Euclidean geometry (out of a given set of points, e.g. the four points of a unit square) by using circles and straight lines, can I always prove if two generated points are equal or not?
This boils down to something like this: If I add the square root operation to $\mathbb{Q}$, and look at a given number (which is the result of applying $+,-,\cdot, /, \sqrt{}$ finitely often to some natural numbers), can I always prove whether this number is equal to zero? In other words: Is there an algorithm that decides this?
Yes, this is a corollary of the Tarski-Seidenberg theorem, which implies that it's algorithmically decidable which statements about Euclidean geometry are true (including statements about whether points are equal).