Overview 



Introduction 


Membership 


Extensionality and WellFoundedness 



The Ontology Axiom 

Subsets
A subset s of t is a set all of whose members are also members of t.
 


ManyOne
The relations used in replacement must be "ManyOne" relations, otherwise the image may be larger than the domain, and Russell's
paradox would reappear.
This definition doesn't really belong here, it doesn't belong anywhere else either.


Galactic Ontology
We now specify with a single axiom the closure requirements which ensure that our universe is adequately populated.
The ontology axiom states that every set is a member of some galaxy which is transitive and closed under formation of powersets
and unions and under replacement.

PowerSets and Union 


Relational Replacement 

RelIm

Separation 

Consistency Proof
The specification which follows is introduced after proving that it is satisfied by a term involving the use of the Image function and the empty set. (This is no longer ideal, a "nicer" proof that separation is conservative is now obtainable from the primitive replacement axiom.) The basic idea is that a nonempty subset of any set, consisting of just those elements which satisfy a give property, can be shown to exist using Imagep. The required subset is obtained using a function which is the identity function on elements of the original which satisfy the property, and which maps the rest to an element selected from those that do by the choice function. A special case is made of the empty subset, which cannot be constructed from a nonempty set using "Imagep". Thus, separation is definable in terms of Imagep but the definition depends on the existence of the empty set and the axiom of choice. Using the more primitive replacement axiom the existence of the empty set The proof script is omitted (but is available in the source code to this page and is invoked as the theory is loaded). If I had formulated replacement in the more traditional manner, using a manyone relation rather than a (HOL) function, neither the axiom of choice not the empty set axiom would not have been necessary. It didn't occur to me at the time that there was a material difference! One day I will rework this with the relational replacement axiom, since the functional one would be definable. The consistency claim and the first step in the proof script showing the witness used to prove the claim are:


Definition
This higher order formulation of separation is accomplished by defining a new constant which takes a property of sets p and a set s and returns the subset of s consisting of those elements which satisfy p.
The definition uses the replacement principle, but since the image of a nonempty set cannot be empty a special case must
be made where the result is the empty set.
The HOL choice function is also used, making this defined version of separation dependent on the axiom of choice as well as
replacement.

Galaxies 




Functional Replacement 


Pair and Unit sets 




Union and Intersection 



Proof Context 




