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.|
iff("if and only if").
|original||Substantiam autem voco, quicquid movet aut movetur.|
|translation||I call substance whatever moves or is moved.|
|original||Virtus infinita est Potentia principalis movendi infinitum.|
|translation||Infinite power is an original capacity to move the infinite.|
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.
has_infinite_parts for compatibility with subsequent premises, and to avoid confusion with
|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.|
|original||Si quid movetur, datur aliud movens.|
|translation||If anything is moved, there is [another] mover.|
|original||Omne corpus movens movetur.|
|translation||Every [body which is a mover] is being moved.|
|original||Motis omnibus partibus movetur totum.|
|translation||If all its parts are moved, the whole is moved.|
|original||Cujuscunque corporis infinitae sunt partes.|
|translation||Every body whatsoever has an infinite number of parts.|
|original||Aliquod corpus movetur.|
|translation||There is a moving body.|
|If x moves y, then x is a mover and y is moved.|
|To be incorporeal means not to have a body.|
|If something is incorporeal, it cannot be moved.|
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.
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.
1: for some A, body[A] and is_moved[A] by p9 2: for some B, moves[B,A] by p5,1
supin 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:
Next, B must be a substance, because it is moving something (A).
infinite_power[B] proof has_infinite_parts[A] by p8,1 so thesis by p3,2,sup,p0c end
So now we know that B is an incorporeal substance with infinite power, making it God.
substance[B] by p2,2,p0a
so God[B] by p1,sup
sup2in 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.
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.
3: for some C, for all x, part[x,C] iff (body[x] and mover[x]) by p4
So there must be some D which moves C, and is neither C nor a part of C.
for all y where part[y,C], is_moved[y] by p6,3 so 4: is_moved[C] by p7,sup2,2,3,p0a
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.
5: for some D where D != C and not part[D,C], moves[D,C] by p5,4
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.
6: incorporeal[D] by 3,5,p0a,p0b
D must also be a substance, since it moves C.
infinite_power[D] proof has_infinite_parts[C] by p8,4,p0b,p0c so thesis by p3,5,6,p0c end
So because D is an incorporeal substance with infinite power, it is God.
substance[D] by p2,5,p0a
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