Permissions and Obligations

PERMISSIONS AND OBLIGATIONS

L. Thorne McCarty Computer Science Department Rutgers University New Brunswick, New Jersey

ABSTRACT: This article describes a formal semantics for the deontic concepts the concepts of perm i ssion and obi igation -- which arises naturally from the representations used in artificial intelligence systems. Instead of treating deontic logic as a branch of modal logic, with the standard possible wor lds semantics. we first develop a language for describing act i ons, and we define the concepts of permission and obligation in terms of these action descriptions. Using our semantic definitions, we then derive a number of intuitively plausible inferences. and we show generally that the paradoxes which are so frequently associated with deontic logic do not arise in our system.*

I INTRODUCTION

The representation of deontic concepts the concepts of permission and obi igation -- has not yet been seriously addressed in the artificial intelligence literature. but there are numerous application areas in which these concepts seem to be required. In our work on the TAX MAN Project [ 1] [2]. for example, we represent the characteristics of various kinds of stocks and bonds by describing the rules of permission and obligation which are binding, at any given time. on the corporation and its securityholders. In our work on the "usufructuary" provisions of the Louisiana Civil Code [3] , just recently init iated, we have encountered a similar need for the representation of complex permissions and obligations. Nor are these examples confined to legal domains. In the classical work on single agent planning systems, e.g., [4]. the operators which change the state of the world can be interpreted as a set of "permitted" actions. but in a more realistic planning environment, with multiple agents, we would expect to see "obligatory" actions as well, and we would expect to see the actions of one agent produce modifications in the rules of permission and obligation binding upon another agent. Similar observations apply to the field of computer security, see. e.g., [5] , where there has been extensive debate over the appropriate "authorization mechanisms" for a community of computer users. For all of these purposes. a formalization of the concepts of . permission and obligation appears to be

essential.

Outside of the field of artificial intelligence. there exists an extensive literature on the deontic concepts, by logicians [6] [7] , philosophers [8] [9] . and lawyers [ 1 0] [ 11] [ 12] . but the attempts to formal ize these concepts have generally led to paradox. Since the 1950's. deontic logic has been treated as a branch of modal logic. w ith the "necessity" operator replaced by the "obl igation" operator. 0 . and the "possibility" operator replaced by the "permission" operator, P. Many of the theorems of modal logic turn out to be intuitively correct under this translation. For example. the dual relationship between necessity and possibility becomes a dual relationship between obligation and permission, Op = -P-p, and this formula certainl y seems plausible. If it is false that you are permitted to do not - p , then you are obligated to do p, and vi ce versa. The formula Op ::> p, which is val id in any modal system with a reflexive accessibility relation between possible worlds, would not be plausible in a deontic logic, since people in the actual world do not always abide by their obligations. but it can be replaced by the more plausible formula Op ::> P p, which is valid as long as every possible world has some possible world accessible from it. This point was first noted by Kripke, in one of his original papers on possible worlds semantics [ 13] .

*This article is based upon work supported by Grant No. MCS-82-03591 from the National Science Foundation, Washington. D.C., and by a grant from the Louisiana State Law Institute, Baton Rouge, Louisiana.

Despite these positive results, there are several other modal formulae which seem counterintuit ive in a deontic logic, and which cannot be so easily modified. For example, the formula for disjunctive permission, Pp ::> P(p v q). contradicts our ordinary understanding of what it means to grant permission to do p v q, but this formula is valid even in the weakest modal systems. Likewise, any formula containing an iterated operator, such as OPp or POp, seems anomalous in a deontic context. and yet the various modal systems are distinguished precisely by the way in which they handle these iterated modal ities. Of course. it may make sense to say that you are permitted to impose a particular obi igation upon someone else. or upon yourself, and we might conceivably write. this as POp, but the inferences we would make about such statements do not correspond at all to the inferences which are valid in the standard possible world semantics. Finally, even the dual relationship between permission and obligation seems problematical if we cast it into the form Pp = -0-p. If it is false that you are obligated to do not-p, i.e., if it is false that you are forbidden to do p, does it follow that p is permitted? Stringing together all of these questionable inferences. it is not surprising that we can generate a host of "deontic paradoxes," and the literature is full of them. For a survey, see [14] and [15].

