Argument · Machine-checked in Rocq, Leo-III and Z3
This page explains the argument in plain terms and what three independent computer programs checked about it. Each program's page gives every premise, its formal version, its English meaning, and a tool to run it yourself.
There are only four ways the existence of the universe could be explained:
The first three are impossible. So if the existence of the universe requires a cause, the only remaining explanation is a necessary first cause. And the universe's existence does require a cause, as the next section explains, so the conclusion holds without the “if”.
Three independent programs checked this argument. Rocq is a proof assistant: every step of the proof is written out and verified by a small, trusted checker. Leo-III is an automated prover: it is given the premises and searches for a proof on its own. Z3 is a solver: it searches for a situation in which the premises hold but the conclusion fails, and reports that none exists. All three agree: from the four premises, the conclusion follows.
Each premise was proved, not assumed. The four possibilities are shown to be the only ones by logic alone. Self-creation is shown to contradict itself: the thing would have to both receive its existence and already possess it. Any circle of causes is shown to collapse into the same contradiction, however long the circle. And existence is shown not to be passed along an endless chain of things that only receive it: whatever gives existence must have it of itself. Put together, if the universe's existence has a cause, the chain ends in a first cause that depends on nothing and has existence of itself, which is what "necessary" means here.
A proof is only as strong as its starting points, so every starting point is stated openly. Three concern what "giving existence" means: a giver cannot receive its existence from what it gives it to; whatever is given existence has it through its giver; and existence received through an intermediary is received, ultimately, from that intermediary's source. One is an observation: everything we see causing anything, whether people, nature or machines, only transforms what already exists; nothing observed gives existence itself. Each was tested by removing it, and each time the conclusion failed, so none of them is decorative.
The argument does not depend on time: it holds whether or not the universe had a beginning. It does not, by itself, show that there is only one necessary being, or establish other attributes of the first cause.
The argument begins: if the existence of the universe requires a cause. That “if” is answered by a simple division. Suppose the universe had no cause. Then, considered in itself, it would have to be one of four things:
What counts as “the universe” matters only for case 3. On our definition, the universe does not include the necessary cause, so case 3 cannot arise and the universe as a whole is caused. On a broader definition, such as Spinoza's, the universe includes the necessary, so case 3 is possible and it is the universe's possible part that is caused. The difference is one of naming, not substance: either way, the necessary is reached.
This step rests on one more principle: existence has to come from somewhere, either from a thing's own nature or from something that gives it existence; nothing exists “from nowhere”. It is checked in all three tools as well, and it is step 3 of dalīl al-imkān, Ibn Sīnā's argument from contingency.
Leo-III · automated prover
Given the four premises, Leo-III finds a proof of the conclusion on its own (it reports “Theorem”). It also proves premises 2 and 4; premises 1 and 3 it did not settle in time, so the page links to their Rocq proofs.
Open the Leo-III proof →Rocq · proof assistant
The complete argument, all four premises and the conclusion, in one file. Rocq accepts every step (it reports “exit 0”), and the only logical assumption is excluded middle.
Open the Rocq proof →Z3 · solver
Z3 is asked whether the premises could hold while the conclusion is false. The answer is no (Z3 reports “unsat”, meaning impossible), so the conclusion follows. With any premise removed, the answer becomes yes (“sat”), so each premise is needed.
Open the Z3 checks →| # | Premise | Rocq | Leo-III | Z3 |
|---|---|---|---|---|
| 1 | The four possibilities are the only ones | Proved every step checked view | Not settled no proof found within 50 seconds; this proves nothing either way · proved in Rocq · view | Not expressible in Z3 (infinite chains) · proved in Rocq |
| 2 | Self-creation is impossible | Proved every step checked view | Proved Theorem: Leo-III found a proof view | Confirmed unsat: the opposite is impossible view |
| 3 | Circular creation is impossible | Proved every step checked view | Not settled stopped without an answer; this proves nothing either way · proved in Rocq · view | Confirmed unsat: the opposite is impossible view |
| 4 | An infinite regress of existence-giving is impossible | Proved every step checked view | Proved Theorem: Leo-III found a proof view | Confirmed unsat: the opposite is impossible view |
| C | The conclusion, given the four premises | Proved every step checked view | Proved Theorem: Leo-III found a proof view | Confirmed unsat: the opposite is impossible view |
| U | The universe is caused (the “if” answered) | Proved every step checked view | Proved Theorem: Leo-III found a proof view | Confirmed unsat: the opposite is impossible view |
| C+U | The conclusion without the “if” | Proved every step checked view | Proved Theorem: Leo-III found a proof view | Confirmed unsat: the opposite is impossible view |
Reading the table. Proved means the tool established the premise. For Leo-III, Not settled means it ran out of time without an answer, which proves nothing either way; those premises are proved in Rocq, linked in the same row.
Reading the Z3 column. Z3 is always asked the opposite of the premise: “could this be false while the other premises hold?” Its answer “unsat” means no, that is impossible, which confirms the premise.
For more on what each status means, see Reading a result.
