Galactic Set Theory and applications
Overview
Galactic Set Theory and some applications.
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.
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.
Formal Theory of Knowledge in Galactic Set Theory (in ProofPower).
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.
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.
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.
directory tok
Formal Theory of Knowledge in Galactic Set Theory (in ProofPower).
A simple formal model is used to explore the minimal conditions necessary for the analytic/synthetic necessary/contingent dichotomies to make sense.
A Formal model of semantics similar to aspects of the Tractatus.
A simple model of semantics and soundness for X-Logic.
Other documents
A formal model of the XML infoset in galactic set theory.

up quick index © RBJ

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