Axioms for galactic set theory.
Overview
 An axiomatisation in Higher Order Logic of a well-founded set theory with pseudo-urelements and galaxies.
 Introduction Galactic set theory is a set theory with "galaxies" (previously known as universes) and "pseudo-urelements" (previously unknown, so far as I know) axiomatised in Higher Order Logic. Membership and Pseudo-urelements 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 psuedo-urelement injection. Extensionality and Well-foundedness The axioms of extensionality and well-foundedness 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. Listing of Theory gst-ax
Introduction
 Galactic set theory is a set theory with "galaxies" (previously known as universes) and "pseudo-urelements" (previously unknown, so far as I know) axiomatised in Higher Order Logic.
 Scope This document is mainly concerned with the axioms of galactic set theory, but includes in addition some definitions and theorems which might easily have been part of the axiomatisation. In the usual first order axiomatisations of set theory, for example, the pair constructor is introduced axiomatically. In this axiomatisation neither unit not pair are primitive, they are introduced by definition once the axioms have been presented. Same goes for separation and intersection. The theory "gst-ax" created by this document, consists of an axiomatic development of a well-founded set theory in ProofPower HOL, and is created as a child of "basic-hol". Placing it at this level makes it possible to use the standard symbols for set theory (which are already in use at the level of the theory "hol"). Why Galactic? This document introduces Galactic Set Theory, which is similar to what has elsewhere been called Universal Set Theory (e.g. by Paul M. Cohn in his "Universal Algebra", but I dare say it came from somewhere else). The "universes" in Cohn, and the galaxies here are mostly models of ZFC, except the smallest in which there is no infinite set. The two other main differences are that galactic set theory is formulated in higher order logic and that it is polymorphic in a type of psuedo-urelements.
 What's a Psuedo-urelement? I started out trying a set theory with urelements since this makes for better integration between the set theory and the rest of the HOL type system. A urelement is something in the domain of discourse in addition to the pure sets (which are constructed from the empty set). The idea was to make possible the use of the set theory for constructing new HOL type constructors , i.e to allow that in the sets are values taken from other types. However, while I was deliberating about how to minimise the additional complications which arise in developing a set theory with urelements, I realised that I could have my cake and eat it. Its not necessary to have extra things, an injection into the already available sets suffices. Even with the urelements we only get a one-one correspondence between the notional type of these urelements and the corresponding objects in the set theory, which is really a bit like an encoding of the type into the sets. We can have such an encoding without having any extra elements at all, and hence while retaining a completely pure well-founded set theory. I don't know of any reason why we need to have extra elements. So I call these things pseudo-urelements, since they look a bit like urelements, and they serve purposes for which I had thought to use urelements, but in fact its a sham, they're just regular sets.
Membership and Pseudo-urelements
 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 psuedo-urelement injection.
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 well-founded set theory, but is polymorphic in a type of psuedo-urelements. 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.
 xl-sml open_theory "basic_hol"; force_new_theory "gst-ax"; force_new_pc "gst-ax"; merge_pcs ["xl_cs__conv"] "gst-ax"; set_merge_pcs ["basic_hol", "gst-ax"]; 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.
 xl-sml new_const ("", 'a GS'a GSBOOL); declare_infix (230,"");

Psuedo-urelements
To provide for the psuedo-urelements we have an injection from an arbitrary HOL type whose range is the psuedo-urelements in the type of galactic sets. Having fallen back from urelements to pseudo-urelements, 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.
 xl-sml new_const ("Pue", 'a 'a GS); val Pue_inj_axiom = new_axiom (["Pue_inj_axiom"], OneOne Pue);

We now define the property of being a urelement, viz., that of being in the range of Pue:
 xl-holconstIsPue : 'a GS BOOL s IsPue s = t Pue t = s
As will be clear from the following, there is nothing special about pseudo-urelements, 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.
 xl-sml new_const ("PueSet", 'a GS); val PueSet_axiom = new_axiom (["PueSet_axiom"], e e PueSet IsPue e);

Extensionality and Well-foundedness
 The axioms of extensionality and well-foundedness 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).
