Tarski's axiomatization of the reals

In 1936, Alfred Tarski gave an axiomatization of the real numbers and their arithmetic, consisting of only the eight axioms shown below and a mere four primitive notions: the set of reals denoted R, a binary relation over R, denoted by infix <, a binary operation of addition over R, denoted by infix +, and the constant 1. 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 also studied the first order theory of the structure (R, +, ·, <), leading to a set of axioms for this theory and to the concept of real closed fields.

Axiom 1 If x < y, then not y < x. [That is, "<" is an asymmetric relation. This implies that "<" is irreflexive, i. e., for all x, not x < x.] Axiom 2 If x < z, there exists a y such that x < y and y < z.
Axiom 3 For all subsets X, Y ⊆ R, if for all x ∈ X and y ∈ Y, x < y, then there exists a z such that for all x ∈ X and y ∈ Y, if x ≠ z and y ≠ z, then x < z and z < y. [In other words, "<" is Dedekind complete, or informally: "If a set of reals X precedes another set of reals Y, then there exists at least one real number z separating the two sets." This is a second order axiom as it refers to sets and not just elements.]

Axiom 4 x + (y + z) = (x + z) + y. [Note that this is an unorthodox mixture of associativity and commutativity.] Axiom 5 For all x, y, there exists a z such that x + z = y. [This allows subtraction and also gives a 0.] Axiom 6 If x + y < z + w, then x < z or y < w.
[This is the contrapositive of a standard axiom for ordered groups.]

Axiom 7 1 ∈ R.
Axiom 8 1 < 1 + 1.

Tarski stated, without proof, that these axioms turn the relation < into a total ordering. The missing component was supplied in 2008 by Stefanie Ucsnay. The axioms then imply that R is a linearly ordered abelian group under addition with distinguished positive element 1, and that this group is Dedekind complete, divisible, and Archimedean. 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,+,<).