Introduction
A new "gst" theory is created as a child of "gstlists".
The theory will be kept below all the theories contributing to (but not applications of) gst.

An axiomatisation in Higher Order Logic of a wellfounded set theory with pseudourelements 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 KnasterTarski 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

