Logic and Logical Philosophy Volume 20 (2011), 59–72 DOI: 10.12775/LLP.2011.003 Robert Trypuz Piotr Kulicki A NORM-GIVER MEETS DEONTIC ACTION LOGIC Abstract. In the paper we present a formal system motivated by a specific methodology of creating norms. According to the methodology, a normgiver before establishing a set of norms should create a picture of the agent by creating his repertoire of actions. Then, knowing what the agent can do in particular situations, the norm-giver regulates these actions by assigning deontic qualifications to each of them. The set of norms created for each situation should respect (1) generally valid deontic principles being the theses of our logic and (2) facts from the ontology of action whose relevance for the systems of norms we postulate. Keywords: deontic action logic, lawmaking, situations, agents' abilities. Introduction Deontic logic can be seen as a formal tool for analysing rational agent's behaviour in the context of systems of norms.1 The interaction can be considered locally, from the perspective of an agent or globally, from the point of view of a norm-giver. In the present paper we focus on the former. We assume the following: • We work within logic in which deontic notions are attached to actions. The paper is in this sense a continuation of the work from [7, 10, 11, 1 We would like to thank the anonymous reviewer of Logic and Logical Philosophy for his/her very constructive and detailed comments. Special Issue: Logic in Cognitive Science. Guest Editors: J. Malinowski and R. Palczewski © Nicolaus Copernicus University (Toruń) 2011 ISSN: 1425-3305 60 Robert Trypuz, Piotr Kulicki 12]. The present paper extends the earlier studies by the explicit introduction of multiple situations into the considerations. • Situations are analysed separately. The history of agent's behaviour does not influence the deontic qualifications of present actions. • We consider only one type of agents. It means that every agent has the same abilities and the same rights and duties. • The norm-giver has a complete knowledge about the agent's abilities in all possible situations. If such an assumption is unrealistic for some applications, we treat the system of norms as dependant on the norm-giver's beliefs. • We restrict ourselves to situations with a finite number of possible actions. If there are infinite possible behaviours we have to group them into a finite number of types. We suggest starting to build the system of norms from analysing the situations (or types of situations) separately. For any of them the normgiver identifies the actions that are ontologically possible. Then deontic qualifications are attached to the actions. Finally, the qualifications are generalised in order to obtain general deontic rules which build the system of norms. There may be actions that are possible in one situation and not in another. We understand that the agent has, in general, the ability to perform an action when there is at least one situation in which the action is possible. For example, we would say that an agent has the ability to turn a light on, when at least in one situation the agent can successfully do that. However, in certain situations it may be impossible because the light is already on or the light bulb is burnt out. In order to generalise norms over situations one has to recognise the same action in different situations. To establish such a correspondence we treat actions as combinations of simple elements, such as taking a left turn, answering a phone call, turning the light on. These elements occur in different situations and can be relatively easily recognised there. Such a vision of norm development can be used for establishing new systems of norms and analysing the existing ones. Its formalisation enables us to discuss several issues connected with the relation between norms and abilities, especially the well known Kant's Law. We can also put new light on the notions of internal and external actions discussed in philosophy and AI, e.g. [5, 4]. Firstly, we present our intuitions in terms of frames which are "mathematical pictures of ontologies" [1]. Then we define an appropriate deA norm-giver meets deontic action logic 61 ontic action logic. Finally, we apply the logic to an example taken from the area of traffic regulations. 1. Deontic action and situation frame A deontic action and situation frame is a structure DAS = 〈E , S, exe,LEG, ILL,REQ〉 E is a nonempty set. Elements of the set represent all the possible modes in which actions can be executed. Every subset of E we shall call an action. S is a set of situations or states, understood as complete (with reference to selected properties) descriptions of the situation.2 exe : S → 2E is an executability function which assigns a set of modes of actions which can occur in s to every situation s ∈ S. Thus, for every s, exe indicates whether certain action mode can or cannot take place in it. We use function exe instead of (action-labeled) accessibility relation between situations, since, as mentioned in the introduction, we are not interested here in how situations are ordered. We say that action mode e is external in s ∈ S iff e ∈ exe(s). Otherwise it remains only internal in s. Thus, an internal action mode in principle belongs to a repertoire of actions3 but it may not be executable in a certain situation. We can extend the notion of external action mode to actions by defining external action. We say that action X ⊆ E is external in state s iff X ∩ exe(s) 6= ∅ (i.e. X contains at least one external action modes in s). Otherwise the action is internal in s. The set of all action modes external in s can be interpreted as the local universal action (the universal action in s). The universal action is the sum of all local universal actions: Exe = ⋃ s exe(s). 2 In some contexts situations can be reduced to the subsets of 2E (i.e. to the sets of actions). This way of thinking was used by Trypuz in [9]. In the approach from the present paper, two situations "consisting of" the same modes of actions may differ due to different deontic classification of those modes or simply different facts may hold in them. Thus, the function exe is introduced in order to connect situations with the appropriate sets of actions. 3 We have borrowed the term from the works of Krister Segerberg (cf. [6, 8]). 62 Robert Trypuz, Piotr Kulicki We assume that exe(s) is never empty ∀s ∈ S, exe(s) 6= ∅ and every action mode is external in at least one situation: E = Exe. (1) The last assumption excludes from our consideration these agent abilities which are not manifested in any situation from S. It is worth noting that (1) is a natural result of our methodological assumption that the normgiver creates a picture of the agent's repertoire of action by analysing what the agent can do in each particular situation. We shall call an action X non-empty iff X 6= ∅. A non-empty action has to be external in at least one situation but does not have to be external in all situations. Now we shall turn to questions about some details of the model.4 The first questions is whether there is a situation in which exe(s) = E . In fact this is a specification of more general issue whether for every X ⊆ E there is s s.t. X = exe(s). This is not required, though possible. Another interesting question goes as follow: "Since every subset X of E is an action, how then to be understood action X = exe(s1) ∩ exe(s2) where s1 6= s2?" It could be said that exe(s1)∩exe(s2), if not impossible (i.e. not empty), is an action which can be carried out in s1 and s2. LEGs, ILLs and REQs are subsets of 2exe(s) and should be understood as sets of legal, illegal and required actions in s, respectively. The basic characterisation of LEGs and ILLs, for any s ∈ S and X, Y ∈ 2exe(s), is the fact that they are ideals, i.e. they satisfy the following two principles: X ∈ LEGs (ILLs) and Y ⊆ X =⇒ Y ∈ LEGs (ILLs), X ∈ LEGs (ILLs) and Y ∈ LEGs (ILL) =⇒ X ∪ Y ∈ LEGs (ILLs). It is also assumed that LEGs and ILLs have nothing in common: LEGs ∩ ILLs = {∅}. A necessary condition for two actions to be required is that their intersection should be required too: X ∈ REQs and Y ∈ REQs =⇒ X ∩ Y ∈ REQs. 4 The questions were formulated by the reviewer of the paper. A norm-giver meets deontic action logic 63 An impossible action is never required: ∅ 6∈ REQs. (2) (2) is on the ground of our framework equivalent with so called Kant's Law which would have the following shape: For every X ∈ 2exe(s), X ∈ REQs =⇒ X ∩ exe(s) 6= ∅. It means that some possible outcomes of the required action in s should be external in s. Required actions are always legal: REQs ⊆ LEGs. We also require that there is no situation in which all external actions are illegal: exe(s) 6∈ ILLs. (3) Situation in which (3) does not hold we named in [11] deontic hell. Everything that the agent can do in this situation is illegal. In our approach such a trap or a moral dilemma should always be excluded by a norm giver. For every X, Y ∈ 2exe(s), if X is an action required in s and its intersection with action Y contains no external events, then Y is illegal in s: X ∈ REQs and X ∩ Y ∩ exe(s) = ∅ =⇒ Y ∈ ILLs. In other words, it means that if the agent (taking into account his abilities and external conditions) is required to do X in s and, at the same time, by doing X cannot bring about action X ∩ Y in this situation, then Y is illegal (in order not to leave the agent any doubts what a norm-giver requires from him). 2. Deontic action logic In this section we present a logical language and a logic, deontic action logic DAL, for the deontic action and situation frame. Deontic action logic is a deontic logic where deontic operators (such as obligation, permission and prohibition) apply to the names of actions. In the papers 64 Robert Trypuz, Piotr Kulicki [10, 11] we introduced a space of deontic action logics and pointed out some applications of the systems in question. The language of DAL is defined in Backus-Naur notation in the following way: φ ::= ⊤ | α ⊜ α | P(α) | F(α) | O(α) | ¬φ | φ ∧ φ | φ (4) α ::= ai | 0 | 1 | α | α ⊔ α | α ⊓ α (5) where ai belongs to a finite set of action generators Act0, "0" is the impossible action and "1" is the universal action; "α ⊔ β" – α or β (a free choice between α and β); "α⊓β" – α and β (parallel execution of α and β); "α" – not α (complement of α); "⊤" is an arbitrary tautology, "α ⊜ β" means that α is locally (i.e. in the actual situation) identical with β (instead of ¬(α ⊜ β) we will also write α 6⊜ β); "P(α)" – α is (strongly) permitted; "F(α)" – α is forbidden, "O(α)" – α is obligatory and "φ" – φ is necessary (in the Leibnizian sense). Further, for fixed Act0, by Act we shall understand the set of formulae defined by (5). Obviously, Act0 ⊆ Act. Thus, operators ⊜, P, F and O are sentence creating and take names as arguments. We add the definitions of all missing standard PC operators and the following ones: α ⊑ β =df α ⊓ β ⊜ α (6) ♦φ =df ¬¬φ (7) Pwe(α) =df ¬F(α) (8) α = β =df (α ⊜ β) (9) ⊙(α) =df α 6⊜ 0 (10) By "α ⊑ β" we mean that "α is locally included in β". "♦" is a dual of "" (7). (8) defines the concept of weak permission. In contrast to a strongly permitted action, a weakly permitted one is permitted in some situations, in combination with some other actions. (9) defines global (i.e. in every context) identity between actions. (10) defines "⊙(α)", meaning that α is executable (in the actual situation). Now we introduce an interpretation for actions from Act. Interpretation function I : Act −→ 2E is defined as follows: I(ai) ⊆ E , for ai ∈ Act0, I(0) = ∅, A norm-giver meets deontic action logic 65 I(1) = E , I(α ⊔ β) = I(α) ∪ I(β), I(α ⊓ β) = I(α) ∩ I(β), I(α) = E \ I(α). Thus, every action from the language is interpreted as an action from DAS, i.e. a set of modes of actions (α's extension), and operations "⊔", "⊓" between actions and " " on a single action are interpreted as the settheoretical operations on actions from the frame. If I(α) 6= ∅, then it is a non-empty action. It is worth noting that introducing the interpretation function I we assumed that we are able to give the same name to different modes of actions and actions occurring in different situations. By Is(α) we understand a local interpretation of action (i.e. relativised to situation s) and define it as follows: Is(α) = I(α) ∩ exe(s). Is(α) = ∅ means that I(α) is not an external action in s, whereas Is(α) 6= ∅ states that it is. Sometimes we will say that α is an external action in s if Is(α) 6= ∅. Thus Is(α) points out those modes of action (named) α which can be carried in s. Of course logic cannot explain why Is(α) consists of these and those elements from I(α). The interpretation I constitutes a global semantics that fixes the meaning of actions independently from situation and the function exe(s) constitutes a local ontology for a state s. Is is a combination of them. Here we should raise the question of the interpretations of Boolean algebra. We shall introduce BA on two levels, a local and a global one. The local BA is always relativised to a certain situation and contains the action generators which are external in it and BA built by means of these generators (subset of Acto). We shall treat it as a description of all possible choices which the agent has in this situation. It means that each situation has its own BA described by means of local identity (⊜). By generalisation we obtain the global BA which applies to actions seen from the bird perspective, i.e. it describes all actions and relations between them relativising in a sense all situations to one. At this level we have all the necessary logical relations between actions (e.g. "(α ⊔ α ⊜ 1)") and the (necessary) ontological statements (e.g. "¬ ⊙ (turn-right ⊓ turn-left)"). The set of action generators here is a sum of all of generators from local BA. The necessary logical and 66 Robert Trypuz, Piotr Kulicki ontological statements would express an ontology of norms and actions and would be used in verification of statements for every situation. It is a well-known fact about BA in general that if a set of generators is finite, then there are elements of BA called atoms such that there is no element between them and 0. In the case of BA of actions we get atomic actions. Atoms in local BAs can be different, because sets of actions possible in different situations are different. Every atom is a combination of all action generators of BA and has the form: δ1 ⊓ * * * ⊓ δn, where δk is a generator ak ∈ X(⊆ Act0) or its complement. Following [2], we accept that the interpretation of every atom is a singleton (two lines over the set denote its cardinality): I(δ) = 1, where δ is an atom of BA. A basic intuition is such that an atomic action corresponding to (a set with) one event/outcome is deterministic. As it was noted by Castro and Maibaum in [2], indeterminism of actions may result from combining atomic (deterministic) actions through the free choice operator (⊔). A class of models consisting of the models from M with deontic action and situation frame DAS together with interpretation and standard valuation function will be represented by C. Satisfaction conditions for the formulae of DAL in any model M ∈ C are defined below: M, s |= P(α) ⇐⇒ Is(α) ∈ LEGs M, s |= F(α) ⇐⇒ Is(α) ∈ ILLs M, s |= O(α) ⇐⇒ Is(α) ∈ REQs M, s |= ⊤ M, s |= α ⊜ β ⇐⇒ Is(α) = Is(β) M, s |= ¬φ ⇐⇒ M, s 6|= φ M, s |= φ ∧ ψ ⇐⇒ M, s |= φ and M, s |= ψ M, s |= φ ⇐⇒ ∀s ∈ S, M, s |= φ Thus, action α is permitted (forbidden, obligatory) in situation s if and only if its local interpretation in s belongs to LEGs (ILLs, REQs). That means in practice that if α is permitted in a situation, then it is A norm-giver meets deontic action logic 67 permitted in combination with any action (cf. theses 22 and 25) in it. The same is true for forbiddance and obligation. Satisfaction conditions for defined concepts are as follows: M, s |= Pwe(α) ⇐⇒ Is(α) 6∈ ILLs M, s |= α = β ⇐⇒ ∀s ∈ S, Is(α) = Is(β) (or I(α) = I(β)) M, s |= ♦φ ⇐⇒ ∃s ∈ S, M, s |= φ M, s |= ⊙(α) ⇐⇒ Is(α) 6= ∅ Axiomatisation. DAL is axiomatised by the following set of axioms and rules: axioms of PC, S5 axioms for "", indegenerate Boolean algebra (BA) of actions from Act, identity axioms: α ⊜ α (11) α ⊜ β → (φ → φ(α/β)), (12) where φ is any sentence not containing  or ♦ and φ(α/β) is a sentence obtained from φ by replacing some or all the occurrences of α with β, and, finally specific axioms for deontic operators: P(α ⊔ β) ≡ P(α) ∧ P(β) (13) F(α ⊔ β) ≡ F(α) ∧ F(β) (14) α ⊜ 0 ≡ F(α) ∧ P(α) (15) ¬F(1) (16) O(α) ∧ O(β) → O(α ⊓ β) (17) O(α) → P(α) (18) O(α) ∧ α ⊓ β ⊜ 0 → F(β) (19) The rules of Modus Ponens and Necessitation for  are also accepted.5 Axiom (13) says that free choice between two actions is permitted if and only if each of them is permitted. Axiom (14) has a similar meaning for forbidden actions. (15) expresses the fact that only the impossible action is at the same time permitted and forbidden. Intuitively, for an action to be permitted (forbidden) means "permitted (forbidden) in any 5 The same intuitions can be formalised using other formal tools. Other approaches towards deontic action logic include the one from [3], where the first theory with modalities was presented. We prefer to use BA as it constitutes a ready-made ontology of actions in a form of simple and well established theory. 68 Robert Trypuz, Piotr Kulicki possible circumstances", i.e. "in combination with any other action" (cf. thesis 22). By (16) we reject situations (called deontic hell) where all actions are forbidden. We also accept that if two actions are obligatory then their parallel execution is obligatory too (17) and that obligation implies permission (18). (19) is a logical counterpart of principle of obligation economy and concerns restrictions which obligation "O(α)" imposes on other actions which cannot be done in parallel with α. We tend to believe that those actions should be forbidden. There is a list of a few self-explanatory theses of DAL below. α = β → α ⊜ β ⊙ (α) → ♦ ⊙ (α) (20) P(β) ∧ α ⊑ β → P(α) F(β) ∧ α ⊑ β → F(α) (21) P(α) → P(α ⊓ β) F(α) → F(α ⊓ β) (22) ⊙(α) ≡ (F(α) → ¬P(α)) (23) P(α) ∧ F(β) → ¬ ⊙ (α ⊓ β) (24) P(α) ∧ ⊙(α ⊓ β) → P(α ⊓ β) ∧ ¬F(β). (25) O(α) → ⊙(α) ¬O(0) (26) O(α) ∧ O(β) → ⊙(α ⊓ β) (27) ¬(O(α) ∧ O(α)) (28) ¬(O(α) ∧ F(α)) (29) O(α) → Pwe(α) (30) F(α) ∧ ⊙(α ⊓ β) → ¬O(β) (31) O(α) ∧ ¬ ⊙ (α ⊓ β) → ¬P(β) (32) Theorem 1. DAL is sound and complete with respect to class C. Proof. It is easy to check that the logic is sound with respect to class C of models. We prove completeness in standard way (in fact we shall only sketch the proof). First we define a canonical model for DAL as below. Definition 1. Let Σ be a set of theses of DAL. Then [α]= be an equivalence class of relation = (note that α = β =df (α ⊜ β)), for α ∈ Act. Then a canonical model for Σ consists of: • SΣ = {Γ : Σ ⊆ Γ and Γ is a maximal consistent set of formulas in Σ} • EΣ = {[δ1 ⊓* * *⊓δn]= : δk is a generator ak ∈ Act0 or its complement} A norm-giver meets deontic action logic 69 • exeΣ : SΣ −→ 2E Σ is whatever function which satisfies conditions:6 (1) if 〈Γ, X〉 ∈ exeΣ, then X = {[α]= ∈ E Σ : α 6⊜ 0 ∈ Γ} (2) exeΣ(Γ) 6= ∅, for any Γ ∈ SΣ. • IΣ(α) = {[β]= ∈ EΣ : β ⊑ α ∈ Σ} • LEGΣΓ = {X ∈ 2 exe Σ(Γ) : for every [α]= ∈ X, P(α) ∈ Γ} • ILLΣΓ = {X ∈ 2 exe Σ(Γ) : for every [α]= ∈ X, F(α) ∈ Γ} • OBLΣΓ = {X ∈ 2 exe Σ(Γ) : for every [α]= ∈ X, O(α) ∈ Γ} It is easy, though time consuming, to prove that C contains model MΣ = 〈DAFΣ, IΣ〉, where DAFΣ = 〈EΣ,LEGΣ, ILLΣ,OBLΣ〉. Then it is enough to show that in a canonical model (defined above) the situations verify exactly the formulas they contain, i.e. that MΣ,Γ |= φ ⇐⇒ φ ∈ Γ, for every Γ in MΣ. This lemma is called "truth lemma" and it is proved by induction on the complexity of φ. From this lemma follows that the formulas true in the canonical model are precisely the theorems of DAL and that the theorems of DAL are just those formulas true in any such canonical model. 3. Example In order to illustrate the notions of our logic we shall answer the question: which norms are in force in the situation depicted in Figure 1: (A) P(turn-right) (B) F(go-straight) (C) O(turn-right ⊔ turn-left) There are two basic assumptions: (1) that any inconsistent set of norms cannot be accepted. In practice it means that set of norms Γ might be acceptable if Γ 0 ⊥ and that (2) we have a "minimal" ontology of action enabling us to decide which actions (by nature) and in a particular situation can be carried out in parallel. We see from the traffic sign that O(turn-right ⊔ turn-left). Thus (C) is a correct answer. From the ontological analysis we know that in every situation any two actions can be carried out in parallel, formally: 6 We shall write φ ∈ Σ meaning the same as ⊢Σ φ. 70 Robert Trypuz, Piotr Kulicki b b b b Figure 1. Crossroad 1 ¬ ⊙ (turn-right ⊓ turn-left), ¬ ⊙ (turn-right ⊓ go-straight) and ¬ ⊙ (turn-left ⊓ go-straight). (A) can be accepted, which follows from the fact that (use (13) and (18)): {O(turn-right ⊔ turn-left)} ⊢ P(turn-right) (B) can be accepted too because (use (19)): {O(turn-right ⊔ turn-left),¬ ⊙ ((turn-right ⊔ turn-left) ⊓ go-straight)} ⊢ F(go-straight) Now let us modify the situation s. It is much like the previous one but now the agent cannot turn left because there has been an accident and the road to the left is closed (cf. Figure 2). Turning left belongs to the agent's repertoire, however, in the situation s it cannot be executed: s |= ¬⊙(turn-left). Our logic immediately provides that turn-left cannot be obligatory since it is impossible and that turn-right is obligatory: {O(turn-right ⊔ turn-left),¬ ⊙ (turn-left)} ⊢ O(turn-right) Thus, the facts about the situation change the norms in such a way that the agent does not have the choice between turning left or right any more. A norm-giver meets deontic action logic 71 b b b b b b b b b b b b Figure 2. Crossroad 2 Conclusions In the paper we have presented a formal system motivated by a specific methodology of creating norms. We believe that a norm-giver before establishing a set of norms should create a picture of the agent by creating his repertoire of actions. Then, knowing what the agent can do in particular situations, the norm-giver regulates these actions by assigning deontic qualifications to each of them. The set of norms created for each situation should respect generally valid deontic principles being the axioms/theses of our logic. As the case study has shown our system can be also used for validation of existing systems of norms. In the future work we shall explore systems that cross the limits defined by the assumptions listed in the introduction. We are especially interested in systems with different types of agents, systems in which the sequence of actions may influence their deontic qualification. References [1] Blackburn, P., M. de Rijke and Y. Venema, Modal Logic, Cambridge University Press, 2001. [2] Castro, P. F., and T. S. E. Maibaum, "Deontic action logic, atomic Boolean algebras and fault-tolerance", Journal of Applied Logic 7, 4 (2009): 441–466. 72 Robert Trypuz, Piotr Kulicki [3] Gert-Jan Lokhorst, C., "Reasoning about actions and obligations in firstorder logic", Studia Logica 57, 1 (1996): 221–237. [4] Lorini, E., and Herzig, A., "A logic of intention and attempt", Synthese 163, 1 (2008): 45–77. [5] O'Shaughnessy, B., "Trying (as the mental 'pineal gland')", Journal of Philosophy 70 (1973): 365–386. [6] Segerberg, K., "Applying modal logic", Studia Logica, 39, 2–3 (1980). [7] Segerberg, K., "A deontic logic of action", Studia Logica, 41, 2–3 (1982). [8] Segerberg, K., "Towards an exact philosophy of actio", Topoi 3, 1 (1984). [9] Trypuz, R., "Setna – prosta teoria norm i działań", Filozofia Nauki 3–4 (2008): 155–175. [10] Trypuz, R., and P. Kulicki, "A systematics of deontic action logics based on Boolean algebra", Logic and Logical Philosophy, 18, 3–4 (2009): 253– 270. [11] Trypuz, R., and P. Kulicki, "Towards metalogical systematisation of deontic action logics based on Boolean algebra", pages 132–147 in: G. Governatori and G. Sartor (eds.), Deontic Logic in Computer Science (DEON 2010), 2010. [12] Trypuz, R., and P. Kulicki, "On deontic action logics based on Boolean algebra", Journal of Applied Logic (submitted). Robert Trypuz Department of Logic Faculty of Philosophy The John Paul II Catholic University of Lublin Al. Raclawickie 14 Lublin, Poland trypuz@kul.pl Piotr Kulicki Department of Foundation of Computer Science Faculty of Philosophy The John Paul II Catholic University of Lublin Al. Raclawickie 14 Lublin, Poland kulicki@kul.pl