Galactic Set Theory and applications
Overview
Galactic Set Theory and some applications. "Galactic" set theory is basically a higher-order set theory in which every set is a member of a "galaxy" and every galaxy is a model of ZFC. (galaxies are what Grothendieck called "universes", which is obviously a misnomer, you can't have more than one universe can you?)
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 creates a theory of pure concrete categories and functors. The theory contains a set of theorems which might serve as an independent axiomatisation of the theory.
A simple model of semantics and soundness for X-Logic.
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 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.
Proof Context
Category Theoretic Foundation Systems
This document creates a theory of pure concrete categories and functors. The theory contains a set of theorems which might serve as an independent axiomatisation of the theory.
Introduction
Work on foundation systems for mathematics which are ontologically category theoretic, i.e. in which the things in the domain of discourse are the stuff of category theory, categories, arrows, 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.
This document creates a theory of pure concrete categories and functors. The theory contains a set of theorems which might serve as an independent axiomatisation of the theory.
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.
A Too-Simple Model of X-Logic
A simple model of semantics and soundness for X-Logic.
Introduction
Purposes and key ideas.
Types
An overview of the model with specifications of the various types of entity involved in it.
Propositions
Three kinds of proposition are defined, concerning truth of documents, correctness of programs and derivation of documents.
Meta Reasoning
Elementary reasoning about inferences and their composition.

up quick index © RBJ

privacy policy

Created:

$Id: index.xml,v 1.3 2006/03/25 22:50:36 rbj01 Exp $

V