Tarski's_axiomatization_of_the_reals Knowpia

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:^[1] 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.

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 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.]

Axioms of addition (primitives: R, <, +)

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.]

Axioms for 1 (primitives: R, <, +, 1)

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

Discussion

Tarski stated, without proof, that these axioms turn the relation < into a total ordering. The missing component was supplied in 2008 by Stefanie Ucsnay.^[2]

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,+,<).^[3]

References

^ Tarski, Alfred (24 March 1994). Introduction to Logic and to the Methodology of Deductive Sciences (4 ed.). Oxford University Press. ISBN 978-0-19-504472-0.
^ Ucsnay, Stefanie (Jan 2008). "A Note on Tarski's Note". The American Mathematical Monthly. 115 (1): 66–68. doi:10.1080/00029890.2008.11920497. JSTOR 27642393.
^ Arthan, Rob D. (2001). "An irrational construction of $\mathbb {R}$ from $\mathbb {Z}$ ". In Boulton, Richard J.; Jackson, Paul B. (eds.). Theorem Proving in Higher Order Logics, 14th International Conference, TPHOLs 2001, Edinburgh, Scotland, UK, September 3–6, 2001, Proceedings. Lecture Notes in Computer Science. Vol. 2152. Berlin: Springer. pp. 43–58. doi:10.1007/3-540-44755-5_5. ISBN 3-540-42525-X. MR 1907599. See in particular Section 4.

[tarski-1] Tarski, Alfred (24 March 1994). Introduction to Logic and to the Methodology of Deductive Sciences (4 ed.). Oxford University Press. ISBN 978-0-19-504472-0.

[total-order-2] Ucsnay, Stefanie (Jan 2008). "A Note on Tarski's Note". The American Mathematical Monthly. 115 (1): 66–68. doi:10.1080/00029890.2008.11920497. JSTOR 27642393.

[3] Arthan, Rob D. (2001). "An irrational construction of $\mathbb {R}$ from $\mathbb {Z}$ ". In Boulton, Richard J.; Jackson, Paul B. (eds.). Theorem Proving in Higher Order Logics, 14th International Conference, TPHOLs 2001, Edinburgh, Scotland, UK, September 3–6, 2001, Proceedings. Lecture Notes in Computer Science. Vol. 2152. Berlin: Springer. pp. 43–58. doi:10.1007/3-540-44755-5_5. ISBN 3-540-42525-X. MR 1907599. See in particular Section 4.

[1]

[2]

[3]