Extensionality
The most fundamental property of membership (or is it of sets?) is extensionality, which tells us what kind of thing a set is. The axiom tells us that if two sets have the same elements then they are in fact the same set.
 xl-sml val gs_ext_axiom = new_axiom (["gs_ext_axiom"], s t:'a GS s = t e e s e t);

It follows from the definitions of IsPue and IsSet and ue_inj_axiom that nothing is both a set and a urelement, and that urelements are equal iff the values from which they were obtained under Pue are equal.
Well-Foundedness
The axiom of well-foundedness asserts the requirement that the elements of ('a)GS are a subset of the cumulative heirarchy of sets formed by iteration of set formation beginning with the empty set. The principle is expressed here as a principle of noetherian induction.
 xl-sml val gs_wf_axiom = new_axiom (["gs_wf_axiom"], p:'a GSBOOL (s (e e s p e) p s) (s p s) );

The remaining axioms are intended to ensure that the subset is a large and well-rounded subset of the cumulative heirarchy. This is to be accomplished by defining a Galaxy as a set satisfying certain closure properties and then asserting that every set is a member of some Galaxy. It is convenient to introduce new constants and axioms for each of the Galactic closure properties before asserting the existence of the Galaxies.
Subsets, PowerSets and Union
 Here we define the subset relation and assert the existence of powersets and unions.
Subsets
A subset s of t is a set all of whose members are also members of t.
 xl-sml declare_infix (230,"");

 xl-holconst\$ : 'a GS 'a GS BOOL s t s t e e s e t
PowerSets

 xl-sml new_const ("", 'a GS'a GS); val _axiom = new_axiom (["_axiom"], s t:'a GS t s t s );

Note that the power set of a urelement is the empty set.
Union

 xl-sml new_const ("", 'a GS'a GS); val _axiom = new_axiom (["_axiom"], s t:'a GS t s e e s t e );

 xl-sml val _thm = get_spec \$; val _eq_thm = save_thm ("_eq_thm", prove_rule [get_spec \$, gs_ext_axiom] A B A = B A B B A); val _refl_thm =save_thm ("_refl_thm", prove_rule [get_spec \$] A A A); val _thm = save_thm ("_thm", prove_rule [get_spec \$] e A B e A A B e B); val _trans_thm = save_thm ("_trans_thm", prove_rule [get_spec \$] A B C A B B C A C); val _thm = save_thm ("_thm", prove_rule [_axiom, _thm] s t:'a GS t s t s);

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.
Introduction

Though a functional formulation of replacement is most convenient for most applications, it has a number of small disadvantages which have persuaded my to stay closer to the traditional formulation of replacement in terms of relations. The more convenient functional version will then be introduced by definition (so if you don't know what I'm talking about, look forward to compare the two versions).

For the record the disadvantages of the functional one (if used as an axiom) are:
1. It can't be used to prove the existence of the empty set.
2. When used to define separation it requires the axiom of choice.
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.
 xl-holconstManyOne : ('a 'b BOOL) BOOL r ManyOne r x y z r x y r x z y = z
Replacement
Since the primitive relational version of replacement will rarely be used I depart from my usual practice by not introducing the axiom with a new constant.
 xl-sml val Replacement_axiom = new_axiom (["Replacement_axiom"], (r:'a GS 'a GS BOOL) s ManyOne r t u u t v v s r v u );

The Empty Set
We can now prove that there is an empty set as follows:
 xl-sml set_goal([], s s ); a (strip_asm_tac (list__elim [x y:'a GS F, s:'a GS T] Replacement_axiom)); (* *** Goal "1" *** *) a (all_asm_ante_tac THEN prove_tac[get_specManyOne]); (* *** Goal "2" *** *) a (_tac t THEN asm_prove_tac[]); xl_set_cs__thm (pop_thm ());

So we define as the empty set:
 xl-holconst : 'a GS s s
Image
Now we prove a more convenient version of replacement which takes a HOL function rather than a relation as its argument. It states that the image of any set under a function is also a set.
 xl-sml set_goal([],Image f:'a GS 'a GS s: 'a GS (x x Image f s e e s x = f e)); a (strip_asm_tac Replacement_axiom); a (_tac g s t u u t ( v v s (i o o = g i) v u) THEN rewrite_tac[]); a (REPEAT _tac THEN all__tac THEN_TRY asm_rewrite_tac[]); a (lemma_tac w w = v u u = f v THEN1 prove__tac); a (spec_nth_asm_tac 2 w); a (lemma_tac ManyOne w THEN1 asm_rewrite_tac [get_spec ManyOne]); a (REPEAT strip_tac THEN asm_rewrite_tac[]); a (spec_nth_asm_tac 2 s); a (_tac t THEN DROP_NTH_ASM_T 1 ante_tac THEN asm_rewrite_tac[get_spec ManyOne]); xl_set_cs__thm (pop_thm ());

"Image f s" is the image of s under f.
 xl-holconstImage : ('a GS 'a GS) 'a GS 'a GS f s x x Image f s e e s x = f e
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.
Existence of Galaxies
Asserting the existence of galaxies falls in the middle ground between an axiom of infinity and a large cardinal axiom. Without it we would be no stronger than Zermelo set theory, with it we are stronger than ZFC.
 xl-sml new_const ("Galaxy", 'a GS'a GS); val Galaxy_axiom = new_axiom (["Galaxy_axiom"], s s Galaxy s t t Galaxy s t Galaxy s t Galaxy s t Galaxy s f Image f t Galaxy s Image f t Galaxy s );

Pair and Unit sets
 Pair is defined using replacement (!), and Unit using Pair.
Pair
Pairs can be defined as the image of some two element set under a function defined by a conditional. A suitable two element set can be constructed from the empty set using the powerset construction a couple of times. However, having proven that this can be done (details omitted), we can introduce the pair constructor by conservative extension as follows. (the ProofPower tool shows that it has accepted my proof by putting this extension into the "definitions" section of the theory listing).
 xl-holconstPair : 'a GS 'a GS 'a GS s t e:'a GS e Pair s t e = s e = t
Pair equality theorem
Extensional proofs about equality of pairs are simplified by the following principle.
 xl-sml set_goal([],s t u v Pair s t = Pair u v s = u t = v s = v t = u); a (prove_tac[ _elim Pair s t gs_ext_axiom, get_spec Pair]); (* *** Goal "1" *** *) a (spec_nth_asm_tac 2 u THEN_TRY all_var_elim_asm_tac THEN_TRY asm_rewrite_tac[]); (* *** Goal "2" *** *) a (spec_nth_asm_tac 2 v THEN_TRY all_var_elim_asm_tac THEN_TRY asm_rewrite_tac[]); val Pair_eq_thm = save_pop_thm "Pair_eq_thm";

Unit definition

 xl-holconstUnit : 'a GS 'a GS s Unit s = Pair s s
Unit extension theorem
The following theorem tells you what the members of a unit sets are.
 xl-sml set_goal([],s e e Unit s e = s); a (prove_tac [ get_specUnit, get_specPair]); val Unit_thm = pop_thm (); add_pc_thms "gst-ax" [get_spec Pair, Unit_thm]; set_merge_pcs ["basic_hol", "gst-ax"];

Unit equality theorem
The following theorem tells you when two unit sets are equal.
 xl-sml set_goal([],s t Unit s = Unit t s = t); a (prove_tac [ _elim Unit s gs_ext_axiom]); val Unit_eq_thm = pop_thm (); add_pc_thms "gst-ax" [Unit_eq_thm]; set_merge_pcs ["basic_hol", "gst-ax"];

Unit-Pair equations
The following theorems tell you when Pairs are really Units.
 xl-sml set_goal([], s t u Unit s = Pair t u s = t s = u); a (prove_tac [ _elim Unit s gs_ext_axiom]); (* *** Goal "1" *** *) a (spec_nth_asm_tac 1 s THEN spec_nth_asm_tac 2 t THEN_TRY all_var_elim_asm_tac THEN_TRY rewrite_tac[]); (* *** Goal "2" *** *) a (spec_nth_asm_tac 1 u THEN_TRY all_var_elim_asm_tac THEN_TRY rewrite_tac[]); val Unit_Pair_eq_thm = pop_thm ();

 xl-sml set_goal([],s t u Pair s t = Unit u s = u t = u); a (prove_tac [ _elim Pair s t gs_ext_axiom]); val Pair_Unit_eq_thm = pop_thm ();

Separation
 Separation is introducted by conservative extension.
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 non-empty subset of any set, consisting of just those elements which satisfy a give property, can be shown to exist using Image. 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 non-empty set using "Image". Thus, separation is definable in terms of Image 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 many-one 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:

 xl-sml set_goal([],Sep s p e e (Sep s p) e s p e ); a (_tac s p if x x s p x then Image (y if p y then y else x x s p x) s else THEN rewrite_tac[] THEN REPEAT _tac);

(rest of proof script not presented)
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 non-empty 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.
 xl-holconstSep : 'a GS ('a GS BOOL) 'a GS s p e e (Sep s p) e s p e

 xl-sml val Sep_thm = get_spec Sep; add_pc_thms "gst-ax" [Sep_thm]; set_merge_pcs ["basic_hol", "gst-ax"];

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

 xl-holconst\$ : 'a GS 'a GS 'a GS s t e e (s t) e s e t

 xl-sml val _thm = get_spec \$; val _thm = save_thm ("_thm", prove_rule [_thm, _thm] A B A A B B A B); val _thm1 = save_thm ("_thm1", prove_rule [_thm, _thm] A B C A C B C A B C); val _thm2 = save_thm ("_thm2", prove_rule [_thm, _thm] A B C D A C B D (A B) (C D));

Distributed Intersection
Distributed intersection doesn't really make sense for the empty set, but under this definition it maps the empty set onto itself.
 xl-holconst : 'a GS 'a GS s s = Sep ( s) (x t t s x t)
Extensional Intersection Theorem

 xl-sml set_goal ([],x s e x s (e s y y s e y)); a (prove_tac [ get_spec ]); val _thm = save_pop_thm "_thm";

 xl-sml set_goal([],s t s t t s); a (rewrite_tac [_thm, _thm]); a (REPEAT strip_tac); a (REPEAT (asm_fc_tac[_thm])); val _thm = save_pop_thm "_thm"; val _thm = save_thm ("_thm", (prove_rule [_thm, gs_ext_axiom, get_spec \$] A B A B C (D D B C D) C B));

Binary Intersection
Binary intersection could be defined in terms of distributed intersection, but its easier not to.
 xl-sml declare_infix (240, "");

 xl-holconst\$ : 'a GS 'a GS 'a GS s t s t = Sep s (x x t)
Extensional Binary Intersection Theorem

 xl-sml set_goal ([],s t e e s t e s e t); a (prove_tac [ get_spec \$]); val _thm = save_thm ("_thm", prove_rule [get_spec \$] s t ee s t e s e t); val _thm = save_thm ("_thm", prove_rule [_thm, _thm] A B A B A A B B); val _thm1 = save_thm ("_thm1", prove_rule [_thm, _thm] A B C A C B C A B C); val _thm2 = save_thm ("_thm2", prove_rule [_thm, _thm] A B C D A C B D (A B) (C D)); val _thm3 = save_thm ("_thm3", prove_rule [_thm, _thm] A B C C A C B C A B);

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

The only principle I know of which assists with elementary proofs in set theory is the principle that set theoretic conjectures can be reduced to the predicate calculus by using extensional rules for relations and for operators.

Too hasty a reduction can be overkill and may convert a simple conjecture into an unintelligible morass. We have sometimes in the past used made available two proof contexts, an aggressive extensional one, and a milder non-extensional one. However, the extensional rules for the operators are fairly harmless, expansion is triggered by the extensional rules for the relations (equality and subset), so a proof context containing the former together with a suitable theorem for the latter gives good control.

Theorems Used Recklessly
This is pretty much guesswork, only time will tell whether this is the best collection.
 xl-sml val gst_ax_thms = [ _spec, _axiom, _axiom, Image_spec, Pair_eq_thm, get_spec Pair, Unit_eq_thm, Unit_thm, Pair_Unit_eq_thm, Unit_Pair_eq_thm, Sep_thm, _thm, _thm ]; val gst_opext_clauses = (all__intro o list__intro o (map all__elim)) gst_ax_thms; save_thm ("gst_opext_clauses", gst_opext_clauses);

Theorems Used Cautiously
The following theorems are too aggressive for general use in the proof context but are needed when attempting automatic proof. When an extensional proof is appropriate it can be initiated by a cautious (i.e. a "once") rewrite using the following clauses, after which the extensional rules in the proof context will be triggered.
 xl-sml val gst_relext_clauses = (all__intro o list__intro o (map all__elim)) [gs_ext_axiom, get_spec\$]; save_thm ("gst_relext_clauses", gst_relext_clauses);

There are a number of important theorems, such as well-foundedness and galaxy closure which have not been mentioned in this context. The character of these theorems makes them unsuitable for the proof context, their application requires thought.
Automatic Proof
The basic proof automation is augmented by adding a preliminary rewrite with the relational extensionality clauses.
 xl-sml fun gst_ax_prove_conv thl = TRY_C (pure_rewrite_conv [gst_relext_clauses]) THEN_C (basic_prove_conv thl);

Proof Context gst-ax

 xl-sml add_rw_thms gst_ax_thms "gst-ax"; add_sc_thms gst_ax_thms "gst-ax"; add_st_thms gst_ax_thms "gst-ax"; set_pr_conv gst_ax_prove_conv "gst-ax"; set_pr_tac (conv_tac o gst_ax_prove_conv) "gst-ax"; commit_pc "gst-ax";

Using the proof context "gst-ax" elementary results in gst are now provable automatically on demand. For this reason it is not necessary to prove in advance of needing them results such as the associativity of intersection, since they can be proven when required by an expression of the form "prove rule[] term" which proves term and returns it as a theorem. If the required proof context for doing this is not in place the form "merge_pcs_rule ["basic_hol", gst-ax"] (prove_rule []) term" may be used. Since this is a little cumbersome we define the function "gst_ax_rule" and illustrate its use as follows:

 xl-sml val gst_ax_rule = (merge_pcs_rule1 ["basic_hol", "gst-ax"] prove_rule) []; val gst_ax_conv = MERGE_PCS_C1 ["basic_hol", "gst-ax"] prove_conv; val gst_ax_tac = conv_tac o gst_ax_conv;

Examples
The following are examples of the elementary results which are now proven automatically:
 xl-sml gst_ax_rule a (b c) = (a b) c; gst_ax_rule a b b; gst_ax_rule b = b; gst_ax_rule a b c d a c b d; gst_ax_rule Sep b p b; gst_ax_rule a b Image f a Image f b;