Architectural speculations concerning globally distributed automation of formal reasoning.

A exploration of a way of doing set theory in HOL without using axioms.
I thought that locales in IsabelleHOL would make this kind of approach workable, and this document is the result of my investigating
this hope.
However, it quickly became apparent that the limitations on the implementation of locales. particularly in relation to the
forms of definition which you can use in a locale, were too severe.
Consequently I don't get very far.
I had hoped to do the construction of the PolySets on this kind of set theory, instead of using an axiomatisation of set theory
in HOL, but I reverted to the latter course.


A model for a set theory with a universal set and its use in the construction of other interesting and possibly useful foundational
ontologies.

This is a theory of preorders, i.e. reflexive transitive relations, obtained in the first instance by taking the theory Orderings
(which means partial orders), removing the antisymmetry axiom, defining a notion of equivalence and substituting equivalence
for equality in the conclusions of theorems.
Also covers linear preorders.

