Synthetic Philosophy and Deductive Engineering
Synthetic philosophy and the SPaDE project are foundational, which is to say that the whole is built on logical and epistemological foundations.
The chosen logical system is that evolved from Alonzo Church’s Simple Theory of Types, by Mike Gordon at the University of Cambridge for use in the verification of digital electronic systems (but since applied more broadly). This is a Higher Order Logic (HOL) often referred to as Cambridge HOL, which has been adopted by a number interactive theorem proving systems including HOL4, HOL Light, Isabelle/HOL and ProofPower.
This page will in due course refer to full formal metatheory in SPaDE for that system but relies at present on references to the existing literature.
It is claimed here that this system, with some small innovation in the semantics is universal for the representation of declarative knowledge and it is an important part of the documents here to make that claim clear and plausible, for which the notion of a foundational institution is introduced. The present account is regrettably disorganised and incomplete.