Abstract
Recent discussions in the Z community have considered the issue of the consistency of the free type construct in Z. A key question is whether free type definitions which met the criterion for consistency given in the Z Reference Manual, [5], are conservative over Zermelo set theory (i.e. ZF without the axiom of replacement). The main purpose of this paper is to give an introduction to the issues and to show that the answer to this question is “yes” (given the axiom of choice). A by-product of the arguments we give here is that the criterion given in the Z reference manual may be replaced by an intuitively simpler one without loss of expressive power from the theoretical or practical point of view.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
J. Barwise, editor. Handbook of Mathematical Logic, volume 90 of Studies in Logic and the Foundations of Mathematics. North Holland, 1977.
Kenneth Kunen. Set Theory: An Introduction to Independence Proofs. North Holland, 1980.
A. Smith. On Recursive Free Types in Z. RSRE Memorandum 91028. MOD PE, RSRE, 1991.
J.M. Spivey. Understanding Z. Cambridge University Press, 1988.
J.M. Spivey. The Z Notation: A Reference Manual Prentice-Hall, 1989.
The HOL System: Description. SRI International, 4 December 1989.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1992 British Computer Society
About this paper
Cite this paper
Arthan, R.D. (1992). On Free Type Definitions in Z. In: Nicholls, J.E. (eds) Z User Workshop, York 1991. Workshops in Computing. Springer, London. https://doi.org/10.1007/978-1-4471-3203-5_2
Download citation
DOI: https://doi.org/10.1007/978-1-4471-3203-5_2
Publisher Name: Springer, London
Print ISBN: 978-3-540-19780-5
Online ISBN: 978-1-4471-3203-5
eBook Packages: Springer Book Archive