Footnotes

 

(1)

In a later version of this note, we plan to specify sequences separately. This allows us to specify infinite streams of arbitrary elements. However, the amount of sequences of streams available in a model may be limited. The more operations on elements we lift (to sequences), the more sequences we get.  

(2)

In a later version of this note we plan to split the specifications DefineBasicReal and BasicReal into smaller specifications, e.g. separate the part on polynomials.  

(3)

See http://www.cl.cam.ac.uk/Research/HVG/Isabelle/library/ZF for a specification of ZFC in Isabelle's first-order logic.  

(4)

A standard model semantics for higher-order logic is philosophically doubtful, since it relies, at the meta-level, on a "standard" model of set theory, and it is unclear what this should be; see study note [HKBM98].  

(5)

Due to the theorem of Löwenheim and Skolem, the first-order theory BasicReal has a countable model (this holds even for ZFC, the standard axiomatization of set theory). But this is besides the point here, since this kind of countability is an external one. Internally, that is, inside the model, the reals are always uncountable.  

(6)

Note that this also holds for HOL with Henkin semantics.  

(7)

N denotes the set of natural numbers, Z the set of integers and R the set of real numbers.  

(8)

In order to obtain our notion of a floating-point system, we replaced the original beta by b, and the original p by l.  

(9)

The notion of a rounding here is not the same as the one introduced in section 6.1. This is because the floating point systems of the IEEE standards do not include the values -infty and +infty. We don't know whether the IEEE standard follows some abstract mathematical rules comparable to our specification AbstractExecutableReal.