In 1936, Alfred Tarski set out an axiomatization of the real numbers and their arithmetic, consisting of only the 8 axioms shown below and a mere four primitive notions: the set of reals denoted R, a binary total order over R, denoted by infix <, a binary operation of addition over R, denoted by infix +, and the constant 1. The literature occasionally mentions this axiomatization but never goes into detail, notwithstanding its economy and elegant metamathematical properties. This axiomatization appears little known, possibly because of its second-order nature. Tarski's axiomatization 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 using unorthodox variants of standard algebraic axioms and other subtle tricks (see e.g. axioms 4 and 5, which combine the usual four axioms of abelian groups). The term "Tarski's axiomatization of real numbers" also refers to the theory of real closed fields, which Tarski showed completely axiomatizes the first-order theory of the structure 〈R, +, ·, <〉. The axioms Axioms of order (primitives: R, <): Axiom 1 If x < y, then not y < x. That is, "<" is an asymmetric relation. This implies that "<" is not a reflexive relationship, i.e. for all x, x < x is false. Axiom 2 If x < z, there exists a y such that x < y and y < z. In other words, "<" is dense in R. Axiom 3 "<" is Dedekind-complete. More formally, for all 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 z ≠ x and z ≠ y, then x < z and z < y. To clarify the above statement somewhat, let X ⊆ R and Y ⊆ R. We now define two common English verbs in a particular way that suits our purpose: X precedes Y if and only if for every x ∈ X and every y ∈ Y, x < y. The real number z separates X and Y if and only if for every x ∈ X with x ≠ z and every y ∈ Y with y ≠ z, x < z and z < y. Axiom 3 can then be stated as: "If a