| “If we had it [a characteristica universalis], we
should be able to reason in metaphysics and morals in much the same
way as in geometry and analysis.”
“If controversies were to arise, there would be no more need of disputation between two philosophers than between two accountants (Computistas). For it would suffice to take their pencils in their hands, to sit down to their slates (abacos), and to say to each other … : Let us calculate (Calculemus).” Gottfried Wilhelm Leibniz |
Computational metaphysics, as we practice it, is the implementation and investigation of formal, axiomatic metaphysics (i.e., the study of metaphysics using formally represented axioms and premises to derive conclusions) in an automated reasoning environment. As our axiomatic metaphysics, we work within the axiomatic theory of abstract objects developed at the Metaphysics Research Lab at Stanford University.
The basic idea is to represent the axioms and definitions of abstract object theory in the syntax of an automated reasoning system. Once this is done, arbitrary propositions in the language of object theory can either be proved or shown to be independent of the basic axioms and definitions. In the past, we have used PROVER9 (and its accompanying model-finding program, MACE4), as our automated reasoning system. (PROVER9 is the successor to OTTER.) This meant representing things in the syntax of PROVER9. For examples, see the links to our work on the theory of forms and the theory of possible worlds.
More recently, we have moved to a more generic framework, namely, TPTP syntax, which can be parsed by all current theorem provers and model-finders.
These web pages has been developed, in part, to support the research we have begun to publish in computational metaphysics. The list of papers published so far is:
The paper describes the basic elements of computational metaphysics, and gives examples of proofs. It then cites this web page as the place to look for the proofs of the other theorems.
We'd like to thank Chris Menzel, discussions with whom have helped us to see how to improve our results.