A Computational Implementation of Leibniz's Paper of 1690

In this project, PROVER9 is used to prove the theorems described by Leibniz in his unpublished paper of 1690. This paper is Leibniz's most mature development of his "calculus of concepts". Actually, Leibniz presents more of an algebra than a calculus; his system provides us with one of the earliest axiom sets for semi-lattices (although he neglected to include the axiom of associativity for the sum operation). Leibniz's paper appears in translation in the collection Leibniz: Logical Papers, edited by G.H.R. Parksinson, and published by Clarendon Press (Oxford) in 1966. A fascimile of the paper can be downloaded here (WARNING: 20 MB PDF file).

The Tools You Will Need

NOTE: The files below all work correctly with the June 2007 version of PROVER9. They may also work with later versions, but they were all checked with the June2007 version. You can download a gzipped tarball of this version here and compile it yourself.

Assuming that you have installed PROVER9, you can download the input and output files linked in below and process them. The standard command-line syntax for running PROVER9 is:

prover9 < theorem.in

or, if you want to append PROVER9's output to a file:

prover9 < theorem.in > theorem.out

If you need further help in running PROVER9, you can consult the manual that goes with the June 2007 version of PROVER9, which can be accessed here.

Similarly, one can use MACE4 to find models of the premises used in the proof of each theorem. This provides a finite verification of the consistency of the axioms and definitions. The standard command-line syntax for running MACE4 is (unless otherwise noted):

mace4 -c -N 8 -p 1 < model.in

or, if you want to append MACE4's output to a file,

mace4 -c -N 8 -p 1 < model.in > model.out

For your convenience, links are included to the PROVER9 and MACE4 output files for each theorem, for the runs we have executed. You can compare your runs to ours.

The Theorems in Leibniz's Paper of 1690

The list of theorems in Leibniz 1690, as formulated in the Parkinson translation, is linked in here (in PDF). Note: (1) Leibniz failed to include the axiom of Associativity for the summation operator ⊕ on concepts. (2) Since the existential quantifier was unavailable to him, Leibniz doesn't use the quantifier in the formulation of any of these theorems.

Before we represented these theorems in PROVER9, we translated them into modern notation. You can download the list of theorems in modern notation here (in PDF). Notes: In these translations, (1) we included the axiom of Associativity for ⊕ in the Basis of the system, and (2) we used the existential quantifier in the formulation of the relation of inclusion (≼) in Definition 3, as well as in Theorems 22 and 23.

In the input files below, we used Sum(x,y) for xy and IsIn(x,y) for xy. So for example, Leibniz's Definition 3 appears in the translation of his original paper as:

That A ‘is in’ L or, that L ‘contains’ A, is the same as that L is assumed to be coincident with several terms taken together, among which is A.

In our translation into modern notation, this definition becomes:

xy ≡ ∃z(xz = y)

And when translated into PROVER9 notation, this becomes:

all x all y (IsIn(x,y) <-> (exists z (Sum(x,z) = y))).

And so on for the other definitions, axioms, and theorems. Note that all of Leibniz's propositions are derivable from the following axiomatic basis:

Idempotence: all x (Sum(x,x) = x).   
Symmetry: all x all y (Sum(x,y) = Sum(y,x)). 
Associativity: all x all y all z (Sum(Sum(x,y),z) = Sum(x,Sum(y,z))).
Dfn Inclusion: all x all y (IsIn(x,y) <-> (exists z (Sum(x,z) = y))). 

In terms of these definitions, we can now use PROVER9 to prove the following theorems. The reader should examine how the theorems as presented in the original and in modern notation are represented in PROVER9's syntax.