Axioms for galactic set theory.
|
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.
|
|
|
|
|
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.
|
|
|
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.
|
|
|
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.
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 form in which we have stated the axiom is not very informative and so the more usual formulation is immediately derived
as a theorem.
We also save the axiom expanded out as an explicit induction theorem.
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
A subset s of t is a set all of whose members are also members of t.
|
xl-sml
declare_infix (230," g");
|
|
|
|
|
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.
|
|
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.
|
|
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:
|
|
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.
|
|
Definition of Galaxy
First we define the property of being a galaxy.
|
|
Definition of Gx
Gx is a function which maps each set onto its smallest enclosing galaxy.
|
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:
|
|
|
|
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.
|
|
|
The Empty Set
We can now prove that there is an empty set as follows:
So we define   g as the empty set:
and the empty set is a member of every galaxy:
|
|
|
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:
- It can't be used to prove the existence of the empty set.
- 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.
"Imagep f s" is the image of s through f.
We now show that galaxies are closed under Image.
|
|
|
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).
|
|
Pair equality theorem
Extensional proofs about equality of pairs are simplified by the following principle.
|
|
Galaxy Closure
|
|
|
Unit definition
|
|
Unit extension theorem
The following theorem tells you what the members of a unit sets are.
|
|
Unit equality theorem
The following theorem tells you when two unit sets are equal.
|
|
Galaxy Closure
|
|
|
Unit-Pair equations
The following theorems tell you when Pairs are really Units.
|
|
|
|
|
Binary Union
|
|
Galaxy Closure
|
|
Distributed Intersection
Distributed intersection doesn't really make sense for the empty set, but under this definition it maps the empty set onto
itself.
|
|
Extensional Intersection Theorem
|
|
Binary Intersection
Binary intersection could be defined in terms of distributed intersection, but its easier not to.
|
xl-sml
declare_infix (240, " g");
|
|
|
Galaxy Closure
|
|
|
Extensional Binary Intersection Theorem
|
xl-sml
set_goal ([], s t e
 e  g s g t  e g s  e g t);
a (prove_tac [
get_spec $g]);
val g_thm = save_thm ("g_thm",
prove_rule [get_spec $g]
s t ee g s g t e g s e g t);
val gg_thm = save_thm ("gg_thm",
prove_rule [g_thm, g_thm]
A B A g B g A A g B g B);
val gg_thm1 = save_thm ("gg_thm1",
prove_rule [g_thm, g_thm]
A B C A g C B g C  A g B g C);
val gg_thm2 = save_thm ("gg_thm2",
prove_rule [g_thm, g_thm]
A B C D A g C B g D (A g B) g (C g D));
val gg_thm3 = save_thm ("gg_thm3",
prove_rule [g_thm, g_thm]
A B C C g A C g B C g A g B);
|
|
|
|
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 = [
g_spec,
get_spec  g,
get_spec  g,
Imagep_spec,
Pair_eq_thm,
get_spec Pair,
Unit_eq_thm,
Unit_thm,
Pair_Unit_eq_thm,
Unit_Pair_eq_thm,
Sep_thm,
 g_thm,
g_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.
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:
|
|
|
|
|
Examples
The following are examples of the elementary results which are now proven automatically:
|
|
GS
GS
x y
s 
s:GS
e = t
g : GS 
