Premium
A note on the axiomatisation of real numbers
Author(s) -
Coquand Thierry,
Lombardi L. Henri
Publication year - 2008
Publication title -
mathematical logic quarterly
Language(s) - English
Resource type - Journals
SCImago Journal Rank - 0.473
H-Index - 28
eISSN - 1521-3870
pISSN - 0942-5616
DOI - 10.1002/malq.200710039
Subject(s) - dedekind cut , mathematics , constructive , axiom , forcing (mathematics) , relation (database) , real number , function (biology) , discrete mathematics , constructive proof , calculus (dental) , topos theory , pure mathematics , algebra over a field , mathematical analysis , computer science , medicine , art , geometry , literature , dentistry , process (computing) , database , evolutionary biology , biology , operating system
Is it possible to give an abstract characterisation of constructive real numbers? A condition should be that all axioms are valid for Dedekind reals in any topos, or for constructive reals in Bishop mathematics. We present here a possible first‐order axiomatisation of real numbers, which becomes complete if one adds the law of excluded middle. As an application of the forcing relation defined in [3, 2], we give a proof that the formula which specifies the maximum function is not provable in this theory. (© 2008 WILEY‐VCH Verlag GmbH & Co. KGaA, Weinheim)