Supercover Semantics for Deontic Action Logic
Abstract
The semantics for a deontic action logic based on Boolean algebra is extended with an interpretation of action expressions in terms of sets of alternative actions, intended as a way to model choice. This results in a nonclassical interpretation of action expressions, while sentences not in the scope of deontic operators are kept classical. A deontic structure based on Simons’ supercover semantics is used to interpret permission and obligation. It is argued that these constructions provide ways to handle various problems related to free choice permission. The main result is a sound and complete axiomatization of the semantics.
Keywords
Action Alternative semantics Choice Deontic logic Free choice permission Supercover semantics1 Introduction
The standard approach to deontic logic, represented by standard deontic logic (SDL), suffers from a large number of socalled paradoxes, where the paradox of free choice permission is perhaps the most discussed in the literature. These are not paradoxes in any strict sense, but rather clashes between inferences valid in formal deontic logics, and intuitively valid and nonvalid inferences as they occur in informal deontic reasoning.
SDL is the normal modal logic KD. Models are of the form \(\langle W, R, V\rangle \), where W is a nonempty set of possible worlds, R is a binary relation on W, and V is a valuation function for the propositional variables of the language. The relation R has the intended meaning that \((w,v)\in R\) if and only if v is ideal from the point of view of w. The set \(I^w=\{v\in W\,{:}\,(w,v)\in R\}\) is the set of ideal worlds from the point of view of w. The relation R is assumed to be serial, i.e. for each \(w\in W\), there is some \(v\in W\) such that \((w,v)\in R\). A sentence \(P(\varphi )\)—where the intended reading of P is ‘it is permitted that...’—is then true at a world w if \(\varphi \) is true in some world that is ideal from the point of view of w, and a sentence \(O(\varphi )\)—where O has the intended reading ‘it is obligatory that...’—is true at a world w if \(\varphi \) is true in all worlds that are ideal from the point of view of w.
where \([\text {go by bus}]\) and \([\text {go by train}]\) are the actions described by the expressions ‘go by bus’ and ‘go by train’, respectively. In general, a sentence of the form ‘Permitted \(\alpha \) or \(\beta \)’ can be analyzed as saying:Jane may choose an action from the set \(\{[\text {go by bus}],[\text {go by train}]\}\),
Given certain natural assumptions, an analysis along these lines will produce the desired properties of free choice permissions. If it is permitted to choose between having pasta and having pizza, then it is also permitted to have pasta and permitted to have pizza. In general, if every action in a set of actions are permitted, then any (nonempty) subset of that set will contain permitted actions only. This idea is not new; according to Hansson,Permitted to choose an action from the set \(\{[\alpha ],[\beta ]\}\).
Hansson does not develop the idea further. In the context of natural language semantics, the alternative semantics approach interprets disjunction as introducing sets of alternatives (see e.g., AlonsoOvalle 2006; Ciardelli and Roelofsen 2011; Ciardelli et al. 2009; Groenendijk and Roelofsen 2009; Roelofsen 2013; Simons 2005a, b). The idea is, essentially, that a disjunctive statement tells you that at least one proposition from a larger set of propositions is true. One of the motivations for this kind of interpretation of disjunction is to account for free choice phenomena. The alternative analysis of disjunction allows interpreting permission modals as operating over sets of alternatives. A permitted disjunction, then, tells you that each proposition from the set of alternatives introduced by the disjunctive statement is permitted. Simons (2005a, b) develops this idea in more detail, introducing a precise notion of how deontic modals interact with a set of alternatives in terms of supercovers. However, her account makes certain counterintuitive predictions with regards to disjunctive statements not in the scope of deontic operators. In addition, Simons does not develop a full formal semantics suitable for a deontic logic....free choice permission should be represented as a property of the set of actiondescribing sentences (\(\{a,b\}\) respectively \(\{a,b,c\}\)) rather than a property of the disjunction of these sentences (\(a\vee b\) respectively \(a\vee b\vee c\)). (2013, p. 218)
In this paper, I will combine Simons’ alternative semantics approach to disjunction and deontic modals with a static deontic action logic based on Boolean algebra. Specifically, I will be concerned with logics in the style of Segerberg (1982) and Trypuz and Kulicki (2009, 2015), and the actiontheoretic layer of the logic of Castro and Maibaum (2009). In these logics, the arguments of deontic operators are names of actions, rather than propositional statements. Action expressions are given a semantics based on an underlying Boolean algebra, and permission is interpreted as an ideal on this algebra. This construction validates the free choice principle; however, substitution of Boolean algebra identities within the scope of the permission operator is a valid rule of inference, so the vegetarian free lunch problem arises. In addition, the distinction between action expressions and propositions is syntactically sharp, but semantically less so—the logical behavior of both types of expressions is essentially classical. When the semantics is extended with an interpretation of action expressions in terms of sets of action types, the logic of action expressions will deviate from the Boolean algebra interpretation, resulting in a system where propositional formulas behave classically, while action expressions do not. I will argue that this move indeed offers ways to avoid the problems of free choice permission.
The structure of the paper is as follows. Section 2 introduces Simons’ supercover semantics and highlights some problems. In Sect. 3.1, basic action theoretic and deontic structures are defined; these structures are then used to construct a formal semantics in Sect. 3.2. I discuss the concepts of permission and obligation in Sect. 4. In Sect. 5, an axiomatization of the semantics is defined, and soundness and completeness results are obtained. In Sect. 6, I discuss certain aspects of the logic in more detail and compare the semantics to related work. Section 7 concludes the paper and discusses ideas for further research.
2 Supercover Semantics
Simons’ supercover semantics is an attempt to deal with free choice phenomena in the context of natural language semantics (Simons 2005a, b).^{1} Simons suggests supplementing the standard semantics for disjunction in the scope of deontic modals with a distribution requirement. This distribution requirement guarantees that \(P(\varphi \,\text {or}\,\psi )\) is true only if there are ideal worlds in both the proposition expressed by \(\varphi \) and the proposition expressed by \(\psi \), and that \(O(\varphi \,\text {or}\,\psi )\) is true only if there are ideal worlds in both disjunct propositions, and the sum of the proposition expressed by \(\varphi \) and the proposition expressed by \(\psi \) contains all ideal worlds.
Formally, this is accomplished in two stages. First, ‘or’ is treated as a setformation operator, introducing sets containing propositions corresponding to the disjuncts. Second, Simons introduces the notion of a supercover. Let U be some background set. A nonempty \(S\subseteq {\mathscr {P}}(U)\) is a supercover of \(A\subseteq U\) if and only if (i) every member of S contains some member of A, and (ii) every member of A belongs to some member of S (Simons 2005a, p. 276). In other words, S is a supercover of A if the union of S is a superset of A, and every element of S has a nonempty intersection with A.

\((\varphi \,\text {or}\,\psi )\) is true at \(w\in W\) iff \(\{\Vert \varphi \Vert ,\Vert \psi \Vert \}\) is a supercover of some \(X\subseteq W\) with \(w\in X\).

\(P(\varphi \,\text {or}\,\psi )\) is true at \(w\in W\) iff \(\{\Vert \varphi \Vert ,\Vert \psi \Vert \}\) is a supercover of some \(X\subseteq I^w\).

\(O(\varphi \,\text {or}\,\psi )\) is true at \(w\in W\) iff \(\{\Vert \varphi \Vert ,\Vert \psi \Vert \}\) is a supercover of \(I^w\).
In the usual Boolean semantics, disjunction introduction is a valid principle, since \(\Vert \varphi \,\text {or}\,\psi \Vert =\Vert \varphi \vee \psi \Vert =\Vert \varphi \Vert \cup \Vert \psi \Vert \). In supercover semantics, on the other hand, disjunction introduction is not valid. Consider the following example sentence given by Simons (2005a, p. 293, n. 33): “Jane dances or \(2+2=5\)”. Under the supercover semantics (provided that “\(2+2=5\)” is false at every possible world), this sentence will turn out false at all worlds, since a supercover cannot contain the empty set. Nevertheless, there is a strong intuition that if “Jane dances” is true, then “Jane dances or \(2+2=5\)” is true as well. In general, any disjunction with a logically impossible disjunct will inevitably be false under the supercover semantics. This constitutes a counterexample to the Boolean principle of disjunction introduction.If \(\varphi \) is true at w, then \((\varphi \,\text {or}\,\psi )\) is true at w.
It is an open question whether it is possible to tinker with the supercover semantics in such a way as to make it agree with Boolean disjunction outside the scope of deontic modals. In this paper, I will take a different approach to this problem. With a careful distinction between action expressions and propositional statements, the usual Boolean story may be told for propositional statements, while a supercover semantics may be developed for action expressions. This makes it possible to deal with free choice phenomena while keeping classical disjunction in purely factual contexts outside the scope of deontic modals.
Are there independent reasons for giving up disjunction introduction for action expressions? Anglberger et al. (2014) argue that there are. One can for example appeal to normality, in the sense that action expressions are taken to refer to normal instances of actions (Pelletier and Asher 1997), or one may argue that action expressions are resource sensitive in the sense of Linear Logic (Girard 1987). Anglberger, Dong, and Roy give an example where action expressions display a kind of resource sensitivity (2014, pp. 24–25). Suppose that you are at a restaurant and are offered to order sushi. This does not imply that you are offered to choose between ordering sushi or pasta. The chef at the restaurant might not know how to cook pasta, or the restaurant might not have the right ingredients for making pasta, etc. In many cases, it seems that choosing between different alternatives is only possible if all the alternatives are live options.
3 A Deontic Logic Based on Supercover Semantics
In Segerberg’s seminal paper (1982), and in the subsequent extensions and variants (Castro and Maibaum 2009; Trypuz and Kulicki 2009, 2015), actions are interpreted as elements of a Boolean algebra, with permission and prohibition interpreted as (disjoint) ideals on this algebra. This means that these logics take notions of strong permission and prohibition as primitive. The model theoretic characterization of these logics interprets elements of the Boolean algebra of actions as sets of action tokens. The semantics to be developed in this paper extends this theory of action by introducing sets of sets of action tokens, and replaces the interpretation of permission by a deontic structure based on Simons’ supercover semantics. The supercover semantics is here developed in a different way compared to the presentation in the previous section. In particular, legal and required sets of sets of action tokens are collected in two sets satisfying certain conditions, similar to neighborhood semantics for modal logics (see e.g. Chellas 1980, Chapter 7).
3.1 Action, Choice and Deontic Status
Assume that a single agent in a single situation has available a (nonempty) set \(H=\{h_1,h_2,\ldots \}\) of action tokens. Action tokens can instantiate action types. Formally, an action type is a subset of H. Let \({\mathscr {A}}={\mathscr {P}}(H)\) be the set of action types. Symbols \(s, t, \ldots \) will be used as variables ranging over action types from \({\mathscr {A}}\). I will also introduce the notion of a choice set. Formally, a choice set is a set of action types. While the impossible action type is represented by the empty set, choice sets are always required to be nonempty. Let \({\mathscr {C}}={\mathscr {P}}({\mathscr {A}}){\setminus } \{\emptyset \}\) be the set of choice sets available to the agent in the situation. Symbols \(S,T, \ldots \) are used as variables ranging over choice sets from \({\mathscr {C}}\). Informally, a choice set represents choosing between the action types in the choice set. As an example, suppose that \(s_1\) and \(s_2\) are the action types denoted by the expressions ‘go by bus’ and ‘go by train’, respectively. The expression ‘go by bus or go by train’ can then be interpreted as denoting the choice set \(\{s_1,s_2\}\). The idea, then, is that the expression ‘go by bus or go by train’ has a reading on which it describes a choice between the action denoted by ‘go by bus’ and the action denoted by ‘go by train’.
Thus, Sempronius is obliged to give a cow or a horse, but neither obliged to give a cow, nor obliged to give a horse. On the other hand, it may be said that Sempronius is obliged to choose one of the alternatives. I will interpret this as meaning that the sum of the action types in a required choice set contains all legal action tokens, and that each action type in a required choice set is legal. The last assumption seems quite natural, since if Sempronius can “fulfill his obligation by giving either of the two things”, it can hardly be the case that he is not permitted to, for example, give a cow. Formally, letThere is e.g. the well known case of Sempronius who has an obligation to give a cow or a horse to Ticius, but he has not the obligation to give Ticius a cow nor has he the obligation to give him a horse. He can fulfill his obligation by giving either of the two things, since he must give one of the two, but he is not obliged to give either in particular. (1971, p. 157)
Theorem 1
 1.
