Introduction
Galactic set theory is a set theory with "galaxies" (previously known as "universes") axiomatised in Higher Order Logic.

Membership
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 and a psuedourelement injection.

Extensionality and WellFoundedness
The axioms of extensionality and wellfoundedness may be thought of as telling us what kind of thing a set is (later axioms
tell us how many of these sets are to be found in our domain of discourse).

The Ontology Axiom
Here we define the subset relation and assert the existence of powersets and unions.

PowerSets and Union
Here we define the powerset and union operators.

Replacement


Pair and Unit sets
Pair is defined using replacement, and Unit using Pair.

Separation
Separation is introduced by conservative extension.

Union and Intersection
Binary union and distributed and binary intersection are defined.

Galaxies
A Galaxy is a transitive set closed under powerset formation, union and replacement.
The Ontology axioms ensures that every set is a member of some galaxy.
Here we define a galaxy constructor and establish some of its properties.

Proof Context
To simplify subsequent proofs a new "proof context" is created enabling automatic use of the results now available.


