Axioms for galactic set theory.
Overview
An axiomatisation in Higher Order Logic of a well-founded set theory with galaxies.
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 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).
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.
Listing of Theory gst-ax
Introduction
Galactic set theory is a set theory with "galaxies" (previously known as "universes") 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 the empty set nor 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". This version of the theory is derived from a previous version in which "pseudo-urelements" were available, and in which the standard set theoretic vocabulary was used (which rendered the theory unusable in combination with the usual ProofPower HOL theory of sets). Pseudo-urelements were dropped because I don't need them, and, however slight the complication they introduce, its not necessary. To enable this theory to be used with the standard set theory (properties in set theoretic clothing) the volcabulary has been systematically subscripted with "g" (for galactic).
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 other main difference is that galactic set theory is formulated 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 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. 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";
new_parent "wf_relp";
force_new_pc "gst-ax";
merge_pcs ["xl_cs__conv"] "gst-ax";
set_merge_pcs ["basic_hol", "gst-ax"];
new_type ("GS", 0);

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 ("g", GSGSBOOL);
declare_infix (230,"g");

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:GS
s = t e e g s e g 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.
xl-sml
val gs_wf_axiom =
new_axiom (["gs_wf_axiom"],
well_founded $g
);

The form in which we have stated the axiom is not very informative and so the more usual formulation is immediately derived as a theorem.
xl-sml
val gs_wf_min_thm = save_thm ("gs_wf_min_thm",
(_elim (_elim $g wf_min_thm) gs_wf_axiom));

We also save the axiom expanded out as an explicit induction theorem.
xl-sml
val gs_wf_ind_thm = save_thm ("gs_wf_ind_thm",
(rewrite_rule [get_spec well_founded] gs_wf_axiom));

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.
The Ontology Axiom
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,"g");


xl-holconst
$g : GS GS BOOL
s t s g t
e e g s e g t

xl-sml
val g_thm = get_spec $g;
val g_eq_thm = save_thm ("g_eq_thm",
prove_rule [get_spec $g, gs_ext_axiom]
A B A = B A g B B g A);
val g_refl_thm = save_thm ("g_refl_thm",
prove_rule [get_spec $g]
A A g A);
val gg_thm = save_thm ("gg_thm",
prove_rule [get_spec $g]
e A B e g A A g B e g B);
val g_trans_thm = save_thm ("g_trans_thm",
prove_rule [get_spec $g]
A B C A g B B g C A g C);

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-holconst
ManyOne : ('a 'b BOOL) BOOL
r ManyOne r x y z r x y r x z y = z
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.
xl-sml
val Ontology_axiom =
new_axiom (["Ontology_axiom"],
s
g s g g

t t g g t g g
(p (v v g p v g t) p g g)
(u (v v g u w v g w w g t) u g g)
(rel ManyOne rel
(r (v v g r w w g t rel w v)
(r g g r g g)))
);

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

