Prev Up Next
Go backward to 5.1 Proof of the Uncountability of the Reals
Go up to 5 More About the Specification BasicReal
Go forward to 5.3 The Specification of the Reals in Higher-Order CASL

5.2 The Categoricity of the Reals

A specification is said to be categorical or monomorphic, if it has exactly one model up to isomorphism. Neither the specification BasicReal nor the specifications of the reals in ZFC or HOL are categorical. Due to the theorem of Löwenheim and Skolem, a categorical axiomatization is impossible6. However, it is possible to prove the internal categoricity of the specification of the reals in ZFC (meaning that within each model of ZFC plus two axiomatizations of the reals, the two reals are isomorphic). A similar result should hold for the reals in HOL (but we are not entirely sure). BasicReal is definitely too weak for such a result, since there is not even an internalized notion of functions on reals.

CoFI Note: M-7 -- Version: 0.2 -- 13 April 1999.
Comments to

Prev Up Next