The Kalām Engine: A Machine-Checked Necessary-Existent Argument

1. Why formalize this at all

"Computational theology" — using proof assistants to check the validity of theological or metaphysical arguments — is a real, published field, not a marketing coinage invented for this site. In 2013, Christoph Benzmüller and Bruno Woltzenlogel Paleo formally verified Kurt Gödel's ontological proof of God's existence in the Isabelle/HOL proof assistant; the result is peer-reviewed and archived in the Isabelle Archive of Formal Proofs. That project is the closest precedent for what this page attempts, and it is a useful model for how to talk about a result like this: Benzmüller and Woltzenlogel Paleo's paper demonstrates that Gödel's argument is formally valid and identifies exactly which of its axioms are doing the controversial work — it does not claim to have proven God exists, and neither does this page claim anything more for Ṭūsī's argument.

A search for prior work specifically formalizing Avicennian or Ṭūsian modal metaphysics in a proof assistant turned up nothing. That absence is reported honestly as "no comparable prior work found" rather than "the first ever" — a smaller, defensible claim, and the same discipline this project has applied elsewhere to superlatives that don't survive checking (the 1913 Wakf Act's "first private member's bill" claim being the clearest example). If this project's Lean file is in fact original in this narrow sense, it is a genuine small contribution — not a repackaging of the Gödel result, which is a different argument entirely.

2. The argument, in Ṭūsī's and Avicenna's terms

The argument rests on a tripartite division of everything that can be thought of into three modal categories: the Necessary (that which cannot not exist), the Contingent (that which can either exist or not, and requires something outside itself to explain which), and the Impossible (that which cannot exist). Given that at least one contingent thing exists — a fact Ṭūsī and Avicenna both take as obvious from experience — each contingent thing requires a cause, and that cause, if itself contingent, requires a further cause, and so on. The argument's engine is a regress-blocking move, historically called Burhān al-Taṭbīq ("the argument from correspondence" or "superimposition"): an infinite regress of causes is ruled out, so the chain of causes must terminate in something that is not itself contingent — and since it exists, and nothing impossible exists, it must be Necessary. This is the load-bearing argument of the Tajrīd's ontology section, and it is the one piece of that section genuinely suited to a complete, checkable formalization at the scale of a single page.

3. The formal argument, worked honestly

Formalizing the argument means stating its premises as explicit axioms — not proving them, just being precise about exactly what is being assumed, so a reader can agree or disagree with each one individually rather than with the argument as an undifferentiated whole.

Theorem. If at least one Contingent entity exists, then a Necessary entity exists.

Proof idea. Take the chain of causal ancestors of a given existing, Contingent entity. Because causation is well-founded (A4), this chain cannot regress forever, so it has a minimal element — an existing, Contingent entity with no contingent cause behind it. By A3 that entity still has a cause; that cause cannot be Contingent (it would extend the chain past its supposed minimum) and cannot be Impossible (A2 rules out an existing Impossible entity); by A1, it must be Necessary. This is exactly the shape of argument well-founded recursion in a proof assistant is built to check.

The Lean 4 source

The theorem is named necessary_root_exists, after the (unfinished, sorry-containing) theorem of the same name in the corpus draft this page replaces. Below is the complete file — nothing has been abbreviated or omitted.

axiom Entity : Type

inductive Status where
  | necessary  : Status
  | contingent : Status
  | impossible : Status
deriving DecidableEq, Repr

axiom status   : Entity → Status
axiom Exists_  : Entity → Prop
axiom cause    : Entity → Entity → Prop

-- A2 (No impossible existents)
axiom A2 : ∀ e : Entity, status e = Status.impossible → ¬ Exists_ e

-- A3 (Principle of Sufficient Reason for contingents)
axiom A3 : ∀ e : Entity, Exists_ e → status e = Status.contingent →
    ∃ c : Entity, Exists_ c ∧ cause c e

-- A4 (Well-foundedness of causation)
axiom A4 : WellFounded cause

theorem necessary_root_exists
    (x0 : Entity) (hx0_exists : Exists_ x0) (hx0_contingent : status x0 = Status.contingent) :
    ∃ n : Entity, Exists_ n ∧ status n = Status.necessary := by
  have main : ∀ e : Entity, Acc cause e →
      Exists_ e → status e = Status.contingent →
      ∃ n : Entity, Exists_ n ∧ status n = Status.necessary := by
    intro e h
    induction h with
    | intro y _ ih =>
      intro hy_exists hy_contingent
      obtain ⟨c, hc_exists, hc_cause⟩ := A3 y hy_exists hy_contingent
      match hstat : status c with
      | .necessary  => exact ⟨c, hc_exists, hstat⟩
      | .impossible => exact absurd hc_exists (A2 c hstat)
      | .contingent => exact ih c hc_cause hc_exists hstat
  exact main x0 (A4.apply x0) hx0_exists hx0_contingent

#print axioms necessary_root_exists

The file uses only Lean 4's own core library (Acc, WellFounded) — no Mathlib import — so the entire dependency graph of this proof is the Lean compiler itself. The full source, project files, and CI configuration are in the kalam-engine directory of this site's repository (§5 below has the build status).

4. The honest complication: Burhān al-Taṭbīq and Cantor

Premise A4 needs its own justification, and the Tajrīd inherits the standard one from Avicenna's Shifāʾ: if an infinite causal chain existed, one could biject a proper sub-chain of it onto the whole chain, which the argument treats as an impossible "part equals whole." Ṭūsī restates and relies on this Avicennian argument rather than originating it — credit for it belongs to Avicenna, with Ṭūsī's use of it noted separately.

The complication is that Georg Cantor showed exactly this kind of bijection is entirely consistent for infinite sets — the natural numbers biject with the even numbers without contradiction — which is precisely the move Burhān al-Taṭbīq treats as impossible. This is a live, published scholarly discussion, not something introduced on this page; see the sources below. The standard defense holds that the argument targets concrete, ordered, existential dependency chains, not abstract set cardinality — whether bijection-without-contradiction (a fact about abstract infinite sets) transfers to a chain of really existing, causally ordered things is exactly what remains disputed. That is a live philosophical position, not a settled rebuttal of Cantor, and not a settled defeat by Cantor either. The proof in §3 is valid regardless of how this dispute is resolved; whether it is sound depends on it, and this page takes no side.

5. Verification status — read this before citing the proof as checked

Bibliography

1. Christoph Benzmüller and Bruno Woltzenlogel Paleo, "Formalization, Mechanization and Automation of Gödel's Proof of God's Existence", arXiv:1308.4526.
2. "Gödel's God" in Isabelle/HOL, Archive of Formal Proofs.
3. "Avicenna's argument against infinite regress in The Metaphysics of the Healing, as a step in proving the existence of God" — Academia.edu.
4. "Avicenna on Mathematical Infinity" (forthcoming, Archiv für Geschichte der Philosophie) — Cambridge repository.
5. "Has Cantor Proved the Muslim Theologians Wrong?" — SeekersGuidance.
6. This project, planning document claude/kalam-computational-theology-scope-v1.md, for the full v1 scope decision and the deferred sections (deontic-logic Walāyah formalization, the Arabic NLP/knowledge-graph pipeline, and the rejected HoTT framing).