5 More About the Specification BasicReal

The specification BasicReal of real numbers in section 4 specifies the reals to be an algebraically closed archimedian ordered field in which every Cauchy sequence converges. Now the completeness condition (every Cauchy sequence converges) is weaker than the usual completeness axiom (every bounded set has a supremum) for two reasons:

• The first reason is that one needs a weak form of the axiom of choice (namely every unbounded set contains an unbounded sequence) to obtain the completeness axiom from the Cauchy sequence condition. Note that adding this axiom only makes sense if we have a sort for (infinite) sets of reals.
• The second reason is that the sort Nat -> RealSequence may not contain all sequences of real numbers, since we do not have comprehension axioms (again, these would only make sense if we have sorts for higher types).

Still, one can show that each model of BasicReal is a subfield of the real numbers in ZFC. Moreover, we think that each such model contains all those real numbers that one needs in practice. And we can even show the (internal) uncountability of the reals (see below).

The limitation of BasicReal only shows up if one wants to carry out real analysis and prove e.g. theorems about integratable or differentiable functions. To overcome this limitation, we can either

• use a higher-order extension of CASL [HKBM98], where one has the full higher-order type system together with lambda-abstraction and comprehension axioms, which suffices to carry out real analysis, or
• specify set theory (usually, for foundations of mathematics, Zermelo-Fraenkel set theory with Choice (ZFC) is used), and then specify the reals within set theory

Both approaches have their pros and cons. Using higher-order CASL leads to shorter specifications, since the type system is already there (while it has to be constructed in ZFC). On the other hand, ZFC basically is a first-order theory³. However, ZFC cannot be directly specified in CASL since it contains comprehension, an axiom scheme which leads to infinitely many axioms.

If one takes Henkin general models⁴ as the semantics of higher-order CASL, the higher-order and the ZFC specification of the reals should roughly be equivalent - higher-order logic can be seen as just a typed variant of ZFC (perhaps ZFC has to be weakened somewhat to get an exact correspondence).

At the moment, we have refrained from extending our specification BasicReal with more sorts corresponding to sets of reals, functions on reals etc., since this would mean to mimick higher-order CASL within first-order CASL, and it is more convenient to directly work with higher-order CASL.

In order to combine our CASL specification BasicReal with the specification of reals in ZFC, it would be useful to define a view from DefineBasicReal to the specification of reals using ZFC. This would allow one to work in the language of BasicReal (which is more usable than that of ZFC), while one can still do all real analysis by moving to the specification of reals using ZFC whenever needed. A similar view can be defined from BasicReal to the specification of the reals in HOL (although it is convenient also to work directly with the reals in HOL).