xl-sml
set_goal([], g s t:GS t g g s t g s);
a (prove__tac THEN strip_tac);
a (strip_asm_tac (_elim s' (Ontology_axiom)));
a (spec_nth_asm_tac 1 s');
a (_tac p THEN asm_rewrite_tac[]);
xl_set_cs__thm (pop_thm ());


xl-holconst
╷ g: GS GS
╷ s t:GS t g g s t g s
Union

xl-sml
set_goal([],g s t t g g s e t g e e g s);
a (prove__tac THEN strip_tac);
a (strip_asm_tac (_elim s' Ontology_axiom));
a (spec_nth_asm_tac 1 s');
a (_tac u THEN asm_rewrite_tac[]);
xl_set_cs__thm (pop_thm ());


xl-holconst
╷ g: GS GS
╷ s t t g g s e t g e e g s

xl-sml
val gg_thm = save_thm ("gg_thm",
prove_rule [get_spec g, g_thm]
s t:GS t g s t g g s);

Relational Replacement
The constant RelIm is defined for relational replacement.
RelIm

xl-sml
set_goal([],RelIm rel s t ManyOne rel (t g RelIm rel s e e g s rel e t));
a (prove__tac THEN REPEAT strip_tac);
a (strip_asm_tac (_elim s' Ontology_axiom));
a (spec_nth_asm_tac 1 s');
a (spec_nth_asm_tac 1 rel');
a (asm_rewrite_tac[]);
a (_tac r THEN strip_tac THEN strip_tac THEN asm_rewrite_tac[]);
a (_tac r THEN strip_tac THEN strip_tac THEN asm_rewrite_tac[]);
xl_set_cs__thm (pop_thm ());


xl-holconst
╷ RelIm: (GS GS BOOL) GS GS
╷ rel s t ManyOne rel (t g RelIm rel s e e g s rel e t)
Separation
Separation is introduced 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 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 non-empty 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 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
fun _FC_T tac thm = GET_ASMS_T
(tac o (fc_rule (fc__canon thm)));
set_goal([],Sep s p e
e g (Sep s p) e g s p e
);
a (prove__tac THEN REPEAT strip_tac);
a (strip_asm_tac (list__elim [s'] (Ontology_axiom)));
a (lemma_tac rel rel = x y p' x y = x
THEN1 prove__tac);
a (lemma_tac ManyOne rel
THEN1 asm_rewrite_tac [get_spec ManyOne rel]);
(* *** Goal "1" *** *)
a (REPEAT strip_tac THEN asm_rewrite_tac[]);
(* *** Goal "2" *** *)
a (_tac RelIm rel s');
a (_FC_T asm_rewrite_tac (get_spec RelIm));
a (prove_tac[]);
xl_set_cs__thm (pop_thm());

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-holconst
Sep : GS (GS BOOL) GS
s p e e g (Sep s p) e g s p e

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

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.
Definition of Galaxy
First we define the property of being a galaxy.
xl-holconst
╷ galaxy: GS BOOL
s
galaxy s (x x g s)
t t g s
t g s
g t g s
g t g s
(rel ManyOne rel
RelIm rel t g s
RelIm rel t g s)

xl-gft
galaxies__thm =
s g s g g galaxy g

Definition of Gx
Gx is a function which maps each set onto its smallest enclosing galaxy.
xl-holconst
╷ Gx: GS GS
╷ s t t g Gx s g galaxy g s g g t g g

xl-tex
Each set is in its smallest enclosing galaxy, which is of course a galaxy and is contained in any other galaxy of which that set is a member:


xl-gft
t_in_Gx_t_thm =
t t g Gx t
galaxy_Gx =
s galaxy (Gx s)
Gx_g_galaxy =
s g galaxy g s g g (Gx s) g g

Galaxy Closure
The galaxy axiom asserts that a Galaxy is transitive and closed under construction of powersets, distributed union and replacement. Galaxies are also closed under most other ways of constructing sets, and we need to demonstrate these facts systematically as the theory is developed.
xl-holconst
transitive : GS BOOL
s transitive s e e g s e g s

xl-gft
GalaxiesTransitive_thm =
s galaxy s transitive s
GCloseSep =
g galaxy g s s g g p Sep s p g g
Gx_transitive_thm =
s transitive (Gx s)
Gx_mono_thm =
s t s g t Gx s g Gx t
Gx_mono_thm2 =
s t s g t Gx s g Gx t
t_sub_Gx_t_thm =
t t g Gx t
Gx_mono_thm3 =
s t s g t s g Gx t
Gx_trans_thm2 =
s t s g t s g Gx t
Gx_trans_thm3 =
s t u s g t t g Gx u s g Gx u

The Empty Set
We can now prove that there is an empty set as follows:
xl-sml
set_goal([], g s s g g);
a (_tac Sep (s:GS T) (x:GS F)
THEN rewrite_tac [get_specSep]);
xl_set_cs__thm (pop_thm ());

So we define g as the empty set:
xl-holconst
g : GS
s s g g
and the empty set is a member of every galaxy:
xl-sml
set_goal([],g galaxy g g g g);
a (REPEAT strip_tac);
a (fc_tac [GCloseSep, get_spec galaxy]);
a (list_spec_nth_asm_tac 1 [x,x:GS F]);
a (lemma_tac g = Sep x ( x F)
THEN1 (rewrite_tac [gs_ext_axiom, get_spec g, get_spec Sep]));
a (asm_rewrite_tac[]);
val GgC = save_pop_thm "GgC";


xl-sml
val gg_thm = save_thm ("gg_thm",
prove_rule [get_spec g, g_thm]
s:GS g g t);
val gg_thm = save_thm ("gg_thm",
prove_rule [get_spec g, get_spec g, gs_ext_axiom]
g g = g);
val g_spec = get_spec g;
add_pc_thms "gst-ax" (map get_spec [g, g] @ [g_spec, gg_thm, gg_thm]);
set_merge_pcs ["basic_hol", "gst-ax"];

Functional Replacement
The more convenient form of replacement which takes a function rather than a relation (and hence needs no "ManyOne" caveat) is introduced here.
Introduction

Though a functional formulation of replacement is most convenient for most applications, it has a number of small disadvantages which have persuaded me 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.
Imagep
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([],Imagep f:GS GS s: GS
(x x g Imagep f s e e g s x = f e));
a (prove__tac THEN REPEAT strip_tac);
a (lemma_tac fr fr = x y y = f' x THEN1 prove__tac);
a (lemma_tac ManyOne fr
THEN1 (asm_rewrite_tac [get_spec ManyOne]
THEN REPEAT strip_tac
THEN asm_rewrite_tac[]));
a (_tac RelIm fr s');
a (_FC_T asm_rewrite_tac (get_spec RelIm));
xl_set_cs__thm (pop_thm ());

"Imagep f s" is the image of s through f.