\(S\in \mathbf {LEG}\) if and only if there is \(X\subseteq G\) such that S is a supercover of X,
 2.
\(S\in \mathbf {REQ}\) if and only if S is a supercover of G.
Proof
 1.
(\(\Rightarrow \)) Suppose that \(S\in \mathbf {LEG}\). Let \(X=\bigcup \{s\cap G\,{:}\,s\in S\}\). Clearly, \(X\subseteq G\). First, every element of S has a nonempty intersection with X. Second, it holds that \(X\subseteq \bigcup S\); hence, S is a supercover of X.
(\(\Leftarrow \)) Suppose that S is a supercover of some \(X\subseteq G\). Then, for every \(s\in S\), \(s\cap X\ne \emptyset \), and so \(s\cap G\ne \emptyset \). It follows that \(S\in \mathbf {LEG}\).
 2.
(\(\Rightarrow \)) Suppose that \(S\in \mathbf {REQ}\). By definition, \(G\subseteq \bigcup S\) and \(S\in \mathbf {LEG}\), so every element of S has a nonempty intersection with G. It follows that S is a supercover of G.
(\(\Leftarrow \)) Suppose that S is a supercover of G. It follows that \(G\subseteq \bigcup S\). By the righttoleft direction of the first item of the theorem, it holds that \(S\in \mathbf {LEG}\). Hence, \(S\in \mathbf {REQ}\). \(\square \)
3.2 Deontic Action/Choice Logic
3.2.1 Language
The language has three types of atomic formulas. First, formulas of the form \(\alpha \doteq \beta \) are used to express typeidentity, with the intended meaning that \(\alpha \) and \(\beta \) refer to the same action type. Second, formulas of the form \(\alpha \rightleftharpoons \beta \) are used to express choiceidentity, meaning that \(\alpha \) and \(\beta \) describe the same choices. Third comes deontic formulas of the form \({\mathbf {P}}(\alpha )\), intended to express that \(\alpha \) is permitted. The operators of propositional logic are then used to form complex statements about equivalence and deontic status of actions and choices.
3.2.2 Algebra of Actions
Since fields of sets are Boolean algebras (Monk 1976, pp. 150–151), there is a straightforward way to construct a semantics based on the theory of action described in Sect. 3.1. Every term from \( Act \) is mapped to an element of the set of action types \({\mathscr {A}}\) such that the designated terms \(\mathbf {1}\) and \(\mathbf {0}\) are mapped to H and \(\emptyset \), respectively, and complex terms involving term operations correspond to the settheoretical operations of union, intersection and complement in the obvious way.
3.2.3 Deontic Action Models and Semantics
In this section, the basic action theoretic and deontic structures defined in Sect. 3.1 will be used to construct a formal semantics.
Theorem 2
For any \(\alpha \in Act \) and \(M=\langle H,G,V\rangle \), \(V(\alpha )=\bigcup \llbracket \alpha \rrbracket _M\).
In light of this result, one can think of \(V(\alpha )\) as the range of \(\alpha \): the set of action tokens which are live options in the choice described by \(\alpha \).
A choice set \(\llbracket \alpha \rrbracket \) should be thought of as the choices described by the term \(\alpha \). A term whose choice set is a singleton describes a trivial choice; a choice with only one alternative. A term describes a genuine choice if its choice set consists of more than one alternative. It is clear that the only way to describe a genuine choice is by means of the \(\sqcup \) operator.
The clause for conjunctive terms interprets \(\alpha \sqcap \beta \) as the pairwise intersection of the choices described by \(\alpha \) and the choices described by \(\beta \). The intuition behind this interpretation can be illustrated with an example. Suppose that you are at a restaurant and you are told that “You may order wine or beer and pasta or sushi”. This sentence can be taken to introduce four permitted courses of action: the action of ordering wine and pasta, the action of ordering wine and sushi, the action of ordering beer and pasta, and the action of ordering beer and sushi. The choice set interpretation of conjunctive terms reflects this: simultaneously choose between ordering wine or beer and ordering pasta or sushi, then perform the two chosen actions together.
Following Ju and van Eijck (2016), I use a notion of ‘to do something else’ in the motivation for the choice set interpretation of \({\overline{\alpha }}\). To do something else than \(\alpha \) is to do an action type that is different from the action types introduced by \(\alpha \). Say that two action types are different if their intersection is empty. For a given choice set S of action types, the set \(\{s\in {\mathscr {A}}\,{:}\,s\cap t=\emptyset \,\text { for all}\,t\in S\}\) contains all action types that are different from the ones in S. However, ‘doing something else than \(\alpha \)’ should not be understood as describing a choice between every possible action type different from the ones described by \(\alpha \). Take a sentence such as “Jane may do something else than going to the movies”. What kind of things are Jane permitted to do? Combining the free choice interpretation of permission with the idea that ‘doing something else than going to the movies’ denotes a choice between every possible action type that is different from going to the movies has counterintuitive consequences. For example, among the action types different from that of going to the movies is the action type of robbing a bank (at least assume so for the sake of the argument). But it seems perfectly consistent that Jane is permitted to do something else than going to the movies, while not being permitted to rob a bank. For a given \(\alpha \), there may be many action types that are different from the ones denoted by \(\alpha \). In order to arrive at a precise interpretation of the choice set \(\llbracket {\overline{\alpha }}\rrbracket \), the set operator \(\textsc {Alt}\) is applied, picking out action types that are maximal in the sense that they are not properly included in any other action type in the set. It is readily verified that the set \(\{s\in {\mathscr {A}}\,{:}\,s\cap t=\emptyset \,\text { for all}\,t\in S\}\) contains a unique maximal action type which is equal to \(H{\setminus }\bigcup \llbracket \alpha \rrbracket \). By Theorem 2, it follows that \(\llbracket {\overline{\alpha }}\rrbracket =\{V({\overline{\alpha }})\}\). Basically, then, negation collapses choice sets into singleton sets.
3.2.4 Some Properties and Abbreviations
4 Permission and Obligation
In this section, I will argue that the semantics just outlined deals quite naturally with the problems connected with free choice permissions, and then discuss the defined concept of obligation.
4.1 Permission in DACL
Suppose that Jane may go by bus or by train. Intuitively, it follows that Jane may go by bus, and that Jane may go by train; Jane is permitted to choose one of the options. In everyday discourse, it seems that the permission to do one thing or another is equivalent to both disjuncts being permitted. In the present semantics, the principle of free choice is valid.
Proposition 1
Proof
For the lefttoright direction, let \(M=\langle H, G, V\rangle \) be a deontic action model and suppose that \(M\vDash {\mathbf {P}}(\alpha \sqcup \beta )\), i.e. \(\llbracket \alpha \sqcup \beta \rrbracket _M\in \mathbf {LEG}\). By the clause defining the choice sets of disjunctive terms and properties of \(\mathbf {LEG}\), it follows that \(\llbracket \alpha \rrbracket _M\in \mathbf {LEG}\) and \(\llbracket \beta \rrbracket _M\in \mathbf {LEG}\), which implies that \(M\vDash {\mathbf {P}}(\alpha )\wedge {\mathbf {P}}(\beta )\). The righttoleft direction follows directly from the fact that \(S,T\in \mathbf {LEG}\) implies that \(S\cup T\in \mathbf {LEG}\). \(\square \)
The deontic action logics based on Boolean algebra (Segerberg 1982; Trypuz and Kulicki 2009, 2015) allow inferring that \(\alpha \sqcap \beta \) is permitted from the permission of \(\alpha \). The reason for this is that these logics take the principle of free choice as an axiom, and allow for substitutions of Boolean algebra identities within the scope of the permission operator. In the semantics in this paper, substitution of Boolean equivalents is in general not a valid rule of inference. This means that, for example, even though the classically valid equation \(a\sqcup {\overline{a}}\doteq b\sqcup {\overline{b}}\) is valid in the semantics, one can find models such that \(M\nvDash {\mathbf {P}}(a\sqcup {\overline{a}})\leftrightarrow {\mathbf {P}}(b\sqcup {\overline{b}})\). Given the free choice reading this is desirable since one may be permitted to choose between going by train or not going by train, while not being permitted to choose between robbing a bank or not robbing a bank. As another example, take the classically valid equation \(a\doteq (a\sqcap b)\sqcup (a\sqcap {\overline{b}})\). Since a and \((a\sqcap b)\sqcup (a\sqcap {\overline{b}})\) are extensionally equivalent, i.e. denote the same action type, the equation is valid in the semantics. However, the two expressions may describe different choices. Indeed, a may not describe a genuine choice at all, while \((a\sqcap b)\sqcup (a\sqcap {\overline{b}})\) describes a choice between doing \(a\sqcap b\) and doing \(a\sqcap {\overline{b}}\). In terms of vegetarian lunches, one may take a to describe the action of ordering a vegetarian meal, \(a\sqcap b\) to describe the action of ordering a vegetarian meal and pay for it, and \(a\sqcap {\overline{b}}\) to describe the action of ordering a vegetarian meal and not pay for it.
Proposition 2
Proof
Let \(M=\langle H, G, V\rangle \) be a deontic action model such that \(H=\{h_1, h_2\}\), \(G=\{h_1\}\), \(V(a_1)=\{h_1\}\) and \(V(a_2)=\{h_2\}\). Since \(\llbracket a_1\rrbracket _M=\{\{h_1\}\}\in \mathbf {LEG}\), it holds that \(M\vDash {\mathbf {P}}(a_1)\). But \(\llbracket a_1\sqcap a_2\rrbracket _M=\{\emptyset \}\not \in \mathbf {LEG}\), so \(M\nvDash {\mathbf {P}}(a_1\sqcap a_2)\). \(\square \)
Thus, DACL keeps the free choice postulate but avoids the vegetarian free lunch problems. Even though intuitively deeply problematic, one may argue that there is nothing wrong with vegetarian free lunches per se: one just needs to give permission operators for which the schema \(P(\varphi )\rightarrow P(\varphi \wedge \psi )\) are valid the right kind of informal reading. For example, one can interpret the permission operator in the strong or open sense (henceforth, I will refer to this interpretation as strong permission, and use \(P_s\) to refer to a strong permission operator). According to the strong permission account, \(P_s(\varphi )\) means that every way to perform the action denoted by \(\varphi \) is legal (Anglberger et al. 2014; Broersen 2004; Segerberg 1982; Trypuz and Kulicki 2009, 2015). This account should be contrasted with the weak reading of permission, where an action being weakly permitted means that at least some way of performing it is legal.^{6}
The strong permission account seems to offer an explanation of the problem of vegetarian free lunches: if every way to perform the action of ordering a vegetarian meal is legal, then it follows that ordering a vegetarian meal and not paying for it, which is indeed a way to order a vegetarian meal, must be legal as well. Given this interpretation, one can argue that the clash with intuition arises because of the incompleteness of informal normative discourse (Broersen 2004, pp. 163–164). When I permit you to order a vegetarian meal, I usually implicitly assume that further properties of the permitted action must be taken into account (e.g. that ordering a vegetarian meal requires paying for it). What was actually permitted in the first place, then, was the action of ordering a vegetarian meal and paying for it.
Dignum et al. (1996) offer a formalization of this idea by introducing an operator on action expressions that allows referring to actions performed in isolation, and special action expressions that, apart from naming actions, also refer to contexts in which the actions can be performed. A contextual action expression \(\alpha _C\) means a performance of the action named \(\alpha \), possibly in combination with actions in the context C. The contextual action expressions are used to refer to a restricted set of all possible ways to perform an action. A permission \(P_s(\alpha _C)\), then, means that every way to perform the action \(\alpha \) in combination with actions in the context C is legal. In the system of Dignum et al. (1996), it is possible to have \(P_s(\alpha _C)\) without having \(P_s(\alpha )\). The correct way of translating the sentence “It is permitted to order a vegetarian meal” into formal language, they argue, is to translate it into \(P_s(a_C)\), where a denotes the action of ordering a vegetarian meal and C is some context specifying actions that are ‘safe’ to perform in combination with the action of ordering a vegetarian meal. In this way, one need not say that every possible way to order a vegetarian meal must be legal, but only those ways which are expressed explicitly using some appropriate context.
Even though I agree that vegetarian free lunches are less problematic under the strong reading of permission, I do not think that this account necessarily is the most natural one or the only account worth investigating when it comes to interpreting free choice permissions. For example, Jane may very well choose freely between driving her Volvo to work and driving her BMW to work. The fact that Jane ought to be sober while driving does not cancel her free choice permission: it seems strange to say that the only free choice Jane is permitted to make is that between driving her Volvo sober and driving her BMW sober. Giordani and Canavotto (2016) make a similar point, arguing that “ordinary choices can be risky: we are ordinarily allowed to choose between alternative actions even if there are ways of performing such actions that lead to a violation of the law.” (2016, p. 89). To capture this property, strong permission is too strong, and weak permission is too weak (cf. van der Meyden 1996, p. 470). Even the contextual permission approach of Dignum et al. (1996) fails to account for permissions of risky choices. The present approach, on the other hand, offers a way to account for free choice permissions without resorting to strong permission. The operator \({\mathbf {P}}\) is a kind of mix between the strong and weak reading of permission: \({\mathbf {P}}(\alpha )\) means that every alternative action in the choice described by \(\alpha \) is weakly permitted. Thus, I accept the idea of a free choice permission being a permission in which every alternative action to choose from is legal, but I reject the idea that an action is legal only if every way to perform it is acceptable. Free choice permission is permission applied to choices, rather than directly to actions.
That being said, the present framework provides a straightforward way to combine two kinds of deontic operators: one referring to action types and the other referring to choice sets. For example, the \({\mathbf {P}}\) and \({\mathbf {O}}\) operators refer to choices, while the \({\mathbf {F}}\) operator is technically equivalent to an operator applying directly to action types. It is not possible to introduce strong permission in DACL as a syntactic abbreviation, but it is straightforward to introduce it as a primitive notion. Adding strong permission to DACL results in an extension of Segerberg’s B.C.D. system (1982).
Turning back to the free choice principle itself, it can be noted that the righttoleft direction of it is also valid in any deontic logic where the permission operator is analyzed as a normal modal diamond, that is, as a weak permission operator. However, such logics also validate a stronger principle: \(P(\varphi )\rightarrow P(\varphi \vee \psi )\). This can be seen as a permission variant of Ross’ paradox, admitting the following counterintuitive instance: “If you may post the letter, then you may post the letter or burn it”. This time, the culprit is closure of permission under logical consequence: from the tautology \(\varphi \rightarrow \varphi \vee \psi \), apply closure of permission under logical consequence to obtain \(P(\varphi )\rightarrow P(\varphi \vee \psi )\). In the present framework, permission is not even closed under logical equivalence (valid equations of Boolean algebra), and \({\mathbf {P}}(\alpha )\rightarrow {\mathbf {P}}(\alpha \sqcup \beta )\) is not valid.
Proposition 3
Proof
These properties nicely illustrate the double nature of permission in DACL: (8) says that permitted conjunctions can be weakened, which is a characteristic property of weak permission. Another characteristic property of weak permission is closure: for every action, either it or its negation is permitted. This property fails for the operator \({\mathbf {P}}\) as shown by (11).
The inference seems intuitively valid, and illustrates that free choice effects are not canceled when ‘or’ is embedded under ‘and’. This property is reflected in the validity (9) of Proposition 3.Jane may sit on the sofa and read a book or watch TV. Therefore, Jane may sit on the sofa and read a book and Jane may sit on the sofa and watch TV.
4.2 Obligation in DACL
Regarding the interaction of permission and obligation, it can be noted that the \({\mathbf {O}}\) and \({\mathbf {P}}\) operators satisfy the following principle, which follows directly from the fact that \(\mathbf {REQ}\subseteq \mathbf {LEG}\).
Proposition 4
Note that a consequence of the above principle is that \({\mathbf {O}}(\alpha \sqcup \beta )\rightarrow {\mathbf {P}}(\alpha )\wedge {\mathbf {P}}(\beta )\) is valid. This is in accordance with the justification for the \(\mathbf {REQ}\) set given in Sect. 3.1.
Proposition 5
Proof
Let \(M=\langle H, G, V\rangle \) be a deontic action model such that \(H=\{h_1, h_2\}\), \(G=\{h_1\}\), \(V(a_1)=\{h_1\}\) and \(V(a_2)=\{h_2\}\). Since \(\llbracket a_1\rrbracket _M=\{\{h_1\}\}\in \mathbf {REQ}\), it holds that \(M\vDash {\mathbf {O}}(a_1)\). However, \(\llbracket a_1\sqcup a_2\rrbracket _M=\{\{h_1\},\{h_2\}\}\not \in \mathbf {REQ}\), so \(M\nvDash {\mathbf {O}}(a_1\sqcup a_2)\). \(\square \)
The semantics also validates the wellknown principles of obligation aggregation, obligation weakening, the impossibility of conflicting obligations and a principle saying that choosing to do an impossible action is never obligatory.
Proposition 6
Proof
The proof of (14) is left to the reader. Here is a proof of (15). Let \(M=\langle H, G, V\rangle \) be a model and assume that \(M\vDash {\mathbf {O}}(\alpha \sqcap \beta )\), i.e. \(\llbracket \alpha \sqcap \beta \rrbracket _M\in \mathbf {REQ}\). By (12) of Proposition 4, it holds that \(M\vDash {\mathbf {P}}(\alpha \sqcap \beta )\), so by (8) of Proposition 3\(M\vDash {\mathbf {P}}(\alpha )\), i.e. \(\llbracket \alpha \rrbracket _M\in \mathbf {LEG}\). By the definition of \(\mathbf {REQ}\) and properties of choice sets, it holds that \(G\subseteq \bigcup \llbracket \alpha \sqcap \beta \rrbracket _M\subseteq \bigcup \llbracket \alpha \rrbracket _M\). Taken together, this implies that \(\llbracket \alpha \rrbracket _M\in \mathbf {REQ}\), i.e. \(M\vDash {\mathbf {O}}(\alpha )\). (16) follows from (18) of Proposition 7 below. (17) follows from the syntactic definition of \({\mathbf {O}}\) and the fact that \(\vDash \lnot {\mathbf {P}}(\mathbf {0})\), the latter being valid because \(\{\emptyset \}\not \in \mathbf {LEG}\).\(\square \)
That \({\mathbf {O}}(\alpha )\) and \({\mathbf {O}}({\overline{\alpha }})\) are not jointly satisfiable guarantees what is known as deontic consistency: one and the same choice can never be both obligatory and prohibited. In fact, Theorem 2 together with the definition of \(\mathbf {REQ}\) shows that conflicting obligations require accepting models where \(G=\emptyset \), i.e. models where there are no legal action tokens available.
Regarding the interaction of obligation and prohibition, the following validities are shown to hold.
Proposition 7
Proof
(18) is immediate from the syntactic definition of \({\mathbf {O}}\) and \({\mathbf {F}}\). For (19), let \(M=\langle H, G, V\rangle \) be a deontic action model and assume that \(M\vDash {\mathbf {F}}(\alpha )\). Then \(G\subseteq V({\overline{\alpha }})\). Since \(\llbracket {\overline{\alpha }}\rrbracket _M=\{V({\overline{\beta }})\}\), it immediately follows that \(\llbracket {\overline{\alpha }}\rrbracket _M\in \mathbf {REQ}\). (20) is a consequence of (19) and (14). \(\square \)
Trypuz and Kulicki (2015, p. 1254) take the principles of obligation economy (18) and obligation trimming (20) together with (17) as axioms characterizing a minimal concept of obligation. The \({\mathbf {O}}\) operator is stronger than this; for example, obligations can be weakened according to (15). In the basic system of Trypuz and Kulicki (2015) where obligation is axiomatized by (17), (18), and (20), it is not possible to derive (15).
Castro and Maibaum (2009) introduce an obligation operator in terms of strong permission and prohibition, which in the present framework corresponds to the abbreviation \({\mathbf {O}}^P_F(\alpha ){\mathop {=}\limits ^{\text {def}}}{\mathbf {P}}_s(\alpha )\wedge {\mathbf {F}}({\overline{\alpha }})\) (where \({\mathbf {P}}_s\) is strong permission with truth conditions \(M\vDash {\mathbf {P}}_s(\alpha )\) iff \(V(\alpha )\subseteq G\)). A consequence of this definition is that there is only one obligatory action type: \({\mathbf {O}}^P_F(\alpha )\wedge {\mathbf {O}}^P_F(\beta )\rightarrow \alpha \doteq \beta \) is valid. As observed by Trypuz and Kulicki (2015, p. 1253), this property makes many of the intuitively desirable properties of obligation trivially valid. The \({\mathbf {O}}\) operator of DACL is introduced using the \({\mathbf {P}}\) operator instead of \({\mathbf {P}}_s\), which guarantees that there may be several different obligations. Consider, for example, a model \(M=\langle H,G,V\rangle \) where \(G=\{h_1,h_2\}\) and \(V(a_1)=\{h_1\}\), \(V(a_2)=\{h_2,h_3\}\) and \(V(a_3)=\{h_1,h_2\}\). In this model, \(M\vDash {\mathbf {O}}(a_1\sqcup a_2)\) and \(M\vDash {\mathbf {O}}(a_3)\), but \(M\nvDash a_1\sqcup a_2\doteq a_3\) and \(M\nvDash a_1\sqcup a_2\rightleftharpoons a_3\).
5 Axiomatization
In this section, the logic DACL is presented axiomatically. The axiom system is shown to be sound and complete with respect to the semantics defined in previous sections. For the rest of what follows, assume a fixed set \( Act _0\) of generators.