In this paper, we will develop a formal semantics for permissions and obligations which seems to avoid these difficulties, and we will do so in a way which is entirely natural for an artificial intelligence system. Instead of representing the deontic concepts as operators applied to proposi tions, as in a standard modal logic, we will represent them as dyadic forms which take condition descriptions and action descriptions as their arguments. The most important part of this representation is the use of action descriptions in the place of propositions. Instead of granting permissions and imposing obligations on the state of the world itself , we will grant permissions and impose obligations on the actions which change the state of the world This is an approach long advocated by Castaneda [ 15] , and pursued in various forms by von Wright [ 16] [ 14], but to carry out this approach in full it seems necessary to establish a connection between the abstract description of an action and the concrete changes that occur in the world when the action takes place. This has been a major concern of artificial intelligence research throughout its history [ 17] [ 18] [ 19] , of course, and we will draw upon this earlier work in constructing our formalisms. Although the actions that we actually discuss in this paper are fairly simple ones, intended to highlight the principal features of the deontic representation, the action descriptions themselves can be extended to more realistic situations, in several ways. We will return to this point in our concluding remarks.

II DEONTIC SEMANTICS

In this section we develop a formal semantic interpretation of the deontic concepts, using a variant of the possible worlds approach. Our strategy proceeds in stages: We start with an ordinary first-order language L 1 , and a set of states S, and we use these materials to construct a new language LA in which we are able to describe actions. The formulae of L 1 are evaluated with respect to the states in S, as usual, but the formulae of LA are evaluated with respect to sequences of states, or worlds. We thus have a way of saying that an action is "true" in, or is "satisfied" by, a particular world The details of these constructions are presented in Sections II.A and 11.8 below. Now consider a state r which is situated at the junction between a "past" world v and a "future" world w. We assume that there exists a set P which tells us, for each past world v, all the future ;:,orlds w which are "permitted." Working exclusively with this permitted set Pr' we construct three expressions which tell us whether an action at is permitted, forbidden, or obi igatory, respectively. These expressions then become part of our deontic language L 0 . The details of these constructions are presented in Section II.C below. This is not the end of the story, however. Since each deontic expression has a definite truth value at each state in S, it turns out that the language L 0 can be embedded within our original first­ order language L 1 , and thus the process of linguistic construction we have outlined here becomes fully recursive. This technique enables us to represent "dynamic" permissions and obligations, i.e., permissions and obligations which change over time, without the use of iterated

modalities. This latter point is developed in Section II.D.

The principal technical difficulty in this development

arises in connection with the definition of "satisfaction" for the language LA Our initial approach is similar in spirit to the approach of Hare I [20] and Rosenschein [2 1] : We define a primitive action to be a relation between two states, and we define the meaning of the more complex formulae of LA by a set of recursive truth definitions on arbitrary sequences of states. But the ordinary notion of satisfaction in L 1 , which takes into account the complete state of the world at a given time, is too imprecise for our purposes here, and we will supplement it with a notion o f strict satisfaction, which associates with each action in LA the specific set of changes in the world attributable to that action It turns out that this notion of strict satisfaction is absolutely essential to the construction of the deontic language L 0 . Without it, our definition of a rule o f permission simply would not work. We will return to this point in Section 111.8.

A. State Descriptions

Let L 1 be a many- sorted function-free first-order language with equality, and let S be a set of states with respect to which the formulae of L 1 are evaluated We will follow the standard procedures for specifying the syntax and the semantics · of a first-order language. Thus, if (Own x y) is a formula of L 1 with free variables x and y, and if o is an assignment of the variables x and y to elements in the domain of interpretation of L 1 , and if Own(s) is the set of tuples defining the extension of the predicate Own for s e S, then we will say that "(Own x yl is true in s under the assignment o" if and only if <o(x),o(y)> e Own(s). We will write this in general as o,s "' (Own x y), but if the assignment o is fixed and clear from the context, we will often omit it from the notation and write s "' (Own x y). Truth conditions for the nonatomic formulae of L 1 will also be defined in the standard way. If there are constraints in our domain of interpretation, expressible as a finite set of formulae in L 1 , we will simply assume that S has been restricted in advance to include only those states in which the constraints are conjunctively satisfied. To avoid any mathematical complexities, however, and to reveal the points of greatest importance to the representational problems of artificial intelligence, we w ill also assume, whenever it is convenient to do so, that the relevant sets are finite. Thus we may assume that the predicate symbols are finite, that the domain of interpretation is finite, and so on. We will attempt to

remove these restrictions at a later date.

We plan to use the states in S to represent the world at different points in time, as in a standard temporal logic, but with one important modification. Normally, each s e S is assumed to provide us with a complete specification o f the state of the world at a particular time, but we wish to work primarily with partial specifications of the state of the world Our approach is similar to the approach o f Barwise and Perry [22]. Since we can think of the complete specification of a state s e S as a collection o f sets, one set for each predicate in L 1 , it is natural to think of a partial specification of s as a collection of subsets, one subset for each predicate and one subset for the complement of each predicate in L 1 . Specifically, for s e S, let s be an ordered collection of sets

