pith. sign in

arxiv: 2605.02331 · v2 · pith:S6VUCCDWnew · submitted 2026-05-04 · 💻 cs.LO · math.LO

Bennett's Conjecture in Lean 4: Counter-Models for the PSR-Reducibility of Spinoza's Propositions V and XIV

Yuki Nakamura This is my paper

Pith reviewed 2026-05-21 00:51 UTC · model grok-4.3

classification 💻 cs.LO math.LO
keywords SpinozaEthicaLean 4formal verificationcounter-modelsPrinciple of Sufficient ReasonBennett conjecturephilosophical logic
0
0 comments X

The pith

Lean 4 formalization yields counter-models showing Spinoza's Proposition V is irreducible to axioms plus substantive PSR.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper encodes Spinoza's Ethica Part I axioms in Lean 4 according to Bennett's reading and tests whether Della Rocca's substantive Principle of Sufficient Reason suffices to derive Proposition V. The formal system reaches only the limited conclusion that substances sharing all attributes are identical, but fails to establish that substances sharing any attribute must be identical. A four-element counter-model satisfies the full axiom set together with the PSR extension yet falsifies the target proposition, supplying the first machine-checked evidence for non-derivability under this reconstruction. An analogous counter-model shows the same result for Proposition XIV via axiom A15.

Core claim

The derivation attempt yields a partial result -- substances sharing all attributes are identical -- but cannot reach the full 'sharing-any-attribute -> identity' content of Proposition V. A four-element counter-model satisfying both axiom sets while falsifying Proposition V's content establishes the irreducibility against this specific augmentation.

What carries the argument

Encoding of Bennett's reading of Spinoza's stated axioms as a typeclass and Della Rocca's substantive PSR as an extension class in Lean 4, together with explicit counter-model construction to witness non-derivability.

Load-bearing premise

The encoding of Bennett's reading of Spinoza's stated axioms as a typeclass and Della Rocca's substantive PSR as an extension class accurately captures the philosophical positions without introducing or omitting commitments that would alter the derivability question.

What would settle it

A successful Lean derivation of the full content of Proposition V from the encoded axioms plus the PSR extension, or a proof that the four-element model violates one of the axioms or the PSR clause, would refute the irreducibility result.

read the original abstract

In A Study of Spinoza's Ethics (1984, {\S}17), Jonathan Bennett argues that the demonstration of Proposition V of Spinoza's Ethica contains identifiable invalid moves and that, even granted those moves, "cannot yield more than the conclusion that two substances could not have all their attributes in common" -- while Spinoza concludes that they cannot share any. Bennett doubts that any valid reconstruction is available from Spinoza's stated resources without importing further commitments. Michael Della Rocca (Spinoza, 2008, ch. 2) responds that the proposition can be derived if the Principle of Sufficient Reason (PSR) is committed substantively. The debate has remained at the level of prose argument for forty years. This paper provides the first machine-checked evidence in the debate. We formalise Ethica Pars I in Lean 4, encoding Bennett's reading of Spinoza's stated axioms as a typeclass and Della Rocca's substantive PSR as an extension class. The derivation attempt yields a partial result -- substances sharing all attributes are identical -- but cannot reach the full "sharing-any-attribute -> identity" content of Proposition V, mechanically tracking Bennett's own all-attributes ceiling. A four-element counter-model satisfying both axiom sets while falsifying Proposition V's content establishes the irreducibility against this specific augmentation. A second counter-model establishes the analogous result for axiom A15, a load-bearing universality clause for Spinoza's Proposition XIV. Bennett's diagnosis receives its first kernel-checked counter-model against the Della-Rocca PSR-substance reconstruction (the non-derivability claim itself a meta-logical consequence of kernel consistency); stronger PSR variants and the broader narrative claim against the full Section I + II + A1--A7 register remain open as future mechanical projects.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

0 major / 2 minor

Summary. The paper formalizes Spinoza's Ethica Pars I in Lean 4 by encoding Bennett's reading of the stated axioms as a typeclass and Della Rocca's substantive PSR as an extension class. It derives the partial result that substances sharing all attributes are identical but cannot reach the full content of Proposition V (sharing any attribute implies identity). This non-derivability is witnessed by a four-element counter-model satisfying both axiom sets and the PSR extension while falsifying Proposition V; an analogous counter-model is given for Proposition XIV via axiom A15.

Significance. If the encodings are accepted as faithful to the respective philosophical positions, the result is significant as the first kernel-checked evidence in the Bennett-Della Rocca debate on PSR-reducibility. The explicit use of machine-checked derivations and concrete counter-models is a clear strength: the non-derivability claim follows directly as a meta-logical consequence of Lean kernel consistency rather than from any ad-hoc parameter or circular definition. This supplies reproducible, falsifiable support for Bennett's 'all-attributes ceiling' diagnosis and demonstrates the value of formal methods for settling long-standing interpretive disputes in early modern philosophy.

