Deus Ex Machina

A famously tricky argument for the existence of God proposed by the British theologian Anselm in the 11^th century recently got simpler with help from an automated reasoning engine. In a forthcoming paper in the Australasian Journal of Philosophy, Stanford philosophers Paul Oppenheimer and Edward Zalta discuss how they used a program called Prover9 to not only validate Anselm’s ontological argument from its admittedly dubious premises, but also greatly reduced the number of premises necessary to reach that conclusion.

This result is one of the more interesting discoveries in the new field of computational metaphysics, which uses computers to reason through problems in metaphysics. "Lots of fields are using computers to explore outstanding questions, and that’s true in philosophy no less than in other fields," says Zalta, a senior research scholar at Stanford University’s Center for the Study of Language.

Philosophers have used computers before Oppenheimer and Zalta did, but its application is remarkable in metaphysics, a branch of philosophy dealing with the ultimate nature of reality. Lofty questions about existence, causation, and identity might seem too abstruse for automated reasoning; however, when formulated with mathematical precision, metaphysical propositions become ideal candidates for computer-assisted proofs in much the same way that mathematical theorems are, says Rutgers University philosopher Branden Fitelson, who’s used automated reasoning in his specialties, logic and the philosophy of science.

When software is doing the philosopher’s work of axiomatic reasoning—stepping logically from the premises to the desired conclusion—much of what’s left for the philosopher is the task of translating the airy language of philosophy into a form the software can work from (and then interpreting the program’s output). But accomplishing that is a nontrivial process, says Fitelson. Since statements in metaphysics use second-order logic, for which there is no guarantee of a proof for valid claims, "you’re outside the realm of being able to do things mechanically at all," Fitelson explains. To get around this problem of undecidability, metaphysicians who want the aid of computers must first translate higher-order claims into the first-order claims of classical logic. But that usually leads to complicated sets of formulas that are hard for humans to work with. What’s more, philosophers must represent those formulas in the syntax of their automated reasoning system.

From there, by using tree search algorithms, the software can reliably find a proof or show a counterexample. And there’s no beating the rigor that computers provide to philosophers, finding logical holes that might not otherwise be apparent. Because a computer stops once it hits a gap in the logic, for it to validate a proof the argument has to be airtight. "In philosophy you’re not always sure that’s true," says Fitelson, noting that metaphysics can be difficult to reason about with the kind of intuition one might apply to, say, geometry.

Zalta had no doubt when Anselm’s premises were fed into Prover9 that it would find a valid proof. "However, when we looked at the actual proof the machine spit out, we saw that it didn’t use all three premises!" Prover9 had found a way to derive Anselm’s conclusion using just one premise.

Whether Anselm’s argument is sound, as opposed to merely valid, depends on whether that premise itself is true—a question that philosophers will continue to debate. Nonetheless, having one premise gives would-be refuters a much clearer target. And, says Zalta, as philosophers develop more results using automated reasoning, the tools’ use should become more widespread.

Back to Top

Back to Top