satisfying the requirement that

Pk(s) c Pk(s) and P~(s) n Pk(s)

{)

for all predicates P k in L 1 . Under these conditions. we will say that s is a substate of s. and we will denote the set of al l such substates by S(s). It is important to note that these definitions depend explicitly on s. Within each S!sl. there exists a natural partial order. given by set inclusion. and an additive binary operation. given by set union. but this will not be the case in general for arbitrary substates. Specif ically, for any s and t in S(s). we define:

Also. for any s and t in S(s). we define s+t to be the ordered collection of all sets of the form P (s) u P (t) and c c . . k k P k (s) u P k (t). so that s+ t IS 1tself a member of S(s). We now extend these ideas from· states and substates. to worlds and subworlds. We define a world w to be a linear sequence of states {s Is. e S} . and we denote the set of all such worlds by w.' Given any w e W , we define a subworld w to be a linear sequence of substates {si I si e S(si) for all si in w}. and we denote the set of all such subworlds by W(w). It is convenient to index these worlds and subworlds as follows:

and to define a shift operator T" which takes w = {s} into T"w = {si+n} . We can then extend the partial ord~r ''<" and the binary operation "+" to subworlds in the obvious way, component by component, with the nonexistent substates in a subworld interpreted as existing, but null, substates. Finally, we define an operation of sequential composition in W(w): if w e W(w) is a subworld ending in sn, and if w 2 e W(T-"wl i~ a subworld beginning

with s 0 , then we set w 1 ;w 2 = w 1 + T"w 2 .

We are primarily interested in these substates and subworlds because they can be used to specify the precise content of an action. In particular. the concept of a subworld is the technical device which we will use to focus on a small set of changes in the world, and to designate these changes as the "meaning" of an action description. while ignoring everything else that is occurring (or not occurring) in the same world at the same time. We will thus be making extensive use of the subworld concept in the remainder of this paper. The concept of a substate will be used only briefly, to define the meaning of the primitive actions, and for this we need only work with the atomic formulae in L 1 . There are two main issues which need to be addressed for both substates and subworlds. however. and these issues are simpler for substates:

1.) Satisfaction. What does it mean to say that a formula A of L 1 is true in a substate s e S(s)? It is

convenient to adopt the following monotonicity condition:

SI=A - ('Vt) [t e S(s) A t~s - ti=A]

to insure that the truth value of A cannot change as we move along the partial order to a more "complete" substate in S(s). However. if A is an atomic formula in L , or if A . 1 IS the negation of an atomic formula in L 1 · we can use the same truth definition here that we used to define truth in a complete state s e S. For example. define:

o,SI= (Own x y) - <o(x).o(y)> e Own(s)

and define:

and it is then clear from our construction of S(s) that the monotonicity condition holds. If A is nonatomic, the intuitionistic truth definitions due to Kripke [23] will give us the results we want. For example, the existential quantifier can be defined in the usual way in each substate, and the monotonicity condition will still hold, but the universal quantifier in a substate s must be defined for all t e S(s) such that t~s. These definitions suggest a model­ theoretic version of some of the recent results in non­ monotonic logic [24] [25] [26] . but we will not pursue this analysis in the present paper. It is sufficient for our present purposes to confine our attention to the atomic

formulae in L 1 .

• 2.) Strict Satisfaction. It is possible. indeed quite probable, for a substate s e S(s) to satisfy a formula A of L 1 and still contain a great deal of "irrelevant" detail. To avoid this situation, we need to develop the notion of strict satisfaction, which we write as Sl= A. The intuitive idea here is that a substate strictly satiffies a formula A if it contains those tuples necessary for the truth of A, but no more. For an atomic formula A. the substate which strictly satisfies A is simple: it consists of a single nonempty set containing a single tuple. For example, the formula (Own x y) is strictly satisfied by the substate s for which Own(s) = {<o(x).o(yl>} , and the formula -(Own x y) is strictly satisfied by the substate s' tor which Ownc(s') = {<o(x).o(y)>} . Note, however. that s and s' cannot both be members of the same set S(s). The nonatomic formulae can be handled in the same intuitive way. If A is a conjunction of two atomic formulae, then o,sl= 0 A if and only if s contains the tuples satisfying both of the conjuncts. but no more; and if A is a disjunction of two atomic formulae. then o,SI= 0 A if and only if s contains a tuple satisfying one of the disjuncts, but no more. Negation cannot be defined in this way, but we can always transform a formula of L 1 so that all negations have atomic scope. At any rate, the notion of strict satisfaction will be used primarily within the context of our language of actions, LA' in which, as we shall see, there are no general negation operators. Thus, once again, it is sufficient for our present purposes to confine our attention to the atomic formulae in L 1 .

