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.
|
|
|
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);
|
|
|
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.
|
|
|
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.
|
|
|
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.
|
|
|
Introduction
A new "gst-rec" theory is created as a child of "gst-fun".
Probably
|
Sums
|
|
|
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
|
|
|
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.
|
|
|
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 gst
xl-sml
merge_pcs ["basic_hol", "gst-ax", "gst-fun", "gst-sumprod", "gst-fixp", "gst-lists","ord"] "gst";
commit_pc "gst";
|
|
|