Philosophy | DOI: 10.1145/1941487.1941496
Deus ex machina
Computational metaphysics is helping philosophers
answer age-old questions, such as whether God exists.
A faMoUsLy trICky argu- ment for the existence of God proposed by the Brit- ish theologian Anselm in the 11th 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 air-
Marina Krakovsky
tight. “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.
© 2011 aCM 0001-0782/11/05 $10.00
IlluSTra TIon By GWen VanHee
Based in San Francisco, Marina Krakovsky is the
co-author of Secrets of the Moneylab: How Behavioral
Economics Can Improve Your Business.
