Overview of holzfc Theories at X-Logic.org
Overview
 The formalisation of ZFC in ProofPower HOL and its applications.
 ZFC in HOL(1) This document is a literate script containing the axiomatisation in ProofPower HOL of Zermelo-Fraenkel set theory. ZFC in HOL(2) This document proves some elementary consequences of the ZFC axioms in HOL, and then introduces further definitions relating to the representation of functions in set theory. Listing of Theory zfc
 Pure Functions - definitions This document defines the concept of a pure function as a preliminary to introducing the type of pure functions. Listing of Theory pf
ZFC in HOL(1)
 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.
ZFC in HOL(2)
 This document proves some elementary consequences of the ZFC axioms in HOL, and then introduces further definitions relating to the representation of functions in set theory.
 Extensionality The principle of extensionality is more easily applied if it is expressed as an equation which can be used for rewriting. Union and Intersection In the introduction we do some preliminaries and introduce the new type of sets. Pairs After proving a theorem about when (un-ordered) pairs are equal we introduce ordered pairs, which are required for representing functions as graphs.
 Relations and Functions A relation is a set of ordered pairs, a function is a many-one relation. Domain Range and Field Empty Set Theorems Functional Abstraction, Abstraction and Extensionality In this section we define function application and functional abstraction, and show that functions are extensional.
Pure Functions - definitions
 This document defines the concept of a pure function as a preliminary to introducing the type of pure functions.
 The definition of a Pure Function Here we define and show the consistency of the concept of a "pure function".
 Application and Extensionality In this section we define function application and show that the pure functions are extensional. The Theory pf