In A Study of Spinoza's Ethics (1984, §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.

翻译：在《斯宾诺莎〈伦理学〉研究》（1984年，§17）中，乔纳森·贝内特主张斯宾诺莎《伦理学》命题V的论证包含可识别的无效推理步骤，且即使认可这些步骤，"该论证充其量只能得出'两个实体不可能共享全部属性'的结论"——而斯宾诺莎实际得出的结论是它们不能共享任何属性。贝内特怀疑，在不引入额外承诺的前提下，斯宾诺莎给定资源中是否真的存在有效的重构方案。迈克尔·德拉·罗卡（《斯宾诺莎》，2008年，第2章）回应指出，若实质性地承诺充足理由律（PSR），该命题便可推导得出。四十年来，这场争论始终停留在散文式论证层面。本文首次为这一争论提供了机器验证证据。我们在Lean 4中将《伦理学》第一部分形式化，将贝内特对斯宾诺莎给定公理的解释编码为类型类，将德拉·罗卡的实质性PSR编码为扩展类。推导尝试产生部分结果——共享全部属性的实体等同——但无法达到命题V"共享任意属性→等同"的完整内容，机械地追踪了贝内特本人所界定的"全属性上限"。一个同时满足两组公理系统但证伪命题V内容的四元素反模型，确立了针对该特定增强方案的不可归约性。第二个反模型为公理A15（斯宾诺莎命题XIV的关键普遍性条款）确立了类似结果。针对德拉·罗卡PSR-实体重构，贝内特的诊断首次获得内核级验证；更强PSR变体的验证仍留待未来作为机械化项目开展。