|
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.
|
|
|
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
|
|
|
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.
|
|
|
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.
|
|
|
|
© 