Formalizing a proof of God by Leibniz

by Tim Smith — 2022-05-08

Leibniz's De Arte Combinatoria ("On the Art of Combination") was published in 1666, when he was 19 or 20 years old. In it, he explores the arithmetical relationship between simple and complex concepts, deriving basic theorems on permutation and combination and applying them to logic, law, theology, etc.

The work also contains a demonstratio existentiae Dei, ad mathematicam certitudinem exacta ("proof of the existence of God, to exact mathematical certitude"). It is a "first mover" argument, with a twist to avoid an infinite regress. The proof is organized into premises and numbered steps, each step citing one or more premises or earlier steps.

I thought it would be fun to formalize this proof in my proof checker Oak. Oak is designed to handle not just mathematical proofs, but philosophical and theological ones as well. It lets you state your premises as axioms, without any restrictions on what they can be, and derive conclusions from them according to the rules of logic.

In translating the proof into Oak, I followed Leibniz's structure as closely as possible. I had to add three premises: a relationship among certain properties, a definition, and an axiom to fill a gap. I restricted another premise to cover just the particular case needed by the proof, and made explicit in others certain conditions which were implicit.

In what follows, I will go through the premises one by one, first giving Leibniz's original text (in Latin), an English translation, and then its formalization into Oak, with commentary on why I formalized it the way I did. Then I will walk through the logic of the proof. The English translations are by Leroy Loemker, with my revisions in square brackets. The original proof (in Latin) can be found here.

If you would like to skip ahead and see the full proof in Oak, it is at the bottom of the page.

Premises

Leibniz gives nine of these, which he calls praecognita ("things previously known"). They are a mix of definitions, postulates, axioms, and observations.

Premise 1

original	Deus est Substantia incorporea infinitae virtutis.
translation	God is an incorporeal substance of infinite power.
oak	`for all x, God[x] iff (substance[x] and incorporeal[x] and infinite_power[x])`

Leibniz labels this a definition, so I have formalized it with iff ("if and only if").

Premise 2

original	Substantiam autem voco, quicquid movet aut movetur.
translation	I call substance whatever moves or is moved.
oak	`for all x, substance[x] iff (mover[x] or is_moved[x])`

Here, movet means "sets in motion", which I have formalized as mover.

Premise 3

original	Virtus infinita est Potentia principalis movendi infinitum.
translation	Infinite power is an original capacity to move the infinite.
oak	`for all x, if (for some y, moves[x,y] and has_infinite_parts[y]) and not is_moved[x] then infinite_power[x]`

Leibniz uses "original capacity" here to distinguish primary from secondary causation, noting that "secondary causes operate by virtue of the primary". I take this to mean that if a mover is being moved by something else, its power is only by virtue of the thing moving it, rather than an original capacity. I therefore require that the mover not be moved itself, for the conclusion of this premise to apply.

I use has_infinite_parts for compatibility with subsequent premises, and to avoid confusion with infinite_power.

Premise 4

original	Liceat quotcunque res simul sumere, et tanquam unum totum supponere.
translation	Any number of things whatever may be taken simultaneously and yet be treated as one whole.
oak	`for some y, for all x, part[x,y] iff (body[x] and mover[x])`

This one I have reduced to the specific instance needed by the proof. The original statement says that any number of things may be treated as a whole, of which they are the parts. This anticipates the notion of a comprehension principle in set theory, which was not developed until 200 years later, and requires great care to formalize. However, in the proof, it is only used in one place, where "any number of things" refers to all bodies which are movers. I have just formalized this specific case, which is all that is required for the proof to go through.

Premise 5

original	Si quid movetur, datur aliud movens.
translation	If anything is moved, there is [another] mover.
oak	`for all x, is_moved[x] implies for some y where y != x and not part[y,x], moves[y,x]`

Loemker's translation has "there is a mover", but aliud means "another". I take this to mean that the mover cannot be the thing being moved, or a part of it.

Premise 6

original	Omne corpus movens movetur.
translation	Every [body which is a mover] is being moved.
oak	`for all x where body[x] and mover[x], is_moved[x]`

Loemker's translation has "Every moving body", but he had previously translated movens as "mover" in Premise 5. From its use in the proof, it is clear that movens here means mover.

Premise 7

original	Motis omnibus partibus movetur totum.
translation	If all its parts are moved, the whole is moved.
oak	`for all x, if (for all y where part[y,x], is_moved[y]) and for some y, part[y,x] then is_moved[x]`

I have made explicit what I take to be implicit in the original, that there must be at least one part for this to apply.

Premise 8

original	Cujuscunque corporis infinitae sunt partes.
translation	Every body whatsoever has an infinite number of parts.
oak	`for all x, body[x] implies has_infinite_parts[x]`

Leibniz believed that every portion of matter is infinitely divisible.

Premise 9

original	Aliquod corpus movetur.
translation	There is a moving body.
oak	`for some x, body[x] and is_moved[x]`

This one is marked as an "observation".

That covers Leibniz's original nine premises. Now for the three I added to make the proof work.

Premise 0a

If x moves y, then x is a mover and y is moved.

for all x,y, moves[x,y] implies (mover[x] and is_moved[y])

This is just stating the relationship among moves, mover, and is_moved.

Premise 0b

To be incorporeal means not to have a body.

for all x, incorporeal[x] iff not body[x]

This is just a definition of "incorporeal".

Premise 0c

If something is incorporeal, it cannot be moved.

for all x, incorporeal[x] implies not is_moved[x]

If something is incorporeal, then it has no body, so there is nothing to be moved. This does not preclude it from moving other things (through whatever incorporeal power it might have), only from being moved itself.

