Synthetic Philosophy and Deductive Engineering
The specification of the deductive Kernel for the SPaDE project will be an iterative process starting from the formal specifications of the ProofPower kernel by Rob Arthan.
It is in the first instance an exercise in metatheoretic reasoning of the kind which will be important to the final product.
That first exercise will be the presentation of inference rules more simple and primitive than the main rules in the ProofPower kernel, and a new directly_derivable_from relation, the demonstration that derivability defined in term of that new notion of direct derivability is the same as the original. Unlike the existing specification, all rules will be functions, and the general policy is that error conditions yield the theorem T.