FOM: Axiomatization of the reals

[Till Mossakowski]

Dear FOMers,

During the development of a standard library for the specification
language CASL (which has the strengh of many-sorted first-order logic
plus some second-order principles with the strength of induction),
I have written down a weak axiomatization of the real
numbers. The axiomatization works as follows:
The is a sort real, a sort sequence (for sequences of reals),
the usual operations, also extended pointwise to sequences,
and axioms stating that we have a cauchy-complete,
algebraically closed, archimedian ordered field.
(Note that archimedianness excludes infinitesimals.)

I want to persuade people that it makes quite sense
to work with this weak axiomatization in many cases,
and therefore it would help to know how relative the notion
of real number is.

The usual axiomatization of the real numbers in ZFC
(which would mean, in strength, to add higher types,
comprehension and choice to the above mentioned axiomatization,
and thereby get more sequences and more reals)
probably suffices for most of mathematics.
But: are there some useful concepts of analysis (or some
other area of mathematics depending on the concept of real numbers)
that require stronger axioms? Do stronger axioms lead
to the possibility to prove the existence of more (or less) real
numbers (and not only of sets of reals, like GCH or V=L)?
Is there an absolute notion of "standard model"
(even if not first-order axomatizable)
of real numbers (like the standard model of natural
numbers constructed by, say, sequences of strokes)?
Or is it true that "the" set of real numbers
is a very relative notion, depending on the background
set theory?

(It seems to me that the usual "monomorphic" second-order
axiomatization of the real numbers depends on the background
set theory in a much stronger sense than the monomorphic
second-order axiomatization of the natural numbers.)


Yours sincerely,
Till Mossakowski

P.S.
I am back on the FOM list (I had unsubscribed because
FOM became too time-consuming, but now from time to time I
encounter FOM questions in my daily work - apart from my
general interest in FOM questions).

My research field:
specification languages, translation and combination of logics

--------------------------------------------------------------------------

Till Mossakowski                 Phone +49-421-218-2935,
Dept. of Computer Science        Fax +49-421-218-4322
University of Bremen             till at informatik.uni-bremen.de
P.O.Box 330440, D-28334 Bremen
http://www.informatik.uni-bremen.de/~till
--------------------------------------------------------------------------