ZF: Zermelo-Fraenkel Set Theory
This directory contains the Standard ML sources of the Isabelle system for
ZF Set Theory. It is loaded upon FOL, not Pure Isabelle. Important files
include
ROOT.ML -- loads all source files. Enter an ML image containing FOL and
type: use "ROOT.ML";
Makefile -- compiles the files under Poly/ML or SML of New Jersey
IMP -- subdirectory containing a semantics equivalence proof between
operational and denotational definitions of a simple programming language.
To execute, enter an ML image containing ZF and type: use "IMP/ROOT.ML";
ex -- subdirectory containing examples. To execute them, enter an ML image
containing ZF and type: use "ex/ROOT.ML";
Isabelle/ZF formalizes the greater part of elementary set theory, including
relations, functions, injections, surjections, ordinals and cardinals.
Results proved include Cantor's Theorem, the Recursion Theorem, the
Schroeder-Bernstein Theorem, and (assuming AC) the Wellordering Theorem.
Isabelle/ZF also provides theories of lists, trees, etc., for formalizing
computational notions. It supports inductive definitions of
infinite-branching trees for any cardinality of branching.
Useful references for Isabelle/ZF:
Lawrence C. Paulson,
Set theory for verification: I. From foundations to functions.
J. Automated Reasoning 11 (1993), 353-389.
Lawrence C. Paulson,
Set theory for verification: II. Induction and recursion.
Report 312, Computer Lab (1993).
Lawrence C. Paulson,
A fixedpoint approach to implementing (co)inductive definitions.
In: A. Bundy (editor),
CADE-12: 12th International Conference on Automated Deduction,
(Springer LNAI 814, 1994), 148-161.
Useful references on ZF set theory:
Paul R. Halmos, Naive Set Theory (Van Nostrand, 1960)
Patrick Suppes, Axiomatic Set Theory (Dover, 1972)
Keith J. Devlin,
Fundamentals of Contemporary Set Theory (Springer, 1979)
Kenneth Kunen
Set Theory: An Introduction to Independence Proofs
(North-Holland, 1980)