A formalization of Spinoza's Ethics, Part 1: Consequences for interpretation Pablo Sierra Márquez Abstract: In order to formalize the first book of Spinoza’s Ethics, we first provide a philosophical interpretation of his philosophy from a perspective aiming at connecting his main ideas in a formal language. This interpretation emphasizes on the original content of Spinoza’s main ideas such as God, infinity, existence, and the true idea rather than the historical content of those concepts for our porpoise is to set the grounds for a formal interpretation of those notions. This work mainly focuses on the Ethics, the Treatise on the Emendation of the Intellect and Letter XII as sources to study those concepts. Based on the interpretation we give a formal analysis of the main concepts found in Ethics, I focusing mainly on the notion of dependence which rules the formal language as the basic relation between the elements of the language, together with its inverse relation causation. Finally we provide a formal language that accounts for the axioms, definitions and the first twenty-three propositions of Ethics, I. This language consists on a extension of First Order Logic with a dependence relation and dependency graphs as models for interpreting the language. Then we give a proof that the set of axioms in our language is consistent and a proof for the twenty-three first proposition of Ethics, I, with some exceptions.