arxiv: 2605.02331 · v1 · submitted 2026-05-04 · 💻 cs.LO · math.LO

Recognition: 3 theorem links

· Lean Theorem

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

Yuki Nakamura

Authors on Pith no claims yet

Pith reviewed 2026-05-08 18:40 UTC · model grok-4.3

classification 💻 cs.LO math.LO

keywords Spinoza EthicsLean 4 formalizationPrinciple of Sufficient Reasoncounter-modelProposition VBennett conjecturereducibilityaxiom A15

0 comments

The pith

A four-element counter-model in Lean 4 satisfies Spinoza's axioms plus substantive PSR yet falsifies the full content of Proposition V.

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

The paper formalizes the axioms of Spinoza's Ethics Part I inside Lean 4, treating Bennett's reading of the stated axioms as one typeclass and Della Rocca's substantive use of the Principle of Sufficient Reason as an extension. Under this augmented theory the system can derive only the limited claim that substances sharing every attribute must be identical; the stronger claim that any shared attribute forces identity remains unreachable. A concrete four-element structure is exhibited that obeys both the original axioms and the PSR extension while violating the full statement of Proposition V, thereby supplying the first machine-checked evidence for Bennett's conjecture of irreducibility. An analogous counter-model is given for Proposition XIV and its supporting axiom A15.

Core claim

Even after the axioms of the Ethics are supplemented by a substantive commitment to the Principle of Sufficient Reason, the full content of Proposition V—that no two distinct substances can share any attribute—still fails to follow, because a four-element model exists that satisfies the augmented axiom set yet contains two distinct substances that share an attribute.

What carries the argument

Lean 4 encoding of Spinoza's axioms as a typeclass, Della Rocca's substantive PSR as an extension class, and explicit counter-model construction that satisfies the theory while falsifying the target proposition.

Load-bearing premise

The Lean encoding of Bennett's reading of Spinoza's stated axioms as a typeclass and Della Rocca's substantive PSR as an extension class faithfully captures the original philosophical commitments without introducing extraneous strength or weakness.

What would settle it

Exhibit a four-element structure in which every axiom and the substantive PSR hold, yet two distinct substances share at least one attribute; if no such structure exists the irreducibility claim is false.

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-level confirmation against the Della-Rocca PSR-substance reconstruction; stronger PSR variants 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.

Desk Editor's Note private letter to a colleague

The paper delivers the first Lean 4 formalization of the Bennett-Della Rocca debate, with explicit four-element counter-models that block full derivation of Spinoza's Prop V under the given PSR augmentation.

read the letter

The paper gives the first machine-checked counter-models in the Bennett-Della Rocca debate on Spinoza's Proposition V. It formalizes Bennett's reading of the axioms in Lean 4 as a typeclass, adds Della Rocca's PSR as an extension, and shows that the derivation reaches only the all-attributes identity but not the full any-attribute version. A four-element model satisfies both but falsifies the proposition's content. A similar result holds for the load-bearing axiom behind Proposition XIV. This is new because the prior discussion stayed in prose for forty years. The work tracks the derivation ceiling mechanically and supplies explicit counter-models that were not available before. The Lean code makes the limits reproducible in principle. The soft spot is the fidelity of the encoding. The counter-models work inside the formal system, but the philosophical claim depends on the typeclasses matching Bennett's and Della Rocca's commitments without added or missing strength. The abstract does not report independent checks on that mapping, so a gap there would limit how far the result travels back to the original standoff. This paper is for people who want to see formal methods applied to interpretive disputes in the history of philosophy. A reader comfortable with Lean or interested in Spinoza's metaphysics will get the most from the models and the partial derivation result. It deserves a serious referee. The formal contribution is concrete and the limitation is clearly stated, so review can focus on the encoding choices and their interpretive accuracy.

Referee Report

2 major / 2 minor

Summary. The paper formalizes Spinoza's Ethica Pars I in Lean 4, encoding Bennett's reading of the stated axioms as a typeclass and Della Rocca's substantive PSR as an extension class. It shows that the derivation reaches only the limited conclusion that substances sharing all attributes are identical, but cannot reach the full content of Proposition V (sharing any attribute implies identity). A four-element counter-model is exhibited that satisfies both axiom sets and the PSR extension while falsifying the full Proposition V; an analogous counter-model is given for Proposition XIV and axiom A15. This supplies the first machine-checked evidence bearing on Bennett's conjecture against the Della Rocca reconstruction.

Significance. If the typeclass encodings faithfully capture the original commitments, the result is significant: it supplies the first mechanically verified counter-models in a forty-year prose debate, confirming Bennett's diagnosis that the stated resources plus substantive PSR reach only an 'all-attributes' ceiling. The work earns credit for reproducible Lean formalization, explicit derivation tracking, and concrete falsifying models rather than abstract argument.

major comments (2)

