Overview of holzfc Theories at X-Logic.org
Overview
The formalisation of ZFC in ProofPower HOL and its applications.
This document is a literate script containing the axiomatisation in ProofPower HOL of Zermelo-Fraenkel set theory.
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.
This document defines the concept of a pure function as a preliminary to introducing the type of pure functions.
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.

up quick index © RBJ

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