*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.

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").
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,

`mover`

.
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`

.

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.

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

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

`mover`

.
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.

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.

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.

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`

.
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".

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.

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```
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: `sup`

in the formalization), Leibniz begins by showing that ```
infinite_power[B] proof
has_infinite_parts[A] by p8,1
so thesis by p3,2,sup,p0c
end
```

Next, `substance[B] by p2,2,p0a`

So now we know that `so God[B] by p1,sup`

`sup2`

in the formalization. If `3: for some C, for all x, part[x,C] iff (body[x] and mover[x]) by p4`

All the parts of ```
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 `5: for some D where D != C and not part[D,C], moves[D,C] by p5,4`

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

Because ```
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 because `so God[D] by p1,6`

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.

```
# 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
```