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-completeordered 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.
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.]
[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]
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]
↑ Arthan, Rob D. (2001). "An irrational construction of from ". 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. ISBN3-540-42525-X. MR1907599. See in particular Section 4.
This page is based on this Wikipedia article Text is available under the CC BY-SA 4.0 license; additional terms may apply. Images, videos and audio are available under their respective licenses.