ZFC in HOL
Overview
 This document is a literate script containing the axiomatisation in ProofPower HOL of Zermelo-Fraenkel set theory.
 Introduction What is the point of all this? HOL and ProofPower Why axiomatise ZFC in HOL (Higher Order Logic), and why use ProofPower? Membership and Extensionality The first thing we do is to introduce a new ProofPower theory and, in that theory, the new TYPE SET together with the membership relation, which we use to assert the extensionality of sets. Well Foundedness An axiom of well-foundedness is introduced in the form of the principle of Noetherian induction.
 The Cumulative Hierarchy We have now characterised our subject matter as a heirarchy of well-founded sets. The remaining axioms serve to place a lower bound on how many of these well-founded sets exist. The Empty Set and Separation There exists a set containing no members, and for any set s and property p there exists a set containing just those members of s which satisfy p. Pairing and Union For any two sets there is a set whose members are just those two sets. For any set of sets there is a set whose members are all the members of the sets. Subset, Powerset and Choice The subset relation is defined and used in the powerset axiom, which asserts that the elements of the power set are the subsets. Replacement Any collection of sets which is smaller than a set is itself a set.
Introduction
 What is the point of all this?
HOL and ProofPower
 Why axiomatise ZFC in HOL (Higher Order Logic), and why use ProofPower?
Membership and Extensionality
 The first thing we do is to introduce a new ProofPower theory and, in that theory, the new TYPE SET together with the membership relation, which we use to assert the extensionality of sets.
The theory "zfc", in which we propose to axiomatise set theory, is created as a child of "hol". The sets under consideration will be the elements of a new type "SET" so the first thing we do is to introduce that new type. Since the theory will not be conservative, we make no attempt to relate the membership of "SET" to any of the types already available.
The Type of SETS

 xl-sml open_theory "hol"; set_pc "hol"; force_delete_theory "zfc" handle _ => (); new_theory "zfc"; new_type ("SETz", 0);

Membership
The most important constant is membership, which is a relation over the sets. We can't define this constant (in this context) so it is introduced as a new constant (about which nothing is asserted except its name and type) and its properties are introduced axiomatically.
 xl-sml new_const ("z", SETzSETzBOOL); declare_infix (230,"z");

Extensionality
The most fundamental property of membership (or is it of sets?) is extensionality, which tells us what kind of thing a set is. The axiom tells us that if two sets have the same elements then they are in fact the same set.
 xl-sml val ext_axiom = new_axiom (["ext_axiom"], s t:SETz (u:SETz u z s u z t) s=t );

Well Foundedness
 An axiom of well-foundedness is introduced in the form of the principle of Noetherian induction.
 Noetherian Induction In the intuition behind classical set theory, a heirarchy of sets is built up from the empty set by an iterative process in each stage of which new sets are formed from sets formed at earlier stages in the process. This intuition makes us comfortable to assert the non-existence of problematic sets whose existence may lead to paradox. Since this intuition is an important element in our confidence that set theory is consistent, it is natural to want to see this stated in the axioms (even though we may not need to know this to make use of the theory, and even though adding an axiom can only increase the risk of inconsistency). In first-order axiomatisations of ZFC well foundedness is expressed by asserting that every set s has a member which is disjoint from s. This formulation has two disadvantages. The first is that the connection between this axiom and well-foundedness may not be obvious to all. The second is that it doesn't guarantee well-foundedness.

Here we assert well-foundedness using the principle of noetherian induction, which relates more directly to the intuition behind the cumulative heirarchy, since it asserts in effect, that any property which is is inherited through this process is true of all sets.

In first order logic this has the disadvantage that it can only be expressed using an axiom scheme, and this scheme fails to guarantee well-foundedness. In higher order logic the principle can be expressed as a single axiom, which under the standard semantics suffices to guarantee well-foundedness.

 xl-sml val wf_axiom = new_axiom ( ["wf_axiom"], p:SETzBOOL (s:SETz (e:SETz e z s p e) p s) s:SETz p s );

The Cumulative Hierarchy
 We have now characterised our subject matter as a heirarchy of well-founded sets. The remaining axioms serve to place a lower bound on how many of these well-founded sets exist.
The Empty Set and Separation
 There exists a set containing no members, and for any set s and property p there exists a set containing just those members of s which satisfy p.
Separation

 xl-sml new_const ("Sepz", (SETzBOOL)SETzSETz); val separation_axiom = new_axiom ( ["separation_axiom"], p:SETzBOOL; s:SETz (u:SETz u z Sepz p s u z s p u) );

The Empty Set
In the first order formulation an axiom may be used for introducing the empty set, for though it is definable from any other set by separation, and thought there must be a set, there may not be description operator to facilitate the definition. In our Higher Order Logic we can use the choice operator (the semantics of which is incidental, definite description would have done just as well).
 xl-holconstz : SETz z = Sepz (eF) (sT)

 xl-sml (* new_const ("z", SETz); val z_axiom = new_axiom ( ["z_axiom"], *) set_goal([], s:SETz s z z); a (prove_tac [get_specz, separation_axiom]); val z_thm = save_pop_thm "z_thm";

Pairing and Union
 For any two sets there is a set whose members are just those two sets. For any set of sets there is a set whose members are all the members of the sets.
Pairing

 xl-sml new_const ("Pair", SETzSETzSETz); val pair_axiom = new_axiom ( ["pair_axiom"], s t u:SETz u z Pair s t u = s u = t );

Union
This is the distributed union operator which takes a set of sets and forms the union of them all
 xl-sml new_const ("z", SETzSETz); val z_axiom = new_axiom ( ["z_axiom"], s u:SETz u z (z s) v u z v v z s );

Subset, Powerset and Choice
 The subset relation is defined and used in the powerset axiom, which asserts that the elements of the power set are the subsets.
Subset

 xl-sml declare_infix (230,"z");

 xl-holconst \$z : SETzSETzBOOL s t s z t = u u z s u z t
The Power Set

 xl-sml new_const ("z", SETzSETz); val z_axiom = new_axiom ( ["z_axiom"], s u:SETz u z z s u z s );

Choice
An axiom of choice is already present in higher order logic. Using this axiom the principle of choice in set theory can be derived and does not therefore need to be asserted as an axiom.
Replacement
 Any collection of sets which is smaller than a set is itself a set.
 The Axiom of Replacement In a first order formulation the axiom of replacement is an axiom schema in which a formula is used to express a relationship, which is required to be functional (so that its range is no larger than its domain). In higher order logic the statement of the principle is simplified, a schema is not required, and the type system permits us to quantify over functions without explicitly stating the many-one requirement. Semantically the axiom is stronger, (assuming standard semantics for hol), since the axiom speaks of all functions, not just those which can be captured in a first order formula.

 xl-sml new_const ("RImage", (SETzSETz)SETzSETz); val replacement_axiom = new_axiom (["replacement_axiom"], f:SETzSETz; s:SETz (u:SETz u z (RImage f s) v v z s u = f v) );