A complete set of axioms for Propositional Logic (PL).

A complete set of axioms for Boolean algebra in terms of \(\doteq \) [e.g. axioms (A1)–(A5), with \(=\) replaced by \(\doteq \)].
 Axioms for \(\rightleftharpoons \):
 Identity axioms: where \(\theta (\alpha )\) is some term with a number of occurrences of \(\alpha \), and \(\theta (\beta )\) is the term obtained from \(\theta (\alpha )\) by replacing some or all occurrences of \(\alpha \) with \(\beta \).
 Bridge axioms:
 Deontic axioms:
 The sole rule of inference is modus ponens (\(\vdash \varphi \) means that \(\varphi \) is a theorem of the axiom system):

(MP) If \(\vdash \varphi \) and \(\vdash \varphi \rightarrow \psi \), then \(\vdash \psi \).

5.1 Some Theorems
The following theorems provide a syntactic characterization of the concept of prohibition, as well as the interaction between prohibitions and permissions.
Lemma 1
Proof
The following theorems give a flavor of the logical behavior of choices.
Lemma 2
Proof
The proofs of these are straightforward. Below I provide proofs of theorem (29) and (33).
5.2 Soundness
Theorem 3
(Soundness theorem) The axiom system is sound with respect to the semantics, that is, if \(\varSigma \vdash \varphi \), then \(\varSigma \vDash \varphi \).
Proof
It must be shown that each axiom is valid, and that the rules of inference preserve validity. I prove some representative cases below.
Axiom (A14). Let \(M=\langle H,G,V\rangle \) be a deontic action model such that \(M\vDash {\overline{\alpha }}\sqsubseteq \beta \sqcup \delta \). This means that \(\llbracket {\overline{\alpha }}\rrbracket _M=\{V({\overline{\alpha }})\}\subseteq \llbracket \beta \sqcup \delta \rrbracket _M=\llbracket \beta \rrbracket _M\cup \llbracket \delta \rrbracket _M\). Hence, \(\llbracket {\overline{\alpha }}\rrbracket _M\subseteq \llbracket \beta \rrbracket _M\) or \(\llbracket {\overline{\alpha }}\rrbracket _M\subseteq \llbracket \delta \rrbracket _M\). It follows that \(M\vDash {\overline{\alpha }}\sqsubseteq \beta \vee {\overline{\alpha }}\sqsubseteq \delta \).
Axiom (A15). Assume that \(M=\langle H,G,V\rangle \) is a deontic action model where \(M\vDash \alpha \sqsubseteq {\overline{\beta }}\), i.e. \(\llbracket \alpha \rrbracket _M\subseteq \llbracket {\overline{\beta }}\rrbracket _M=\{V({\overline{\beta }})\}\). This is only possible if \(\llbracket \alpha \rrbracket _M=\emptyset \) or every element of \(\llbracket \alpha \rrbracket _M\) is equal to \(V({\overline{\beta }})\). Since the first case is ruled out by definition, it follows that \(\llbracket \alpha \rrbracket _M=\llbracket {\overline{\beta }}\rrbracket _M\), i.e. \(M\vDash \alpha \rightleftharpoons {\overline{\beta }}\).
Axiom (A22). Assume that \(M=\langle H,G,V\rangle \) is a deontic action model where \(M\vDash {\mathbf {P}}(\overline{\overline{\alpha \sqcup \beta }})\), i.e. \(\llbracket \overline{\overline{\alpha \sqcup \beta }}\rrbracket _M\in \mathbf {LEG}\). Since \(\llbracket \overline{\overline{\alpha \sqcup \beta }}\rrbracket _M=\{V(\overline{\overline{\alpha \sqcup \beta }})\}=\{V(\alpha \sqcup \beta )\}\), it holds that there is some \(h\in G\) such that \(h\in V(\alpha \sqcup \beta )=V(\alpha )\cup V(\beta )\). It follows that \(h\in V(\alpha )=V(\overline{{\overline{\alpha }}})\) or \(h\in V(\beta )=V(\overline{{\overline{\beta }}})\). This, in turn, shows that \(\llbracket \overline{{\overline{\alpha }}}\rrbracket _M\in \mathbf {LEG}\) or \(\llbracket \overline{{\overline{\beta }}}\rrbracket _M\in \mathbf {LEG}\), i.e. \(M\vDash {\mathbf {P}}(\overline{{\overline{\alpha }}})\vee {\mathbf {P}}(\overline{{\overline{\beta }}})\). The other direction is similar.\(\square \)
5.3 Disjunctive Negative Translation
The completeness proof utilizes the fact that every term has a certain normal form. First, I will define the disjunctive negative translation of a term \(\alpha \), denoted \(\textsc {Dnt}(\alpha )\). This translation is similar to the one defined by Ciardelli and Roelofsen (2011, p. 69) in the context of inquisitive logic. If X is a set of terms, then \(\bigsqcup X\) is a term that is a disjunction of the terms in X.
Definition 1

