Dalīl al-imkān · al-Kalam

Since something exists, a Necessary Existent exists.

Ibn Sīnā's argument from contingency, checked step by step by three independent computer programs. It starts from nothing but the fact that something exists. Each program's page gives every step, its formal version, its English meaning, and a tool to run it yourself.

The argument

Twelve steps

Every existent is either necessary in itself (wājib al-wujūd bi-dhātihi) or possible in itself (mumkin al-wujūd bi-dhātihi), but not both.
If an existent is necessary in itself, its non-existence is not possible.
If an existent is possible in itself, its existence and non-existence are both possible; therefore its existence requires a determining cause (murajjiḥ).
A possible existent cannot be the sufficient cause of its own existence: that would require it to be both dependent upon and independent of itself in the same respect.
Consider the aggregate of all existing beings that are possible in themselves, including every possible cause invoked to explain their existence. Whether one, finitely many, or infinitely many, no possible cause lies outside the aggregate.
The aggregate, considered collectively, is itself possible in itself and therefore requires a determining cause.
A sufficient cause of the existence of the entire aggregate must account for the existence of every constituent. If that cause were a member, or a subset of members considered collectively, it would have to account for its own existence, contrary to step 4.
Neither an individual possible, nor a subset of possibles, nor an aggregate composed entirely of possibles can sufficiently cause its own existence.
The existence of the aggregate therefore requires a cause outside the aggregate of possibles.
By the exhaustive division, an existing cause that is not possible in itself is necessary in itself.
The cause upon which the possible depends must therefore be a Necessary Existent.
Since something exists, a Necessary Existent must exist.

What the computers checked

In plain terms

Every thing that exists either has its existence from its own nature, or it does not. The first is necessary in itself; the second is possible in itself. Nothing is both. This division was proved from logic alone. A possible thing is not defined as “needing a cause”; that it needs one was proved, from the principle that existence has to come from somewhere: from a thing's own nature, or from something that gives it existence.

The heart of the argument is Ibn Sīnā's move to the aggregate: take all possible things together, however many, even infinitely many. The whole is possible too, because putting possible things together does not make something necessary. So the whole needs a cause. That cause cannot be a member, or a group of members, since it would then give existence to itself, through a chain if not directly, and a circle of giving is impossible. So the cause lies outside all possible things. It exists and is not possible, so it is necessary in itself.

The argument starts only from the fact that something exists, which Ibn Sīnā treats as self-evident rather than observed: even a person with no senses at all knows that he exists. If what exists is necessary, the conclusion holds at once; if it is possible, the aggregate argument applies. No time appears anywhere, so the argument holds even if the world has always existed: a thing can be possible in itself and yet always exist, necessitated by its cause.

A proof is only as strong as its starting points, so every one is stated openly on the proof pages, and each was tested by removing it: each time, the conclusion failed. The steps critics are most likely to press are the claim that the collection of all possibles is a real whole, that possibles cannot add up to something necessary, and that whatever gives existence to a whole gives it to each of its members. The argument does not, by itself, show that there is only one Necessary Existent, or establish its further attributes.

A second, shorter proof reaches the same conclusion without the aggregate, using the observation that everything we see causing anything only transforms what already exists, the same observation that grounds dalīl al-kalima. The aggregate proof is the primary one, because it does not share that premise, so the two arguments stand independently.

Check it yourself

Three independent tools

Rocq · proof assistant

Every step checked

All twelve steps and both proofs in one file. Rocq accepts every step (it reports “exit 0”), and the only logical assumption is excluded middle.

Open the Rocq proof →

Leo-III · automated prover

The steps yield the conclusion

Given the proved steps and “something exists”, Leo-III finds on its own a proof that a Necessary Existent exists (it reports “Theorem”), by both proofs.

Open the Leo-III proof →

Z3 · solver

No counterexample exists

Z3 is asked whether the premises could hold while the conclusion is false. The answer is no (“unsat”, meaning impossible), so the conclusion follows. The premises themselves can all hold together (“sat”, meaning possible).

Open the Z3 checks →

Steps and their proofs

Step by step

Step	Claim	Rocq
1	The division	Proved every step checked view
2	The necessary cannot fail	Proved every step checked view
3	The possible needs a cause	Proved every step checked view
4	Nothing causes itself	Proved every step checked view
5–6	The aggregate is possible	Proved every step checked view
7–11	Its cause is outside and necessary	Proved every step checked view
12	A Necessary Existent exists	Proved every step checked view
(b)	The short route	Proved every step checked view

Leo-III and Z3 independently confirm that these steps yield the conclusion, by both proofs. For what each status means, see Reading a result.