[§3] §3 (Formalization of axioms and PSR): The central philosophical claim—that the counter-models establish irreducibility against Della Rocca's reconstruction—depends on the typeclass definitions preserving exactly the logical strength of Bennett's reading of the stated axioms plus the substantive PSR extension. The manuscript must supply an explicit item-by-item mapping (or Lean instance code with commentary) between the original axiom statements and the typeclass declarations; without it, a mismatch would render the four-element model irrelevant to the original debate.
[§4.1] §4.1 (Four-element counter-model for Proposition V): The claim that the model satisfies both axiom sets while falsifying the full content of Proposition V is load-bearing. The paper must include the explicit Lean instance definitions or a machine-checked verification script showing that every required axiom and the PSR extension hold in the model; mere assertion of satisfaction is insufficient for a formal-methods paper.

minor comments (2)

[Abstract] Abstract: the term 'kernel-level confirmation' is non-standard and potentially misleading; replace with 'machine-checked confirmation' or 'formal verification inside the Lean kernel'.
[§3] The paper should include a short table or prose list mapping each Spinoza axiom (A1–A8, A15) to its Lean encoding for quick cross-reference by philosophical readers.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for their careful reading and constructive comments on our formalization of Spinoza's Ethica Pars I in Lean 4. The points raised have prompted us to enhance the transparency of our encodings and the verifiability of the counter-models. We address each major comment below, with revisions incorporated into the manuscript.

read point-by-point responses

Referee: [§3] §3 (Formalization of axioms and PSR): The central philosophical claim—that the counter-models establish irreducibility against Della Rocca's reconstruction—depends on the typeclass definitions preserving exactly the logical strength of Bennett's reading of the stated axioms plus the substantive PSR extension. The manuscript must supply an explicit item-by-item mapping (or Lean instance code with commentary) between the original axiom statements and the typeclass declarations; without it, a mismatch would render the four-element model irrelevant to the original debate.

Authors: We agree that an explicit mapping is required to substantiate the claim that our typeclass encodings faithfully capture Bennett's reading of the axioms together with the substantive PSR. In the revised manuscript we have inserted a new subsection in §3 containing an item-by-item table. Each row lists (i) the original axiom statement as interpreted by Bennett, (ii) the corresponding Lean 4 typeclass declaration, and (iii) a brief commentary on how the logical strength is preserved. Relevant Lean code snippets are included for each axiom and for the PSR extension class. This addition directly addresses the risk of mismatch and makes the philosophical relevance of the counter-models fully transparent. revision: yes
Referee: [§4.1] §4.1 (Four-element counter-model for Proposition V): The claim that the model satisfies both axiom sets while falsifying the full content of Proposition V is load-bearing. The paper must include the explicit Lean instance definitions or a machine-checked verification script showing that every required axiom and the PSR extension hold in the model; mere assertion of satisfaction is insufficient for a formal-methods paper.

Authors: We accept that, in a formal-methods context, assertion alone is insufficient and that explicit, machine-checkable code must be supplied. We have therefore revised §4.1 to include the complete Lean 4 instance definitions for the four-element counter-model. In addition, we now provide a self-contained verification script (presented as a Lean code block) that confirms, via #check or similar commands, that every axiom and the PSR extension are satisfied in the model while the full content of Proposition V is falsified. The same treatment has been applied to the counter-model for Proposition XIV and axiom A15. These additions render the counter-models fully reproducible and verifiable. revision: yes

Circularity Check

0 steps flagged

No circularity; explicit counter-model construction is independent of inputs

full rationale

The paper's chain consists of encoding Bennett's reading of Spinoza's axioms as a Lean typeclass, Della Rocca's PSR as an extension, attempting derivation (yielding only a partial result), and exhibiting concrete four-element models that satisfy the encoded axioms yet falsify Prop V (and similarly for A15). This is a direct, machine-checked non-entailment inside the formal system; the models are constructed to witness the gap rather than being fitted or renamed from prior results. No step reduces by definition to its inputs, no self-citation is load-bearing for the central claim, and the formalization is presented as self-contained evidence against the specific reconstruction. External philosophical fidelity is a separate correctness question, not a circularity reduction.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 0 invented entities

The work rests on two interpretive encodings of Spinoza's axioms plus one added PSR principle; no numerical parameters are fitted.

axioms (2)

domain assumption Spinoza's stated axioms of Ethica Pars I as read by Bennett
Encoded as Lean typeclass; the paper treats this as the baseline resource set.
domain assumption Della Rocca's substantive Principle of Sufficient Reason
Added as extension class; the paper tests whether this augmentation suffices for full Prop V.

pith-pipeline@v0.9.0 · 5588 in / 1401 out tokens · 34437 ms · 2026-05-08T18:40:52.846811+00:00 · methodology

discussion (0)

Lean theorems connected to this paper

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

n/a — does not engage J-cost, φ, 8-tick, or constants chain (Cost.FunctionalEquation, Foundation.DimensionForcing, Constants.*) reality_from_one_distinction unclear

?

unclear
Relation between the paper passage and the cited Recognition theorem.

The central result is the partial reduction theorem prop_5_demote_via_PSR_all_attributes plus counter-model A12CounterModel.

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

4 extracted references

[1]

The Lean 4 Theorem Prover and Programming Language

Bennett, Jonathan. 1984. A Study of Spinoza’s Ethics . Indianapo- lis: Hackett. 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 Language.” In Automated De- duction — CADE 28 , edited by André Platz...

1984
[2]

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. 38

1990
[3]

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

2018
[4]

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- 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 1281....

1997