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 x⊕y and IsIn(x,y) for x ≼ y. 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:

x ≼ y ≡ ∃z(x⊕z = 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.

• Proposition 01:

  Original Formulation:	If A=B, then B=A.
  Modern Notation:	x=y → y=x

  • prop01.in
  • prop01.out

  Note: This theorem can be proved from the laws of identity alone, which are built into the logic of PROVER9. Thus it can be proved from the empty set of premises, and so no input model files are provided.

• Proposition 02:

  Original Formulation:	If A ≠ B then, B ≠ A
  Modern Notation:	x ≠ y → y ≠ x

  • prop02.in
  • prop02.out

  Note: This theorem can be proved from the laws of identity alone, which are built into the logic of PROVER9. Thus it can be proved from the empty set of premises, and so no input model files are provided.

• Proposition 03:

  Original Formulation:	If A = B and B = C, then A = C.
  Modern Notation:	[x = y & y = z] → x = z

  • prop03.in
  • prop03.out

  Note: This theorem can be proved from the laws of identity alone, which are built into the logic of PROVER9. Thus it can be proved from the empty set of premises, and so no input model files are provided.

• Proposition 04:

  Original Formulation:	If A = B and B ≠ C, then A ≠ C.
  Modern Notation:	x = y & y ≠ z → x ≠ z

  • prop04.in
  • prop04.out

  Note: This theorem can be proved from the laws of identity alone, which are built into the logic of PROVER9. Thus it can be proved from the empty set of premises, and so no input model files are provided.

• Proposition 05:

  Original Formulation:	If A is in B, and A = C, then C is in B.
  Modern Notation:	[x ≼ y & x = z] → z ≼ y

  • prop05.in
  • prop05.out

  Note: This theorem can be proved from the laws of identity alone, which are built into the logic of PROVER9. Thus it can be proved from the empty set of premises, and so no input model files are provided.

• Proposition 06:

  Original Formulation:	If C is in B and A = B, then C is in A
  Modern Notation:	[x ≼ y & z = y] → x ≼ z

  • prop06.in
  • prop06.out

  Note: This theorem can be proved from the laws of identity alone, which are built into the logic of PROVER9. Thus it can be proved from the empty set of premises, and so no input model files are provided.

• Proposition 07:

  Original Formulation:	A is in A
  Modern Notation:	x ≼ x

  • prop07.in
  • prop07.out
  • model07.in
  • model07.out

• Proposition 08:

  Original Formulation:	A is in B, if A = B
  Modern Notation:	x = y → x ≼ y

  • prop08.in
  • prop08.out
  • model08.in
  • model08.out

• Proposition 09:

  Original Formulation:	If A = B, then A⊕C = B⊕C
  Modern Notation:	x = y → [x⊕z = y⊕z]

  • prop09.in
  • prop09.out

  Notes: (1) This theorem can be proved from the laws of identity alone, which are built into the logic of PROVER9. Thus it can be proved from the empty set of premises, and so no input model files are provided. (2) Leibniz explicitly mentions that this theorem cannot be ‘converted’, meaning that the converse of this theorem is not a theorem. MACE indeed finds a countermodel to the converse:

  • prop09converse-countermodel.in
  • prop09converse-countermodel.out

• Proposition 10:

  Original Formulation:	If A = L and B = M, then A⊕B = L⊕M
  Modern Notation:	[x = z & y = w] → x⊕y = z⊕w

  • prop10.in
  • prop10.out

  Notes: (1) This theorem can be proved from the laws of identity alone, which are built into the logic of PROVER9. Thus it can be proved from the empty set of premises, and so no input model files are provided. (2) Leibniz explicitly mentions that this theorem cannot be ‘converted’, meaning that the converse of this theorem is not a theorem. MACE indeed finds a countermodel to the converse:

  • prop10converse-countermodel.in
  • prop10converse-countermodel.out

• Proposition 11:

  Original Formulation:	If A = L and B = M and C = N, then A⊕B⊕C = L⊕M⊕N
  Modern Notation:	[x = u & y = v & z = w] → x⊕y⊕z = u⊕v⊕w

  We skip this theorem as it is a generalization of Theorems 9 and 10.

• Proposition 12:

  Original Formulation:	If B is in L, then A⊕B will be in A⊕L
  Modern Notation:	y ≼ z → [x⊕y ≼ x⊕z]

  • prop12.in
  • prop12.out
  • model12.in
  • model12.out

• Proposition 13:

  Original Formulation:	If L⊕B = L, then B will be in L
  Modern Notation:	x⊕y = x → y ≼ x

  • prop13.in
  • prop13.out
  • model13.in
  • model13.out

• Proposition 14:

  Original Formulation:	If B is in L, then L⊕B = L
  Modern Notation:	y ≼ x → x⊕y = x

  • prop14.in
  • prop14.out
  • model14.in
  • model14.out

• Proposition 15:

  Original Formulation:	If A is in B and B is in C, then A is in C
  Modern Notation:	[x ≼ y & y ≼ z] → x ≼ z

  • prop15.in
  • prop15.out
  • model15.in
  • model15.out

• Proposition 15 Corollary:

  Original Formulation:	If A⊕N is in B, then N is in B
  Modern Notation:	[x⊕z ≼ y] → z ≼ y

  • prop15-cor.in
  • prop15-cor.out
  • model15-cor.in
  • model15-cor.out

• Proposition 16:

  Original Formulation:	If A is in B and B is in C and C is in D, then A is in D
  Modern Notation:	[x ≼ y & y ≼ z & z ≼ w] → x ≼ w

  We omit this theorem as it is a trivial generalization of Proposition 15.

• Proposition 17:

  Original Formulation:	If A is in B and B is in A, then A = B
  Modern Notation:	[x ≼ y & y ≼ x] → x = y

  • prop17.in
  • prop17.out
  • model17.in
  • model17.out

• Proposition 18:

  Original Formulation:	If A is in L and B is in L, then A⊕B will be in L
  Modern Notation:	[x ≼ z & y ≼ z] → x⊕y ≼ z

  • prop18.in
  • prop18.out
  • model18.in
  • model18.out

• Proposition 19:

  Original Formulation:	If A is in L and B is in L and C is in L, then A⊕B⊕C is in L
  Modern Notation:	[x ≼ z & y ≼ z & w ≼ z] → x⊕y⊕w ≼ z

  We omit this theorem as it is a trivial generalization of Proposition 18.

• Proposition 20:

  Original Formulation:	If A is in M and B is in N, then A⊕B will be in M⊕N
  Modern Notation:	[x ≼ z & y ≼ w] → x⊕y ≼ z⊕w

  • prop20.in
  • prop20.out
  • model20.in
  • model20.out

• Proposition 21:

  Original Formulation:	If A is in M and B is in N and C is in P, then A⊕B⊕C will be in M⊕N⊕P
  Modern Notation:	[x ≼ u & y ≼ v & z ≼ w] → x⊕y⊕z ≼ u⊕v⊕w

  We omit this theorem as it is a trivial generalization of Proposition 20.

• Proposition 22:

  Original Formulation:	Given two disparate terms, A and B, to find a third term C which is different them and which together with them makes up the subalternants A⊕C and B⊕C: that is, although neither of A and B is in the other, yet one of A⊕C and B⊕C is in the other.
  Modern Notation:	[x ⋠ y & y ⋠ x] →     ∃z(z ≠ x & z ≠ y & (x⊕z ≼ y⊕z ∨ y⊕z ≼ x⊕z))

  • prop22.in
  • prop22.out
  • model22.in
  • model22.out

• Proposition 23:

  Original Formulation:	Given two disparate terms, A and B, to find a third term C different from them such that A⊕B = A⊕C
  Modern Notation:	(x ⋠ y & y ⋠ x) → ∃z(z ≠ x & z ≠ y & x⊕y = x⊕z)

  • prop.in
  • prop.out
  • model.in
  • model.out

• Proposition 24: (Exercise)

  Original Formulation:

  To find several terms which are different, each to each, as many as shall be desired, such that from them there cannot be composed a term which is new, i.e., different from any of them.