We examine the possibility of applying knowledge representation and automated reasoning in the context of philosophical ontology. For this purpose, we use the axioms and propositions in the ¯rst book of Spinoza's Ethics as knowledge base and a tableau-based satis¯ability tester as reasoner. We are able to reconstruct most of Spinoza's system with formal logic, but this requires additional axioms which are assumed implicitly by Spinoza. This study illustrates how tools developed in computer science can be of practical use for philosophy.
The structure of the Ethics is very clear: after sequences of de¯nitions and axioms, a sequence of propositions together with proofs follows. Each of these is assigned a number, and thus we refer to a de¯nition, axiom or proposition by the letters D, A, or P, respectively, together with its number.
Since our aim is to e®ectively decide the validity of Spinoza's proofs, we
cannot use full ¯rst order predicate logic (FO), since it is undecidable. Instead,
we use a decidable fragment of FO, namely the Guarded Fragment (GF ) [
For GF , there exists the tableau-based satis¯ability tester Saga [
Although Spinoza's style bears a high similarity with mathematical language, his statements require interpretation before they can be translated into formal logic. We will illustrate this with two examples. Firstly, there is no clear distinction between universal and existential quanti¯cation: by D3, \a substance is conceivable through itself". If this is interpreted as existential quanti¯cation, it reads: \Substance is at least conceivable through itself (but possibly also through something di®erent)." With universal quanti¯cation, it means: \Substance is only conceivable through itself (but possibly not conceivable at all)." In this case and in several similar ones, we think that only both statements together re°ect Spinoza's intention, since this eliminates the possibilities in the parentheses. Secondly, in the Latin text there are two words which translate into English as \or": \vel" (e.g. A1, P4) stands for a logical alternative, and therefore has to be translated into formal logic as \_". In contrast, \sive" (e.g. D1, D4, A5) means rather \or also", i.e. it is followed by an alternative de¯nition. Thus logically, this \or" has to be translated into \^".
In order to express the axioms and de¯nitions, we use nine unary, eight binary and two ternary relations, which are explained in Table 1. In the following, we present our translation of the de¯nitions and axioms. Starting with (the English translation of) Spinoza's original formulation, we present our understanding ¯rst in ordinary language, then in formal logic.
D1 By that which is \self-caused" I mean that of which the essence involves existence, or that of which the nature is only conceivable as existent. This is rather an axiom than a de¯nition, since \self-caused" is a complex term: something has itself and only itself as cause if and only if its existence follows from its conceivability. Note that this implies that everything which exists and everything which is not conceivable is self-caused.
8x((x = x) ! ((co(x; x) ^ (8y(co(y; x) ! (x = y)))) $ (C(x) ! (E(x))))) D2 A thing is called \¯nite in1 its kind" when it can be limited by another thing of the same nature [. . . ] A thing is ¯nite in its kind if and only if there exists a di®erent thing with the same nature by which it can be limited.
8x((x = x) ! (F(x) $ 9y(lb(x; y) ^ sn(x; y) ^ (x 6= y))))
D3 By \substance" I mean that which is in itself, and is conceived through itself [. . . ] A substance exists in itself (and only in itself), and it is conceivable through itself (and only through itself). 8x((x = x) ! (S(x) $ ei(x; x) ^ ct(x; x) ^ 8y(ei(x; y) ! (x = y)) ^ 8y(ct(x; y) ! (x = y)))) D4 By \attribute" I mean that which the intellect perceives as constituting the essence of substance. An attribute is conceivable, and it is an attribute of a substance (and only of substances), which are also conceivable. Moreover, every substance has an attribute. 8x(S(x) ! 9y(ao(y; x))) 8x((x = x) ! (A(x) $ C(x) ^ 9y(ao(x; y)) ^ 8y(ao(x; y) ! (S(y) ^ C(y))))) D5 By \mode" I mean the modi¯cations (\a®ectiones") of substance, or that which exists in, and is conceived through, something other than itself. A mode exists (only) in and is (only) conceivable through a substance. 8x((x = x) ! (M(x) $ C(x) ^ 9y(mo(x; y)) ^ 8y(mo(x; y) ! (ei(x; y) ^ ct(x; y) ^ S(y))))) D6 By \God" I mean a being absolutely in¯nite|that is, a substance consisting in in¯nite attributes, of which each expresses eternal and in¯nite essentiality. If a god is absolutely in¯nite, he must also be in¯nite in his kind. We omit the predicate \eternal", since it is not used in any other proposition considered in this paper. Regarding the meaning of \in¯nite attributes", see our explanation for I1 below. 8x((x = x) ! (G(x) $ (S(x) ^ :F(x)))) 1 We think that the literal translation \in" re°ects Spinoza's intention better than \after".
A1 Everything which exists, exists either in itself or in something else. Everything existing exists in something, which leaves open the possibility that it is something else or the same. 8x(E(x) ! 9y(ei(x; y)))
A2 That which cannot be conceived through anything else must be conceived through itself. Everything conceivable is conceivable through something (possibly itself) which, as is suggested by D3 and D5, must be a substance. 8x(C(x) ! 9y(ct(x; y) ^ S(y)))
A3 From a given de¯nite cause an e®ect necessarily follows; and, on the other hand, if no de¯nite cause be granted, it is impossible that an e®ect can follow. Every cause has an e®ect, and vice versa. 8x(CA(x) ! 9y(co(x; y) ^ EF(y))) 8x(EF(x) ! 9y(co(y; x) ^ CA(y)))
A4 The knowledge of an e®ect depends on and involves the knowledge of a cause. Since \knowledge" does not appear in any other axiom or de¯nition and is used synonymously with \conception" in the corollary of P6, we treat the two terms as synonymous. Thus, something is a conceivable e®ect if and only if it has a cause and is conceivable through its causes.
8x((x = x) ! ((EF(x) ^ C(x)) $ (9y(co(y; x)) ^ 8y(co(y; x) ! (ct(x; y)))))) A5 Things which have nothing in common cannot be understood, the one by means of the other; the conception of one does not involve the conception of the other. Expressed positively, this means: if x is conceivable through y, then x and y have something in common. 8x; y(ct(x; y) ! sc(x; y))
We omit D7, D8 and A6 since they are not used for the propositions considered in this paper, and A7 because it is merely a repetition of D1.
As mentioned in Section 1, we added implicit axioms, i.e. axioms which follow immediately from the semantics of the words used (e.g. if x is the cause of y, then x is a cause and y is an e®ect), or assumptions which are only revealed in the proofs (e.g. in the proof of P4, it is argued that substances and modes are the only existing things). In the following list, we enumerate and justify these additional axioms.
I1 In D6, god is described as a substance having \in¯nite attributes". In the proof of P14, it becomes clear that not the attributes themselves are in¯nite, but their number, or more precisely that god has all attributes: \god is a being [. . . ], of whom no attribute [. . . ] can be denied (by D6)". Thus, every attribute is an attribute of god. Moreover, since every substance has an attribute, it has a common attribute with god.2 8x(A(x) ! 9y(ao(x; y) ^ G(y))) 8x(S(x) ! 9y; z(ca(x; y; z) ^ G(y)))
I2 In the proof of P4, Spinoza states that \outside3 of the intellect, there is nothing except substance and its modi¯cations." Hence, everything existing is either substance or mode. 8x(E(x) ! (S(x) _ M(x)))
I3 In the proof of P2, Spinoza (implicitly) assumes that if two things are not
conceivable through each other, then they have nothing in common, i.e. that the
implication of A5 also holds in the opposite direction. Therefore, we also add
2 We have to state this explicitly since we cannot fully express P5 in GF , see our
explanation for P5 below.
3 We think that translating \extra" literally as \outside" instead of \in addition to"
makes more sense in this context, since then \extra intellectum" simply means \in
nature", whereas otherwise its meaning becomes unclear (see [
I4 In P5, Spinoza mentions \substances having the same nature or (`sive') attribute", which indicates that the term \same nature" in D2 has to be interpreted as \same attribute". For this purpose, we introduce the relation ca(x; y; z), with the semantics that both x and y have attribute z, and they have something in common (namely z). 8x; y(sn(x; y) ! 9z(ca(x; y; z))) 8x; y; z(ca(x; y; z) ! (ao(z; x) ^ ao(z; y) ^ co(x; y)))
I5 The relation sc is symmetric and re°exive. 8x; y(sc(x; y) ! sc(y; x)) 8x((x = x) ! sc(x; x))
I6 If x is conceivable through (or exists in) y, then both x and y are conceivable (or existing, respectively). If x is the cause of y, then x is a cause and y is an e®ect. Analogous axioms hold for the relations ao and mo. 8(x; y)(ct(x; y) ! (C(x) ^ C(y))) 8(x; y)(ao(x; y) ! (A(x) ^ S(y))) 8(x; y)(ei(x; y) ! (E(x) ^ E(y))) 8(x; y)(mo(x; y) ! (M(x) ^ S(y))) 8(x; y)(co(x; y) ! (CA(x) ^ EF(y)))
I7 The sets of substances, attributes and modes are pairwise disjoint. 8x(S(x) ! :A(x)) 8x(S(x) ! :M(x)) 8x(A(x) ! :M(x))
I8 We express the relation \x is divisible into y and z" as used in P12 and P13 as \x is cause of two di®erent things y and z, but not equal to either." 8x; y; z(di(x; y; z) ! (co(x; y) ^ co(x; z) ^ (x 6= y) ^ (x 6= z) ^ (y 6= z))) 3
In this section, we consider the propositions in detail. As in Section 2, we ¯rst give the original formulation by Spinoza, followed by our interpretation and the translation into GF . In order to improve readability, we use the notation ® ! ¯ for :® _ ¯ (material implication), and ' ) Ã for the (logical) implication claimed in the proposition, though the translation of both into GF is identical. Consequently, the satis¯ability of ' ^ :Ã was tested by Saga.
P1 Substance is by nature prior to its modi¯cations. The term \prior" is not formally de¯ned in the axioms and de¯nitions. If we interpret it logically and not temporally (which is suggested by the proof, since time is not mentioned in D3 and D5), we obtain the following: if there exist a mode, then there also exists a substance. This proposition really follows from D5, and thus Saga cannot ¯nd a counter-model. M(x) ) 9y(S(y))
P2 Two substances, whose attributes are di®erent, have nothing in common. If z is an attribute of the substance x, but not of the substance y, then x and y have nothing in common. Here, Spinoza only proves that the conception of x does not involve the conception of y. Without I3, Saga ¯nds a counter-model with two substances which have something in common, but are not conceivable through each other. If we add I3, this proposition follows from the fact that in order to have something in common, one of the substances has to be conceivable through the other one, but every substance is only conceivable through itself.
(S(x) ^ S(y) ^ A(z) ^ ao(z; x) ^ :ao(z; y)) ) :sc(x; y)
P3 Things which have nothing in common cannot be one the cause of the other. Spinoza's proof relies on A4, but this axiom is only applicable if conceivability of the e®ect is assumed. However, if the e®ect is not conceivable, it is (by D1) self-caused, and thus (by I5) has something in common with its cause, so the proposition also holds in this case. :sc(x; y) ) :co(x; y)
P4 Two or more distinct things are distinguished one from the other, either by the di®erence of the attributes of the substances, or by the di®erence of their modi¯cations. Two things x; y having a common attribute z and a common mode w are identical. This proposition holds; the explanation is similar to the one for P5 below. (ca(x; y; z) ^ mo(w; x) ^ mo(w; y)) ) (x = y)
P5 There cannot exist in the universe two or more substances having the same nature or attribute. The intuitive translation of this proposition into FO is: 8x; y; z((S(x)^S(y)^A(z)^ao(z; x)^ao(z; y)) ) (x = y)), which is not guarded, since x and y appear together in the body, but not in the guard. In order to express this in GF , we introduce the relation ca and the axiom I4. Then, we can express the proposition as follows: two substances with a common attribute are identical. This results from P2 and therefore also depends on I3: without this additional axiom, Saga ¯nds a counter-model with two ¯nite substances having a common attribute. (S(x) ^ S(y) ^ ca(x; y; z)) ) (x = y)
P6 One substance cannot be produced by another substance. The proof only shows that one substance cannot be the cause of another one, which suggests that the terms \cause of" and \produced by" are used synonymously, and thus we can express this as follows: if two substances are di®erent, then one cannot be the cause of the other; this follows from A4. (S(x) ^ S(y) ^ (x 6= y)) ) :co(x; y)
P7 Existence belongs to the nature of substances. Every substance is existing. This follows directly from D3 and I6. S(x) ) E(x)
P8 Every substance is necessarily in¯nite. This indeed follows from D2 and P5, which state that a thing can only be limited by another thing of the same nature, but substances with the same nature are identical. S(x) ) :F(x)
P9 The more reality or being a thing has, the greater the number of its attributes. We do not see a possibility of expressing this in GF or even in FO. Since this proposition is not used in any other proof in the ¯rst book of the ethics, it probably serves merely as a justi¯cation for a substance to have several attributes. Hence, we do not consider it any further.
P10 Each particular attribute of the one substance must be conceived through itself. Spinoza's proof shows only that the attribute of a substance must be conceived through this substance. Still, no counter-model can be found: by I5, everything has something in common with itself, and by I3, this implies that it is conceivable through itself. A(x) ) ct(x; x)
P11 God [. . . ] necessarily exists. There can be no model in which there is no individual with the predicate G. To avoid an empty structure4, we add an individual x with the predicate C(x), so that our proposition reads \If something is conceivable, then there exists a god", which also re°ects the structure of the ontological argument used by Spinoza.5 C(x) ) 9y(G(y))
P12 No attribute of substance can be conceived from which it would follow that substance can be divided. The main problem of this and the next proposition is the interpretation of \division". The reference to P6 indicates that if a 4 In an empty structure, even a formula like 8x(C(x) ^ :C(x)) is satis¯able. 5 Note that the naive translation G(x) ) E(x) follows directly from the de¯nition of substance, and it does not show that god necessarily exists. substance x is divided into y and z, then it must be the cause of y and z, but not equal to either. Then, neither y nor z can be a substance (by P6), nor can both be something di®erent and thus x cease to exist (P7).
A(w) ^ C(w) ^ S(x) ^ ao(w; x) ^ di(x; y; z) ) :S(y) ^ :S(z) ^ E(x) P13 Substance absolutely in¯nite is indivisible. The absolutely in¯nite substance is god. Beyond this, P13 is merely a repetition of P12 without the attribute w. G(x) ^ di(x; y; z) ) :S(y) ^ :S(z) ^ E(x)
P14 Besides God no substance can be granted or conceived. The argument relies on the assumptions that god has all attributes (D6, I1), that two substances x and y which have something (e.g. an attribute) in common are conceivable through each other (I3), and that every substance is only conceivable through itself (D3), such that x and y must be identical. Again, without I3 there exists a counter-model with a ¯nite substance that has a common attribute with god, but is not conceivable through him. S(x) ^ (E(x) _ C(x)) ) G(x)
P15 Whatsoever is, is in God, and without God nothing can be, or be conceived. This follows quite easily from P14, since everything existing (i.e. substances and modes) exists in and is conceivable through a substance, and god is the only substance. (E(x) ) 9y(ei(x; y) ^ G(y))) ^ (C(x) ) 9y(ct(x; y) ^ G(y)))
Summary. Out of the 15 propositions under consideration, 12 can be proved using Spinoza's axioms and de¯nitions and the implicit axioms mentioned above. P11 can be proved with some appropriate pre-condition. P5 cannot be expressed fully in GF , but it can be reformulated in a way that renders it provable. Only one proposition remains: the meaning of P9 is very vague and cannot be expressed in GF . The implicit axiom I3 (\if two things have something in common, then one of them is conceivable through the other") is crucial for the high number of provable propositions. Although it is not explicitly formulated by Spinoza and its legitimacy is questionable from a philosophical point of view, it is clearly assumed by Spinoza in the proof of P2, and without it, counter-models for the propositions 2, 4, 5, 8, 10, 14 and 15 can be found. This dependency is also re°ected in Spinoza's proofs: P14 relies on P5, which in turn relies on P2.
In Figure 1, the subsumption hierarchy of the unary relations is shown: an arrow A ! B indicates that the relation A is subsumed by B, i.e. that every instance of A is an instance of B. To improve readability, we show only direct subsumption; note that the subsumption relation is transitive and thus A ! B ! C implies A ! C. Here, the symbol ? stands for an inconsistent relation, which is subsumed by all other ones, and > is the universal relation, which subsumes all other ones. The trivial arrows from ? and to > are shown as dashed. If two relations mutually subsume each other, they are displayed as one. = finite substance = god attribute mode
existing Fig. 1. Subsumption hierarchy cause effect conceivable =
This hierarchy reveals additional propositions which follow from the set of axioms but are not mentioned or proved by Spinoza. Firstly, everything is conceivable, since everything has something in common with itself (I5), and is therefore conceivable through itself (I3). This result again demonstrates the problematic implications of I3. Secondly, `¯nite' is inconsistent. It has been shown that substances are in¯nite (P8), but why cannot something else, e.g. a mode, be ¯nite? The reason for this is D2, which de¯nes `¯nite' as something which can be limited by some other thing of the same nature. By I4, `nature' means `attribute', but only substances have attributes. Thus, anything other than a substance cannot be ¯nite either. Thirdly, everything existing is cause as well as e®ect. This results from D1, since everything existing is self-caused. All other subsumptions are mentioned more or less explicitly by Spinoza. This is an indicator that our system is not over-constrained, i.e. through our translation and the additional axioms we did not introduce any conclusions which do not follow from Spinoza's system. 4
We developed an ontology based on the arguments made in the ¯rst part of Spinoza's Ethics. While testing the validity of the proofs provided, it turned out that most of them require additional axioms, which are only revealed inside the proofs. In particular, the main theorem depends crucially on an implicit assumption which is not justi¯ed anywhere. The counter-models provided by Saga proved to be very helpful in the detection of these missing prerequisites. With the additional axioms, we are able to prove most of the propositions. The restrictions imposed by the language GF cause problems only in one case, and a workaround is possible. In addition to the propositions claimed by Spinoza, we are able to derive additional theorems following from the axioms. In summary, we think that this illustrates the use of automated reasoning tools for philosophy.