minor comments (2)
  1. Abstract: the clause 'mechanically tracking Bennett's own all-attributes ceiling' is concise but could be glossed in one additional sentence for readers outside the Spinoza literature so that the partial result is immediately intelligible.
  2. The description of the four-element model would benefit from a short remark on why models with fewer elements fail to satisfy the combined axiom set, thereby clarifying the minimality of the counter-example.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for their careful reading of the manuscript and for the positive assessment and recommendation to accept. The referee summary accurately captures the formalization approach, the partial result on shared attributes, and the role of the counter-models in establishing non-derivability under the stated encodings.

Circularity Check

0 steps flagged

No significant circularity

full rationale

The paper encodes Bennett's reading of Spinoza's axioms as a Lean 4 typeclass and Della Rocca's PSR as an extension class, then exhibits explicit four-element counter-models that satisfy both while falsifying the full content of Propositions V and XIV. Non-derivability follows directly as a meta-logical consequence of model existence plus Lean kernel consistency; the construction contains no fitted parameters renamed as predictions, no self-definitional loops, no load-bearing self-citations, and no imported uniqueness theorems. The result is self-contained against the external benchmark of the verified formal system.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 0 invented entities

The central claim rests on the faithful encoding of Spinoza's historical axioms and the construction of finite models in dependent type theory; no free parameters are introduced and no new entities are postulated beyond the formal language itself.

axioms (2)
  • domain assumption Spinoza's stated axioms A1-A7 and background principles of Ethica Pars I as read by Bennett
    Encoded directly as a Lean typeclass; the counter-models are required to satisfy this class.
  • domain assumption Della Rocca's substantive Principle of Sufficient Reason as an extension class
    Added to the typeclass hierarchy; models must satisfy both the base class and this extension.

pith-pipeline@v0.9.0 · 5855 in / 1474 out tokens · 46639 ms · 2026-05-21T00:51:58.319862+00:00 · methodology

Review history (2 revisions) →

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Lean theorems connected to this paper

Citations machine-checked in the Pith Canon. Every link opens the source theorem in the public Lean library.

What do these tags mean?
matches
The paper's claim is directly supported by a theorem in the formal canon.
supports
The theorem supports part of the paper's argument, but the paper may add assumptions or extra steps.
extends
The paper goes beyond the formal theorem; the theorem is a base layer rather than the whole result.
uses
The paper appears to rely on the theorem as machinery.
contradicts
The paper's claim conflicts with a theorem or certificate in the canon.
unclear
Pith found a possible connection, but the passage is too broad, indirect, or ambiguous to say the theorem truly supports the claim.

Reference graph

Works this paper leans on

5 extracted references · 5 canonical work pages

  1. [1]

    Bennett, Jonathan. 1984. A Study of Spinoza’s Ethics . Indianapo- lis: Hackett

    work page 1984

  2. [2]

    The Lean 4 Theorem Prover and Programming Language

    Carneiro, Mario. 2019. The Type Theory of Lean . MSc thesis, Carnegie Mellon University . https://github.com/digama0/lean- type-theory/releases. Curley , Edwin, ed. and trans. 1985. The Collected Works of Spinoza. Vol. 1. Princeton: Princeton University Press. de Moura, Leonardo, and Sebastian Ullrich. 2021. “The Lean 4 Theorem Prover and Programming Lang...

    work page 2019

  3. [3]

    Ethics IP5: Shared Attributes and the Basis of Spinoza’s Monism

    Garrett, Don. 1990. “Ethics IP5: Shared Attributes and the Basis of Spinoza’s Monism.” In Central Themes in Early Modern Philos- ophy: Essays Presented to Jonathan Bennett , edited by J. A. Cover and Mark Kulstad, 69–107. Indianapolis: Hackett

    work page 1990

  4. [4]

    Garrett, Don. 2018. Nature and Necessity in Spinoza’s Philoso- phy. New York: Oxford University Press

    work page 2018

  5. [5]

    Sets in Types, Types in Sets

    Spinoza, Benedictus de. 1677. Ethica Ordine Geometrico Demon- strata. In B. d. S. Opera Posthuma , edited by Jarig Jelles. Amster- 41 dam: Jan Rieuwertsz. Werner , Benjamin. 1997. “Sets in Types, Types in Sets.” In Theoretical Aspects of Computer Software (TACS ’97) , edited by Martín Abadi and Takayasu Ito, 530–546. Lecture Notes in Com- puter Science 12...

    work page 1997