Galactic Set Theory and applications
Overview
 Galactic Set Theory and some applications.
 gst files 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. Pure Categories and Functors This document defines the concepts "pure category" and "pure functor" as a preliminary to developing a foundation system whose domains of discourse are the pure categories and functors.
 directory tok Formal Theory of Knowledge in Galactic Set Theory (in ProofPower). Other documents
gst files
 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.
 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. Axioms An axiomatisation in Higher Order Logic of a well-founded set theory with pseudo-urelements and galaxies. Functions This document introduces definitions and derives results relating to the representation of functions in galactic set theory. Sums and Products
 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. Recursion Lists This document introduces definitions and derives results relating to the theory of lists in galactic set theory. Proof Context
Pure Categories and Functors
 This document defines the concepts "pure category" and "pure functor" as a preliminary to developing a foundation system whose domains of discourse are the pure categories and functors.
 Introduction Pure functors and categories are the concrete functors and categories which can be constructed by an iterative process starting from the empty category. Functor Functions A functor function is a graph together with its domain and codomain. Application and Composition Application and composition of functor functions is very similar to ordinary function application and composition. Concrete Categories A concrete category is (in our special world) just a set of functor functions which is closed under composition and has left and right identities. Concrete Functors A concrete functor is a functor function whose domain and codomains are sets of functor functions and which respects composition.
 Category-Functors and Functor-Categories A category-functor (ccat_cfunc) is a concrete functor whose domain and codomain are concrete categories (not just sets) while a functor-category (cfunc_ccat) is a concrete category whose elements are concrete functors (not just functor functions). Hereditary Properties Hereditary properties are those which are inherited as new (concrete) functors and categories are constructed from old. Pure Functors Pure functors are the concrete functors which can be built starting from the empty category using a sequence of alternating constructions of categories and functors from functors and categories (resp.) already constructed. Pure Categories Pure categories are the concrete categories which can be built starting from the empty category using a sequence of alternating constructions of categories and functors from functors and categories (resp.) already constructed. Listing of Theory pcf-defs
directory tok
 Formal Theory of Knowledge in Galactic Set Theory (in ProofPower).
 Fundamental Dichotomies A simple formal model is used to explore the minimal conditions necessary for the analytic/synthetic necessary/contingent dichotomies to make sense. The Tractatus A Formal model of semantics similar to aspects of the Tractatus.
 X-Logic A simple model of semantics and soundness for X-Logic.
 Other documents
 The XML Infoset A formal model of the XML infoset in galactic set theory.

©

\$Id: index.xml,v 1.1.1.1 2000/12/04 17:24:13 rbjones Exp \$