Two Necessities in a Machine-Checked Ethics: What Survives Without Causa Sui
Near the end of Part One of the Ethics, Spinoza draws a quiet distinction between two ways a thing can be necessary:
Res aliqua necessaria dicitur vel ratione suae essentiae vel ratione causae. Rei enim alicujus existentia vel ex ipsius essentia et definitione vel ex data causa efficiente necessario sequitur. (E1p33s1)
“A thing is called necessary either by reason of its essence or by reason of its cause. For a thing’s existence follows necessarily either from its essence and definition, or from a given efficient cause.”
In prose commentary, it is easy to nod past that distinction. Essence is not modality: saying that existence belongs to what a thing is says more than saying the thing exists at every possible world (Fine 1994). Yet when you port Part One more geometrico—definitions, axioms, propositions, and demonstrations—into a dependent-type-theory kernel, erasing the difference between those two necessities breaks the system in an unexpected place.
Building on Yuki Nakamura’s (2026) Lean 4 formalization of Ethics Part One (lean 4.13.0, zero Mathlib dependencies), I grouped the axioms into swappable typeclass registers to run a controlled experiment: what in Part One actually depends on causa sui (self-causation)?
1. Why the Modal Bridge Must Run One Way
Nakamura’s modal layer introduces a bridge axiom, A18, identifying a thing’s essence involving existence (involvesExistence x, which Definition 1 equates with causa sui) with existing at every possible world (∀ w, existsAt w x).
Left to right (involvesExistence x → ∀ w, existsAt w x), that bridge is unobjectionable: whatever exists by its very essence exists in every world. Right to left ((∀ w, existsAt w x) → involvesExistence x), however, counts everything that exists at every world as necessary by its essence—collapsing necessity-by-cause into necessity-by-essence.
In Lean’s kernel, two consequences surface immediately:
- Collision with E1p24. Together with the causal axioms (where God’s eternal causality produces modes across worlds), the right-to-left half of
A18forces everything caused by God at every world to be causa sui—flatly contradicting E1p24 (“The essence of things produced by God does not involve existence”). DroppingA18’s converse repairs the conflict cleanly: in the Lean witness modelOneWayBridge, a mode exists at every world through God while its essence does not involve existence. - Essence vs. modal shadow. Upstream treats the derivation of
A13(“a substance’s essence involves existence”, i.e., E1p7) from world-by-world self-causation (A23) as an equal-strength translation. That proof runs straight through the half ofA18that E1p24 rules out. OnceA18is made one-way,A23capturesA13’s modal shadow (∀ w, existsAt w x) and nothing more.
2. Cutting E1p7 at “id est”
Spinoza’s demonstration of E1p7 makes two moves in a single breath:
Substantia non potest produci ab alio (per corollarium propositionis praecedentis); erit itaque causa sui, id est (per definitionem 1) ipsius essentia involvit necessario existentiam… (E1p7d)
“A substance cannot be produced by another (by the corollary of the preceding proposition); it will therefore be cause of itself, that is (by Definition 1), its essence necessarily involves existence…”
What happens if we replace A13 with its outright denial (∀ x, ¬involvesExistence x), keep the repaired one-way modal bridge (TwoNecessitiesRecheck, 58 theorems), re-elaborate every Part One proof verbatim in Lean, and require a machine-checked countermodel for every failure and a consistency witness for every non-trivial survivor?
Lean 4.13 Axiom-Toggle Explorer · Ethica Pars I
Toggle axioms & interpretive readings; click any proposition node below
Recheck R2 (58 theorems: 13 fail & refuted, 20 witnessed, 25 untouched): failures are the exact cone downstream of E1p7. Existence falls, yet God’s self-determined acting (E1p17) survives!
Lean: prop_17_fromNature · prop_17_byXV
Deus ex solis suae naturae legibus et a nemine coactus agit.
“God acts from the laws of its own nature alone, and compelled by no one.”
Headline separation in base R2: because E1p15 proves nothing is outside God, God is determined to act by itself alone in ActingGod — even while causa sui is false!
Three structural surprises emerge from the recheck tables:
First: every failure is downstream of E1p7—and every failure is about existence, not action
In the repaired recheck (R2), 13 of 58 theorems fail (each refuted by a finite Lean model) and 45 survive (20 witnessed in models of the whole altered register; 25 untouched). An automated graph check over Lean’s environment confirms that the failures are exactly the dependency cone downstream of A13 (or A18’s dropped converse):
- E1p7 in all three forms, E1p11’s first demonstration (“God necessarily exists”, which explicitly cites P7), and E1p29 from E1p16’s omnia fail.
- Meanwhile, the substance-attribute architecture (E1p1–6, E1p8, E1p10, E1p14), E1p7’s first step (
Modal.substance_causes_itself_at: any substance that does exist at a world causes itself there), and E1p11’s second demonstration (fromPSRNonExistence, the absence of any preventing cause) all survive and are witnessed.
Second: Definition 7’s two clauses of freedom split cleanly in half
Spinoza defines freedom in E1d7 by pairing existence and action:
Ea res libera dicitur quae ex sola suae naturae necessitate existit et a se sola ad agendum determinatur. (E1d7)
“That thing is called free which exists from the necessity of its nature alone, and is determined to act by itself alone.”
Under the causa sui toggle, nothing satisfies the existence clause—so God is no longer “free” under Definition 7 (god_freeVII fails). Yet E1p17 (“God acts from the laws of its own nature alone, and compelled by no one”) survives! Its proof runs through E1p15 (all things are in God, so nothing exists outside God to compel it), without mentioning A13. In the Lean model ActingGod, God produces a mode and is determined to act by itself alone, while not existing from its own essence.
Third: E1p34 is the exact hinge that ties action back to causa sui
Does causa sui really carry existence and leave action untouched in Spinoza? Only until you encode E1p34 (“God’s power, by which it and all things are and act, is its very essence”) or E1p25s (“in the sense in which God is said to be cause of itself, it must also be said to be cause of all things”).
Added as explicit opt-in reading classes (Prop34.lean), either passage reconnects self-determined action to causa sui. Toggle E1p34 ON alongside ¬A13 in the explorer above and E1p17 collapses with E1p7 (NoCausaSui.no_god_of_power): nothing acts from itself alone, and with E1p17’s own route there is no God. Formalization doesn’t settle how much weight a reader should place on E1p34—it pinpoints where the load-bearing bolt actually sits.
3. Cutting One Step Earlier: Denying Efficient Self-Causation
The causa sui toggle denies Definition 1’s essentialist gloss while still permitting a substance to cause itself at a world. Adding a third toggle—forbidding efficient self-causation outright (∀ x w, ¬causeAt x x w)—turns E1p7’s first step into a three-way squeeze:
- Could an existing substance at world
wbe caused by nothing? Ruled out by E1a3’s second clause (without a determinate cause, no effect can follow). - Could it be caused by another? Ruled out by E1a4 + E1d3 (knowledge of an effect depends on its cause, contradicting substance’s conceptual independence).
- Could it be caused by itself? Ruled out by the toggle.
With all three horns closed—a pattern structurally reminiscent of the fourfold negation (catuṣkoṭi) opening Nāgārjuna’s Mūlamadhyamakakārikā (MMK 1.1)—Lean proves NoSelfCause.no_substance_exists and NoSelfCause.no_god. Yet the resulting theory is still consistent and non-empty: Lean verifies MutualDependenceWitness, a world containing no substance at all, inhabited solely by two finite modes that cause, explain, and compel (coacta, E1p28) one another in a closed loop.