| “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 or interactive reasoning environment.
While we have investigated arguments in philosophy both formally and computationally (e.g., the ontological argument – see the links below), the most significant strand of our research has been to implement the axiomatic theory of abstract objects (henceforth ‘object theory’) developed at the Metaphysics Research Lab at Stanford University. By representing the axioms and definitions of abstract object theory in the syntax of various computer-based reasoning systems, we can find proofs of the claims (expressible in the formal language of object theory) that otherwise have to be proved by hand as theorems. These systems also allow us to find models of the axioms and show that some claims are independent of the basic axioms and definitions.
In our earliest efforts to implement object theory, we represented subsystems of object theory in the syntax of PROVER9 (and its accompanying model-finding program, MACE4). The axioms and theorems expressed in the language of PROVER9 and MACE4 were then sometimes re-expressed in TPTP syntax. This allowed us to find proofs using the other major theorem provers (e.g., Vampire, E, etc.) and model-finders (e.g., Paradox).
But the latest and most significant work in the computational implementation of the object theory has been developed by Daniel Kirchner, using the higher-order, interactive proof system Isabelle/HOL. Kirchner has:
Artifactual theorems are theorems derivable directly from the primitive mathematical notions and principles of the model theory – these primitive mathematical notions and principles are not part of object theory. So by eliminating artifactual theorems, the resulting interactive proof system yields only theorems of object theory. Interestingly, the mathematical notions and principles that are not primitive to object theory can be reconstructed or reduced/derived in object theory by using only the primitives and principles of object theory.
Acknowledgments: Zalta and Oppenheimer would like to thank Chris Menzel, discussions with whom have helped us to see how to improve our results.