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.