\(\textsc {Dnt}(a_i)=\overline{\overline{a_i}}\), for \(a_i\in Act _0\).

\(\textsc {Dnt}(\mathbf {1})=\overline{{\overline{\mathbf {1}}}}\).

\(\textsc {Dnt}(\mathbf {0})=\overline{{\overline{\mathbf {0}}}}\).

\(\textsc {Dnt}(\alpha \sqcup \beta )=\textsc {Dnt}(\alpha )\sqcup \textsc {Dnt}(\beta )\).
 \(\textsc {Dnt}(\alpha \sqcap \beta )=\bigsqcup \{\overline{\alpha _i\sqcup \beta _j}\,{:}\,1\le i\le k, 1\le j\le l\}\), where

\(\textsc {Dnt}(\alpha )=\overline{\alpha _1}\sqcup \cdots \sqcup \overline{\alpha _k}\),

\(\textsc {Dnt}(\beta )=\overline{\beta _1}\sqcup \cdots \sqcup \overline{\beta _l}\).


\(\textsc {Dnt}({\overline{\alpha }})=\overline{\textsc {Dnt}(\alpha )}\).
Say that two terms \(\alpha ,\beta \in Act \) are choiceidentical if \(\llbracket \alpha \rrbracket _M=\llbracket \beta \rrbracket _M\) is true for any model M.
Theorem 4
For any \(\alpha \in Act \), \(\alpha \) is choiceidentical to \(\textsc {Dnt}(\alpha )\).
Proof

