Computational metaphysics (nonfiction)

Computational metaphysics is a formal, axiomatic metaphysics (i.e., the study of metaphysics using formally represented axioms and premises to derive conclusions) in an automated reasoning environment. It is based on the axiomatic theory of abstract objects developed at the Metaphysics Research Lab at Stanford University.

Computational Metaphysics is also the name of the academic team which is developing this formal, axiomatic metaphysics.

The team's web site states:

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.

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.

Leibniz wrote:

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.

Leibniz again:

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).

Fiction cross-reference

• Crimes against mathematical constants
• Gnomon algorithm
• Mathematics

Nonfiction cross-reference

• Computation (nonfiction)
• Gottfried Wilhelm Leibniz (nonfiction)

External links:

• Computational Metaphysics - project home page @ stanford.edu