Introduction
Galactic set theory is a set theory with "galaxies" (previously known as universes) and "pseudourelements" (previously unknown, so far as I know) axiomatised in Higher Order Logic.

Membership and Pseudourelements
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).

Subsets, PowerSets and Union
Here we define the subset relation and assert the existence of powersets and unions.

Replacement
The replacement axiom embodies the "limitation of size" principle (or its converse) by stating that any collection which is no larger than a known set is also a set.


Galaxies
A Galaxy is a transitive set closed under powerset formation, union and replacement.
We assert that everything (of type GS) is a member of a Galaxy.

Pair and Unit sets
Pair is defined using replacement (!), and Unit using Pair.

Separation
Separation is introducted by conservative extension.

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

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


