Abstract
Fairly deep results of Zermelo-Frænkel (ZF) set theory have been mechanized using the proof assistant Isabelle. The results concern cardinal arithmetic and the Axiom of Choice (AC). A key result about cardinal multiplications is κ ⊗ κ=κ, where κ is any infinite cardinal. Proving this result required developing theories of orders, order-isomorphisms, order types, ordinal arithmetic, cardinals, etc.; this covers most of Kunen, Set Theory, Chapter I. Furthermore, we have proved the equivalence of 7 formulations of the Well-ordering Theorem and 20 formulations of AC; this covers the first two chapters of Rubin and Rubin, Equivalents of the Axiom of Choice, and involves highly technical material. The definitions used in the proofs are largely faithful in style to the original mathematics.
This is a preview of subscription content, log in via an institution to check access.
Similar content being viewed by others
Explore related subjects
Discover the latest articles, news and stories from top researchers in related subjects.References
Abrial, J. R. and Laffitte, G.: Towards the mechanization of the proofs of some classical theorems of set theory, Preprint, 1993.
Bancerek, Grzegorz: Countable sets and Hessenberg's theorem, Formalized Mathematics 2 (1990), 499–503. On the World Wide Web at http://math.uw.bialystok.pl/ ∼Form.-Math/Vol2/dvi/card_4.dvi.
Boyer, R. S. and Strother Moore, J.: A Computational Logic, Academic Press, 1979.
Boyer, R. S. and Strother Moore, J.: A Computational Logic Handbook, Academic Press, 1988.
Gilles Dowek: The Coq Proof Assistant User's Guide, Technical Report 154, INRIA-Rocquencourt, 1993.
Farmer, W. M., Guttman, J. D., and Thayer, J. F.: IMPS: An interactive mathematical proof system, J. Automated Reasoning 11(2) (1993), 213–248.
Gardner, M.: The Unexpected Hanging and Other Mathematical Diversions, University of Chicago Press, 1991.
Gordon, M. J. C. and Melham, T. F.: Introduction to HOL: A Theorem Proving Environment for Higher Order Logic, Cambridge University Press, 1993.
Halmos, P. R.: Naive Set Theory, Van Nostrand, 1960.
Huet, G.: Residual theory in λ-calculus: A formal development, Journal of Functional Programming 4(3) (1994), 371–394.
van Bentham Jutting, L. S.: Checking Landau's ‘Grundlagen’ in the AUTOMATH System, PhD thesis, Eindhoven University of Technology, 1977.
Kunen, K.: Set Theory: An Introduction to Independence Proofs, North-Holland, 1980.
Miller, D.: Unification under a mixed prefix, Journal of Symbolic Computation 14(4) (1992), 321–358.
Nederpelt, R. P., Geuvers, J. H., and de Vrijer, R. C.: Selected Papers on Automath, North-Holland, 1994.
Noël, Ph.: Experimenting with Isabelle in ZF set theory, J. Automated Reasoning 10(1) (1993), 15–58.
Paulson, L. C.: Constructing recursion operators in intuitionistic type theory, Journal of Symbolic Computation 2 (1986), 325–355.
Paulson, L. C.: Isabelle: The next 700 theorem provers, in P. Odifreddi (ed.), Logic and Computer Science, Academic Press, 1990, pp. 361–386.
Paulson, L. C.: Set theory for verification: I. From foundations to functions, J. Automated Reasoning 11(3) (1993), 353–389.
Paulson, L. C.: A fixedpoint approach to implementing (co)inductive definitions, in Alan Bundy (ed.), Automated Deduction — CADE-12, LNAI 814, Springer, 1994, pp. 148–161, 12th international conference.
Paulson, L. C.: Isabelle: A Generic Theorem Prover, LNCS 828, Springer, 1994.
Paulson, L. C.: Set theory for verification: II. Induction and recursion, J. Automated Reasoning 15(2) (1995), 167–215.
The QED manifesto: On the World Wide Web at http://www.mcs.anl.gov/home/lusk/qed/manifesto.html, 1995.
Art Quaife: Automated deduction in von Neumann-Bernays-Gödel set theory, J. Automated Reasoning 8(1) (1992), 91–147.
Rubin, H. and Rubin, J. E.: Equivalents of the Axiom of Choice, II, North-Holland, 1985.
Russinoff, D. M.: A mechanical proof of quadratic reciprocity, J. Automated Reasoning 8(1) (1992), 3–22.
Shankar, N.: Metamathematics, Machines, and Gödel's Proof, Cambridge University Press, 1994.
Suppes, P.: Axiomatic Set Theory, Dover, 1972.
Yu, Yuan: Computer proofs in group theory, J. Automated Reasoning 6(3) (1990), 251–286.
Author information
Authors and Affiliations
Rights and permissions
About this article
Cite this article
Paulson, L.C., Grabczewski, K. Mechanizing set theory. J Autom Reasoning 17, 291–323 (1996). https://doi.org/10.1007/BF00283132
Received:
Issue Date:
DOI: https://doi.org/10.1007/BF00283132