Automating Leibniz's Theory of Concepts
Computational Metaphysics Group at the Metaphysics Research Lab
Jesse Alama, Paul Oppenheimer, and Edward Zalta

  1. Introduction
  2. The Tools You Will Need
  3. The Main Theorems
  4. An Interactive Interface to our Master File
  5. The Two Fundamental Theorems

1. Introduction

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:

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.

2. The Tools You Will Need

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.

3. The Main Theorems

List of Main Theorems

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

4. An Interactive Interface to our Master File

Master File with Links to Produce Derivations

5. The Two Fundamental Theorems

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 individual u has property F but might not have had F, then (a) the (complete individual) concept of u contains the concept of F, and (b) some (complete) individual concept that is a counterpart to the concept of u fails to contain the concept of F and appears at some non-actual possible world.

This was reconstructed in Zalta 2000 as:

Theorem 40a:
(Fu & ◊¬Fu) → [cucF & ∃c(Counterparts(c, cu) & ccF & ∃w(wwα & Appears(c, w)))]

where the following are all defined in object theory:

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 individual u fails to have property F but might have had F, then (a) the (complete individual) concept of u fails to contain the concept of F, and (b) some (complete) individual concept that is a counterpart to the concept of u contains the concept of F and appears at some non-actual possible world.

This was reconstructed in Zalta 2000 as:

Theorem 40b:
Fu & ◊Fu) → [cucF & ∃c(Counterparts(c, cu) & ccF & ∃w(wwα & 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