Formalizing a proof of God by Leibniz
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.
