Edward Zalta
Stanford University

"Steps Towards a Computational Metaphysics"

Abstract:
In this presentation, the authors describe their work in developing the new discipline of computational metaphysics. Our method is to implement an axiomatic metaphysics in the automated reasoning program OTTER. In the first part of the talk, we review the basic principles of E. Zalta's axiomatic theory of abstract objects. This metaphysics is couched in a syntactically second-order modal predicate calculus with one new atomic mode of predication ("xF", read: x encodes F). The basic comprehension principle for the theory asserts that for every condition on properties, there is an abstract object which encodes just the properties satisfying the condition. Identity conditions are also given: abstract x and y are identical iff they encode the same properties. Comprehension and identity conditions for properties, relations and propositions are also given. Then, objects such as Forms, Monads, concepts, possible worlds, natural numbers, etc., are defined and the basic principles about them are derived from the proper axioms. In the second part of the talk, we show how the resulting theory can be represented in OTTER's first-order syntax. The basic idea is to use a multi-sorted first-order language, with sorts for objects, properties, propositions, etc. Once the axioms and definitions are represented in OTTER's syntax, we then formulate the claims we expect OTTER to prove. OTTER then uses classic theorem-proving techniques, such as hyperresolution, to derive a contradiction from the negation of the claims we want to prove. The resulting computational system can find proofs of interesting theorems of metaphysics that are consequences of the axiomatic theory, such as the theorem that every possible world is maximal. This is joint work with Branden Fitelson.

Back to Talks Page