Body of the proof

We will refer to premise 1 as p1, premise 2 as p2, etc.

Leibniz begins by observing that by p9, we know that some body A is in motion, and by p5, we know that there is something B which moves it.

1: for some A, body[A] and is_moved[A] by p9
2: for some B, moves[B,A] by p5,1

We have labelled these statements as 1 and 2, so we can refer back to them later. There are two cases to consider: B is incorporeal, or it is a body.

Case 1: B is incorporeal

In the case that B is incorporeal (which we label as sup in the formalization), Leibniz begins by showing that B must have infinite power. This is because (i) A has infinite parts, (ii) B is moving A, and (iii) being incorporeal, B is not itself moved. Therefore, B is moving an infinite number of parts using its own original capacity, which takes infinite power. Formally:

infinite_power[B] proof
  has_infinite_parts[A] by p8,1
  so thesis by p3,2,sup,p0c
end

Next, B must be a substance, because it is moving something (A).

substance[B] by p2,2,p0a

So now we know that B is an incorporeal substance with infinite power, making it God.

so God[B] by p1,sup

Case 2: B is a body

Now take the case in which B is a body, which we label as sup2 in the formalization. If B is itself moved by something incorporeal, then we can repeat the reasoning from before, with B in the place of A. But if B is moved by another body, which in turn is moved by another body, and so on, then we face either an infinite regress or a cycle, with each body moving the next. To handle this, Leibniz invokes p4, taking together all bodies which are movers, and referring to the whole as C.

3: for some C, for all x, part[x,C] iff (body[x] and mover[x]) by p4

All the parts of C, being bodies that are movers, are themselves moved (by p6). Since we know that C has at least one part (B), we can invoke p7 to conclude that C itself is moved.

for all y where part[y,C], is_moved[y] by p6,3
so 4: is_moved[C] by p7,sup2,2,3,p0a

So there must be some D which moves C, and is neither C nor a part of C.

5: for some D where D != C and not part[D,C], moves[D,C] by p5,4

Now, this D must be incorporeal, because we have already included all bodies which are movers in C, and we know that D is not a part of C.

6: incorporeal[D] by 3,5,p0a,p0b

Because C is moved, it must be a body, hence it must have an infinite number of parts. So D, which is incorporeal and moves C, must have infinite power.

infinite_power[D] proof
  has_infinite_parts[C] by p8,4,p0b,p0c
  so thesis by p3,5,6,p0c
end

D must also be a substance, since it moves C.

substance[D] by p2,5,p0a

So because D is an incorporeal substance with infinite power, it is God.

so God[D] by p1,6

Conclusion

Leibniz has now shown that in both case 1 (B is incorporeal) and case 2 (B is a body), there is a God. Since one or the other must apply, this completes the proof.

What Leibniz, the 17th-century polymath who envisioned a calculus ratiocinator ("calculus of reason") through which reasoning could be reduced to calculation, would have thought of a 21st-century formalization of his work in a computer proof-checking system, I don't know.

But I like to think he would approve.

Full proof

Here is the full proof formalized in Oak. You can try out Oak for yourself by downloading it from oakproof.org. If you have any questions, comments, or suggestions for other proofs to be formalized, I would be happy to hear from you. You can reach me at timsmith3@gmail.com.

# A formalization of Leibniz's proof of the existence of God in his Dissertatio
# de Arte Combinatoria, published in 1666.

# Leibniz's original nine premises
axiom p1: for all x,
  God[x] iff (substance[x] and incorporeal[x] and infinite_power[x])
axiom p2: for all x, substance[x] iff (mover[x] or is_moved[x])
axiom p3: for all x,
  if (for some y, moves[x,y] and has_infinite_parts[y]) and not is_moved[x]
  then infinite_power[x]
axiom p4: for some y, for all x, part[x,y] iff (body[x] and mover[x])
axiom p5: for all x,
  is_moved[x] implies for some y where y != x and not part[y,x], moves[y,x]
axiom p6: for all x where body[x] and mover[x], is_moved[x]
axiom p7: for all x,
  if (for all y where part[y,x], is_moved[y]) and for some y, part[y,x]
  then is_moved[x]
axiom p8: for all x, body[x] implies has_infinite_parts[x]
axiom p9: for some x, body[x] and is_moved[x]

# three extra premises I added to make the proof work
axiom p0a: for all x,y, moves[x,y] implies (mover[x] and is_moved[y])
axiom p0b: for all x, incorporeal[x] iff not body[x]
axiom p0c: for all x, incorporeal[x] implies not is_moved[x]

for some x, God[x]
proof
  1: for some A, body[A] and is_moved[A] by p9
  2: for some B, moves[B,A] by p5,1
  suppose sup: incorporeal[B]
    infinite_power[B] proof
      has_infinite_parts[A] by p8,1
      so thesis by p3,2,sup,p0c
    end
    substance[B] by p2,2,p0a
    so God[B] by p1,sup
  end
  suppose sup2: body[B]
    3: for some C, for all x, part[x,C] iff (body[x] and mover[x]) by p4
    for all y where part[y,C], is_moved[y] by p6,3
    so 4: is_moved[C] by p7,sup2,2,3,p0a
    5: for some D where D != C and not part[D,C], moves[D,C] by p5,4
    6: incorporeal[D] by 3,5,p0a,p0b
    infinite_power[D] proof
      has_infinite_parts[C] by p8,4,p0b,p0c
      so thesis by p3,5,6,p0c
    end
    substance[D] by p2,5,p0a
    so God[D] by p1,6
  end
  so thesis by p0b
end