ZFC in HOL
Overview
This document is a literate script containing the axiomatisation in ProofPower HOL of Zermelo-Fraenkel set theory.
What is the point of all this?
Why axiomatise ZFC in HOL (Higher Order Logic), and why use ProofPower?
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.
An axiom of well-foundedness is introduced in the form of the principle of Noetherian induction.
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.
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.
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.
The subset relation is defined and used in the powerset axiom, which asserts that the elements of the power set are the subsets.
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-holconst
z : 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)
);


up quick index © RBJ

$Id: holzfc1.xml,v 1.1.1.1 2000/12/04 17:24:40 rbjones Exp $