South American Journal of Logic Vol. 5, n. 1, pp. 49–80, 2019 ISSN: 2446-6719 A First-Order Modal Theodicy: God, Evil, and Religious Determinism Gesiel Borges da Silva and Fábio Maia Bertato Abstract Edward Nieznański developed in 2007 and 2008 two different systems in formal logic which deal with the problem of evil [11, 12]. Particularly, his aim is to refute a version of the logical problem of evil associated with a form of religious determinism. In this paper, we revisit his first system to give a more suitable form to it, reformulating it in first-order modal logic. The new resulting system, called N1, has much of the original basic structure, and many axioms, definitions, and theorems still remain; however, some new results are obtained. If the conclusions attained are correct and true, then N1 solves the problem of evil through the refutation of a version of religious determinism, showing that the attributes of God in Classical Theism, namely, those of omniscience, omnipotence, infallibility, and omnibenevolence, when adequately formalized, are consistent with the existence of evil in the world. We consider that N1 is a good example of how formal systems can be applied in solving interesting philosophical issues, particularly in Philosophy of Religion and Analytic Theology, establishing bridges between such disciplines. Keywords: Logical Problem of Evil, theodicy, formal theodicy, first-order modal logic, determinism, religious determinism. Introduction The problem of evil is one of the most famous issues in the history of philosophy. Among its formulations, David Hume's is one of the most famous. It states that the existence of God is in some sense incompatible with the existence of evil in the world. In his work Dialogues concerning natural religion, Hume makes the following considerations about God and His attributes: "Epicurus' old questions are yet unanswered. Is he willing to prevent evil, but not able? then is he impotent. Is he able, but not 50 G. B. da Silva and F. M. Bertato willing? then is he malevolent. Is he both able and willing? Whence then is evil?"1 Although scathing, Hume's allegation was not strong sufficiently to bring an effective trouble to theists' belief in God. As Alvin Plantinga affirms, it is not enough to put difficult questions to theism; the challenger should try to show that it is irrational to believe both in God and that evil exists in the world (cf. [13, p. 11]). In this direction, the philosopher John Mackie stated a version of the problem that now is known as the Logical Problem of Evil. Mackie says that theistic belief is positively irrational, for it is contradictory : "I think, however, that a more telling criticism can be made by way of the traditional problem of evil. Here it can be shown, not that religious beliefs lack rational support, but that they are positively irrational, that the several parts of the essential theological doctrine are inconsistent with one another." [9, p. 200.] In other words, this challenge to theism is a problem of consistency between the existence of God and the existence of evil; it is a problem within the framework of classical logic. Many solutions were proposed to the Logical Problem of Evil, and among those, Plantinga's is the most famous. We will not explore his answer, and we do not put in question the merits of a Free Will Defense as a response to the problem. Anyway, even if it is correct, there are other correlate challenges to deal with. For instance, one could agree that the Free Will Defense is enough to deal with the questions raised by Mackie, but think that to have a theodicy, a stronger response to the Logical Problem of Evil, would be even better than a Defense as a philosophical response.2 Other questions regarding the Logical Problem of Evil are still relevant and can be more deeply explored. One of them is the question regarding the logical consistency between divine attributes like omnipotence and omniscience and the existence of evil. Regarding this, one can simply use the apparatus of Formal Logic, formalizing sentences like the attributes of God or the relation between God and the situations in the world, developing proofs and deducing rigorous results. These results, hopefully, can clarify the problem, solving ambiguities and exposing or demising contradictions through adequate tools provided by the vast field of Formal Logic. Such a task is contemplated by the "Formal Theodicies" developed by the Polish philosopher and logician Edward Nieznański [11, 12]. He exposes in the 1[8, part 10, 23] 2Maybe Mackie had this in mind when recognized that Plantinga's solution dealt with his objections to theism, but still puts in question the character of his response as a "real solution" (cf. [1]). A First-Order Modal Theodicy 51 abstract of his 2007 work his project of establishing a theodicy, that aims to show that the existence of God is logically compatible with the existence of evil: "The author of the article uses St. Thomas Aquinas' and G.W. Leibniz's philosophical inspirations to demonstrate by means of formal-logical means [sic] that inferring non-existence of evil from existence of God, as well as non-existence of God from existence of evil is a logical error." [11, p. 217.] One way by which one can address the Problem of Evil is the following: it is contradictory to believe in the existence of the God of Classical Theism and in the existence of evil. God is omnipotent and omniscient, so one can assume that everything that happens is due to God's will. In other words, "if a situation is the case, then God wills such a situation to be the case", a determinist could argue.3 This means that, if a situation is evil, then God wills such an evil situation, and this would contradict his omnibenevolence. To give an answer to such a determinism is the main concern of Nieznański in his papers, and is also ours here. Let p denote a possible situation in the world, P (p) denote "p is the case", and Cθ denote "God wills", then, this claim can be formalized in the following way: (DET1) ∀p(P (p)→ CθP (p)) (If a situation is the case, then God wills such a situation to be the case.) Another determinist claim can be stated as follows: "if God knows that a situation is the case, then God wills such a situation to be the case". The relation between knowledge and will is more intricate in this claim; but perhaps, it is at least conceivable that if God knows a situation, but did not act in order to avoid it, it is because He willed it, for He is omnipotent. Thus, the proposition above requires an answer. If Wθ denotes "God knows", and the other symbols are interpreted as before, it is possible to formalize such a claim as follows: (DET2) ∀p(WθP (p)→ CθP (p)) (If God knows that a situation is the case, then God wills such a situation to be the case.) 3By "situation" we mean a certain configuration of elements. 52 G. B. da Silva and F. M. Bertato Originally, Nieznański developed two different approaches that aim at denying such religious determinism related to the Logical Problem of Evil. In order to do this, in both systems, Nieznański states the "constitutive properties of God", in which the attributes of omniscience, infallibility, and omnipotence are formally described, as well as some other attitudes of God regarding situations. Then, he develops a formal axiology relating good, evil, and neutral situations to finally deal with versions of DET1 and DET2. However, although Nieznański's philosophical insights are penetrating and inventive, and his general methodology of formalization is very inspiring, some issues led us to revisit his first system [11] proposing some changes. Such changes can be summarized as follows: we proceed first by reestablishing the formal language to one that is logically more adequate according to our vision, defining it in first-order modal logic, as well as establishing the metalanguage, the rules of inference and other related features. Then, we define a new set of axioms schemes, many of them inspired in the work of Nieznański, but with a new formulation, to finally prove some theorems. Thus, the new resulting system, called N1, has much of the original basic structure, and many axioms, definitions and theorems still remain in a reformulate way; but, some new results are obtained. If the conclusions attained by N1 are correct and true, then this system solves the problem of evil regarding religious determinism, showing that the attributes of God in Classical Theism, namely, those of omniscience, omnipotence, infallibility, and omnibenevolence, when adequately formalized, are logically compatible with the existence of evil in the world. We hope that it serves, as well, as a first presentation of some of Nieznański's insights published originally in Polish to a wider audience. 1 The system N1: language, rules, and axioms The adaptation we make here from the system proposed by Nieznański is henceforward called N1. The basis of this system is a First-Order Modal Logic, i.e., a First-Order Classical Logic with the addition of two modal operators, Wθ and Cθ.4 The language LN1 of N1 has the following symbols as primitives: (i) Unary predicate symbols: B,P, d, z, n; (ii) A binary predicate symbol: Op; (iii) A symbol of constant (a distinguished element): θ; (iv) Variables for situations: p, q, r, possibly with indexes; 4Among the works consulted are: the book written by Walter Carnielli and Claudio Pizzi about Modal Logics and Modalities [3], the widely-known introductory book of George Hughes and Max Cresswell on Modal Logic, specially chapter 13 [7], and Fitting and Mendelsohn's book on First-Order Modal Logic [5]. A First-Order Modal Theodicy 53 (v) The symbols for connectives: ¬,→; (vi) The symbol of universal operator: ∀; (vii) Two symbols for specific modal operators: Cθ,Wθ. The definition of a well-formed formula (abbreviated as wff ) and the employ of parentheses is the usual, with the expected extensions. The formation rules are the following: (FR1) Any sequence of symbols consisting of an n-ary predicate followed by n individual variables is a wff. (FR2) If φ is a wff, so are ¬φ, Wθφ, and Cθφ. (FR3) If φ and ψ are wff, so is (φ→ ψ). (FR4) If φ is a wff and v is a variable that stands for situations, then ∀vφ(v) is a wff. Some rules of deduction of N1 are: Modus Ponens (MP), Uniform Substitution (US), Rule of Necessitation (Nec) and Substitution of Equivalents (Eq). They are stated below:5 (MP) φ, φ→ ψ `N1 ψ. (US) [7, p. 25] The result of uniformly replacing any variable or variables v1, ..., vn in a theorem by any wff φ1, ..., φn, respectively, is itself a theorem. (Nec) If `N1 φ, then `N1 Wθφ and `N1 Cθφ. (Eq) [7, p. 32] If φ is a theorem and ψ differs from φ in having some wff δ as a subformula at one or more places where φ has a wff γ as a subformula, then if γ ↔ δ is a theorem, ψ is also a theorem. The Deduction Theorem (DT) is valid in the system: Theorem 1 (Deduction Theorem). If φ,Γ `N1 ψ, then Γ `N1 φ→ ψ.6 Other symbols of the language are defined as follows (φ and ψ are wff s): Def. 1. ∃vφ :↔ ¬∀v¬φ Def. 2. (φ↔ ψ) :↔ (φ→ ψ) ∧ (ψ → φ) Def. 3. (φ ∨ ψ) :↔ (¬φ→ ψ) 5Not all the rules presented here are used to prove the theorems of this paper, but by listing them we make explicit what is the modal characterization of our system. 6Hakli and Negri establish the conditions for using this theorem in modal logic: through defining a formal notion of derivation from assumptions, it is possible to prove the theorem for modal logics as stated above (cf. [6, p. 859-861]). 54 G. B. da Silva and F. M. Bertato Def. 4. (φ ∧ ψ) :↔ ¬(φ→ ¬ψ) We will use the following convention: α(p) stands for any wff that involves only the variable p, where p is free; Thus, we will refer to a wff α that involves only a particular situation p as the 'state of affairs' α(p). We use the term 'state of affairs' here to indicate circumstances (possibly a fact) about a given situation.7 So, any situation denoted by p is such that there are many states of affairs involving it. For instance, the formula α(p) ≡ P (p) ∧ ¬P (p) represents a state of affairs that does not occur, for it is contradictory. For ease of reading, we have included in parentheses the standard interpretations for each wff. The following shall be considered as abbreviations or standard semantics in natural language: θ := 'God'; P (p) := 'p is the case';8 B(θ) := 'θ is divine'. d(p) := 'p is good'; z(p) := 'p is evil'; n(p) := 'p is neutral'; K(p) := 'p is contingent'; Op(p, q) := 'p is opposed to q';9 Cθα(p) := 'God wills the state of affairs α(p)'; Wθα(p) := 'God knows the state of affairs α(p)'. As usual, all theorems, rules, and laws of Propositional Calculus are axioms, rules, and laws in our system, respectively. The abbreviation PC denotes steps in proofs that are based on rules and laws in Propositional Calculus; and the abbreviation PC-Theorem is used whenever a valid PC-schema is evoked. 7Naturally, those possible facts that are expressible in the language of N1. 8We do not need to assume here that 'to be the case', is the same as 'to be actual'. To say that 'p is the case' can be considered closer to 'p occurs' or to 'p has correspondence in reality' in a given considered world. 9We consider that two situations are opposite if they are contrary, that is, two opposite situations may at the same time both not be the case, but cannot at the same time both be the case. It will not be necessary here, but accordingly, we could assume as axioms to regulate Op the following formulas: ∀p∀q(Op(p, q) ↔ Op(q, p)) ∀p∀q(Op(p, q) → (P (p) → ¬P (q))). A First-Order Modal Theodicy 55 Thus, we present below the proper axioms of N1.10 The first axiom establishes that the distinguished element θ satisfies the primitive predicate B: A1. B(θ) (God is divine.) The second axiom corresponds to a quantification over the well known Axiom 4 of alethic modal logic, that characterizes the system S4, where the operator  is substituted by Cθ. A2. ∀p(Cθα(p)→ CθCθα(p)) (For all situations, if God wills a state of affairs, then He wills to will such a state of affairs.) The following axiom is, similarly, associated with the formula 5, the characteristic axiom schema of S5 system. One can see easily that there is an analogy between ♦, the operator of possibility in alethic modal logic, and Dθ, the operator for permission in N1: A3. ∀p(Dθα(p)→ CθDθα(p)) (For all situations, if God permits a state of affairs, then He wills to permit such a state of affairs.) Another axiom here establishes something relevant, and easy to assume, in the context of the Logical Problem of Evil, i.e., that not all situations are good: A4. ¬∀p(P (p)→ d(p)) (Not all the situations that are the case are good.) Next, we introduce three axioms in order to regulate the axiology of our system. The following axiom aims at capturing the attribute of omnibenevolence of God: A5. ∀p(CθP (p)↔ d(p)) (For all situations, God wills a situation to be the case iff the situation is good.) The next axiom is one that relates good to evil situations: 10For simplicity, we will call simply axioms to both axioms properly speaking and axiom schemes. 56 G. B. da Silva and F. M. Bertato A6. ∀p(z(p)→ ¬d(p)) (For all situations, if a situation is evil, then it is not good.) In order to establish the relation between good and evil situations, when they are opposite, we assume the following axiom: A7. ∀p∀q(Op(p, q)→ (d(p)↔ z(q))) (For all situations, if two situations are opposite, then one is good iff the other is evil.) The following axioms A8 and A9 introduce relations between will, opposition, and permission of God regarding states of affairs: A8. ∀p(Sθα(p)↔ Cθ¬α(p)) (For all situations, God opposes a state of affairs iff He wills the opposite.) A9. ∀p(Dθα(p)↔ ¬Sθα(p)) (For all situations, God permits a state of affairs iff He does not oppose to it.) The next axiom states the relation between the opposition of God and neutral situations. Intuitively, a situation is neutral iff God does not will it and is not opposed to it. Therefore, if God is opposed to a situation, we can assume that such a situation is not neutral. A10. ∀p(SθP (p)→ ¬n(p)) (For all situations, if God opposes a situation to be the case, then the situation is not neutral.) Thus, each situation admits one of three possible axiological values. In this sense, the next axiom establishes that neutral situations are neither good nor evil. A11. ∀p(n(p)↔ (¬d(p) ∧ ¬z(p))) (For all situations, a situation is neutral iff it is neither good nor evil.) The system N1 has eleven axioms. The axiom A1 establishes that our distinguished element θ ('God') is divine. The axioms A2 and A3 govern the iteration and the composition of the operators Cθ and Dθ, which clearly shows A First-Order Modal Theodicy 57 a modal character. The axiom A4 guarantees that there is at least one evil situation. The axiom A5 expresses that the will of God is the criterion for good. Axioms A6 and A7 provide a type of opposition between good and evil. Axioms A8 and A9 establish relations between the will and the opposition of God, and between the permission and the opposition of God with respect to states of affairs, while A10 establishes the relation between the opposition of God and neutral situations. Finally, the axiom A11 establishes that a situation is neutral iff such a situation is neither good nor evil. In the following, we will give precise definitions of the divine attributes and deduce a series of theorems relevant to the solution of the Logical Problem of Evil and the constitution of a formal theodicy. 2 The attributes of God The following definitions delineate some attributes of the God of Classical Theism and are essential to the understanding and discussion of the Logical Problem of Evil: omniscience, infallibility, and omnipotence. Def. 5 (Omniscience of God). WW :↔ ∀p(α(p)→Wθα(p)) (God is omniscient iff for all situations, if a state of affairs is the case, then God knows it.) Def. 6 (Infallibility of God). NM :↔ ∀p(Wθα(p)→ α(p)) (God is infallible iff, for all situations, if God knows a state of affairs, then it is the case.) Def. 7 (Omnipotence of God). WM :↔ ∀p(Cθα(p)→ α(p)) (God is omnipotent iff, for all situations, if God wills a state of affairs, then it is the case.) Such definitions try to capture the historical conceptions and intuitions of the great religions that helped to shape an entire concept apparatus for the Classical Theism. It is not difficult to find foundations in such a religious and philosophical traditions to support such definitions, but we do not assign ourselves to such a task here. The following definition sets what means to be 'divine' in the context of the system N1, according to our standard interpretation: Def. 8 (God). B(θ) :↔WW ∧NM ∧WM (God is divine iff He is omniscient, infallible, and omnipotent.) As God satisfies the predicate of divinity, we have theorem T1: 58 G. B. da Silva and F. M. Bertato T1. WW ∧NM ∧WM (God is omniscient, infallible, and omnipotent.) Proof. 1. B(θ) [A1] 2. B(θ) :↔WW ∧NM ∧WM [Def. 8] 3. WW ∧NM ∧WM [PC, 1, 2] Theorems T2, T3, and T4 are also easily deduced from T1, and describe extensively God's attitudes regarding states of affairs. As Nieznański observes about the corresponding theorems in his system, theorems T2 and T3 formalize a fact that is in agreement with the observation of Thomas Aquinas, who says that "God knows all things whatsoever that in any way are" [11, p. 204].11 T2. ∀p(α(p)→Wθα(p)) (For all situations, if a state of affairs is the case, then God knows it.) T3. ∀p(Wθα(p)→ α(p)) (For all situations, if God knows a state of affairs, then it is the case.) Theorems T2 and T3 establish the correspondence between the knowing of God and the states of affairs that are the case. Every state of affairs that God knows is the case and, conversely, if a state of affairs is the case, then God knows it. Theorem T4, on the other hand, deals with another relevant attribute here: the omnipotence of God, related with what God wills: T4. ∀p(Cθα(p)→ α(p)) (For all situations, if God wills a state of affairs, then it is the case.) The following theorem states that God cannot will contradictions. This follows immediately from the underlying Classical Logic. T5. ¬∃p(Cθ(α(p) ∧ ¬α(p))) (There is no situation such that God wills some contradiction.) 11"Deus scit omnia quaecumque sunt quocumque modo" (Thomas Aquinas, Summa Theologiae, I, q. 14, a. 9 co.). A First-Order Modal Theodicy 59 Proof. 1. Cθ(α(p) ∧ ¬α(p))→ (α(p) ∧ ¬α(p))) [T4, α(p)/(α(p) ∧ ¬α(p)), Spec] 2. ¬(α(p) ∧ ¬α(p))→ ¬Cθ(α(p) ∧ ¬α(p)) [PC, 1] 3. ¬(α(p) ∧ ¬α(p)) [PC-Theorem] 4. ¬Cθ(α(p) ∧ ¬α(p)) [MP, 2, 3] 5. ∀p¬Cθ(α(p) ∧ ¬α(p)) [Gen, 4] 6. ¬∃pCθ(α(p) ∧ ¬α(p)) [PC, 5] It is easy to see that T5 could be derived using just the theorem stated in line 3 of the proof above and Necessitation Rule (Nec). The same thing could be made with the operator Wθ: God cannot know contradictory states of affairs. The following definition states what it means for God to be coherent regarding a situation, and T6 states another result about the will of God: Def. 9 (Coherence). coherentθ(p) :↔ (Cθα(p)→ ¬Cθ¬α(p)) (God is said to be "coherent with Himself regarding a situation" whenever the following occurs: if He wills a state of affairs involving that situation, then He does not will the opposite.) T6. ∀p(Cθα(p)→ ¬Cθ¬α(p)) (For all situations, if God wills a state of affairs, then it is not the case that He wills the opposite.) Proof. 1. Cθ¬α(p)→ ¬α(p) [T4, α(p)/¬α(p), Spec] 2. ¬¬α(p)→ ¬Cθ¬α(p) [PC, 1] 3. α(p)→ ¬Cθ¬α(p) [PC, 2] 4. Cθα(p)→ α(p) [T4, Spec] 5. Cθα(p)→ ¬Cθ¬α(p) [PC, 4, 3] 6. ∀p(Cθα(p)→ ¬Cθ¬α(p)) [Gen, 5] By definition, it follows from T6: T7. ∀p(coherentθ(p)) (Regarding all situations, God is coherent with Himself.) 60 G. B. da Silva and F. M. Bertato Proof. 1. Cθα(p)→ ¬Cθ¬α(p) [T6, Spec.] 2. coherentθ(p) [Def. 9, 1] 3. ∀p(coherentθ(p)) [Gen, 2] Next, some theorems are stated in order to explore the relations between "attitudes" of God towards states of affairs. T8. ∀p(Sθα(p)↔ ¬Dθα(p)) (For all situations, God is opposed to a state of affairs iff He does not permits it.) Proof. 1. Dθα(p)↔ ¬Sθα(p) [A9, Spec.] 2. ¬Dθα(p)↔ Sθα(p) [PC] 3. ∀p(Sθα(p)↔ ¬Dθα(p)) [PC, Gen, 2] The theorem below states the relation between Cθ and Dθ: T9. ∀p(Dθα(p)↔ ¬Cθ¬α(p)) (For all situations, God permits a state of affairs iff He does not will the opposite.) Proof. 1. Sθα(p)↔ Cθ¬α(p) [A8, Spec] 2. Sθα(p)↔ ¬Dθα(p) [T8, Spec] 3. Dθα(p)↔ ¬Cθ¬α(p) [PC, 1, 2] 4. ∀p(Dθα(p)↔ ¬Cθ¬α(p)) [Gen, 3] From T9 it is easy to recognize the analogy between alethic modal operators  and ♦ and N1 modal operators Cθ and Dθ, respectively. It becomes also clear that T6 is linked to formula D, the axiom that characterizes the KD modal system; in terms of the equivalence stated in T9, T6 can be written as ∀p(Cθα(p)→ Dθα(p)). It is easy to see that the following theorems can be deduced from T9: T9.1 ∀p(¬Dθα(p)↔ Cθ¬α(p)) T9.2 ∀p(Dθ¬α(p)↔ ¬Cθα(p)) A First-Order Modal Theodicy 61 T9.3 ∀p(¬Dθ¬α(p)↔ Cθα(p)) One more analogy between N1 and normal modal systems comes here: T10 below is related to the formula T♦, valid in KT modal logic. Furthermore, it is philosophically meaningful, for it states the relation between the permission of God and the states of affairs: T10. ∀p(α(p)→ Dθα(p)) (For all situations, if a state of affairs is the case, then it is permitted by God.) Proof. 1. Cθ¬α(p)→ ¬α(p) [T4, α(p)/¬α(p), Spec.] 2. Dθα(p)↔ ¬Cθ¬α(p) [T9, Spec] 3. α(p)→ Dθα(p) [PC, 1, 2] 4. ∀p(α(p)→ Dθα(p)) [Gen, 3] Theorems T11 and T12, on the other hand, characterize the relation between God's opposition regarding states of affairs: T11. ∀p(Sθα(p)→ ¬α(p)) (For all situations, if God is opposed to a state of affairs, then such a state of affairs is not the case.) Proof. 1. Cθ¬α(p)→ ¬α(p) [T4, α(p)/¬α(p), Spec] 2. Sθα(p)↔ Cθ¬α(p) [A8, Spec] 3. Sθα(p)→ ¬α(p) [PC, 1, 2] 4. ∀p(Sθα(p)→ ¬α(p)) [Gen, 3] T12. ∀p(Sθα(p)→ Dθ¬α(p)) (For all situations, if God is opposed to a state of affairs, then He permits the opposite.) Proof. 1. Sθα(p)→ ¬α(p) [T11, Spec] 2. ¬α(p)→ Dθ¬α(p) [T10, α(p)/¬α(p), Spec] 3. Sθα(p)→ Dθ¬α(p) [PC, 1, 2] 4. ∀p(Sθα(p)→ Dθ¬α(p)) [Gen, 3] 62 G. B. da Silva and F. M. Bertato Theorems from T13 to T23 state some inner relations between will, opposition, and permission of God regarding states of affairs. T13. ∀p(CθCθα(p)↔ Cθα(p)) (God wills to will a state of affairs iff He wills such a state of affairs.) Proof. 1. CθCθα(p)→ Cθα(p) [T4, α(p)/Cθα(p), Spec] 2. Cθα(p)→ CθCθα(p) [A2, Spec] 3. CθCθα(p)↔ Cθα(p) [PC, 1, 2] 4. ∀p(CθCθα(p)↔ Cθα(p)) [Gen, 3] T14. ∀p(CθDθα(p)↔ Dθα(p)) (For all situations, God wills to permit a state of affairs iff He permits such a state of affairs.) Proof. 1. CθDθα(p)→ Dθα(p) [T4, α(p)/Dθα(p), Spec] 2. Dθα(p)→ CθDθα(p) [A3, Spec] 3. CθDθα(p)↔ Dθα(p) [PC, 1, 2] 3. ∀p(CθDθα(p)↔ Dθα(p)) [Gen, 3] T15. ∀p(DθDθα(p)↔ Dθα(p)) (For all situations, God permits to permit a state of affairs iff He permits such a state of affairs.) Proof. 1. CθCθ¬α(p)↔ Cθ¬α(p) [T13, α(p)/¬α(p), Spec] 2. Dθα(p)↔ ¬Cθ¬α(p) [T9, Spec] 3. ¬Dθα(p)↔ Cθ¬α(p) [PC, 2] 4. Cθ¬Dθα(p)↔ ¬Dθα(p) [Eq, 3 in 1] 5. ¬DθDθα(p)↔ ¬Dθα(p) [Eq, 3 in 4] 6. DθDθα(p)↔ Dθα(p) [PC, 5] 7. ∀p(DθDθα(p)↔ Dθα(p)) [Gen, 6] A First-Order Modal Theodicy 63 The formula ∀p(Cθ(Cθα(p))→ Dθ(Dθα(p))) corresponds to a formula which is originally an axiom in the system of Nieznański. It is easily demonstrated from T6, A9, T13, and T15: 12 T16. ∀p(CθCθα(p)→ DθDθα(p)) (For all situations, if God wills to will a state of affairs, then God permits to permit such a state of affairs.) Proof. 1. Cθα(p)→ ¬Cθ¬α(p) [T6, Spec] 2. Dθα(p)↔ ¬Cθ¬α(p) [T9, Spec] 3. Cθα(p)→ Dθα(p) [Eq, 2 in 1] 4. CθCθα(p)↔ Cθα(p) [T13, Spec] 5. CθCθα(p)→ Dθα(p) [Eq, 4 in 3] 6. DθDθα(p)↔ Dθα(p) [T15, Spec] 7. CθCθα(p)→ DθDθα(p) [Eq, 6 in 5] 8. ∀p(CθCθα(p)→ DθDθα(p)) [Gen, 7] T17. ∀p(DθCθα(p)↔ Cθα(p)) (For all situations, God permits to will a state of affairs iff He wills such a state of affairs.) Proof. 1. CθDθ¬α(p)↔ Dθ¬α(p) [T14, α(p)/¬α(p), Spec] 2. Dθ¬α(p)↔ ¬Cθα(p)) [T9.2, Spec] 3. Cθ¬Cθα↔ ¬Cθα [Eq, 2 in 1] 4. ¬DθCθα(p)↔ Cθ¬Cθα(p)) [T9.1, α(p)/Cθα(p), Spec] 5. ¬DθCθα(p)↔ ¬Cθα(p)) [Eq, 3 in 4] 6. DθCθα(p)↔ Cθα(p) [PC, 5] 7. ∀p(DθCθα(p)↔ Cθα(p)) [Gen, 6] T18. ∀p(CθSθα(p)↔ Sθα(p)) (For all situations, God wills to oppose a state of affairs iff He is opposed to such a state of affairs.) 12Nieznański called the axiom associated with this theorem "Axiom of justice" [11, p. 208]. The original version was quite different of that in this paper, for it quantifies over modal operators and we have avoided to do this throughout N1. Written in our notation, it would be ∀p(∃xCθCxα(p) → ∀x(DθDθα(p))). 64 G. B. da Silva and F. M. Bertato Proof. 1. CθCθ¬α(p)↔ Cθ¬α(p) [T13, α(p)/¬α(p), Spec] 2. Sθα(p)↔ Cθ¬α(p) [A8, Spec] 3. CθSθα(p)↔ Sθα(p) [Eq, 2 in 1] 4. ∀p(CθSθα(p)↔ Sθα(p)) [Gen, 3] T19. ∀p(DθSθα(p)↔ Sθα(p)) (For all situations, God permits to oppose a state of affairs iff He opposes such a state of affairs.) Proof. 1. DθCθ¬α(p)↔ Cθ¬α(p) [T17, α(p)/¬α(p), Spec] 2. Sθα(p)↔ ¬Cθα(p) [A8, Spec] 3. DθSθα(p)↔ Sθα(p) [Eq, 2 in 1] 4. ∀p(DθSθα(p)↔ Sθα(p)) [Gen, 3] T20. ∀p(SθDθα(p)↔ Sθα(p)) (For all situations, God opposes to permit a state of affairs iff He opposes such a state of affairs.) Proof. 1. DθDθα(p)↔ Dθα(p)) [T15, Spec] 2. ¬DθDθα(p)↔ ¬Dθα(p) [PC, 1] 3. Sθα(p)↔ ¬Dθα(p) [T8, Spec] 4. SθDθα(p)↔ Sθα(p) [Eq, 3 in 2] 5. ∀p(SθDθα(p)↔ Sθα(p)) [Gen, 4] T21. ∀p(SθCθα(p)↔ Dθ¬α(p)) (For all situations, God opposes to will a state of affairs iff He permits the state of affairs not to be the case.) Proof. 1. CθDθ¬α(p)↔ Dθ¬α(p) [T14, α(p)/¬α(p), Spec] 2. Dθ¬α(p)↔ ¬Cθα(p) [T9.2, Spec.] 3. Cθ¬Cθα(p)↔ Dθ¬α(p) [Eq, 2 in 1] 4. SθCθα(p)↔ Cθ¬Cθα(p) [A8, α(p)/Cθα(p), Spec] 5. SθCθα(p)↔ Dθ¬α(p) [Eq, 4 in 3] 6. ∀p(SθCθα(p)↔ Dθ¬α(p)) [Gen, 5] A First-Order Modal Theodicy 65 T22. ∀p(SθSθα(p)↔ Dθα(p)) (For all situations, God opposes to oppose a state of affairs iff He permits such a state of affairs.) Proof. 1. SθSθα(p)↔ Cθ¬Sθα(p) [A8, α(p)/Sθα(p), Spec] 2. Sθα(p)↔ ¬Dθα(p) [T8, Spec] 3. SθSθα(p)↔ Cθ¬¬Dθα(p) [Eq, 2 in 1] 4. SθSθα(p)↔ CθDθα(p) [PC, 3] 5. CθDθα(p)↔ Dθα(p) [T14, Spec] 6. SθSθα(p)↔ Dθα(p) [Eq, 5 in 4] 7. ∀p(SθSθα(p)↔ Dθα(p)) [Gen, 6] T23. ∀p(Cθα(p)→ ¬CθCθ¬α(p)) (For all situations, if God wills a state of affairs, then He does not will to will the opposite.) Proof. 1. Cθα(p)→ α(p) [T4, Spec] 2. α(p)→ Dθα(p) [T10, Spec] 3. Cθα(p)→ Dθα(p) [PC, 1, 2] 4. DθDθα(p)↔ Dθα(p) [T15, Spec] 5. ¬Cθ¬Dθα(p)↔ DθDθα(p) [T9, α(p)/Dθα(p), Spec] 6. ¬Cθ¬Dθα(p)↔ Dθα(p) [Eq, 5 in 4] 7. ¬Dθα(p)↔ Cθ¬α(p) [T9.1, Spec] 8. ¬CθCθ¬α(p)↔ Dθα(p) [Eq, 7 in 6] 9. Cθα(p)→ ¬CθCθ¬α(p) [Eq, 8 in 3] 10. ∀p(Cθα(p)→ ¬CθCθ¬α(p)) [Gen, 9] 3 God and values: a theistic axiology In this section, we deal with a formal axiology, i. e., a formal treatment of our ordinary notions of "good", "evil", and "neutral" situations. Good, evil, and neutral situations are established in the axioms A5, A6, A10, and A11. Theorems from T24 to T31 are consequences of such axioms. They show some of the relations between good, evil, and neutral situations and their opposites. T24. ∀p(¬n(p)↔ (d(p) ∨ z(p))) 66 G. B. da Silva and F. M. Bertato (A situation is not neutral iff either it is good or evil.) Proof. 1. n(p)↔ (¬d(p) ∧ ¬z(p)) [A11, Spec] 2. ¬n(p)↔ ¬(¬d(p) ∧ ¬z(p)) [PC, 1] 3. ¬n(p)↔ (¬¬d(p) ∨ ¬¬z(p)) [PC, 2] 4. ¬n(p)↔ (d(p) ∨ z(p)) [PC, 3] 5. ∀p(¬n(p)↔ (d(p) ∨ z(p))) [Gen, 4] T25. ∀p(n(p) ∨ d(p) ∨ z(p)) (Every situation is neutral, good, or evil.) Proof. 1. ¬n(p)↔ (d(p) ∨ z(p)) [T24, Spec] 2. ¬n(p)→ (d(p) ∨ z(p)) [PC, 1] 3. n(p) ∨ (d(p) ∨ z(p)) [Def. 3, 2] 4. n(p) ∨ d(p) ∨ z(p) [PC, 3] 5. ∀p(n(p) ∨ d(p) ∨ z(p)) [Gen, 4] T26. ∀p∀q(Op(p, q)→ (d(p)→ ¬d(q))) (For all situations, if two situations are opposite, then if one is good, the other is not good.) Proof. 1. Op(p, q) [Hip.] 2. Op(p, q)→ (d(p)↔ z(q)) [A7, Spec] 3. d(p)↔ z(q) [MP, 1, 2] 4. z(q)→ ¬d(q) [A6, Spec] 5. d(p)→ ¬d(q) [Eq, 3 in 4] 6. Op(p, q)→ (d(p)→ ¬d(q)) [DT, 1−5] 7. ∀p∀q(Op(p, q)→ (d(p)→ ¬d(q))) [Gen, 6] T27. ∀p(d(p)→ ¬z(p)) (For all situations, if a situation is good, then it is not evil.) A First-Order Modal Theodicy 67 Proof. 1. z(p)→ ¬d(p) [A6, Spec] 2. d(p)→ ¬z(p) [PC, 1] 3. ∀p(d(p)→ ¬z(p)) [Gen, 2] T28. ∀p(¬d(p)→ (n(p) ∨ z(p))) (For all situations, if a situation is not good, then it is neutral or evil.) Proof. 1. n(p) ∨ d(p) ∨ z(p) [T25, Spec] 2. d(p) ∨ (n(p) ∨ z(p)) [PC, 1] 3. ¬d(p)→ (n(p) ∨ z(p)) [PC, 2] 4. ∀p(¬d(p)→ (n(p) ∨ z(p))) [Gen, 3] T29. ∀p(((n(p) ∨ z(p))→ ¬d(p))) (For all situations, if a situation is neutral or evil, then it is not good.) Proof. 1. ¬((n(p) ∨ z(p))→ ¬d(p)) [Hip.] 2. (n(p) ∨ z(p)) ∧ ¬¬d(p) [PC, 1] 3. n(p) ∨ z(p) [PC, 2] 4. d(p) [PC, 2] 5. z(p) [Hip., 3] 6. z(p)→ ¬d(p) [A6, Spec] 7. ¬d(p) [MP, 5, 6] 8. n(p) [Hip., 3] 9. n(p)↔ (¬d(p) ∧ ¬z(p)) [A11, Spec] 10. (¬d(p) ∧ ¬z(p)) [MP, 8, 9] 11. ¬d(p) [PC, 10] 12. ¬d(p) [5-11] 13. ¬¬((n(p) ∨ z(p))→ ¬d(p)) [¬ Hip, 1, 4, 12] 14. ((n(p) ∨ z(p))→ ¬d(p)) [PC, 13] 15. ∀p((n(p) ∨ z(p))→ ¬d(p)) [Gen, 14] T30. ∀p(¬d(p)↔ (n(p) ∨ z(p))) (A situation is not good iff either it is neutral or evil.) 68 G. B. da Silva and F. M. Bertato Proof. 1. ¬d(p)→ (n(p) ∨ z(p)) [T28] 2. ((n(p) ∨ z(p))→ ¬d(p)) [T29] 3. ¬d(p)↔ (n(p) ∨ z(p)) [PC, 1, 2] 4. ∀p(¬d(p)↔ (n(p) ∨ z(p))) [Gen, 3] T31. ∀p∀q(Op(p, q)→ (n(p)↔ n(q))) (If two situations are opposite, then one of them is neutral iff the other is also neutral.) Proof. 1. Op(p, q) [Hip] 2. Op(p, q)→ (d(p)↔ z(q)) [A7, Spec] 3. d(p)↔ z(q) [MP, 1, 2] 4. n(p)↔ (¬d(p) ∧ ¬z(p)) [A11, Spec] 5. n(q)↔ (¬d(q) ∧ ¬z(q)) [A11, p/q, Spec] 6. d(q)↔ z(p) [US, 3] 7. n(p)↔ (¬z(q) ∧ ¬d(q)) [Eq, 3 & 6 in 4] 8. n(p)↔ (¬d(q) ∧ ¬z(q)) [PC, 7] 9. n(p)↔ n(q) [PC, 5, 8] 10. Op(p, q)→ (n(p)↔ n(q)) [DT, 1−9] 11. ∀p∀q(Op(p, q)→ (n(p)↔ n(q))) [Gen, 10] T32. ∀p(CθP (p)→ d(p)) (For all situations, if God wills a situation to be the case, then such a situation is good.) Proof. 1. d(p)↔ CθP (p) [A5, Spec] 2. CθP (p)→ d(p) [PC, 1] 3. ∀p(CθP (p)→ d(p)) [Gen, 2] T33. ∀p(SθP (p)→ ¬d(p)) (For all situations, if God opposes to a situation that is the case, then such a situation is not good.) A First-Order Modal Theodicy 69 Proof. 1. d(p)↔ CθP (p) [A5] 2. ¬d(p)↔ ¬CθP (p) [PC, 1] 3. CθP (p)→ ¬Cθ¬P (p) [T6, α(p)/P (p)), Spec] 4. Cθ¬P (p)→ ¬CθP (p) [PC, 3] 5. Cθ¬P (p)→ ¬d(p) [Eq, 2 in 4] 6. SθP (p)↔ Cθ¬P (p) [A8, α(p)/P (p), Spec] 7. SθP (p)→ ¬d(p) [Eq, 6 in 5] 8. ∀p(SθP (p)→ ¬d(p)) [Gen, 7] It is easy to prove the following theorem from A10, A11, and T33: T34. ∀p(SθP (p)→ z(p)) (For all situations, if God opposes to a situation to be the case, then the situation is evil.) The following theorems T35, T36, and T37 establish the relation between the axiological values of situations and the permission of God. T35. ∀p(d(p)→ DθP (p)) (For all situations, if a situation is good, then God permits it to be the case.) Proof. 1. SθP (p)→ ¬d(p) [T33, Spec.] 2. d(p)→ ¬SθP (p) [PC, 1] 3. DθP (p)↔ ¬SθP (p) [A9, α(p)/α(p), Spec] 4. d(p)→ DθP (p) [Eq, 3 in 2] 5. ∀p(d(p)→ DθP (p)) [Gen, 4] T36. ∀p(¬d(p)→ Dθ¬P (p)) (For all situations, if a situation is not good, then God permits it not to be the case.) Proof. 1. Cθα(p)→ d(p)) [T32, Spec] 2. ¬d(p)→ ¬CθP (p) [PC, 1] 3. ¬CθP (p)↔ Dθ¬P (p) [T9.2, α(p)/P (p), Spec] 4. ¬d(p)→ Dθ¬P (p) [Eq, 3 in 2] 5. ∀p(¬d(p)→ Dθ¬P ) [Gen, 4] 70 G. B. da Silva and F. M. Bertato T37. ∀p(n(p)→ (DθP (p) ∧ Dθ¬P (p))) (For all situations, if a situation is neutral, then God permits it to be or not to be the case.) Proof. 1. n(p)↔ (¬d(p) ∧ ¬z(p)) [A11, Spec] 2. ¬z(p)→ ¬SθP (p) [T35, Spec, PC] 3. SθP (p)↔ ¬DθP (p) [A9, α(p)/P (p), Spec] 4. ¬z(p)→ DθP (p) [Eq, 2 in 3, PC] 5. ¬d(p)→ Dθ¬P (p) [T36, Spec] 6. n(p)→ (DθP (p) ∧ Dθ¬P (p)) [PC, 1, 4, 5] 7. ∀p(n(p)→ (DθP (p) ∧ Dθ¬P (p))) [Gen, 6] The latter theorem states that some situations, namely neutral situations, are such that both their occurrence and non-occurrence are permitted by God. The results established so far allow us to address the problem of determinism. 4 Refutation of determinism As stated earlier, our main concern is to give an answer to the following determinist claim: (DET1) ∀p(P (p)→ CθP (p)) We are now in position to answer this claim through formal means. The axiom A4 can be informally interpreted as saying that "not everything is flowers" in the world, or, as stated by Nieznański, "not all events are good" [11, p. 211.]: A4. ¬∀p(P (p)→ d(p)) In N1, however, we derive T38, a very important theorem, since that it is the negation of DET1: T38 (¬DET1). ¬∀p(P (p)→ CθP (p)) (Not all situations is such that, if a situation is the case, then God wills such a situation to be the case.) Proof. 1. ¬¬∀p(P (p)→ CθP (p)) [Hip] A First-Order Modal Theodicy 71 2. ∀p(P (p)→ CθP (p)) [PC, 1] 3. P (p)→ CθP (p) [2, Spec] 4. ∀p(CθP (p)→ d(p)) [T32] 5. CθP (p)→ d(p) [Spec, 4] 6. P (p)→ d(p) [PC, 3, 5] 7. ∀p(P (p)→ d(p)) [Gen, 6] 8. ¬∀p(P (p)→ d(p) [A4] 9. ¬¬¬∀p(P (p)→ CθP (p)) [¬ Hip, 7, 8] 10. ¬∀p(P (p)→ CθP (p)) [PC, 9] In what follows, it is defined what it means for God to be a 'want-it-all', the kind of person that always wills some state of affairs. Def. 10 (Want-it-all). OW :↔ ∀p(Cθα(p) ∨ Cθ¬α(p)) (God is a 'want-it-all' regarding situations iff for all situations God wills a state of affairs or its opposite.) The following theorem shows that, in N1, God is not a 'want-it-all'. T39. ¬OW (God is not a 'want-it-all') Proof. 1. ∀p(Cθα(p) ∨ Cθ¬α(p)) [Hip] 2. ∀p(¬Cθα(p)→ Cθ¬α(p)) [PC, 1] 3. ¬Cθα(p)→ Cθ¬α(p) [Spec, 2] 4. Cθ¬α(p)→ ¬α(p) [T4, α(p)/¬α(p)] 5. ¬Cθα(p)→ ¬α(p) [PC, 3, 4] 6. ∀p(¬Cθα(p)→ ¬α(p)) [Gen, 5] 7. ∀p(α(p)→ Cθα(p)) [PC, 6] 8. ¬∀p(α(p)→ Cθα(p)) [T38] 9. ¬∀p(Cθα(p) ∨ Cθ¬α(p)) [¬ Hip, 1] 10. ¬OW [Def. 10, 9] Another statement of interest here is the following: (DET2) ∀p(WθP (p)→ CθP (p)) It is a remarkable fact that, in N1, DET1 and DET2 are equivalent, as T40 shows: 72 G. B. da Silva and F. M. Bertato T40 (DET2 ↔ DET1). ∀p(WθP (p)→ CθP (p))↔ ∀p(P (p)→ CθP (p)) (For all situations, to affirm that if God knows a situation to be the case, then God wills such a situation to be the case, is equivalent to affirm that if a situation is the case, then God wills it to be the case.) Proof. 1. P (p)→WθP (p) [T2, α(p)/P (p), Spec] 2. WθP (p)→ P (p)) [T3, α(p)/P (p), Spec] 3. WθP (p)↔ P (p) [PC, 1, 2] 4. (P (p)→ CθP (p))↔ (P (p)→ CθP (p)) [PC-Theorem] 5. (WθP (p)→ CθP (p))↔ (P (p)→ CθP (p)) [Eq, 3 in 4] 6. ∀p(WθP (p)→ CθP (p))↔ ∀p(P (p)→ CθP (p)) [Gen, 5] But DET1 is false, thus, from T40, DET2 is also false: T41 (¬ DET2). ¬∀p(WθP (p)→ CθP (p)) (Not all situations are such that if God knows a situation to be the case, then God wills such a situation to be the case.) The definition that follows sets up a new operator, and the theorems that follow extend the meaning of some results just stated above. We interpret it as 'God is the cause of':13 Def. 11 (God is the direct cause of). (Aθα(p) :↔ Cθα(p)) (God is the direct cause of a state of affairs iff He wills such a state of affairs.) The following two theorems establish the relation between God as direct cause of situations and situations that are the case. T42. ∀p(Aθα(p)→ α(p)) (For all situations, if God is the direct cause of a state of affairs, then such a state of affairs is the case.) 13Although recognizing Nieznański's merit on defining this operator and its meaning in the context of a formal theodicy (as an attempt to deal with the will of God, His responsibility and the fact that He is the cause of everything in some sense), we interpret it in a different way: instead of interpreting the operator defined in what follows as 'God is the cause of', 'God is the direct cause of', for God's will is effective. Another relevant difference is that, in N1, the only person involved is God, and by doing this we avoid problems with quantifiers and multi-modalities – for instance, the definition above in his system would be stated as Axα(p) :↔ Cxα(p), where x can be quantified. A First-Order Modal Theodicy 73 Proof. 1. Aθα(p)↔ Cθα(p) [Def. 11] 2. Cθα(p)→ α(p) [T4, Spec] 3. Aθα(p)→ α(p) [Eq, 1 in 2] 4. ∀p(Aθα(p)→ α(p)) [Gen, 3] T43. ¬∀p(P (p)→ AθP (p)) (God is not the direct cause of every situation that is the case.) Proof. 1. ∀p(P (p)→ AθP (p)) [Hip] 2. P (p)→ AθP (p) [Spec, 1] 3. AθP (p)↔ CθP (p) [Def. 11, α(p)/P (p)] 4. P (p)→ CθP (p) [Eq, 3 in 2] 5. ∀p(P (p)→ CθP (p)) [Gen, 4] 6. ¬∀p(P (p)→ CθP (p)) [T38] 7. ¬∀p(P (p)→ AθP (p)) [¬ Hip, 5, 6] Next, we introduce the definition of contingent situation, that is a situation such that God permits it to be the case or not to be the case. Theorems from T44 to T49 show the relation between the will of God and contingent situations, and as a result, they show that there are contingent situations: Def. 12 (Contingency). K(p) :↔ (DθP (p) ∧ Dθ¬P (p)) (A situation is contingent iff God permits it to be or not to be the case.) T44. ∀p(K(p)↔ (¬CθP (p) ∧ ¬Cθ¬P (p))) (For all situations, a situation is contingent iff neither God wills that situation to be the case, nor wills its opposite to be the case.) Proof. 1. K(p)↔ (DθP (p) ∧ Dθ¬P (p)) [Def. 12] 2. DθP (p)↔ ¬Cθ¬P (p) [T9, Spec] 3. Dθ¬P (p)↔ ¬CθP (p) [T9.2, Spec] 4. K(p)↔ (¬Cθ¬P (p) ∧ ¬CθP (p)) [Eq, 2 & 3 in 1] 5. K(p)↔ (¬CθP (p) ∧ ¬Cθ¬P (p)) [PC, 4] 6. ∀p(K(p)↔ (¬CθP (p) ∧ ¬Cθ¬P (p))) [Gen, 5] 74 G. B. da Silva and F. M. Bertato T45. ∀p(K(p)↔ (¬CθP (p) ∧ ¬SθP (p))) (For all situations, a situation is contingent iff neither God wills that situation to be the case, nor is opposed to that.) Proof. 1. K(p)↔ (¬CθP (p) ∧ ¬Cθ¬P (p)) [T44, Spec] 2. SθP (p)↔ Cθ¬P (p) [A8, Spec] 3. ¬Cθ¬P (p)↔ ¬SθP (p) [PC, 2] 4. K(p)↔ (¬CθP (p) ∧ ¬SθP (p)) [Eq, 3 in 1] 5. ∀p(K(p)↔ (¬CθP (p) ∧ ¬SθP (p))) [Gen, 4] T46. ∀p(K(p)↔ ¬(CθP (p) ∨ SθP (p))) (For all situations, a situation is contingent iff it is not the case that God wills that situation to be the case or He is opposed to that.) Proof. 1. K(p)↔ (¬CθP (p) ∧ ¬SθP (p)) [T45, Spec] 2. K(p)↔ ¬(CθP (p) ∨ SθP (p)) [PC, 1] 3. ∀p(K(p)↔ ¬(CθP (p) ∨ SθP (p))) [Gen, 2] T47. ∃pK(p)↔ ¬∀p(CθP (p) ∨ SθP (p)) (There is a contingent situation iff it is not the case that, for all situations, God wills that situation to be the case or He is opposed to that.) Proof. 1. K(p)↔ ¬(CθP (p) ∨ SθP (p)) [T46, Spec] 2. ∃pK(p)↔ ∃p¬(CθP (p) ∨ SθP (p)) [∃, 1] 3. ∃pK(p)↔ ¬∀p¬¬(CθP (p) ∨ SθP (p)) [Def. 1] 4. ∃pK(p)↔ ¬∀p(CθP (p) ∨ SθP (p)) [PC, 3] T48. ∃pK(p)↔ ¬OW (There is a contingent situation iff God is not a 'want-it-all'.) Proof. 1. ∃pK(p)↔ ¬∀p(CθP (p) ∨ SθP (p)) [T47] 2. SθP (p)↔ Cθ¬P (p) [A8, α(p)/P (p)] 3. ∃pK(p)↔ ¬∀p(CθP (p) ∨ Cθ¬P (p)) [Eq, 2 in 1] 4. OW ↔ ∀p(CθP (p) ∨ Cθ¬P (p)) [Def. 10] A First-Order Modal Theodicy 75 5. ∃pK(p)↔ ¬OW [Eq, 4 in 3] T49. ∃pK(p) (There is at least one situation that is contingent.) Proof. 1. ∃pK(p)↔ ¬OW [T48] 2. ¬OW [T39] 3. ∃pK(p) [MP, 1, 2] An attempt to formalize the intuitive notion of responsibility is made below, where 'to be responsible for' is defined as an operator, Oθ. 14 Def. 13 (Responsibility). Oθα(p) :↔ Aθα(p) (God is responsible for a state of affairs iff He is the direct cause of that.) Theorem T50 is simply the generalization of definition above: T50. ∀p(Oθα(p)↔ Aθα(p)) (For all situations, God is responsible for a state of affairs iff He is the direct cause of such a state of affairs.) In the following last three theorems of N1, it is shown that if God is responsible for some situation, then it is good. But if some situation is evil, God is not responsible for. And, finally, if some evil happens, but God does not oppose to it (what would imply that it would not be the case), then the situation is contingent. T51. ∀p(OθP (p)→ d(p)) (For all situations, if God is responsible for a situation that is the case, then the situation is good.) 14Originally, definition 13 was stated by Nieznański as Oxα(p) :↔ (Axα(p) ∨ (¬Sxα(p) ∧ WxCθSxα(p))), in the notation of this work. We recognize the merits of Nieznański's intuition: according to his thought, some person can be said "responsible" for a state of affairs whenever this person is the cause of that, or the person is not opposed to it, although knowing that God wills that person to be opposed to this state of affairs [11, p. 213]. But here, changing to θ all occurrences of x avoided problems with multi-modalities. This led as consequence to a simplification of the definition of responsibility, for God is the only person "formalized" in the system. 76 G. B. da Silva and F. M. Bertato Proof. 1. CθP (p)→ d(p)) [T32, Spec] 2. AθP (p)↔ CθP [Def. 11, α(p)/P (p)] 3. OθP (p)↔ AθP (p) [T51, Spec] 4. OθP (p)↔ CθP (p) [Eq, 3 in 2] 5. OθP (p)→ d(p) [Eq, 4 in 1] 6. ∀p(OθP (p)→ d(p)) [Gen, 5] T52. ∀p(z(p)→ ¬OθP (p)) (For all situations, if a situation is evil, then God is not responsible for such a situation.) Proof. 1. z(p) [Hip] 2. OθP (p)→ d(p) [T50, Spec] 3. ¬d(p)→ ¬OθP (p) [PC, 2] 4. z(p)→ ¬d(p) [A6, Spec] 5. ¬d(p) [MP, 1, 4] 6. ¬OθP (p) [MP, 5, 3] 7. z(p)→ ¬OθP (p) [DT, 1-6] 8. ∀p(z(p)→ ¬OθP (p)) [Gen, 7] T53. ∀p((z(p) ∧ ¬SθP (p))→ K(p)) (For all situations, if a situation is evil, and God is not opposed to it, then the situation is contingent.) Proof. 1. z(p) ∧ ¬SθP (p) [Hip.] 2. z(p) [PC, 1] 3. ¬SθP (p) [PC, 1] 4. z(p)→ ¬OθP (p) [T52, Spec] 5. ¬OθP (p) [MP, 2, 4] 6. OθP (p)↔ AθP (p) [T50, Spec.] 7. ¬OθP (p)↔ ¬AθP (p) [PC, 6] 8. ¬AθP (p) [MP, 5, 7] 9. AθP (p)↔ CθP (p) [Def 11, α(p)/P (p)] 10. ¬AθP (p)↔ ¬CθP (p) [PC, 9] 11. ¬CθP (p) [PC, 8, 10] 12. ¬CθP (p) ∧ ¬SθP (p) [PC, 11, 3] A First-Order Modal Theodicy 77 13. K(p)↔ ¬CθP (p) ∧ ¬SθP (p) [T45, Spec] 14. K(p) [Eq, 13 in 12] 15. (z(p) ∧ ¬SθP (p))→ K(p) [DT, 1–14] 16. ∀p((z(p) ∧ ¬SθP (p))→ K(p)) [Gen, 15] 5 Semantics for N1 A modelM for N1 consists of a quadruple 〈W,R,D, V 〉, in which W is a set of 'worlds', R is a relation on W , D is a domain of 'objects', and V is a function such that, if P is an n-ary predicate in LN1, then V (P) is a set of n+1-tuples in the form (u1, u2, ..., un, w), in which u1, ..., un ∈ D, and w ∈W . In such model every assignment μ is such that, for each variable p of LN1, μ(p) ∈ D. Since N1 has only one constant ('θ'), we fix an element t ∈ D to be its interpretation, i. e., for every μ, μ(θ) = t, where t is a fixed element in D. Every wff φ has a truth-value (1 or 0) at a world with respect to an assignment μ according to the following conditions: (a) Vμ(φ(x), w) = 1 iff (μ(x), w) ∈ V (φ), and 0 otherwise; (b) Vμ(¬φ,w) = 1 iff Vμ(φ,w) = 0, and 0 otherwise; (c) Vμ(φ→ ψ,w) iff Vμ(φ,w) = 0 or Vμ(ψ,w) = 1, and 0 otherwise; (d) Vμ(φ ∨ ψ,w) = 1 iff Vμ(φ,w) = 1 or Vμ(ψ,w) = 1, and 0 otherwise; (e) Vμ(φ ∧ ψ,w) = 1 iff Vμ(φ,w) = 1 and Vμ(ψ,w) = 1, and 0 otherwise; (f) Vμ(Cθφ,w) = 1 iff Vμ(φ,w′) = 1 for every w′ ∈ W such that wRw′, and 0 otherwise; (g) Vμ(Wθφ,w) = 1 iff Vμ(φ,w) = 1, and 0 otherwise; (h) Vμ(∀xφ(x), w) = 1 iff Vμ(φ(x), w) = 1 for every x ∈ D− {t}, and 0 otherwise. A wff φ is valid in M iff Vμ(φ,w) = 1, for every w ∈ W and every assignment μ. In the following, we introduce a particular model for N1. LetM = 〈W,R,D, V 〉 be an interpretation for N1, such that W = {w0, w1, ..., wn, ...}, where n ∈ N, R = W ×W , D = Z, and V is the union of the following sets: V (B) = {(0, wn) : n ∈ N}; V (z) = {(−1, wn) : n ∈ N}; V (P ) = V (B) ∪ V (z) ∪ {(2n,wn) : n ∈ N}; V (d) = V (P )− V (z); 78 G. B. da Silva and F. M. Bertato V (n) = {(3n,wn) : n ∈ N∗}; V (Op) = {(i,−i, wn) : i ∈ Z∗ and n ∈ N}. We fix 0 as the interpretation of θ, then for every assignment μ: μ(θ) = 0; μ(p) = k, where k ∈ Z∗. It is possible to show that M is a model for N1, and consequently, the axioms of N1 are valid in M. 6 Final remarks We presented here our system N1, which deals with the Logical Problem of Evil, based essentially on the system introduced by Edward Nieznański in [11]. We believe that N1 has a more adequate modal characterization. Our philosophical concern was to investigate the allegation that God's omnipotence implies that every situation which is the case, including evil ones, is willed by God. We showed that actually, given a formalization that could be easily accepted by many theists, it is possible to deduce that the attributes of God are not inconsistent with the existence of evil, and more, that religious determinism (as formalized in the system) is false. We showed also that, assuming the formalization given in N1, God is neither the direct cause of, nor responsible for every situation; that there are contingent situations; that evil situations that God does not oppose are contingent; among other results. As a secondary result, we think that N1 establishes also a very promising approach in applications of formal systems. That contemporary logic has powerful tools to solve relevant problems is beyond any doubt, but we think that our system is an example of how formal logic can be applied to deal with philosophical problems in the fields of Philosophy of Religion and Analytic Theology. Finally, to elaborate a formal theodicy is just one more way to contribute for the establishment of bridges between the fields of Logic and Religion, and we aim at colaborating even more to that. 7 Acknowledgments This research was made possible through the support of grant No. 61108 ("Formal Approaches to Philosophy of Religion and Analytic Theology") from the John Templeton Foundation. The opinions expressed in this paper are those A First-Order Modal Theodicy 79 of the authors and do not necessarily reflect the views of the John Templeton Foundation. This study was also financed in part by Brazilian National Council for Scientific and Technological Development (CNPq). References [1] James Beebe. Logical Problem of Evil. Internet Encyclopedia of Philosophy, 2003 (online). [2] Cambridge Polish-English Dictionary. Cambridge University Press (online), 2019. [3] Walter Carnielli and Claudio Pizzi. Modalities and multimodalities, volume 12. Springer Science & Business Media, 2008. [4] Gesiel Borges da Silva and Fábio Maia Bertato. Logic and philosophical issues: an axiomatic approach to theodicy. In XXV Congresso de Iniciação Cientıfica da Unicamp, Campinas, Galoá, 2017. [5] Melvin Fitting and Richard L. Mendelsohn. First-order modal logic, volume 277. Springer Science & Business Media, 2012. [6] Raul Hakli and Sara Negri. Does the deduction theorem fail for modal logic? Synthese, 187(3):849–867, 2012. [7] George Edward Hughes and Max J. Cresswell. A new introduction to modal logic. Routledge, 1996. [8] David Hume. Dialogues Concerning Natural Religion: And Other Writings, Cambridge University Press, 2007/1779. [9] John Mackie. Evil and omnipotence. Mind, 64(254):200–212, 1955. [10] Angelo Margaris. First-order mathematical logic. Dover, 1990. [11] Edward Nieznański. Aksjomatyczne ujecie problemu teodycei. Roczniki Filozoficzne, 55(1):201–217, 2007. [12] Edward Nieznański. Elements of modal theodicy. Bulletin of the Section of Logic, 37(3):4, 2008. [13] Alvin Plantinga. God, freedom, and evil. Eerdmans, 1977. 80 G. B. da Silva and F. M. Bertato Gesiel Borges da Silva Institute of Philosophy and the Humanities (IFCH) University of Campinas (Unicamp) Rua Cora Coralina, 100 Cidade Universitária, CEP 13083-896, Campinas, SP, Brazil E-mail: gesiel.gbs@gmail.com Fábio Maia Bertato Centre for Logic, Epistemology, and the History of Science University of Campinas (Unicamp) R. Sérgio Buarque de Holanda, 251 Cidade Universitária, CEP 13083-859, Campinas, SP, Brazil E-mail: fbertato@unicamp.br