Axioms for galactic set theory.
Overview
An axiomatisation in Higher Order Logic of a well-founded set theory with galaxies.
Galactic set theory is a set theory with "galaxies" (previously known as "universes") axiomatised in Higher Order Logic.
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 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).
Here we define the subset relation and assert the existence of powersets and unions.
Here we define the powerset and union operators.
Pair is defined using replacement, and Unit using Pair.
Separation is introduced by conservative extension.
Binary union and distributed and binary intersection are defined.
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.
To simplify subsequent proofs a new "proof context" is created enabling automatic use of the results now available.
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", qqco.gifGS→GS→BOOL⌝);
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•
ftbr 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 =
fttabnew_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",
fttab(⇒_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",
fttab(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 ⇔
fttab∀e• e ∈g s ⇒ e ∈g t

xl-sml
val ⊆g_thm = get_spec ⌜$⊆g⌝;
val ⊆g_eq_thm = save_thm ("⊆g_eq_thm",
fttabprove_rule [get_spec ⌜$⊆g⌝, gs_ext_axiom]
fttab⌜∀A B• A = B ⇔ A ⊆g B ∧ B ⊆g A⌝);
val ⊆g_refl_thm = save_thm ("⊆g_refl_thm",
fttabprove_rule [get_spec ⌜$⊆g⌝]
fttab⌜∀A• A ⊆g A⌝);
val ∈gg_thm = save_thm ("∈gg_thm",
fttabprove_rule [get_spec ⌜$⊆g⌝]
fttab⌜∀e A B• e ∈g A ∧ A ⊆g B ⇒ e ∈g B⌝);
val ⊆g_trans_thm = save_thm ("⊆g_trans_thm",
fttabprove_rule [get_spec ⌜$⊆g⌝]
fttab⌜∀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 =
fttabnew_axiom (["Ontology_axiom"],
⌜ ∀s•
fttab∃g• s ∈g g

fttab∀t• t ∈g g ⇒ t ⊆g g
fttab∧ (∃p• (∀v• v ∈g p ⇔ v ⊆g t) ∧ p ∈g g)
fttab∧ (∃u• (∀v• v ∈g u ⇔ ∃w• v ∈g w ∧ w ∈g t) ∧ u ∈g g)
fttab∧ (∀rel• ManyOne rel ⇒
fttabfttab(∃r• (∀v• v ∈g r ⇔ ∃w • w ∈g t ∧ rel w v) ∧
fttabfttabfttab(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 ∈gg 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 ∈gg s ⇔ t ⊆g s
Union

xl-sml
set_goal([],⌜∃⋃g• ∀s t• t ∈gg 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 ∈gg s ⇔ ∃e• t ∈g e ∧ e ∈g s

xl-sml
val ∈gg_thm = save_thm ("∈gg_thm",
fttabprove_rule [get_spec ⌜⋃g⌝, ⊆g_thm]
fttab⌜∀s t:GS• t ∈g s ⇒ t ⊆gg 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
fttab(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⌝
fttabTHEN1 prove_∃_tac);
a (lemma_tac ⌜ManyOne rel⌝
fttabTHEN1 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•
fttabgalaxy s ⇔ (∃x• x ∈g s)
fttab∧ ∀t• t ∈g s
fttabfttab⇒ t ⊆g s
fttabfttab∧ ℘g t ∈g s
fttabfttab∧ ⋃g t ∈g s
fttabfttab∧ (∀rel• ManyOne rel
fttabfttabfttab⇒ RelIm rel t ⊆g s
fttabfttabfttab⇒ RelIm rel t ∈g s)

xl-gft
galaxies_∃_thm =
fttab⊢ ∀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 =
fttab⊢ ∀ t• t ∈g Gx t
galaxy_Gx =
fttab⊢ ∀s• galaxy (Gx s)
Gx_⊆g_galaxy =fttab
fttab⊢ ∀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 =
fttab⊢ ∀s• galaxy s ⇒ transitive s
GCloseSep =
fttab⊢ ∀g• galaxy g ⇒ ∀s• s ∈g g ⇒ ∀p• Sep s p ∈g g
Gx_transitive_thm =
fttab⊢ ∀ s• transitive (Gx s)
Gx_mono_thm =
fttab⊢ ∀s t• s ⊆g t ⇒ Gx s ⊆g Gx t
Gx_mono_thm2 =
fttab⊢ ∀s t• s ∈g t ⇒ Gx s ⊆g Gx t
t_sub_Gx_t_thm =
fttab⊢ ∀ t• t ⊆g Gx t
Gx_mono_thm3 =
fttab⊢ ∀ s t• s ⊆g t ⇒ s ⊆g Gx t
Gx_trans_thm2 =
fttab⊢ ∀ s t• s ∈g t ⇒ s ∈g Gx t
Gx_trans_thm3 =
fttab⊢ ∀ 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 ∈gg⌝);
a (∃_tac ⌜Sep (εs:GS• T) (λx:GS• F)⌝
fttabTHEN rewrite_tac [get_spec⌜Sep⌝]);
xl_set_cs_∃_thm (pop_thm ());

So we define ⌜∅g⌝ as the empty set:
xl-holconst
g : GS
∀s• ¬ s ∈gg
and the empty set is a member of every galaxy:
xl-sml
set_goal([],⌜∀g• galaxy g ⇒ ∅gg 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)⌝
fttabTHEN1 (rewrite_tac [gs_ext_axiom, get_spec ⌜∅g⌝, get_spec ⌜Sep⌝]));
a (asm_rewrite_tac[]);
val G∅gC = save_pop_thm "G∅gC";


xl-sml
val ∅gg_thm = save_thm ("∅gg_thm",
fttabprove_rule [get_spec ⌜∅g⌝, ⊆g_thm]
fttab⌜∀s:GS• ∅gg t⌝);
val ⋃gg_thm = save_thm ("⋃gg_thm",
fttabprove_rule [get_spec ⌜∅g⌝, get_spec ⌜⋃g⌝, gs_ext_axiom]
fttab⌜⋃gg = ∅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•
fttab(∀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⌝
fttabTHEN1 (asm_rewrite_tac [get_spec ⌜ManyOne⌝]
fttabfttabTHEN REPEAT strip_tac
fttabfttabTHEN 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.
xl-holconst
Imagep : (GS → GS) → GS → GS
∀f s•
fttab∀x• x ∈g Imagep f s
fttab⇔ ∃e• e ∈g s ∧ x = f e

xl-sml
val Imagep_spec = get_spec ⌜Imagep⌝;
add_pc_thms "gst-ax" (map get_spec [⌜Imagep⌝]);
set_merge_pcs ["basic_hol", "gst-ax"];

We now show that galaxies are closed under Image.
xl-sml
set_goal([],⌜∀g• galaxy g
fttab⇒ ∀s• s ∈g g
fttab⇒ ∀f• Imagep f s ⊆g g
fttab⇒ Imagep f s ∈g g⌝);
a (REPEAT_N 5 strip_tac);
a (lemma_tac ⌜∃fr• fr = λx y• y = f x⌝ THEN1 prove_∃_tac);
a (lemma_tac ⌜ManyOne fr⌝
fttabTHEN1 (asm_rewrite_tac [get_spec ⌜ManyOne⌝]
fttabfttabTHEN REPEAT strip_tac
fttabfttabTHEN asm_rewrite_tac[]));
a (lemma_tac ⌜Imagep f s = RelIm fr s⌝);
(* *** Goal "1" *** *)
a (pure_rewrite_tac [gs_ext_axiom]);
a (⇔_FC_T pure_once_rewrite_tac (get_spec ⌜RelIm⌝));
a (asm_rewrite_tac[] THEN REPEAT strip_tac);
(* *** Goal "2" *** *)
a (once_asm_rewrite_tac[]);
a (fc_tac[get_spec ⌜galaxy⌝]);
a (list_spec_nth_asm_tac 5 [⌜s⌝,⌜fr⌝]
fttabTHEN asm_rewrite_tac[]);
val GImagepC = save_pop_thm "GImagepC";

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-holconst
Pairg : GS → GS → GS
∀s t e:GS•
fttabe ∈g Pairg s t
fttab⇔ e = s ∨ e = tfttab
Pair equality theorem
Extensional proofs about equality of pairs are simplified by the following principle.
xl-sml
set_goal([],⌜∀s t u v•
fttabPairg s t = Pairg u v
fttab⇔ s = u ∧ t = v
fttab∨ s = v ∧ t = u⌝);
a (rewrite_tac[
fttab∀_elim ⌜Pairg s t⌝ gs_ext_axiom,fttab
fttabget_spec ⌜Pairg⌝]
fttabTHEN REPEAT strip_tac
fttabTHEN_TRY all_var_elim_asm_tac
fttabTHEN REPEAT strip_tac);
(* *** Goal "1" *** *)
a (spec_nth_asm_tac 2 ⌜s⌝
fttabTHEN_TRY all_var_elim_asm_tac
fttabTHEN_TRY asm_rewrite_tac[]);
(* *** Goal "2" *** *)
a (spec_nth_asm_tac 2 ⌜u⌝
fttabTHEN_TRY all_var_elim_asm_tac
fttabTHEN_TRY asm_rewrite_tac[]);
(* *** Goal "3" *** *)
a (spec_nth_asm_tac 2 ⌜v⌝
fttabTHEN_TRY all_var_elim_asm_tac
fttabTHEN_TRY asm_rewrite_tac[]);
(* *** Goal "4" *** *)
a (spec_nth_asm_tac 2 ⌜t⌝
fttabTHEN_TRY all_var_elim_asm_tac
fttabTHEN_TRY asm_rewrite_tac[]);
val Pairg_eq_thm =
fttabsave_pop_thm "Pairg_eq_thm";

Galaxy Closure

xl-sml
set_goal([],⌜∀g• galaxy g ⇒ ∀s t• s ∈g g ∧ t ∈g g ⇒ Pairg s t ∈g g⌝);
a (REPEAT strip_tac);
a (lemma_tac ⌜Pairg s t = Imagep (λx• if x = ∅g then s else t) (℘g (℘gg))⌝);
(* *** Goal "1" *** *)
a (once_rewrite_tac [gs_ext_axiom]);
a (rewrite_tac (map get_spec [⌜Pairg⌝,⌜Imagep⌝]));
a (REPEAT strip_tac THEN asm_rewrite_tac[]);
(* *** Goal "1.1" *** *)
a (∃_tac ⌜∅g⌝ THEN rewrite_tac[get_spec ⌜$⊆g⌝]);
(* *** Goal "1.2" *** *)
a (∃_tac ⌜℘gg⌝ THEN rewrite_tac[get_spec ⌜$⊆g⌝]);
a (lemma_tac ⌜¬ ℘gg = ∅g⌝);
(* *** Goal "1.2.1" *** *)
a (rewrite_tac [gs_ext_axiom]
fttabTHEN strip_tac
fttabTHEN ∃_tac ⌜∅g
fttabTHEN rewrite_tac[]);
(* *** Goal "1.2.2" *** *)
a (asm_rewrite_tac[]);
(* *** Goal "1.3" *** *)
a (cases_tac ⌜e' = ∅g
fttabTHEN asm_rewrite_tac[]);
a (asm_ante_tac ⌜e = (if e' = ∅g then s else t)⌝
fttabTHEN asm_rewrite_tac[]);
(* *** Goal "2" *** *)
a (asm_rewrite_tac[]);
a (fc_tac [GImagepC]);
a (list_spec_nth_asm_tac 1 [⌜℘g (℘gg)⌝,⌜λ x• if x = ∅g then s else t⌝]);
a (fc_tac [G∅gC]);
a (lemma_tac ⌜∀s• s ∈g g ⇒ ℘g s ∈g g⌝
fttabTHEN1 (REPEAT (fc_tac [get_spec ⌜galaxy⌝])));
a (REPEAT (asm_fc_tac []));
(* *** Goal "2.2" *** *)
a (swap_nth_asm_concl_tac 1);
a (rewrite_tac [get_spec ⌜$⊆g⌝]);
a (REPEAT strip_tac);
a (POP_ASM_T ante_tac
fttabTHEN cases_tac ⌜e' = ∅g
fttabTHEN asm_rewrite_tac[]
fttabTHEN strip_tac
fttabTHEN asm_rewrite_tac[]);
val GClosePairg = save_pop_thm "GClosePairg";

Unit definition

xl-holconst
Unit : GS → GS
∀s• Unit s = Pairg s s
Unit extension theorem
The following theorem tells you what the members of a unit sets are.
xl-sml
set_goal([],⌜∀s e•
fttabe ∈g Unit s ⇔ e = s⌝);
a (rewrite_tac [
fttabget_spec⌜Unit⌝,
fttabget_spec⌜Pairg⌝]
fttabTHEN REPEAT strip_tac);
val Unit_thm = pop_thm ();
add_pc_thms "gst-ax" [get_spec ⌜Pairg⌝, 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•
fttabUnit s = Unit t
fttab⇔ s = t⌝);
a (prove_tac [
fttab∀_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"];

Galaxy Closure

xl-sml
set_goal([],⌜∀g• galaxy g ⇒ ∀s• s ∈g g ⇒ Unit s ∈g g⌝);
a (REPEAT strip_tac
fttabTHEN rewrite_tac [get_spec ⌜Unit⌝]);
a (REPEAT (asm_fc_tac[GClosePairg]));
val GCloseUnit = save_pop_thm "GCloseUnit";

Unit-Pair equations
The following theorems tell you when Pairs are really Units.
xl-sml
set_goal([],
fttab⌜∀s t u•
fttabUnit s = Pairg t u
fttab⇔ s = t ∧ s = u⌝);
a (prove_tac [
fttab∀_elim ⌜Unit s⌝ gs_ext_axiom]);
(* *** Goal "1" *** *)
a (spec_nth_asm_tac 1 ⌜s⌝
fttabTHEN spec_nth_asm_tac 2 ⌜t⌝
fttabTHEN_TRY all_var_elim_asm_tac
fttabTHEN_TRY rewrite_tac[]);
(* *** Goal "2" *** *)
a (spec_nth_asm_tac 1 ⌜u⌝
fttabTHEN_TRY all_var_elim_asm_tac
fttabTHEN_TRY rewrite_tac[]);
val Unit_Pairg_eq_thm = pop_thm ();


xl-sml
set_goal([],⌜∀s t u•
fttabPairg s t = Unit u
fttab⇔ s = u ∧ t = u⌝);
a (prove_tac [
fttab∀_elim ⌜Pairg s t⌝ gs_ext_axiom]);
val Pairg_Unit_eq_thm = pop_thm ();

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

xl-holconst
$∪g : GS → GS → GS
∀s t e• e ∈g (s ∪g t) ⇔ e ∈g s ∨ e ∈g t

xl-sml
val ∪g_thm = get_spec ⌜$∪g⌝;
val ⊆gg_thm = save_thm ("⊆gg_thm", prove_rule
fttab[⊆g_thm, ∪g_thm]
fttab⌜∀A B• A ⊆g A ∪g B ∧ B ⊆g A ∪g B⌝);
val ∪gg_thm1 = save_thm ("∪gg_thm1", prove_rule
fttab[⊆g_thm, ∪g_thm]
fttab⌜∀A B C• A ⊆g C ∧ B ⊆g C ⇒ A ∪g B ⊆g C⌝);
val ∪gg_thm2 = save_thm ("∪gg_thm2", prove_rule
fttab[⊆g_thm, ∪g_thm]
fttab⌜∀A B C D• A ⊆g C ∧ B ⊆g D ⇒ (A ∪g B) ⊆g (C ∪g D)⌝);
val ∪gg_clauses = save_thm ("∪gg_clauses", prove_rule
fttab[gs_ext_axiom, ∪g_thm]
fttab⌜∀A• (A ∪gg) = A
fttab∧ (∅gg A) = A⌝);

Galaxy Closure

xl-sml
set_goal([],⌜∀g• galaxy g ⇒ ∀s t• s ∈g g ∧ t ∈g g ⇒ s ∪g t ∈g g⌝);
a (REPEAT strip_tac THEN fc_tac [get_spec ⌜galaxy⌝]);
a (lemma_tac ⌜s ∪g t = ⋃g (Pairg s t)⌝
fttabTHEN1 (once_rewrite_tac [gs_ext_axiom]
fttabfttabTHEN rewrite_tac [get_spec ⌜⋃g⌝, get_spec ⌜$∪g⌝]
fttabfttabTHEN prove_tac[]));
a (asm_rewrite_tac []);
a (lemma_tac ⌜Pairg s t ∈g g⌝
fttabTHEN1 (REPEAT (asm_fc_tac [GClosePairg])));
a (REPEAT (asm_fc_tac[]));
val GClose∪g = save_pop_thm "GClose∪g";

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
g : GS → GS
∀s• ⋂g s = Sep (⋃g s) (λx• ∀t• t ∈g s ⇒ x ∈g t)
Extensional Intersection Theorem

xl-sml
set_goal ([],⌜∀x s e• x ∈g s ⇒
fttab(e ∈gg s ⇔ ∀y• y ∈g s ⇒ e ∈g y)⌝);
a (prove_tac [
fttabget_spec ⌜⋂g⌝]);
val ⋂g_thm = save_pop_thm "⋂g_thm";


xl-sml
set_goal([],⌜∀s t• s ∈g t ⇒ ⋂g t ⊆g s⌝);
a (rewrite_tac [⋂g_thm, ⊆g_thm]);
a (REPEAT strip_tac);
a (REPEAT (asm_fc_tac[⋂g_thm]));
val ⋂gg_thm = save_pop_thm "⋂gg_thm";

val ⊆gg_thm = save_thm ("⊆gg_thm",
fttab(prove_rule [⊆g_thm, gs_ext_axiom,
fttabget_spec ⌜$⋂g⌝]
fttab⌜∀A B• A ∈g B ⇒ ∀C•fttab
fttab(∀D• D ∈g B ⇒ C ⊆g D)
fttab⇒ C ⊆gg B⌝));

val ⋂gg_thm = save_thm ("⋂gg_thm",
fttab(prove_rule [gs_ext_axiom,fttabget_spec ⌜$⋂g⌝]
fttab⌜⋂gg = ∅g⌝));

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


xl-holconst
$∩g : GS → GS → GS
∀s t• s ∩g t = Sep s (λx• x ∈g t)
Galaxy Closure

xl-sml
set_goal([],⌜∀g• galaxy g ⇒ ∀s• s ∈g g ⇒ ⋂g s ∈g g⌝);
a (REPEAT strip_tac
fttabTHEN rewrite_tac[get_spec ⌜⋂g⌝]);
a (fc_tac [GCloseSep, get_spec ⌜galaxy⌝]);
a (list_spec_nth_asm_tac 1 [⌜⋃g s⌝, ⌜λ x• ∀ t• t ∈g s ⇒ x ∈g t⌝]);
a (asm_fc_tac[]);
val GClose⋂g = save_pop_thm "GClose⋂g";


xl-sml
set_goal([],⌜∀g• galaxy g ⇒ ∀s t• s ∈g g ∧ t ∈g g ⇒ s ∩g t ∈g g⌝);
a (REPEAT strip_tac
fttabTHEN rewrite_tac[get_spec ⌜$∩g⌝]);
a (fc_tac [GCloseSep]);
a (list_spec_nth_asm_tac 1 [⌜s⌝, ⌜λ x• x ∈g t⌝]);
val GClose∩g = save_pop_thm "GClose∩g";

Extensional Binary Intersection Theorem

xl-sml
set_goal ([],⌜∀s t e•
fttabe ∈g s ∩g t ⇔ e ∈g s ∧ e ∈g t⌝);
a (prove_tac [
fttabget_spec ⌜$∩g⌝]);
val ∩g_thm = save_thm ("∩g_thm",
fttabprove_rule [get_spec ⌜$∩g⌝]
fttab⌜∀s t e•fttabe ∈g s ∩g t ⇔ e ∈g s ∧ e ∈g t⌝);
val ⊆gg_thm = save_thm ("⊆gg_thm",
fttabprove_rule [⊆g_thm, ∩g_thm]
fttab⌜∀A B• A ∩g B ⊆g A ∧ A ∩g B ⊆g B⌝);
val ∩gg_thm1 = save_thm ("∩gg_thm1",
fttabprove_rule [⊆g_thm, ∩g_thm]
fttab⌜∀A B C• A ⊆g C ∧ B ⊆g C ⇒ A ∩g B ⊆g C⌝);
val ∩gg_thm2 = save_thm ("∩gg_thm2",
fttabprove_rule [⊆g_thm, ∩g_thm]
fttab⌜∀A B C D• A ⊆g C ∧ B ⊆g D ⇒ (A ∩g B) ⊆g (C ∩g D)⌝);
val ∩gg_thm3 = save_thm ("∩gg_thm3",
fttabprove_rule [⊆g_thm, ∩g_thm]
fttab⌜∀A B C• C ⊆g A ∧ C ⊆g B ⇒ C ⊆g A ∩g 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 = [
fttabg_spec,
fttabget_spec ⌜℘g⌝,
fttabget_spec ⌜⋃g⌝,
fttabImagep_spec,
fttabPairg_eq_thm,
fttabget_spec ⌜Pairg⌝,
fttabUnit_eq_thm,
fttabUnit_thm,
fttabPairg_Unit_eq_thm,
fttabUnit_Pairg_eq_thm,
fttabSep_thm,
fttabg_thm,
fttabg_thm
];
val gst_opext_clauses =
fttab(all_∀_intro
fttabo list_∧_intro
fttabo (map all_∀_elim))
fttabgst_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 =
fttab(all_∀_intro
fttabo list_∧_intro
fttabo (map all_∀_elim))
fttab[gs_ext_axiom,
fttabget_spec⌜$⊆g⌝];
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 =
fttabTRY_C (pure_rewrite_conv [gst_relext_clauses])
fttabTHEN_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
fttab(conv_tac o gst_ax_prove_conv)
fttab"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 =
fttab(merge_pcs_rule1
fttab["basic_hol", "gst-ax"]
fttabprove_rule) [];
val gst_ax_conv =
fttabMERGE_PCS_C1
fttab["basic_hol", "gst-ax"]
fttabprove_conv;
val gst_ax_tac =
fttabconv_tac o gst_ax_conv;

Examples
The following are examples of the elementary results which are now proven automatically:
xl-sml
gst_ax_rule ⌜
fttaba ∩g (b ∩g c)
fttab= (a ∩g b) ∩g c⌝;
gst_ax_rule ⌜a ∩g b ⊆g b⌝;
gst_ax_rule ⌜∅gg b = b⌝;
gst_ax_rule ⌜
fttaba ⊆g b ∧ c ⊆g d
fttab⇒ a ∩g c ⊆g b ∩g d⌝;
gst_ax_rule ⌜Sep b p ⊆g b⌝;
gst_ax_rule ⌜a ⊆g b ⇒
fttabImagep f a ⊆g Imagep f b⌝;


up quick index © RBJ

privacy policy

Created:

$Id: gst-axioms.xml,v 1.5 2012/08/11 21:01:52 rbj Exp $

V