B. Action Descriptions

Let us now extend the concepts of satisfaction and strict satisfaction to the language of actions: LA. We begin by constructing a set of primitive actions, and defining the truth conditions for these actions on a subworld consisting of only two substates: w = <s,t>. Our primitive actions are thus elementary statechanges, a familiar construct in artificial intelligence. It is convenient to work with the following set of actions:

• 1.) Affirmative Statechanges. Let A and 8 be atomic formulae in L 1 , and let E be a (possibly empty) conjunction of equality and inequality constraints on the variables appearing in A and B. Suppose we can show that o,s ~ (AA8A£) for all o and for all s e S. We will say in this case that A and 8 are incompatible in S, given the constraints in £ . A fact of this sort would generally be established, not by an inspection of S, but by a deduction from the axiomatic constraints we have imposed on our domain. For example, if our language L contains the predicate Own, we might naturally impose 1 the constraint that a single property can be owned by only one actor:

(Vx 1 )(Vx 2 )(Vy)[(Own x 1 y) A (Own x 2 y) ::> (x 1 = x 2 )] in which case we could take A = (Own x 1 y) and 8 = (Own x y) as atomic formulae which are incompatible given th~ constraint E = (x ~ x 2 ). Under these conditions we can construct an exp~ession (A I 8) to describe the action in which we "change the world from a situation in which A is true to a situation in which 8 is true."

Definition 1: Let A and 8 be atomic formulae which are incompatible in S, given the constraints in E, and let s and t be substates of some states s and t in S. Then (A I 8)E is true on <s,t> under the assignment a if and only if a,s I= A and a,t ~: 8 and a ~: E

We will write this in general as a,<s,t> ~: (A I 8)E, as long as order formula by a particular state. Obviously, if A =

it is understood that the symbol "!=" in this context designates the satisfaction of an action description by a particular world, rather than the satisfaction of a first­ (Own x y) and 8 = (Own x 2 y), then the expression (A I 8)E 1 f t " describes a "transfer of the property y rom x 1 o x 2 . The definition of strict satisfaction in this situation is straightforward. We simply replace the symbol "!=" by the symbol " != " in the previous definition. Thus, in our example, the action ° (A 1 8) would be strictly satisfied by the deletion of an ownershit tuple from the first state, and the addition of an ownership tuple to the second state, and this is precisely the result we want.

• 2.} Creative and Destructive Statechanges. These are special cases of the previous actions, where we take either A = -8 or 8 = -A. For example, if A = (Love x y) and 8 = (Hate x y). then (A !-A) represents the destruction of love, (-8 1 8) represents the creation of hate, and we make no claims at all about the compatibility or the incompatibility of these two actions.
• 3.} Identities. Here, we construct the expression (A I A), and define it to be true on <s,t> if and only if ~A and ti=A. A useful special case is the expression (A), which is defined to be true on <s,s> if and only if ~A. Note that this is the only action which can be reflexively true on a single state. A similar device is used extensively by Harel [20] to represent the conditional test in a programming language.

We now specify the meaning of the compound actions in L , beginning with the definition of disjunction, parallel com~osition and sequential composition. We need to provide a separate recursive definition for " !=" and " != 0 " in each case.

Definition 2: Let ex and 13 be actions in LA, and let a be an assignment of the free variables in ex and 13 to elements in the domain of interpretation of L 1 . Then. for all w e W, and for all w e W(w). the truth conditions for the actions cxViJ , cxAIJ, and cx;ll are given as follows:

Disjunction:

a,wl= cxViJ "* a,wl=cx or a,wl=iJ

a,wl= 0 cxViJ "* a, w~: 0 cx or a, w~: 0 13

Parallel Composition:

a,w~: cxAil ..., a,wl=cx and a,w!=IJ

a, WI= 0 cxAIJ "* for some w 1 and w 2 in W(w). w=w 1 +w 2 and a,w 1 1= 0 cx and a,w 2 1= 0 iJ Sequential Composition: a, w~: cx;iJ "* a,wl=cx and a,Tnw!=iJ a,WF 0 cx;iJ *" for some w 1 e W(w) and w 2 e W(T-nw). w=w 1 ;w 2 and a,w 1 1= 0 cx and a,w 2 1= 0 il ·

