The theory gst
Overview
This document is an overview of and conclusion to the work in which Galactic set theory is developed, creating the theory gst which should be cited as ancestor by applications of GST and a proof context suitable for applications.
A new "gst" theory is created as a child of "gst-lists". The theory will be kept below all the theories contributing to (but not applications of) gst.
An axiomatisation in Higher Order Logic of a well-founded set theory with pseudo-urelements and galaxies.
This document introduces definitions and derives results relating to the representation of functions in galactic set theory.
In this document I am investigating how hard it is to prove the Knaster-Tarski fixedpoint theorem in GST. I am following Larry Paulson's paper, to whatever extent that is possible with ProofPower.
This document introduces definitions and derives results relating to the theory of lists in galactic set theory.
Introduction
A new "gst" theory is created as a child of "gst-lists". The theory will be kept below all the theories contributing to (but not applications of) gst.
The Theory gst
The new theory is first created, together with a proof context which we will build up as we develop the theory.
xl-sml
open_theory "gst-lists";
force_new_theory "gst";
new_parent "gst-sumprod";
new_parent "gst-fixp";
new_parent "gst-rec";
force_new_pc "gst";
val rewrite_thms = ref ([]:THM list);

Axioms
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.
Functions
This document introduces definitions and derives results relating to the representation of functions in galactic set theory.
Introduction
A new "gst-fun" theory is created as a child of "gst-ax". The theory will contain the definitions of ordered pairs, relations and functions and related material for general use.
Ordered Pairs
We now introduce ordered pairs, which are required for representing functions as graphs.
Relations
A relation is defined as a set of ordered pairs. Cartesian product and relation space are defined.
Domain, Range and Field
The domain, range and field of a relation are defined.
Functions
Definition of partial and total functions and the corresponding function spaces.
Functional Abstraction
Functional abstraction is defined as a new variable binding construct yeilding a functional set.
Application and Extensionality
In this section we define function application and show that functions are extensional.
Proof Context
Sums and Products
Introduction
A new "gst-rec" theory is created as a child of "gst-fun". Probably
Sums
Products
Proof Context
Fixedpoints
In this document I am investigating how hard it is to prove the Knaster-Tarski fixedpoint theorem in GST. I am following Larry Paulson's paper, to whatever extent that is possible with ProofPower.
Introduction
A new "gst-fixp" theory is created as a child of "gst-fun". Probably
Monotonicity and Closure Definitions
Definitions of the notion of a bounded monotonic function, and of the closure of a set under such a function.
Least Closure and Fixed Point Definitions
The concepts fixed point, least closed, and a function yielding an intersection of closures are defined.
Monotonicity and Closure Lemmas
In this section lemmas are proven following Paulson's proof as closely as possible.
Least Fixed Point Lemmas
Least Fixed Point Theorem and Definition
Induction
Recursion
Introduction
A new "gst-rec" theory is created as a child of "gst-fun". Probably
Definitions
Definition of the function "recdef" which converts a recursion functional into the function defined by that functional.
Recursion Theorem
Proof Context
In this section I will create a decent proof context for recursive definitions, eventually.
Lists
This document introduces definitions and derives results relating to the theory of lists in galactic set theory.
Introduction
A new "gst-lists" theory is created as a child of "gst-fun". Probably This is really a placeholder, it is probably that lists will end up a special case of a more general theory of inductively defined types.
Lists
Though we could do n-ary tuples for n>2, lists are better.
Proof Context
In this section I will create a decent proof context for lists, maybe.
Proof Context
Proof Context gst

xl-sml
merge_pcs ["basic_hol", "gst-ax", "gst-fun", "gst-sumprod", "gst-fixp", "gst-rec", "gst-lists"] "gst";
commit_pc "gst";


up quick index © RBJ

$Id: gst-final.xml,v 1.1.1.1 2000/12/04 17:23:52 rbjones Exp $