\(\alpha =\alpha '\sqcup \alpha ''\). By the induction hypothesis, \(\llbracket \alpha '\rrbracket _M=\llbracket \textsc {Dnt}(\alpha ')\rrbracket _M\) and \(\llbracket \alpha ''\rrbracket _M=\llbracket \textsc {Dnt}(\alpha '')\rrbracket _M\). It follows by the definition of choice sets that \(\llbracket \alpha '\sqcup \alpha ''\rrbracket _M=\llbracket \alpha '\rrbracket _M\cup \llbracket \alpha ''\rrbracket _M=\llbracket \textsc {Dnt}(\alpha ')\rrbracket _M\cup \llbracket \textsc {Dnt}(\alpha '')\rrbracket _M=\llbracket \textsc {Dnt}(\alpha '\sqcup \alpha '')\rrbracket _M\).

\(\alpha =\alpha '\sqcap \alpha ''\). It holds that \(\llbracket \alpha '\sqcap \alpha ''\rrbracket _M=\{V(\gamma )\cap V(\delta )\,{:}\,V(\gamma )\in \llbracket \alpha '\rrbracket _M, V(\delta )\in \llbracket \alpha ''\rrbracket _M\}\). Assuming that \(\textsc {Dnt}(\alpha ')=\overline{\alpha '_1}\sqcup \cdots \sqcup \overline{\alpha '_k}\) and \(\textsc {Dnt}(\alpha '')=\overline{\alpha ''_1}\sqcup \cdots \sqcup \overline{\alpha ''_l}\), it follows by the induction hypothesis that \(\llbracket \alpha '\sqcap \alpha ''\rrbracket _M=\{V(\overline{\alpha '_i})\cap V(\overline{\alpha ''_j})\,{:}\,V(\overline{\alpha '_i})\in \llbracket \textsc {Dnt}(\alpha ')\rrbracket _M\,\text {and}\, V(\overline{\alpha ''_j})\in \llbracket \textsc {Dnt}(\alpha '')\rrbracket _M\}=\{V(\overline{\alpha '_i\sqcup \alpha ''_j})\,{:}\,1\le i\le k, 1\le j\le l\}=\llbracket \textsc {Dnt}(\alpha '\sqcap \alpha '')\rrbracket _M\).

\(\alpha =\overline{\alpha '}\). It holds that \(\llbracket \overline{\alpha '}\rrbracket _M=\{V(\overline{\alpha '})\}\) by definition. By the induction hypothesis, \(\llbracket \alpha '\rrbracket _M=\llbracket \textsc {Dnt}(\alpha ')\rrbracket _M\), so by Theorem 2, \(V(\alpha ')=V(\textsc {Dnt}(\alpha '))\). It follows that \(\llbracket \overline{\alpha '}\rrbracket _M=\{V(\overline{\alpha '})\}=\{H{\setminus } V(\alpha ')\}=\{H{\setminus } V(\textsc {Dnt}(\alpha '))\}=\{V(\overline{\textsc {Dnt}(\alpha ')})\}=\llbracket \overline{\textsc {Dnt}(\alpha ')}\rrbracket _M\).
The mapping \(\textsc {Dnt}\) always results in a term which is a disjunction of negations. Using Theorem 4, every choice set can be expressed in a standardized way. For any term \(\alpha \in Act \) and any model \(\langle H,G,V\rangle \), it holds that \(\llbracket \alpha \rrbracket _M=\llbracket \textsc {Dnt}(\alpha )\rrbracket _M=\llbracket \overline{\alpha _1}\rrbracket _M\cup \cdots \cup \llbracket \overline{\alpha _k}\rrbracket _M=\{V(\overline{\alpha _i}){:}\,1\le i\le k\}\), where \(\textsc {Dnt}(\alpha )=\overline{\alpha _1}\sqcup \cdots \sqcup \overline{\alpha _k}\).
Two terms \(\alpha \) and \(\beta \) are said to be provably choiceidentical, denoted \(\alpha \dashv \vdash \beta \), if \(\vdash \alpha \rightleftharpoons \beta \). It is shown that any term is provably choiceidentical to its disjunctive negative translation.
Theorem 5
For any \(\alpha \in Act \), \(\alpha \) is provably choiceidentical to \(\textsc {Dnt}(\alpha )\).
Proof

\(\alpha =\alpha '\sqcup \alpha ''\). By the induction hypothesis, \(\alpha '\dashv \vdash \textsc {Dnt}(\alpha ')\) and \(\alpha ''\dashv \vdash \textsc {Dnt}(\alpha '')\). Now, starting from \(\alpha '\sqcup \alpha ''\dashv \vdash \alpha '\sqcup \alpha ''\), axiom (A19) implies that \(\alpha '\sqcup \alpha ''\dashv \vdash \textsc {Dnt}(\alpha ')\sqcup \textsc {Dnt}(\alpha '')\); since \(\textsc {Dnt}(\alpha ')\sqcup \textsc {Dnt}(\alpha '')=\textsc {Dnt}(\alpha '\sqcup \alpha '')\), it holds that \(\alpha '\sqcup \alpha ''\dashv \vdash \textsc {Dnt}(\alpha '\sqcup \alpha '')\).

\(\alpha =\alpha '\sqcap \alpha ''\). By the induction hypothesis, \(\alpha '\dashv \vdash \textsc {Dnt}(\alpha ')\) and \(\alpha ''\dashv \vdash \textsc {Dnt}(\alpha '')\). Starting from \(\alpha '\sqcap \alpha ''\dashv \vdash \alpha '\sqcap \alpha ''\), it follows by axiom (A19) that \(\alpha '\sqcap \alpha ''\dashv \vdash \textsc {Dnt}(\alpha ')\sqcap \textsc {Dnt}(\alpha '')\). Assuming that \(\textsc {Dnt}(\alpha ')=\overline{\alpha '_1}\sqcup \cdots \sqcup \overline{\alpha '_k}\) and \(\textsc {Dnt}(\alpha '')=\overline{\alpha ''_1}\sqcup \cdots \sqcup \overline{\alpha ''_l}\), axiom (A9) implies that \(\alpha '\sqcap \alpha ''\dashv \vdash \bigsqcup \{\overline{\alpha '_i}\sqcap \overline{\alpha ''_j}:1\le i\le k, 1\le j\le l\}\). By axiom A10, \(\overline{\alpha '_i}\sqcap \overline{\alpha ''_j}\dashv \vdash \overline{\alpha '_i\sqcup \alpha ''_j}\) for \(1\le i\le k, 1\le j\le l\). By axiom (A19), it follows that \(\alpha '\sqcap \alpha ''\dashv \vdash \textsc {Dnt}(\alpha '\sqcap \alpha '')\).

\(\alpha =\overline{\alpha '}\). By the induction hypothesis, \(\alpha '\dashv \vdash \textsc {Dnt}(\alpha ')\). From \(\overline{\alpha '}\dashv \vdash \overline{\alpha '}\), axiom (A19) implies that \(\overline{\alpha '}\dashv \vdash \overline{\textsc {Dnt}(\alpha ')}\), i.e. \(\overline{\alpha '}\dashv \vdash \textsc {Dnt}(\overline{\alpha '})\).
5.4 Completeness
The completeness proof follows the same structure as the corresponding proofs given by Castro and Maibaum (2009) and Trypuz and Kulicki (2009). Completeness is proved by proving the equivalent result that each consistent set of formulas has a model.
Definition 2

\(H^\varPhi =\{[\gamma ]_{\doteq }\,{:}\,\gamma \text { is an atom of } Act \}\);

\(V^\varPhi (a_i)=\{[\gamma ]_{\doteq }\in H^\varPhi \,{:}\,\gamma \le a_i\in \varPhi \}\);

\(G^\varPhi =H^\varPhi {\setminus } \bigcup \{V^\varPhi (\alpha )\,{:}\,{\mathbf {F}}(\alpha )\in \varPhi \}\).
The following two lemmas are proved along the same lines as done by Castro and Maibaum (2009, p. 448) (the proofs are stated here for completeness of presentation).
Lemma 3
For any atom \(\gamma \) of \( Act \), \(\gamma \le \alpha \in \varPhi \) if and only if \([\gamma ]_{\doteq }\in V^\varPhi (\alpha )\).
Proof

\(\alpha =\alpha '\sqcup \alpha ''\). Suppose that \([\gamma ]_{\doteq }\in V^\varPhi (\alpha '\sqcup \alpha '')=V^\varPhi (\alpha ')\cup V^\varPhi (\alpha '')\). By the induction hypothesis, \(\gamma \le \alpha '\in \varPhi \) or \(\gamma \le \alpha ''\in \varPhi \). By properties of Boolean algebra, it follows that \(\gamma \le \alpha '\sqcup \alpha ''\in \varPhi \). Suppose that \(\gamma \le \alpha '\sqcup \alpha ''\in \varPhi \). By properties of Boolean algebra, it follows that \(\gamma \le \alpha '\in \varPhi \) or \(\gamma \le \alpha ''\in \varPhi \). By induction hypothesis, it holds that \([\gamma ]_{\doteq }\in V^\varPhi (\alpha ')\) or \([\gamma ]_{\doteq }\in V^\varPhi (\alpha '')\), i.e. \([\gamma ]_{\doteq }\in V^\varPhi (\alpha ')\cup V^\varPhi (\alpha '')=V^\varPhi (\alpha '\sqcup \alpha '')\).

\(\alpha =\alpha '\sqcap \alpha ''\). Similar to the first case.

\(\alpha =\overline{\alpha '}\). Suppose that \([\gamma ]_{\doteq }\in V^\varPhi (\overline{\alpha '})\). Then \([\gamma ]_{\doteq }\not \in V^\varPhi (\alpha ')\), so by the induction hypothesis, \(\gamma \le \alpha '\not \in \varPhi \). Since \(\gamma \) is an atom, properties of Boolean algebra imply that \(\gamma \le \overline{\alpha '}\in \varPhi \). Suppose that \(\gamma \le \overline{\alpha '}\in \varPhi \). By properties of Boolean algebra, it follows that \(\gamma \le \alpha '\not \in \varPhi \), so by the induction hypothesis, \([\gamma ]_{\doteq }\not \in V^\varPhi (\alpha ')\), i.e. \([\gamma ]_{\doteq }\in V^\varPhi (\overline{\alpha '})\). \(\square \)
Lemma 4
\(\alpha \doteq \beta \in \varPhi \) if and only if \(V^\varPhi (\alpha )=V^\varPhi (\beta )\).
Proof
(\(\Rightarrow \)) Assume that \(\alpha \doteq \beta \in \varPhi \). It follows that \(\alpha \le \beta \in \varPhi \). This, in turn, means that for every atom \(\gamma \), if \(\gamma \le \alpha \in \varPhi \), then \(\gamma \le \beta \in \varPhi \). By Lemma 3, it follows that \(V^\varPhi (\alpha )\subseteq V^\varPhi (\beta )\). \(V^\varPhi (\beta )\subseteq V^\varPhi (\alpha )\) is proved analogously. Hence, \(V^\varPhi (\alpha )=V^\varPhi (\beta )\).
(\(\Leftarrow \)) Assume that \(V^\varPhi (\alpha )=V^\varPhi (\beta )\). If \(V^\varPhi (\alpha )=V^\varPhi (\beta )=\emptyset \), then there is no atom \(\gamma \) such that \(\gamma \le \alpha \in \varPhi \) or \(\gamma \le \beta \in \varPhi \). This means that \(\alpha \doteq \mathbf {0}\in \varPhi \) and \(\beta \doteq \mathbf {0}\in \varPhi \), from which it follows that \(\alpha \doteq \beta \in \varPhi \). For \(V^\varPhi (\alpha )=V^\varPhi (\beta )\ne \emptyset \), let \(\chi \) be the sum of all atoms \(\gamma \) for which \([\gamma ]_{\doteq }\in V^\varPhi (\alpha )=V^\varPhi (\beta )\). Then, by Lemma 3 and properties of Boolean algebra, \(\chi \doteq \alpha \in \varPhi \) and \(\chi \doteq \beta \in \varPhi \); hence, \(\alpha \doteq \beta \in \varPhi \). \(\square \)
The two lemmas above show that the interpretation function \(V^\varPhi \) has the right behavior, and so:
Lemma 5
\(M^\varPhi =\langle H^\varPhi , G^\varPhi , V^\varPhi \rangle \) is a deontic action model.
Proof
First, note that \(G^\varPhi \subseteq H^\varPhi \). It is shown that \(G^\varPhi \) is nonempty. Suppose that there are n atoms of \( Act \). Suppose, for a proof by contradiction, that for every atom \(\gamma _i\), \(1\le i\le n\), it holds that \([\gamma _i]_{\doteq }\in \bigcup \{V^\varPhi (\alpha )\,{:}\,{\mathbf {F}}(\alpha )\in \varPhi \}\). This implies that \({\mathbf {F}}(\gamma _i)\in \varPhi \), \(1\le i\le n\) by (27). By (21), it follows that \({\mathbf {F}}(\gamma _1\sqcup \cdots \sqcup \gamma _n)\in \varPhi \). But \(\gamma _1\sqcup \cdots \sqcup \gamma _n\doteq \mathbf {1}\in \varPhi \), so \({\mathbf {F}}(\mathbf {1})\in \varPhi \) by (26). This is, however, a contradiction since it holds that \(\lnot {\mathbf {F}}(\mathbf {1})\in \varPhi \) by (23). \(\square \)
Using these results, the completeness proofs by Castro and Maibaum (2009) and Trypuz and Kulicki (2009) can be extended to cover identity of choice sets and deontic operators. First, I will state a number of useful lemmas.
Lemma 6
\({\overline{\alpha }}\rightleftharpoons {\overline{\beta }}\in \varPhi \) if and only if \(\llbracket {\overline{\alpha }}\rrbracket _{M^\varPhi }=\llbracket {\overline{\beta }}\rrbracket _{M^\varPhi }\).
Proof
(\(\Rightarrow \)) Assume that \({\overline{\alpha }}\rightleftharpoons {\overline{\beta }}\in \varPhi \). By (35), \({\overline{\alpha }}\doteq {\overline{\beta }}\in \varPhi \) holds. By Lemma 4, it holds that \(V^\varPhi ({\overline{\alpha }})=V^\varPhi ({\overline{\beta }})\), and so \(\llbracket {\overline{\alpha }}\rrbracket _{M^\varPhi }=\llbracket {\overline{\beta }}\rrbracket _{M^\varPhi }\) by the definition of choice sets.
(\(\Leftarrow \)) Assume that \(\llbracket {\overline{\alpha }}\rrbracket _{M^\varPhi }=\llbracket {\overline{\beta }}\rrbracket _{M^\varPhi }\). It follows that \(V^\varPhi ({\overline{\alpha }})=V^\varPhi ({\overline{\beta }})\), from which it follows by Lemma 4 that \({\overline{\alpha }}\doteq {\overline{\beta }}\in \varPhi \). By (35), \({\overline{\alpha }}\rightleftharpoons {\overline{\beta }}\in \varPhi \). \(\square \)
Lemma 7
For all \(\textsc {Dnt}(\alpha )\in Act \) and all \(V^\varPhi ({\overline{\beta }})\in \llbracket \textsc {Dnt}(\alpha )\rrbracket _{M^\varPhi }\), it holds that \({\overline{\beta }}\sqsubseteq \textsc {Dnt}(\alpha )\in \varPhi \).
Proof
The proof is by induction over \(\textsc {Dnt}(\alpha )\). For the induction base, note that for \(\textsc {Dnt}(\alpha )=\overline{\alpha '}\), it holds that \(\llbracket \overline{\alpha '}\rrbracket _{M^\varPhi }=\{V^\varPhi (\overline{\alpha '})\}\). By axiom (A6), it holds that \(\overline{\alpha '}\sqsubseteq \overline{\alpha '}\in \varPhi \), so the claim in the lemma holds.
For the induction step, assume that the statement holds true for \(\textsc {Dnt}(\alpha '), \textsc {Dnt}(\alpha '')\). Consider the term \(\textsc {Dnt}(\alpha )=\textsc {Dnt}(\alpha ')\sqcup \textsc {Dnt}(\alpha '')\). Assume that \(V^\varPhi ({\overline{\beta }})\in \llbracket \textsc {Dnt}(\alpha ')\sqcup \textsc {Dnt}(\alpha '')\rrbracket _{M^\varPhi }\). It follows by definition that \(V^\varPhi ({\overline{\beta }})\in \llbracket \textsc {Dnt}(\alpha ')\rrbracket _{M^\varPhi }\cup \llbracket \textsc {Dnt}(\alpha '')\rrbracket _{M^\varPhi }\), and so by the induction hypothesis, \({\overline{\beta }}\sqsubseteq \textsc {Dnt}(\alpha ')\in \varPhi \) or \({\overline{\beta }}\sqsubseteq \textsc {Dnt}(\alpha '')\in \varPhi \). By (3031), therefore, \({\overline{\beta }}\sqsubseteq \textsc {Dnt}(\alpha ')\sqcup \textsc {Dnt}(\alpha '')\in \varPhi \), i.e. \({\overline{\beta }}\sqsubseteq \textsc {Dnt}(\alpha )\in \varPhi \). \(\square \)
Lemma 8
\(\alpha \rightleftharpoons \beta \in \varPhi \) if and only if \(\llbracket \alpha \rrbracket _{M^\varPhi }=\llbracket \beta \rrbracket _{M^\varPhi }\).
Proof
(\(\Rightarrow \)) Assume that \(\alpha \rightleftharpoons \beta \in \varPhi \). By Theorem 5, \(\alpha \rightleftharpoons \textsc {Dnt}(\alpha )\in \varPhi \) and \(\beta \rightleftharpoons \textsc {Dnt}(\beta )\in \varPhi \), and so \(\textsc {Dnt}(\alpha )\rightleftharpoons \textsc {Dnt}(\beta )\in \varPhi \). Assuming that \(\textsc {Dnt}(\alpha )=\overline{\alpha _1}\sqcup \cdots \sqcup \overline{\alpha _k}\) and \(\textsc {Dnt}(\beta )=\overline{\beta _1}\sqcup \cdots \sqcup \overline{\beta _l}\), it holds by (29) that \(\overline{\alpha _i}\sqsubseteq \textsc {Dnt}(\alpha )\in \varPhi \), for \(1\le i\le k\). By the initial assumption and axiom (A19), it holds that \(\overline{\alpha _i}\sqsubseteq \textsc {Dnt}(\beta )\in \varPhi \) for each \(\overline{\alpha _i}\) occurring in \(\textsc {Dnt}(\alpha )\), \(1\le i\le k\). By axioms (A14) and (A15), it follows that for each \(\overline{\alpha _i}\) occurring in \(\textsc {Dnt}(\alpha )\), \(1\le i\le k\), there is some \(\overline{\beta _j}\) occurring in \(\textsc {Dnt}(\beta )\), \(1\le j\le l\), such that \(\overline{\alpha _i}\rightleftharpoons \overline{\beta _j}\in \varPhi \). By Lemma 6, it follows that \(\llbracket \textsc {Dnt}(\alpha )\rrbracket _{M^\varPhi }\subseteq \llbracket \textsc {Dnt}(\beta )\rrbracket _{M^\varPhi }\). By the same reasoning, it is shown that \(\llbracket \textsc {Dnt}(\beta )\rrbracket _{M^\varPhi }\subseteq \llbracket \textsc {Dnt}(\alpha )\rrbracket _{M^\varPhi }\). This together with Theorem 4 implies that \(\llbracket \alpha \rrbracket _{M^\varPhi }=\llbracket \textsc {Dnt}(\alpha )\rrbracket _{M^\varPhi }=\llbracket \textsc {Dnt}(\beta )\rrbracket _{M^\varPhi }=\llbracket \beta \rrbracket _{M^\varPhi }\).
(\(\Leftarrow \)) Assume that \(\llbracket \alpha \rrbracket _{M^\varPhi }=\llbracket \beta \rrbracket _{M^\varPhi }\). By Theorem 4, \(\llbracket \alpha \rrbracket _{M^\varPhi }=\llbracket \textsc {Dnt}(\alpha )\rrbracket _{M^\varPhi }\) and \(\llbracket \beta \rrbracket _{M^\varPhi }=\llbracket \textsc {Dnt}({\beta })\rrbracket _{M^\varPhi }\). Assuming that \(\textsc {Dnt}(\alpha )=\overline{\alpha _1}\sqcup \cdots \sqcup \overline{\alpha _k}\) and \(\textsc {Dnt}(\beta )=\overline{\beta _1}\sqcup \cdots \sqcup \overline{\beta _l}\), Lemma 7 implies that for each \(V^\varPhi (\overline{\beta _i})\in \llbracket \textsc {Dnt}(\beta )\rrbracket _{M^\varPhi }=\llbracket \textsc {Dnt}(\alpha )\rrbracket _{M^\varPhi }\), \(1\le i\le l\), it holds that \(\overline{\beta _i}\sqsubseteq \textsc {Dnt}(\alpha )\in \varPhi \). It follows that \(\textsc {Dnt}(\beta )\sqsubseteq \textsc {Dnt}(\alpha )\in \varPhi \) by (32). By the same reasoning, it holds that \(\textsc {Dnt}(\alpha )\sqsubseteq \textsc {Dnt}(\beta )\in \varPhi \). It follows that \(\textsc {Dnt}(\alpha )\rightleftharpoons \textsc {Dnt}(\beta )\in \varPhi \) by (33). By Theorem 5, \(\alpha \rightleftharpoons \beta \in \varPhi \). \(\square \)
Lemma 9
\({\mathbf {F}}(\alpha )\in \varPhi \) if and only if \(V^\varPhi (\alpha )\cap G^\varPhi =\emptyset \).
Proof
(\(\Rightarrow \)) Assume that \({\mathbf {F}}(\alpha )\in \varPhi \). It follows that \(V^\varPhi (\alpha )\subseteq \bigcup \{V^\varPhi (\beta ):{\mathbf {F}}(\beta )\in \varPhi \}\), so \(V^\varPhi (\alpha )\cap G^\varPhi =\emptyset \) by the definition of \(G^\varPhi \).
(\(\Leftarrow \)) Assume that \(V^\varPhi (\alpha )\cap G^\varPhi =\emptyset \). This implies that \(V^\varPhi (\alpha )\subseteq \bigcup \{V^\varPhi (\beta ):{\mathbf {F}}(\beta )\in \varPhi \}\) by the definition of \(G^\varPhi \). It follows that for each \([\gamma ]_{\doteq }\in V^\varPhi (\alpha )\), there is some \(\beta \) such that \([\gamma ]_{\doteq }\in V^\varPhi (\beta )\) and \({\mathbf {F}}(\beta )\in \varPhi \). Therefore by Lemma 3, \(\gamma \le \beta \in \varPhi \) holds. By (27), it can be inferred that \({\mathbf {F}}(\gamma )\in \varPhi \). Let \(\chi \) be the disjunction of all \(\gamma \) for which \([\gamma ]_{\doteq }\in V^\varPhi (\alpha )\). It then holds that \(\chi \doteq \alpha \in \varPhi \). By (21), it follows that \({\mathbf {F}}(\chi )\in \varPhi \), and hence \({\mathbf {F}}(\alpha )\in \varPhi \) by (26). \(\square \)
Lemma 10
\({\mathbf {P}}(\alpha )\in \varPhi \) if and only if \(\llbracket \alpha \rrbracket _{M^\varPhi }\in \mathbf {LEG}^\varPhi \).
Proof
Lemma 11
(Truth lemma) \(\varphi \in \varPhi \) if and only if \(M^\varPhi \vDash \varphi \).
Proof
The proof is inductive. For the PL operators, the proof is standard. All the remaining cases follow from Lemmas 4, 8, and 10.\(\square \)
Lemma 11 shows that the canonical model has the desired behavior, and completeness is then proved by a routine argument.
Theorem 6
(Completeness theorem) For each consistent set \(\varSigma \) of formulas of DACL, there is a model which satisfies it.
Proof
If \(\varSigma \) is consistent, then there exists a maximally consistent set \(\varSigma '\) which is an extension of \(\varSigma \). By the definition of the canonical model and Lemma 11, it follows that \(M^{\varSigma '}\vDash \varSigma \), so \(\varSigma \) has a model which satisfies it. This concludes the proof. \(\square \)
6 Discussion
In this section, I will discuss some aspects of the approach in this paper that deserve further attention. First, I will briefly compare choice sets with the interpretation of propositions in inquisitive semantics. Second follows a discussion of the algebraic properties of choice sets, and finally, I will make a comparison with the conceptually similar Action Type Deontic Logic of Bentzen (2014).
6.1 Alternativeness in Inquisitive Semantics
It should be stressed that arbitrary sets of action types count as choice sets under the present action theory. One may reasonably think that the notion of a choice set should be much more restricted. For example, a standard assumption in decision theoretic settings is that alternative actions are mutually exclusive.
In the literature on inquisitive semantics (Ciardelli and Roelofsen 2011; Ciardelli et al. 2009; Groenendijk and Roelofsen 2009; Roelofsen 2013), propositions are interpreted as sets of possibilities, where possibilities, in turn, are sets of possible worlds. Weak forms of inquisitive semantics (for example the system \(\textsf {Inq}\emptyset \); Ciardelli et al. 2009) do not put any restrictions on propositions (conceived of as sets of possibilities), and the resulting semantics comes very close to how choice sets are characterized in this paper. In stronger forms of inquisitive semantics (for example the system \(\textsf {InqB}\); Ciardelli and Roelofsen 2011), two possibilities are said to be alternatives if neither of them is a proper subset of the other. In a similar spirit, why not restrict the notion of choice set so as they contain alternative (in the sense used above for possibilities) action types only? In the present action theoretic context, a restricted version of the concept of a choice set may be defined as follows: a choice set S is restricted if for all \(s\in S\), there is no \(s'\in S\) such that \(s\subset s'\). In other words, the interpretation of terms as restricted choice sets is obtained by applying the operator \(\textsc {Alt}\), defined in Sect. 3.2.3, to the unrestricted choice sets of terms of any form, not only those of the form \({\overline{\alpha }}\).
The reason for not making this move is the use of Simons’ supercover semantics. By using supercover semantics for permission and obligation in terms of the sets \(\mathbf {LEG}\) and \(\mathbf {REQ}\), information will be lost by moving to restricted choice sets. For example, if \(S=\{s\}\), \(T=\{t\}\) and \(t\subset s\), it follows that \(\textsc {Alt}(S\cup T)=\{s\}\). If \(s\cap G\ne \emptyset \) and \(t\cap G=\emptyset \), it follows that \(\textsc {Alt}(S\cup T)\in \mathbf {LEG}\), even though \(\textsc {Alt}T\not \in \mathbf {LEG}\). In order to keep the free choice principle, there is a point in allowing a more liberal definition of choice sets, even though this makes the algebraic properties of choice sets more complex.^{7}
6.2 Algebraic Considerations
The behavior of choices in DACL deviates from the Boolean interpretation of actions. Indeed, the algebraic structure defined on choice sets does not even form a lattice, since absorption is missing. On the other hand, a straightforward extension of DACL turns out to have an underlying semiring structure.

\(\langle {\mathscr {P}}({\mathscr {P}}(H)),\cup ,\emptyset \rangle \) is a joinsemilattice;

\(\langle {\mathscr {P}}({\mathscr {P}}(H)),\otimes ,\{H\}\rangle \) is a commutative monoid;

\(\otimes \) distributes over \(\cup \) and \(\emptyset \) is an annihilator for \(\otimes \);

\(\langle B,\otimes ,{\sim },\{\emptyset \},\{H\}\rangle \) is a Boolean algebra, where B is the set of singleton choice sets;

\({\sim }\) is an operation mapping every choice set to the set containing the complement of its union.
6.3 Bentzen’s Action Type Deontic Logic
A deontic action logic that is conceptually related to the present approach is presented by Bentzen (2014). Bentzen uses a distinction between action expressions (terms) and propositional statements, and introduces a kind of distribution requirement in the interpretation of disjunctive action expressions. The semantics is intended to solve many of the problems with the standard approach to deontic logic.
In order to account for the special interaction between deontic operators and disjunction, Bentzen introduces a disjunctive term operator which is interpreted so as to be nonempty: the action type denoted by the disjunctive term \((\alpha \,\text {or}\, \beta )\) is instantiated by an action token h if and only if h instantiates the action type denoted by \(\alpha \) or h instantiates the action type denoted by \(\beta \) and there are action tokens instantiating the action type denoted by \(\alpha \) and action tokens instantiating the action type denoted by \(\beta \).^{9} Bentzen interprets this nonemptiness condition as a “a criterion of relevance or availability” (2014, p. 405).
In the semantics presented in this paper, the possibility of agents having illegal action tokens available is included. Whether it is possible to extend Bentzen’s semantics in order to account for normviolations is a question that will be left open here: suffice it to note that the approach in the present paper represents an alternative formal implementation of the ideas underlying Bentzen’s semantics....the normative dimension ceases to be of interest: the actual does not depart from the ideal, so nothing is lost by merely describing what agents in fact do. (Carmo and Jones 2002, p. 265)
7 Conclusion
I have presented an approach to deontic action logic where action expressions have two kinds of formal interpretations: as action types, and as choice sets. This distinction is then utilized when interpreting deontic concepts. A formal deontic logic based on the logics of Trypuz and Kulicki (2009, 2015) was developed. In this logic, permissions are sensitive to the choice meaning of action expressions, and substitution of logical equivalents within the scope of the permission operator is not in general a valid rule of inference. The main result is the completeness of an axiomatization of the logic.
The logic is intended to capture properties of informal deontic reasoning, and in particular provide ways to handle the various problems related to the interaction of permission and disjunction. The present approach is conceptually similar to Bentzen’s Action Type Deontic Logic (2014), but the formal implementation is different. Unlike Bentzen’s approach, it allows for the modeling of nonideal actions. This opens up possibilities for modeling normviolations, for example contrarytoduty obligations (Carmo and Jones 2002). This is an interesting topic for further research.
There are additional requirements one may put on choice sets. For example, the notion of alternative could be made more restrictive as done in inquisitive semantics and in decision theory in general. What kind of logic such different restrictions give rise to is a topic for further research. In the approach taken here, the interpretation of actionnegation essentially collapses the choice sets of negated terms into singleton choice sets. This makes it possible to utilize the disjunctive negative translation in the completeness proof. On the other hand, one might think that this interpretation lacks sufficient philosophical motivation.
At present, the logic is quite limited in its scope. It cannot be used to talk about performances and consequence of actions and choices. It would be interesting to consider the approach developed here in a dynamic setting (see e.g. Castro and Maibaum 2009; Meyer 1988), thus arriving at a considerably more expressive theory. Neither are there any resources for reasoning about sequential composition of actions, and I did not consider contrarytoduty normative reasoning. These are all topics for further inquiry.
Finally, the algebraic foundations of DACL deserve closer attention. I argued in Sect. 6.2 that a straightforward extension gives rise to a special kind of semiring structure. Because of the close connection with inquisitive semantics, research in this direction may provide results not only on the algebraic properties of choice sets, but also regarding the algebraic foundations of versions of inquisitive semantics with nonmaximal possibilities.
Footnotes
 1.
The term ‘supercover semantics’ is used by Humberstone (2011, p. 811), but not, as far as I am aware, by Simons herself.
 2.
I have omitted any references to specific models.
 3.
The deontic status of action types and choice sets is thus reduced to the claim that certain action tokens are legal or not. I leave the legalness of action tokens as a primitive notion here. This notion could, for example, be analyzed in terms of sanctions or violations as done in some variants of dynamic deontic logic, e.g. Broersen (2004), Dignum et al. (1996) and Meyer (1988).
 4.
This set must be distinguished from the set \( Leg \) defined by Segerberg (1982), which corresponds to the set denoted by G here.
 5.
I will sometimes leave out the subscript M when there is no risk of misunderstandings.
 6.
A different way of characterising the difference between strong and weak permission is to say that an action is strongly permitted if no way of executing it leads to a violation state; a weakly permitted action is such that at least some way of executing it does not lead to a violation state (Broersen 2004; Dignum et al. 1996).
 7.
Propositions in inquisitive semantics defined in terms of alternative possibilities (in the sense used above) form a Heyting algebra (Roelofsen 2013).
 8.
Note that \({\mathbf {f}}\) must be introduced as a designated term in order to keep functional completeness: no combination of terms of the original DACL language has the empty set as its choice set interpretation.
 9.
Bentzen uses symbols \(S, T, \ldots \) as variables ranging over terms, and lower case Greek letters as ranging over action tokens. To avoid confusion, I have changed Bentzen’s notation here.
 10.
I have omitted the interpretation function for propositional constants originally used by Bentzen.
Notes
Acknowledgements
I wish to thank Valentin Goranko, Magnus Hjelmblom and Piotr Kulicki for helpful discussions and comments on earlier drafts of this work, and the three anonymous reviewers for their helpful suggestions. Parts of this work were carried out while I was affiliated with the Decision, Risk, and Policy Analysis group at the Faculty of Engineering and Sustainable Development, University of Gävle, Sweden.
References
 Alchourrón, C. E., & Bulygin, E. (1971). Normative systems. New York: Springer.CrossRefGoogle Scholar
 AlonsoOvalle, L. (2006). Disjunction in alternative semantics. Ph.D. Dissertation, University of Massachusetts Amherst.Google Scholar
 Anglberger, A. J. J., Dong, H., & Roy, O. (2014). Open reading without free choice. In F. Cariani, D. Grossi, J. Meheus, & X. Parent (Eds.), Deontic logic and normative systems (pp. 19–32). Heidelberg: Springer.Google Scholar
 Asher, N., & Bonevac, D. (2005). Free choice permission is strong permission. Synthese, 145(3), 303–323.CrossRefGoogle Scholar
 Bentzen, M. M. (2014). Action type deontic logic. Journal of Logic, Language and Information, 23(4), 397–414.CrossRefGoogle Scholar
 Broersen, J. (2004). Action negation and alternative reductions for dynamic deontic logics. Journal of Applied Logic, 2, 153–168.CrossRefGoogle Scholar
 Carmo, J., & Jones, A. J. I. (2002). Deontic logic and contrarytoduties. In D. M. Gabbay & F. Guenthner (Eds.), Handbook of philosophical logic (Vol. 8, pp. 265–343). Dordrecht: Kluwer.CrossRefGoogle Scholar
 Castro, P. F., & Maibaum, T. S. E. (2009). Deontic action logic, atomic Boolean algebras and faulttolerance. Journal of Applied Logic, 7(4), 441–466.CrossRefGoogle Scholar
 Chellas, B. F. (1980). Modal logic: An introduction. Cambridge: Cambridge University Press.CrossRefGoogle Scholar
 Ciardelli, I., Groenendijk, J., & Roelofsen, F. (2009). Attention! might in inquisitive semantics. In S. Ito & E. Cormany (Eds.), Proceedings of semantics and linguistic theory (Vol. XIX, pp. 91–108). Ithaca: Cornell University, CLC Publications.Google Scholar
 Ciardelli, I., & Roelofsen, F. (2011). Inquisitive logic. Journal of Philosophical Logic, 40(1), 55–94.CrossRefGoogle Scholar
 Davey, B., & Priestley, H. (2002). Introduction to lattices and order. Cambridge: Cambridge University Press.CrossRefGoogle Scholar
 Dignum, F., Meyer, J.J. C., & Wierenga, R. J. (1996). Free choice and contextually permitted actions. Studia Logica, 57, 193–220.CrossRefGoogle Scholar
 Giordani, A., & Canavotto, I. (2016). Basic action deontic logic. In O. Roy, A. Tamminga, & M. Willer (Eds.), Deontic logic and normative systems (pp. 80–92). London: College Publications.Google Scholar
 Girard, J.Y. (1987). Linear logic. Theoretical Computer Science, 50(1), 1–101.CrossRefGoogle Scholar
 Groenendijk, J., & Roelofsen, F. (2009). Inquisitive semantics and pragmatics. In J. M. Larrazabal & L. Zubeldia (Eds.), Meaning, content, and argument: Proceedings of the ILCLI international workshop on semantics, pragmatics, and rhetoric (pp. 41–72). San Sebastián: University of the Basque Country Publication Service.Google Scholar
 Hansson, S. O. (2013). The varieties of permission. In D. Gabbay, J. Horty, X. Parent, R. van der Meyden, & L. van der Torre (Eds.), Handbook of deontic logic and normative systems (pp. 195–240). London: College Publications.Google Scholar
 Hilpinen, R. (1982). Disjunctive permissions and conditionals with disjunctive antecedents. Acta Philosophica Fennica, 35, 175–194.Google Scholar
 Humberstone, L. (2011). The connectives. Cambridge, MA: MIT Press.CrossRefGoogle Scholar
 Ju, F., & van Eijck, J. (2016). To do something else. In O. Roy, A. Tamminga, & M. Willer (Eds.), Deontic logic and normative systems (pp. 109–122). London: College Publications.Google Scholar
 Kamp, H. (1973). Free choice permission. Proceedings of the Aristotelian Society, 74, 57–74.CrossRefGoogle Scholar
 Meyer, JJ Ch. (1988). A different approach to deontic logic: Deontic logic viewed as a variant of dynamic logic. Notre Dame Journal of Formal Logic, 29(1), 109–136.CrossRefGoogle Scholar
 Monk, J. D. (1976). Mathematical logic. New York: Springer.CrossRefGoogle Scholar
 Pelletier, F. J., & Asher, N. (1997). Generics and defaults. In J. van Benthem & A. G. B. ter Meulen (Eds.), Handbook of logic and language (pp. 1125–1177). Amsterdam: Elsevier.CrossRefGoogle Scholar
 Roelofsen, F. (2013). Algebraic foundations for the semantic treatment of inquisitive content. Synthese, 190, 79–102.CrossRefGoogle Scholar
 Ross, A. (1941). Imperatives and logic. Theoria, 7, 53–71.Google Scholar
 Segerberg, K. (1982). A deontic logic of action. Studia Logica, 41(2–3), 269–282.CrossRefGoogle Scholar
 Simons, M. (2005a). Dividing things up: The semantics of or and the modal/or interaction. Natural Language Semantics, 13(3), 271–316.CrossRefGoogle Scholar
 Simons, M. (2005b). Semantics and pragmatics in the interpretation of or. In E. Georgala & J. Howell (Eds.), Proceedings of semantics and linguistic theory (Vol. XV, pp. 205–222). Ithaca: Cornell University, CLC Publications.Google Scholar
 Trypuz, R., & Kulicki, P. (2009). A systematics of deontic action logics based on Boolean algebra. Logic and Logical Philosophy, 18(3–4), 253–270.Google Scholar
 Trypuz, R., & Kulicki, P. (2015). On deontic action logic based on Boolean algebra. Journal of Logic and Computation, 25(5), 1241–1260.CrossRefGoogle Scholar
 van der Meyden, R. (1996). The dynamic logic of permission. Journal of Logic and Computation, 6(3), 465–479.CrossRefGoogle Scholar
 von Wright, G. H. (1951). Deontic logic. Mind, 60, 1–15.CrossRefGoogle Scholar
Copyright information
OpenAccessThis article is distributed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits unrestricted use, distribution, and reproduction in any medium, provided you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license, and indicate if changes were made.