Although we are using the familiar logical symbols "v" and "A" here, the meaning of these connectives in LA is slightly different from their meaning in L 1 . When we perform the action cxViJ, we are either performing the action ex, or we are performing the action 13. but we are not performing the actions ex and 13 together, because of our definition of strict satisfaction. This interpretation has consequences for our analysis of disjunctive permissions, as we will see in Section 111.8 below. The notion of a conjunction of actions in L is ambiguous. and we have distinguished here only two A simple cases: a strictly "parallel" conjunction, and a strictly "sequential" conjunction. In a more realistic language of actions. we would attempt to include some more complex methods of composition, using overlapping time intervals and uncertain endpoints [27]. but the present language is complex enough to reveal the principal features of the deontic concepts.

We now define three additional operations on the actions in L : predicate restriction. which restricts one of the sorts in Athe action cx(x) to a predicate R; and existential and universal quantification, which are likewise restricted to the individuals satisfying a predicate R. We will omit the definition of "!=" when it is identical to the definition ot "!= " o·

Definition 3: Let cx(x) be an acti<;m in LA which contains the free variable x , and let R be a unary predicate in L,. Let a be an assignment of the free variables in ex to elements in the domain of interpretation of L 1 , and let a(x I u) be the assignment which is identical to a except that it assigns the variable x to the individual u. Then, for all w e W, and for all w e Wlw). the truth conditions for the actions cxR) x), (3:Rx)cx(x) and (V:Rx)cx(x) are given as follows:

Predicate Restriction:

a,wF 0 cxRx(x) *" a,WF 0 cx(x) and a.s 0 1=(R x)

Existential Quantification:

a,WF (3:RX)cx(X) "* 0

for some u, a(xl u).s 0 1=(R x) and a(xl u).w!= 0 cx(x)

Universal Quantification:

a ,WF (V:Rx)cx(X) "*

for every u such that a(x/u) , s 0 ~:(R x), a(x/u),w~:cx(x)

a,WF (V:Rx)cx(x) *"

0 for every ui such that a(x/ui),s 0 1=(R x). there exists a w . in W(w) such that I

We can illustrate these definitions with several simple examples. Suppose o:(x,yJ represents the "transfer of a property y to an actor x ," and (5 yl represents the fact that "y is a stock." Then the predicate restriction o: 5 (x,y) represents the "transfer of a stock y to an acto/ x ." Suppose furthermore that (C x i represents the fact that "x is a corporation." Then (3:CxJo: 5 (x.y) represents the "transfer of a stock y to some corpo}ation x ," a disjunctive action. and (V:Cx)o: 5 (x,y) represents the "transfer of a stock y to a/ I corporatid'ns x ," a parallel composition of actions. Notice that it is necessary for our definitions to refer to the complete · state s 0 in w , even though we are only specifying truth conditions for a subworld w e W(w).

C. Permissions and Obligations

We are now in a position to define the semantics of permission and obligation. relative to a state r. First, for any two worlds v and w , if r is both the last state in v and the first state in w , we will say that the pair <v,w> is "joined together" at r. Let us consider the set of pairs {<v,w>} where w is a subworld of w , and where <v,w> is joined together at r. We will assume that there exists. at each r. a subset P of the set {<v,w>} which informs us r of our "permitted courses of action" in the following way: If v is the world up to the present state, then the subworld w is a permitted course of action if and only if <v,w> e P,- It is helpful to think of the set P, as an "oracle," and to imagine that we can consult with this oracle whenever we are contemplating a course of action w. We will never have full access to the set P, or its complement, of course, but we will knoyv some of its members. and some of its 'nonmembers. by virtue of the rules of permission and obligation.

We begin by defining the notion: permitted. We write <4> lo: >P to represent the English sentence: "i f 4> is satisfied ·up to the present, then the action o: is permitted."

<4> I o:) P is true at r under the

Definition 4: assignment o if and only if. for all <v,w> joined

together at r. and for all w e W(w):

It is important to note that this definition incorporates the concept of strict satisfaction. instead of ordinary satisfaction. and that any subworld which strictly satisfies the action o: belongs to the set P,. Therefore. two separate rules of permission will cumulate by set theoretic union. and a· course of action will be permitted if it is permitted by any one of these rules.

We now define, in a similar manner. the notion: forbidden. We write <4> I o:) F to represent the English sentence: "if 4> is satisfied up to the present, then the action o: is forbidden."

<4> I o:) F is true at r under the

Definition 5: assignment o if and only if, for all <v,w> joined together at r, and for all w e W(w):

Note that this definition incorporates the ordinary concept

of satisfaction, instead of the concept of strict satisfaction. In effect. we are saying here that if o: is forbidden, then it is not only the subworlds strictly satisfying o: which are forbidden. but also all supersets of these subworlds.

To arrive at the definition of obligation, let us consider the preceding definition with the symbol "-ex" formally substituted for the action ex. The final line of this definition could then be rewritten as:

We will not actually construct "negative" actions in LA, for both technical and philosophical reasons. but this formal manipulation suggests an appropriate step to take. We will replace the expression "-o.wl=-ex" with the expression " o.wl=ex." Accordingly, let us write <4> I ex) 0 to represent the English sentence: "if 4> is satisfied up to the present, then the action ex is obligatory," and let us recast our previous truth condition to read as follows:

