Higher Order Set Theory
Overview
Set theory has been fundamental to mathematics throughout the twentieth century. We propose for it a broader foundational role in formal analytics.
We define a universal semantic foundation system as one which can be used to give an abstract semantics to any coherent language, and argue that Higher Order Set Theory is one (among many).
The formalisation of ZFC in ProofPower HOL and its applications.
Galactic Set Theory and some applications.
Introduction
Universal Semantic Foundations
We define a universal semantic foundation system as one which can be used to give an abstract semantics to any coherent language, and argue that Higher Order Set Theory is one (among many).
ZFC in HOL
The formalisation of ZFC in ProofPower HOL and its applications.
This document is a literate script containing the axiomatisation in ProofPower HOL of Zermelo-Fraenkel set theory.
This document proves some elementary consequences of the ZFC axioms in HOL, and then introduces further definitions relating to the representation of functions in set theory.
This document defines the concept of a pure function as a preliminary to introducing the type of pure functions.
Galactic Set Theory
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).
Other documents

up quick index © RBJ

$Id: host.xml,v 1.1.1.1 2000/12/04 17:22:18 rbjones Exp $