Tarski's axiomatization of the reals

Tarski's axiomatization, which is a second-order theory, can be seen as a version of the more usual definition of real numbers as the unique Dedekind-complete ordered field; it is however made much more concise by avoiding multiplication altogether and using unorthodox variants of standard algebraic axioms and other subtle tricks.

Tarski did not supply a proof that his axioms are sufficient or a definition for the multiplication of real numbers in his system.

Tarski stated, without proof, that these axioms turn the relation < into a total ordering.

Tarski never proved that these axioms and primitives imply the existence of a binary operation called multiplication that has the expected properties, so that R becomes a complete ordered field under addition and multiplication.

It is possible to define this multiplication operation by considering certain order-preserving homomorphisms of the ordered group (R,+,<).