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 Isabelle-HOL 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 pre-orders, 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 pre-orders.