Definition 6: <4> I ex) 0 is true at r under the assignment o if and only if. for all <v.w> joined together at r. and for all w e W(wJ: <v,w> e P, => [o,vl=(j> =<> o,wl=ex]

This final definition has a structural similarity to the standard definition of modal logic. The action ex is obi i gatory if and only if it is true in all permitted worlds.

D. Dynamic Permissions and Obligations

Notice that every expression in our deontic language L 0 is either true or false. under the assignment o, in each state r. If one of these expressions has free variables in it, then it expresses a relationship among individuals in the domain of interpretation of L 1 · and we can define a new predicate in L 1 which holds just in case the expression in L 0 holds. Thus. we can assert the existence of permissions and obligations in the same way we assert any other first-order statement. Using the machinery for defining statechanges. we can then construct actions which modify the deontic assertions, we can make these actions permitted. or forbidden. or obligatory, and so on. In other words, the process of linguistic construction, from L 1 to LA to L 0 , is fully recursive.

Now, suppose the following formulae are true. in each

state r, for a particular 4> and ex:

Then we have satisfied the conditions for constructing an affirmative statechange, and we can define a general action which makes ex permitted, forbidden, or obligatory, in sequence. as we wish. But. as we shall see in Section 111.0 below, these formulae are true for a/ I 4> and ex. This makes the management of deontic modifications particularly simple and elegant.

Ill DEONTIC AXIOMATICS

In this section we consider various formulae involving the deontic expressions, and we prove that these formulae are true in our system, for all r, and for all assignments o. We thus present part of a sound axiomatization of our proposed deontic logic, and we indicate this fact by writing the formulae as deontic theorems. denoted "1- 0 ." We will not be able to present a complete axiomatization, however, since the rules of inference in our system are considerably

more complex than the rules of inference in a standard modal logic. This point will be discussed in Section lll.F. There is a second purpose to our discussion of deontic axiomatics. however, and that is to demonstrate that the · familiar paradoxes of deontic logic do not arise in our system. To this end, we will examine the intuitive interpretations of our deontic formulae in some detail.

A. Compound Obligations

Let us first consider a disjunctive obligation. We establish the following result:

Proof: Assume either <<t>lex 1 ) 0 or <<t>lex 2 > 0 is true at r. Using Definition 6, we pick <v,w> in P, and assume that vt=.p. On this assumption, if the first disjunct on the left hand side of ( 1) is true, then wt=ex 1 ; and if the second disjunct on the left hand side of ( 1) is true. then wt=ex 2 . Thus wt=ex 1 vex 2 . Since this result holds for arbitrary <v,w>, it follows that < </> I ex 1 vex 2 > 0 is true at r.

Note that the converse implication is false. To see this, let <v,w 1 > e P, be a permitted subworld for which w 1 t=ex 1 and -w 1 t=ex 2 , and let <v,w 2 > e P, be a permitted subworld for which w 2 t=ex 2 and -w 2 t=ex 1 . For example, if ex 1 is the action "open the door" and ex 2 is the action "turn on the light" then w 1 would be the subworld in which the door is opened but the light remains off, and w 2 would be the subworld in which the light is turned on but the door remains closed. Since both subworlds are permitted, neither <<t>lex 1 > 0 nor <<t>lex 2 > 0 would be true. Suppose. however. that these are the only permitted subworlds, at least when the initial condition </> is satisfied. Since both w 1 and w 2 satisfy ex 1 vex 2 , it is easy to see that the disjunctive obligation <<t> I ex 1 vex 2 > Q is true at r. In other words, one can be obligated to 'open the door or turn on the light," without being obligated to "open the door," and without being obligated to "turn on the light"

Now consider a conjunctive obligation. In this case .. the implication goes both ways:

Proof: The proof is analogous to the proof of ( 1 ). To establish the implication from left to right, we pick <v,w> e P, , assume that vt=.p, and show that wt=ex 1 Aex 2 . To establish the implication from right to left, we show separately that <v,w> e P, implies wt=ex 1 and that <v,w> e P, implies wt=ex 2 .

B. Compound Permissions

The formula for a disjunctive permission takes the following form:

Proof: To establish the implication from left to right, we assume that both <9'>lex 1 )P and <<t>lex 2 >P are true at r. Using Definition 4, we pick a <v,w> such that vt=.p and wt= 0 ex 1 vex 2 . By the definition of strict satisfaction, this means that wt= ex 1 or wt= 0 ex 2 . But in either case, <v, w> e P, and thus <<t>fex 1 vex 2 >P is true. To establish the implication from right to left we construct a similar argument for both <<t>lex 1 )P and <<t>lex 2 >P. For example, if vt=.p and wt= 0 ex 1 , then wt= 0 ex 1 vex 2 , and the right hand side of (3) then tells us that <v,w> e P . r

The implication in (3) from a single disjunctive permission to a conjunction of two permissions vio~at!ls the standard results of modal logic, but it corresponds closely to our ordinary usage of deontic terminology. To use our earlier example, if we are permitted to "open the door or turn on the light," then surely we are permitted to "open the door." In our ordinary deontic language, an agent is free to choose among the disjuncts, a fact that is captured in our semantics and revealed in (3).

Our analysis becomes somewhat more complex, however, if we consider the following plausible theorem:

Should this result be provable in our system? It is easy to see that (4) cannot be derived from the semantic assumptions we have made so far. Consider our earlier example: Let ex 1 be the action "open the door," let ex 2 be the action "turn on the light," let w 1 be the subworld in which the door is opened, but nothing else occurs. and let w 2 be the subworld in which the light is turned on, but nothing else occurs. Suppose furthermore that <v, w 1 > and <v,w 2 > are the only members of P,- If 9'> is satisfied whenever the door is initially closed and the light is initially off . then w ,t= ex 1 and w 2 t= 0 cx 2 , and we can see from an inspection of f>efinition 4 that both <<t> I ex 1 > P and <</>I ex 2 > P are true. But a subworld in which we both opened the door and turned on the light would not be permitted under these assumptions, and hence <<t>lex 1 Aex 2 >P cannot be true. We have thus refuted the implication in (4) from left to right and a similar example can be constructed to refute any attempted implication from right to left Notice. though, that this refutation depends critically on our use of the concept of strict satisfaction in Definition 4. In fact. if we replaced "t= 0 " by "t=" in our definition of <</>I ex ) P we could establish an even stronger result.

by an argument closely analogous to our proof of (3). But since (5) would hold for any action ex 2 , it would be totally unacceptable. Alternatively, and less drastically, we could constrain our definition of P, by the following closure axiom:

<v,w 1 > e P, and <v,w 2 > e P, ==- <v,w 1 +w 2 > e P, With this assumption, the proof of (4) would go through. but the proof of (5) would be blocked.

Which result do we want7 Suppose we have been told separately that we are "permitted to open the door," and that we are "permitted to turn on the light." Would we then conclude that we are permitted simultaneously to open the door and to turn on the light? Maybe yes, maybe no. We would not want (4) to hold in all cases, because that would totally conflate a very useful distinction between disjunction and conjunction. But if we were given a long list of permitted actions, intended to be composable in parallel, in would be inefficient to list all possible combinations of these actions. and to grant permissions separately for each one. As a pragmatic alternative, we might construct a special rule of inference that would operate on "independent" permissions, applying the formula in (4) only to a designated set of expressions <</>I ex> p· In particular, if the expressions <<t> I ex 1 > P and <<t> I ex 2 ) P had originally been derived from the expression <<t> I ex 1 vex 2 > P by the use of (3). then the special rule of inference would not be applicable, thus preserving the distinction between a disjunctive and a conjunctive rule of permission.

