The Type GS
The sets under consideration will be the elements of a new type "GS" so the first thing we do is to introduce that new type.
GST is a pure wellfounded set theory, but is polymorphic in a type of psuedourelements.
This is intended to provide a greater level of integration between the set theory and the rest of the HOL type system.
In particular, it allows in principle for the use of set theory to build inductive types over other HOL types.
Since the theory will not be conservative, we make no attempt to relate the membership of "GS" to any of the types already available.
xlsml
open_theory "basic_hol";
force_new_theory "gstax";
force_new_pc "gstax";
merge_pcs ["xl_cs__conv"] "gstax";
set_merge_pcs ["basic_hol", "gstax"];
new_type ("GS", 1);


Membership
The most important constant is membership, which is a relation over the sets.
We can't define this constant (in this context) so it is introduced as a new constant (about which nothing is asserted except its name and type) and its properties are introduced axiomatically.


Psuedourelements
To provide for the psuedourelements we have an injection from an arbitrary HOL type whose range is the psuedourelements in the type of galactic sets.
Having fallen back from urelements to pseudourelements, the existence of this injection is all that remains, and in the context in which we are introducing the theory the injections exist whether we mention them or not, so its not wholly clear at this point whether it is buying us much.
However, though they exist, proving that they exist is non trivial, and the claim that they exist for arbitrary types is not expressible in HOL without the following axiom.
We now define the property of being a urelement, viz., that of being in the range of Pue:
As will be clear from the following, there is nothing special about pseudourelements, they are just sets and we don't know which sets they are.

The Set of Urelements
Thus far we have added very little (if any) in strength or risk, stating only that 'a GS is at least as large as 'a .
However for the purposes cited we really need there to be a set containing the urelements, which the following axiom asserts.
This implies that 'a GS is quite a bit larger than 'a , and we get a heirarchy of ever larger types as we iterate the GS type constructor.

