Go backward to References
Go up to Top
- 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.
- 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.
- See http://www.cl.cam.ac.uk/Research/HVG/Isabelle/library/ZF for a
specification of ZFC in Isabelle's first-order logic.
- 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].
- Due to the theorem of Löwenheim and Skolem, the
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.
- Note that this also holds for HOL with Henkin
denotes the set of natural numbers, Z the set of integers and
R the set of real numbers.
- In order
to obtain our notion of a floating-point system, we replaced the
original beta by b, and the original p by l.
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
Note: M-7 -- Version: 0.2 -- 13 April 1999.
Comments to firstname.lastname@example.org