C. Compound Deontic Conditions

For the sake of completeness, we include here several results on the conditional component of the deontic expressions:

Proof: Omitted, but analogous to prior · proofs. D. The Relation Between Permission and Obligation

Let us now consider two questions which were initially raised in Section I as part of our discussion of standard modal logic. First, does the formula Pp = -0-p hold for permissions and obl igations? In particular. if it is false that you are forbidden to do p, does it follow that p is permitted? Second, does the formula Op ~ Pp hold? In other words. is every obligatory action permitted?

The answer to the first question is negative. The following implication holds in only one direction in our system:

Proof: Immediate. from Definitions 4 and 5. For a counter example to the reverse implication. we pick any a which is strictly satisfied by two subworlds w 1 and w 2 . and we put <v,w 1 > e P, and <v,w 2 > f! P, Then the right side of 1101

is true. while the left side is false.

The answer to the second question is also negative, if it is translated literally into our notation. Since obligations cumulate by set theoretic intersection, each obligation narrowing the scope of the remaining permitted acts. there is no reason to expect that all the courses of action within a single rule of obligation will be permitted by other rules of obligation. A weaker version of this formula is more plausible: namely, that if o: is obligatory there exists some permitted course of action which satisfies a. It turns out that this weaker formula is true in our system only if P, satisfies an additional assumption: (Vv)(3w)[<v,w> e P,l which asserts that P has no "dead ends." Under this r assumption, we can prove the following:

Proof: We will assume <~I a> F and derive a contradiction.

By Definition 5, if we pick a v such that vt=~. then for all w. wt=a =- <v,w> f! P . Because of the assumption that P has no "dead ends," there exists a w' such that <v,w'> e' P, Clearly this w' cannot satisfy a. Since <~la> 0 is also true. however, Definition 6 tells us that w' t=a, a contradiction.

Note that I 1 0) and I 1 1) are equivalent to the formulae cited in Section II.D above, thus allowing us to construct a general action for the modification of an arbitrary deontic expression.

