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 galaxies.
This document introduces definitions and derives results relating to ordinal numbers in galactic set theory.
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.
Miscellaneous proof work using the gst axioms.
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 "ord";
force_new_pc "gst";
val rewrite_thms = ref ([]:THM list);

Axioms
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.
Ordinals
This document introduces definitions and derives results relating to ordinal numbers in galactic set theory.
Introduction
A new "ord" theory is created as a child of "gst-ax". The theory will contain the definitions of ordinals and related material for general use, roughly following "Set Theory" by Frank Drake, chapter 2 section 2. The subsections in this document correspondend to the subsections in the book.
Definitions 2.1 and 2.3
An ordinal is defined as a transitive and connected set. The usual ordering over the ordinals is defined and also the successor function.
Theorem 2.2
We prove that the empty set is an ordinal, and that the members of an ordinal and the successor of an ordinal are ordinals.
Theorem 2.4
We prove that the ordinals are linearly ordered by $<o.
Definition 2.6
Successor and limit ordinals are defined. Natural numbers are defined.
Theorem 2.7
Induction theorems over ordinals and natural numbers.
Theorem 2.8
The set of natural numbers.
The Definition of Rank
We define the rank of a set.
Proof Context
In this section we define a proof context for ordinals.
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 Contexts
Finalisation of a 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
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.
Miscellany
Miscellaneous proof work using the gst axioms.
Introduction
Proof of a putative strong infinity axiom for HOL and a speculative axiomatisation for the surreal numbers in HOL.
Strong Infinity in HOL
This section demonstrates the truth of a proposed strong infinity principle.
Axioms for the Surreal Numbers
This section supplies an axiomatisation of surreal numbers independent of set theory.
Proof Context
Proof Context gst

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


up quick index © RBJ

privacy policy

Created:

$Id: gst-final.xml,v 1.2 2003/02/01 14:30:08 rbj Exp $

V