Computational Metaphysics Group at the Metaphysics Research Lab

Jesse Alama, Paul Oppenheimer, and Edward Zalta

- Introduction
- The Tools You Will Need
- The Main Theorems
- An Interactive Interface to our Master File
- The Two
*Fundamental*Theorems

The goal of this project is to use automated theorem provers and finite model building programs to prove the theorems of Leibniz's theory of concepts, as reconstructed in the theory of abstract objects. Leibniz's theory of concepts has three components:

- a calculus of concepts (really, an algebraic semi-lattice of concepts),
- a concept containment theory of truth, and
- a modal metaphysics of complete individual concepts.

All three of these components of Leibniz's theory have been reconstructed within the theory of abstract objects, in the following paper:

Edward N. Zalta, 2000, “A (Leibnizian) Theory of Concepts”,Philosophiegeschichte und logische Analyse/Logical Analysis and History of Philosophy, 3: 137–183.

In the paper listed below, we explain how we used automated theorem provers and finite model building programs to investigate the object-theoretic reconstruction of Leibniz's theory in Zalta 2000:

Jesse Alama, Paul E. Oppenheimer, and Edward N. Zalta, 2015, “Automating Leibniz's Theory of Concepts”, in A. Felty and A. Middeldorp (eds.),Proceedings of the 25th International Conference on Automated Deduction, Lecture Notes in Artificial Intelligence, Dordrecht: Springer, forthcoming.

Preprint available online

This paper was presented as one of the invited lectures of the 25th International Conference on Automated Deduction (Berlin, August 2015). In it, we explain our basic methodology for representing the object-theoretic reconstruction of Leibniz's theory in TPTP syntax.

Note that the first component of Leibniz's theory, namely his calculus of concepts, was studied separately, by taking his summation operator ⊕ and concept inclusion relation ≼ as primitive. See the web page for the project: A Computational Implementation of Leibniz's Paper of 1690. At some point, we hope to investigate the object-theoretic reconstruction of this part of Leibniz's theory as well.

Since we developed our theorems using TPTP syntax, any automated reasoning system that takes premises and conclusions in TPTP syntax should work. We used both the E theorem prover system and VAMPIRE, which can be downloaded and/or compiled from here:

We also used PARADOX to build models and find countermodels. See:

Finally, we used Jesse Alama's TIPI tools, available here:

These latter helped us to find minimal premise sets, among other things.

If you skip this link, then note the two *fundamental* theorems
listed in Section 5 below.

The containment theory of truth and Leibniz's modal metaphysics of complete individual concepts combine to yield the following, fundamental theorem (using the numbering scheme of Zalta 2000):

If ordinary individualuhas propertyFbut might not have hadF, then (a) the (complete individual) concept ofucontains the concept ofF, and (b) some (complete) individual concept that is a counterpart to the concept ofufails to contain the concept ofFandappears atsome non-actual possible world.

This was reconstructed in Zalta 2000 as:

Theorem 40a:

(Fu& ◊¬Fu) → [c_{u}≽c_{F}& ∃c(Counterparts(c,c_{u}) &c⋡c_{F}& ∃w(w≠w_{α}&Appears(c,w)))]

where the following are all defined in object theory:

**c**_{u}is the complete individual concept of*u*,**c**_{F}is the concept of*F*,*c*is a variable ranging over complete individual concepts,*w*is a variable ranging over possible worlds, and**w**_{α}is the distinguished actual world.

When Theorem 40a is represented in TPTP syntax, as explained in the Alama et al. 2015, the result is:

Theorem 40a:

fof(theorem_40a,conjecture,

(! [U,F] : ((object(U) & property(F)) =>

((ex1_wrt(o,U,d) & ex1_wrt(F,U,d) &

(? [D] : (point(D) & ~ex1_wrt(F,U,D)))) =>

(? [X,Y] : (object(X) & object(Y) & ex1_wrt(c,X,d) &

ex1_wrt(c,Y,d) & is_the_concept_of_individual_wrt(X,U,d) &

is_the_concept_of_wrt(Y,F,d) & contains_wrt(X,Y,d) &

(? [Z] : (object(Z) & ex1_wrt(c,Z,d) &

counterparts_wrt(Z,X,d) & ~contains_wrt(Z,Y,d) &

(? [A,W] : (object(A) & object(W) &

is_the_actual_world_wrt(A,d) & world_wrt(W,d) &

~equal_wrt(W,A,d) & appears_in_wrt(Z,W,d))))))))))).

The input file for this theorem is:

theorem40a.p

By comparison, Theorem 40b asserts:

If ordinary individualufails to have propertyFbut might have hadF, then (a) the (complete individual) concept ofufails to contain the concept ofF, and (b) some (complete) individual concept that is a counterpart to the concept ofucontains the concept ofFandappears atsome non-actual possible world.

This was reconstructed in Zalta 2000 as:

Theorem 40b:

(¬Fu& ◊Fu) → [c_{u}⋡c_{F}& ∃c(Counterparts(c,c_{u}) &c≽c_{F}& ∃w(w≠w_{α}&Appears(c,w)))]

Finally, this was represented in TPTP syntax as:

Theorem 40a:

fof(theorem_40a,conjecture,

(! [U,F] : ((object(U) & property(F)) =>

((ex1_wrt(o,U,d) & ~ex1_wrt(F,U,d) &

(? [D] : (point(D) & ex1_wrt(F,U,D)))) =>

(? [X,Y] : (object(X) & object(Y) & ex1_wrt(c,X,d) &

ex1_wrt(c,Y,d) & is_the_concept_of_individual_wrt(X,U,d) &

is_the_concept_of_wrt(Y,F,d) & ~contains_wrt(X,Y,d) &

(? [Z] : (object(Z) & ex1_wrt(c,Z,d) &

counterparts_wrt(Z,X,d) & contains_wrt(Z,Y,d) &

(? [A,W] : (object(A) & object(W) &

is_the_actual_world_wrt(A,d) & world_wrt(W,d) &

~equal_wrt(W,A,d) & appears_in_wrt(Z,W,d))))))))))).

The input file for this theorem is:

theorem40b.p