E. Quantification Over Actions

Let a(x) be an action in LA containing a free variable x, and let ~ be a condition in . LA which does not contain x as a tree variable. Think of the existential quantifier as a disjunctive operator, and think of the universal quantifier as a conjunctive operator. Then. by analogy to 11 ), (2), (3) and (4), we can write down the following variants of the Barcan formulae of standard modal logic:

Proof: These results can be established by modifying the proofs of I 1). 121. 131 and 141. respectively. so that they apply to the quantified expressions of Definition 3. The most interesting case is I 141. Reading from r ight to left: "If we are permitted to transfer stock to some corporation x. then. for every corporation x, we are permitted to transfer stock to that x ."

F. Rules of Inference

Most axiomatizations of modal logic include an axiom:

and a rule of inference:

which enable us to transfer provable formulae from nonmodal contexts into modal contexts, and to carry out deductions inside the modal operators. However, as Moore has pointed out [ 1 8] , these axiomatizations are notoriously inefficient for automatic theorem proving. In our present formalization of deontic logic, of course, the modal axiom makes no sense at all . and the rule of inference applies only to trivial cases. What we need instead are a number of specialized rules of inference which would enable us to "lift" deductions from the language L 1 up to the language LA' and then up to the language L 0 , and to do so in an efficient manner.

For example. consider the action a 5 (y) in which a(y) represents the "transfer of a property y" and the predicate restriction IS y) represents either the fact that "y is a stock" or that "y is a security." Suppose (lfy) [!Stock y) ~ (Security y)] in the language L,. Then any subworld w which strictly satisfies a Stock (y) also strictly satisfies aSecurit)YI. and we can show:

In ordinary language: "If we are obligated to transfer a stock y, then we are obligated to transfer a security y." Conversely: "If we are permitted to transfer a security y, then we are permitted to transfer a stock y." Given our previous discussion of the intuitive meaning of permissions and obligations. these results seem correct. What is needed. however, is a more general set of rules to carry out these inferences. We have some partial results along these lines, but they are not yet complete.

IV CONCLUSION

We have presented in this paper a formal semantics for the concepts of permission and obligation which seems to avoid the paradoxes of the standard deontic logics. The major deficiencies at the moment are two: we have not yet worked out the complete rules of inference for our system; and we have confined our attention so far to a relatively simple language of actions. Unfortunately, these two points are intimately connected. The rules of inference proposed for our system are complex because they take into account the structure of the language of actions LA' and as we add further complexity to LA we will certainly add complexity to the rules of inference. too. Nevertheless. we believe that the semantics of the deontic language itself, the language L 0 . is basically correct. and robust. and that it will remain in its present form as the language LA evolves. Perhaps this is even a fact of our cognitive lives: that the concepts of permission and obligation are relatively simple, and the complexity arises instead from our concept of action.

Acknowledgments: The author wishes to thank N.S. Sridharan. Ray Reiter. Alex Borgida and David Raab for their many helpful discussions. The design of a computational version of the present deontic representation is the subject matter of a dissertation proposal by David Raab.