Very interesting; just one more question: can we use similar methods to compute a symmetric model extensions?

@JoelDavidHamkins I wouldn't be surprised if it were the case. My question is asking about personal opinions and views, and possibly some arguments to support them.

I might be missing something, how can we deduce a=a from this single axiom?

I'll have to go through this argument in detail later, but thanks a lot for this.

Could you elaborate a bit, or give a reference, on why we only need to verify the fact for modulus of $\emptyset'$? I thought that I'd be able to figure that out myself, but I cannot.

It's interesting how for every type of degree I can think of there already exists a name for it :) Thanks a lot.

One theorem of his shows that theory of real ordered fields is decidable, another says so about his axiomatization of Euclidean geometry. Tarski's undefinability theorem can also be thought as concerning decidability (there is no predicate which "decides" truth of statements).

Which Tarski's theorem do you have in mind? I think he had few...