=Paper=
{{Paper
|id=Vol-2710/paper3
|storemode=property
|title=Disentangling Deontic Positions and Abilities: a Modal Analysis
|pdfUrl=https://ceur-ws.org/Vol-2710/paper3.pdf
|volume=Vol-2710
|authors=Giovanni Sileno,Matteo Pascucci
|dblpUrl=https://dblp.org/rec/conf/cilc/SilenoP20
}}
==Disentangling Deontic Positions and Abilities: a Modal Analysis==
https://ceur-ws.org/Vol-2710/paper3.pdf
Disentangling Deontic Positions and
Abilities: a Modal Analysis
1 2
Giovanni Sileno and Matteo Pascucci
1
University of Amsterdam, Amsterdam, The Netherlands
2
Slovak Academy of Sciences, Bratislava, Slovakia
g.sileno@uva.nl, matteo.pascucci@savba.sk
Abstract. Computational systems are traditionally approached from
control-oriented perspectives; however, as soon as we move from central-
ized to decentralized computational infrastructures, direct control needs
to be replaced by distributed coordination mechanisms that are on par
with institutional constructs observable in human societies (contracts,
agreements, enforcement mechanisms, etc.). This paper presents a for-
malization of Hohfeld’s framework building upon a logic whose language
includes primitive operators of ability and parametric deontic operators.
The proposal is meant to highlight the fundamental interaction between
deontic and potestative concepts and contains proofs of soundness and
completeness with respect to a class of relational models.
· Ability · Modal Logic · Normative
·
Keywords: Institutional Powers
Positions Hohfeldian Relations
1 Introduction
In access control models, “privileges” of users result to be both permissions (for
the user to perform the action, and the system can not sustain any claim against
it) and powers (as the user creates a duty on the system to perform the action by
requesting it). However, merging permission with power, despite being common
in control-oriented approaches, is not always a sound choice. For example, data
access to distinct public data-sources might be unconditionally enabled, but pro-
cessing of the aggregated data might still result in illicit outcomes (e.g. producing
discriminatory decisions). More generally, as soon as we move from centralized
to decentralized systems (e.g. data-sharing infrastructures, distributed machine
learning, smart contracts on distributed ledgers, digital market-places), direct
control needs more and more to be replaced by distributed coordination mech-
anisms that are on par with institutional constructs observable in human soci-
eties (contracts, agreements, regulations, and related enforcement mechanisms).
This requirement emerges because any decision-making of autonomous compo-
nents/agents requires relatively reliable expectations of the behaviour of the
*
©
Copyright 2020 for this paper by its authors. Use permitted under Creative Com-
mons License Attribution 4.0 International (CC BY 4.0).
2 G. Sileno and M. Pascucci
other components/agents, as well as of the measures holding to maintain these
expectations, e.g. penalties in case of violations. Making these expectations clear
can be seen as the main function of normative artefacts. Strengthening them, of
the associated mechanisms of enforcement.
This paper aims to present a logical framework attempting to reduce the
gaps amongst existing approaches to normative specifications, on the basis of the
higher-granularity given by Hohfeld’s framework of normative relationships [8],
further investigated in the last decades by several contributions in the analytical
and theory of law tradition [10, 11, 7, 15, 14, 12].
A few contemporary efforts are focusing on the operationalization of Ho-
hfeld’s framework in practical settings [17, 2], but so far only few attempts have
been concerned with the underlying formal properties in a systematic way. This
work is analytical in nature but starts from a pragmatic view: actions will be
given first-class citizenship, and deontic notions (obligations, permission, or pro-
hibition) will be reinterpreted in terms of the actions they enable. Our contri-
bution consists in showing how a language of multimodal logic including labels
for action-types, objects and object-configurations—but involving no form of
quantification—is adequate to define several concepts at the basis of the Ho-
hfeld’s framework (such as change, ability, disability, duty and power). On the
one hand, the proposed language is more expressive than standard languages
of propositional modal logic used for similar purposes (e.g., those in Brown’s
approaches to represent ability [3, 4] or those in the STIT-framework [9], dis-
cussed in section 2.3), since it allows one to analyse the internal structure of
propositions. On the other hand, logical systems built over it, such as the cal-
culus Θ in this article, can be axiomatized by focusing on a restricted set of
primitive modalities, since more fine-grained notions can be treated via purely
syntactic definitions. Furthermore, such a language will be proved to make room
for a formal rendering of coordination mechanisms, starting shading light on the
relationships between deontic and potestative notions.
The paper proceeds a follows. Section 2 presents the background underlying
and motivating the proposal. Section 3 presents the formal notation, and dis-
cusses several examples of syntactic definitions, together with their application in
the analysis of some types of normative scenarios (sale contracts, data protection,
delegation). It also illustrates a procedure to transform object-configurations into
propositions and addresses the issue of coordination mechanisms. Section 4 pro-
vides proofs of soundness and completeness for an example of axiomatic calculus
over our language. A note on further developments ends the paper.
2 Conceptual framework
2.1 Types of normative specifications
Three macro-families of normative specifications can be identified in computa-
tional settings: (i) access and usage control models, specifying that actions of an
agent on certain resources are either permitted or prohibited, under certain con-
ditions; a typical example for this family is access rules for webservers (Fig. 1);
Disentangling Deontic Positions and Abilities: a Modal Analysis 3
(ii) deontic logic(s), defining which actions or more often which situations are
under obligation, permission or prohibition depending on certain conditions; the
relationships between these three concepts can be illustrated on the square of
opposition (Fig. 2); (iii) logics inspired by Hohfeld’s framework, according to
which normative concepts are seen as relationships holding between two parties,
and are primarily about actions; the deontic positions of duty and liberty on
one party correlate respectively with claim and no-claim of another party; the
potestative positions of power and disability of one party correlate respectively
with liability and immunity of the other party; the relationships between these
concepts are traditionally illustrated on two squares (Fig. 3), named obligative
(or first-order) and potestative (or second-order) square.
Some major distinction can be highlighted: access-control models neglect
positive obligations (e.g. about actions that need to be performed by the user),
which are instead covered by languages coming from the deontic logic tradition;
Hohfeld’s framework is the only one making explicit the presence of another party
besides the norm addressee, and introducing the category of power, meant to
capture the (potential) dynamics of normative relationships as driven by parties.
The mainstream tradition within deontic logic, which draws inspiration from
general modal logic, is the only approach focusing primarily on situations [1].
2.2 Actions and situations
Normative directives aiming to regulate behaviour are generally expressed in
terms of (wrong/correct) actions (or courses of actions, i.e. behaviours), or in
terms of (wrong/correct) situations. Situations are more easily expressed in
propositional terms, and this explains why historically deontic logic moved from
actions to situations (see, e.g., [1]). Yet, these are two sides of a coin. On the
one hand, agents are deemed to be primarily evaluated for the conduct they
engage with. Norms are meant to give indications about the specific actions that
agents may, may not, or have to perform. On the other hand, law’s aim is not
to regulate intent, but actual outcome. An enforcer agent is primarily concerned
about situations, because even actions can be seen in terms of occurred perfor-
mances. These internal and external perspectives, i.e. of the subjects acting, and
of the subjects observing consequences of actions (or their absence), are clearly
interrelated, but carry specific, plausibly distinct representational requirements.
Mapping these concepts to computational actors can be particularly illustra-
tive for our purposes. Performances of actions correspond in this context to func-
tion executions, while their consequences are values in certain registers or other
memory components. Action-types and the matter specifying situations can here
be labeled respectively with function names and register/variable names. The
Order Deny , Allow
Deny from all
Allow from example . org
Fig. 1: Example of access-control rules, from an Apache web-server configuration
4 G. Sileno and M. Pascucci
contrary
Oφ Fφ
subaltern
subaltern
contradictory
Pφ P ¬φ
subcontrary
Fig. 2: Deontic concepts, illustrated on the square of opposition
correlative correlative
Claim Duty Power Liability
opposite
opposite
opposite
opposite
No-Claim Privilege Disability Immunity
correlative correlative
Fig. 3: Hohfeldian squares of normative relationships between two parties
ongoing or occurred performance of an action (execution of a function) can be
easily reified by means of dedicated boolean variables. However, the most intu-
itive way e.g. to constrain a program at runtime not to invoke a certain function
is to make use of some specific data-structure that explicitly identifies allowed
and/or not allowed functions. In the context of operationalization of norms, be-
cause there will be eventually a (computational) agent deciding how to behave,
actions gain a primary role, as well as the related concept of ability.
2.3 Ability
The concept of ability has been long investigated in formal logic. In [3] Brown
introduces an intensional operator for ability which takes formulas expressing
propositions as arguments and inherits some features of the well-known operator
for possibility, being associated with one of the meanings of the modal verb ‘can’
in English. This operator, here denoted by A, is a non-normal one, since it is not
closed under the following schema, where A(x, φ) means that agent x is able to
bring about the proposition expressed by φ: A(x, φ ∨ ψ) → (A(x, φ) ∨ A(x, ψ)).
An alternative approach is presented by Brown in [4], where he defines ability
in terms of a a bimodal language with two normal operators □ and , where □
represents historical necessity and encodes the notion of ‘bringing about’. If
we take ◊ to be the dual of □ and make explicit reference to an agent in formulas
within the scope of , then we can say that in this approach x has the ability
to produce the proposition expressed by φ iff there is a possible course of events
in which x brings about φ, that is: A(x, φ) =def ◊(x, φ).
Disentangling Deontic Positions and Abilities: a Modal Analysis 5
Another popular analysis of the notion of ability in modal terms is offered
within the framework of STIT logic (see, e.g., [9]), where ability is usually de-
fined via a combination of the deliberative STIT operator (here represented as
[x ∶ dstit], and meaning “agent x deliberately brings about”) and historical
possibility, as follows: A(x, φ) =def ◊[x ∶ dstit]φ.
By contrast, in our formal framework the notion of ability will be treated
as a more complex relation involving an agent, an action and a configuration
of object(s). The primary motivation for this approach comes from computa-
tional environments, considering “actions” (that is, primitive operators, labeled
procedural blocs) as first-class citizen. Further inspiration comes from the psy-
chological concept of affordance, firstly introduced by [6], whose basic outline
(see e.g. [5]) can be logically captured as Affords-β(environment, organism),
where β is the behaviour of the organism which is afforded by the environment.
A representational account of affordances has been discussed from a roboticist
perspective in [13], with—neglecting indexing optimizations—the data model
(effect, (agent, (entity, behavior ))), meaning that the agent can perform a cer-
tain behaviour on a certain object to obtain a certain effect. On similar lines,
[19] suggests that considering actions as events driven by agents, ability can be
seen as a more refined form of the initiates predicate used in event calculus
[16], and thus as a reification of agent-driven causal mechanisms.
2.4 Temporal aspects
Our treatment of ability and deontic positions will rely on the assumption that
the portion of the world in which agents operate is a system evolving in a non-
deterministic way over time. Non-deterministic systems can be modeled via rela-
′
tional structures consisting of a set of nodes denoted by w, w , etc., and ordered
as a tree by a precedence relation. The tree can be imagined as being left-to-right
oriented: it is linear towards the past (left) and possibly branching towards the
future (right). The truth of a proposition will be evaluated at a node of a struc-
ture, hereafter called the evaluation node. Nodes that are vertically aligned to
the evaluation node are simultaneous alternatives of it; nodes that lie immedi-
ately on the right of the evaluation node are successive alternatives of it. In our
formal language we will use an intensional operator ⊞ to quantify over the set of
successive alternatives of the evaluation node, as well as an intensional operator
□ to quantify over the set of simultaneous alternatives of the evaluation node.
For our purposes we do not need the expressive power of operators like ‘until’
∗
(U) that are commonly employed in temporal logics of computation (e.g., CTL ).
3 Formal framework
3.1 A minimal language for directed and located change
In the present section we introduce the symbolic language that will be used for
the formal rendering of our theoretical analysis of ability and deontic positions.
6 G. Sileno and M. Pascucci
We start with a minimal language denoted by L and able to express factual
information about a non-deterministic world.
Definition 1 (Vocabulary of L) The language L includes:
– a set OBJ of labels for objects, entities that may suffer change, denoted by x,
y, z, etc. and including a special element, the ‘whole’ (i.e., the whole system
analysed), denoted by ∗;
– a set AGE of labels for agents, entities that may produce change; we assume
all agents being part of the whole, and therefore being objects: AGE ⊆ OBJ;
– a set CONF of labels for configurations denoted by S1 , S2 , S3 , etc. (each
configuration being a possibly partial description of an object at an instant);
– a set ACT of labels for action-types, denoted by a1 , a2 , a3 , etc.;
– the modal operators □ (“at all alternative simultaneous nodes”) and ⊞ (“at
all alternative successor nodes”)
– the binary predicates is and performs;
– the boolean connectives ¬ and →.
Definition 2 (Well-formed formulas in L) The set of well-formed formulas
over L, denoted by WFF, is described by the grammar below, where x ∈ AGE,
n
z ∈ OBJ, S ∈ CONF, and α ∈ ACT × OBJ , for some n ∈ N:
φ ∶= performs(x, α) ∣ is(z, S) ∣ ¬φ ∣ φ → φ ∣ □ φ ∣ ⊞ φ
We say that α is a (label for a) refined action-type; it highlights the objects which
are involved in its instantiation (e.g., the objects ‘taxes’ and ‘bank transfer’ in
the notion of ‘paying taxes with a bank transfer’). A formula of the form □φ
means that φ is the case in every simultaneous alternative of the evaluation
node (e.g., in the current node Anna is not paying taxes, but we can imagine
an alternative arrangement at this time in which Anna pays taxes). A formula
of the form ⊞φ means that φ is the case in every successive alternative of the
evaluation node. A formula of the form performs(x, α) means that x performs a
refined action of type α. A formula of the form is(x, S) means that x is in the
configuration S.
Basic formulas in L are formulas of type performs(x, α) and of type is(x, S).
A basic formula in L describes an atomic proposition. The boolean connectives
for conjunction, disjunction and material equivalence, as well as dual modal
operators of possibility (◊ and ), can be defined in the usual way.
3.2 Relevant definitions
Configurations and propositions In L we can define predicates that are
in a one-one correspondence with configurations. For instance, suppose that
the whole system is in the configuration raining. Then, we can define a 0-ary
predicate (i.e., atomic proposition) raining as follows:
raining =def is(∗, raining)
Disentangling Deontic Positions and Abilities: a Modal Analysis 7
Vice versa, we can associate configurations of the whole system with the propo-
sitional formulas describing them. More formally, for any φ ∈ WFF which is not
in the form is(∗, . . .) we can extend the set CONF with a symbol Sφ , denoting
the arrangement that holds when φ is the case:
is(∗, Sφ ) ↔ φ
The constraint on φ is to avoid recursive nesting, e.g. raining, is(∗, raining),
is(∗, Sraining ), is(∗, Sis(∗,raining) ), etc.
Change and continuity A binary predicate becomes, meant to capture a
change of configuration concerning an object, can be defined as follows:
becomes(y, S) =def ¬is(y, S) ∧ ⊞(is(y, S))
We can also define the dual concept of absence of change, or continuity:
keeps(y, S) =def is(y, S) ∧ ⊞(is(y, S))
Ability Extending the approach proposed in [19], a general schema to represent
the ability of an agent x to produce a configuration Sφ via a refined action of
type α is as follows:
has ability(x, α, Sφ ) =def ◊performs(x, α) ∧ ¬is(∗, Sφ ) ∧
□ [(performs(x, α) ∧ ¬is(∗, Sφ )) → ⊞is(∗, Sφ )]
From this, one can infer that if an agent x has the ability to produce a configura-
tion Sφ by performing a refined action of type α, then x can cause Sφ to become
a new configuration of the whole (whereas without performance this needs not
be the case). In other words, our definition of ability entails that becomes(∗, Sφ )
is true consecutively at all nodes in which x performs an action of type α and
Sφ is not already holding.
Disability and Inhibition A concept dual to ability is disability. One way to
define it would be by applying negation on ability. In this way, we get disability
of obtaining an effect with respect to a particular type of refined action:
¬◊performs(x, α) ∨ ⊞is(∗, Sφ ) ∨ ◊ [performs(x, α) ∧ ¬is(∗, Sφ ) ∧ ¬is(∗, Sφ )]
The negation implies either that the agent cannot perform the refined action
α, or the outcome will be in any case present, or that the connection between
performance and outcome does not necessarily works, i.e. that there is some lack
of controllability, because there is some consecutive node for which the change
does not occur. Strengthening this characteristic, i.e. making in sort that for all
8 G. Sileno and M. Pascucci
consecutive nodes the change will not occur in presence of performance, allows
us to define the ability of inhibiting a world configuration, or negative ability:
has neg ability(x, α, Sφ ) =def ◊performs(x, α) ∧ is(∗, Sφ )∧
□ (performs(x, α) ∧ is(∗, ¬Sφ ) → keeps(∗, ¬Sφ ))
Because negative ability is still a form of controllability (although in negative
sense), a full disability can to be defined as lack of ability and of negated ability:
has disability(x, α, Sφ ) =def ¬has ability(x, α, Sφ ) ∧ ¬has neg ability(x, α, Sφ )
Disability, positive and negative abilities can be used to introduce further notions
as enabling and disabling actions, interference, etc., see e.g. [19].
3.3 Integrating normative concepts
We can extend the minimal language L in a modular way. In this article we focus
N
on an extension L including normative concepts: for any x, y ∈ AGE, we take
an operator x Oy . In the definition below, we rely on the notion of subformula of
a formula φ, which is understood in the usual way.
N N
Definition 3 (Well-formed formulas in L ) We denote by WFF the set of
formulas which can be obtained from any φ ∈ WFF by prefixing a finite (possibly
empty) sequence of operators of kind x Oy to any of its subformulas.
A formula of the form x Oy φ means that φ is obligatory for x with respect to
y (directed obligation, see e.g. [7]). We use the standard definition of prohibition
(F ) and permission (P ): x Fy φ =def x Oy ¬φ, and x Py φ =def ¬x Oy ¬φ.
Hohfeld’s framework of concepts The normative relationships identified by
Hohfeld [8] consists of two groups of concepts, illustrated on the obligative and
potestative squares (Fig. 3). Several axiomatizations have been proposed along
the years [10, 11, 7, 15, 12], in the great majority relying on some framework for
agency logic with no explicit reference to action-types; however, a systematic
joint treatment of deontic and potestative concepts has not been yet developed.
Our proposal is distinct as it considers “action” to be a primitive object of
analysis. Using the proposed notation, we can set the following definitions. For
the obligative square:
– duty: x DTy (α) =def x Oy performs(x, α)
– claim-right: y CRx (α) =def x DTy (α)
– privilege (liberty): x P Ry (α) =def x Py performs(x, α) ∧ x Py ¬performs(x, α)
– no-claim: y N Cx (α) =def x P Ry (α)
For the potestative square:
– power: x P OWy (α, φ) =def has ability(x, α, Sy Ox φ )
– liability: y LBLx (α, φ) =def x P OWy (α, φ)
Disentangling Deontic Positions and Abilities: a Modal Analysis 9
– disability: x DISy (α, φ) =def has disability(x, α, Sy Ox φ )
– immunity: y IM Mx (α, φ) =def x DISy (α, φ)
These definitions follow assumptions implicit in Hohfeld’s presentation, namely
that duty is a directed obligation about a performance of the duty-holder and
that, following the legal tradition, institutional power is primarily about cre-
ating duties. We also followed the approach suggested in [18] to consider the
privilege position as corresponding to liberty, and disability as a conjunction of
lack of ability and lack of negative ability, so as to recover the original symmetry
3
between the two squares that is lost in the other formalizations.
Extending Hohfeld’s framework Hohfeld’s assumptions might be however
relaxed for a general application of the notation. First, one could specify a duty
independently of the person performing that action; for instance, parents have
the duty that their kids go to school. Second, duties might be about configura-
tions, e.g. landowners have to maintain their land in an adequate state to prevent
propagation of fire. For these reasons, for the concepts of the obligative square,
we propose to replace the performance of α by x with any formula φ from L:
– duty: x DTy (φ) =def x Oy φ
For the potestative square, Hohfeld’s power is about creating duties, but one
could extend the term to cover the abilities of releasing from a duty, and in
principle, also the abilities of creating or destroying powers. Such an approach
would allow us to identify the whole structure that determines the dynamics of
a normative system, not only its superficial layer. We have then:
– power: x P OW (α, φ ) =def has ability(x, α, Sφ′ )
′
where φ is a formula definitionally equivalent to one in the form y DTx (φ) or
′
y P Rx (φ), or in the form x P OW (β, φ ) or x DIS(β, φ ). Accepting conjunctions
′ ′
of those terms implies that several parties might be associated to duty-holder po-
sitions. Note that the party/parties in the correlative position of power positions
can be omitted as those are determined by the inner formulas.
3.4 Examples of application
Sale contract Using Hohfeld’s primitive concepts (here in the extended form),
the execution of a sale would be characterized in terms of mutual duties and
claims holding between a buyer x and a seller y:
x DTy (performs(x, pay)) ∧ y DTx (performs(y, deliver))
3
This choice supports the introduction of additional positions otherwise neglected:
protection, correlative to a negative duty (prohibition), and negative power, correla-
tive to negative liability, illustrated on the Hohfeldian prisms [18].
10 G. Sileno and M. Pascucci
The formation of such a contract, in the bilateral case, consists of offer and ac-
ceptance steps, associated to two forms of power. The overall normative pattern
can be modeled as:
y P OW (offer ,
x P OW (accept,
x DTy (performs(x, pay)) ∧ y DTx (performs(y, deliver)))
Data protection Following data protection regulations (e.g. GDPR), legal pro-
cessing of personal data requires consent from data subjects. Usually this mech-
anism is seen as a conditional duty (simplifying, if data belongs to y, x must
collect consent from y). However, this is an arguable choice; this duty can be
literally violated (e.g. because y may not provide consent) without any legal
consequence. The normative relevant positions are that processing is in general
prohibited, unless there is consent. This means that a data controller has the
power to release the prohibition existing by default, by collecting consent:
x DTy (¬performs(x, process)) ∧
x P OW (collect consent, x P Ry (performs(x, process)))
Delegation Power reifies a causal mechanism that modifies normative relation-
ships holding between parties. The reification enables to treat this mechanism
as an object, i.e. to create or destroy it at need. This is not possible if the rep-
resentation is limited on conditional statements modeling the content of power.
We consider an example. As an institutional pattern, delegation holds in cases
in which x is granted a power associated to some refined action α, but is also
granted to grant this power to someone else, (possibly) losing the original power:
x P OW (α, φ) ∧
x P OW (delegate, y P OW (α, φ) ∧ x DIS(α, φ))
3.5 Coordination mechanisms
Deontic notions can be seen as setting up specific social coordination mecha-
nisms. Three activities might be generally associated to any norm regulating
behaviour: performance concerns the abilities of the duty-holder x, monitor-
ing concerns the abilities of duty-claimant y (whose role, from a coordination
perspective, is to signal whether expectations are met), enforcement typically
concerns a judiciary system j to which y refers to protect its rights (see e.g. [12]).
We will present here an elaboration on a simplified form of the signaling aspect,
leaving the rest to future study.
Let us denote with V and F the configurations of the whole in which a norm
having content N is deemed to be respectively violated and fulfilled. Separating
performance from monitoring, the creation of V or F can occur only after inter-
vention of the duty-claimant y, so this actor needs to have the associated abilities
Disentangling Deontic Positions and Abilities: a Modal Analysis 11
for doing so. Yet, these abilities are not arbitrary, but conditioned by the actual
state of the world, in relevance to the norm. Thus, any active prescriptive norm
N as x DTy φ comes also with two conditional powers:
N ⇒ [¬is(∗, Sφ ) → has ability(y, δV , V )] ∧ [is(∗, Sφ ) → has ability(y, δF , F )]
where Sφ is the configuration associated to φ, δV and δF are distinct signal-
ing actions possibly performed by the duty-claimant, respectively associated to
violation and fulfillment. In contrast, with an active permissive norm Nperm as
x P Ry φ, the duty-holder x gains immunity from any attempt of y to signal vio-
lation in case of performance and of non-performance (i.e. always):
Nperm ⇒ has disability(y, δV , V ) ∧ has ability(y, δF , F )
Note that, on a normative system level, these mechanisms need to override (to
inhibit) where necessary all precedent norms. A complete treatment of this aspect
is beyond the scope of this paper.
4 Logical system
In the present section we define an axiomatic calculus Θ and a class of standard
models for a rigorous transposition of the conceptual framework discussed in the
previous part of the article; Θ will be shown to be sound and complete with
respect to its standard models.
4.1 Syntactic derivability
Definition 4 (Axiomatic basis) The calculus Θ is fully specified by the fol-
lowing list of axioms and rules:
A0 All substitution instances of tautologies of the Propositional Calculus;
R0 Modus Ponens;
A1-R1 S5-principles for the operator □;
A2-R2 K-principles for the operator ⊞;
R3 To infer (x Oy φ ↔ x Oy ψ) from (φ ↔ ψ), for any x, y ∈ AGE.
A3 □ ⊞ φ → ⊞ □ φ;
A4 ◊ ⊞ ⊥ → □ ⊞ ⊥;
A5 x Oy φ → ◊φ.
A few remarks on the basis are helpful to clarify the ideas behind: axioms A0,
A1 and A2, together with rules R1 and R2, are standard principles for normal
multimodal systems. Rule R3 says that operators of kind x Oy are congruential: if
two propositions are provably equivalent, then either each of them is obligatory
or neither of them is obligatory. This is a very weak deductive principle for
obligations, able to avoid many paradoxes of deontic reasoning affecting normal
modal operators (see, e.g, [1]). Axioms A3 and A4 capture the relation between
simultaneous alternatives and successive alternatives of the evaluation node.
Axiom A5 conveys a simple form of the Ought-imples-Can thesis: if something
is obligatory, then it holds in some successive alternative of some simultaneous
alternative of the evaluation node.
12 G. Sileno and M. Pascucci
Definition 5 (Derivation) A derivation in Θ is a finite sequence of formulas
σ = φ1 , ..., φn s.t., for 1 ≤ i ≤ n, φi is either an axiom of Θ or is obtained from
′
some formulas in the sub-sequence σ = φ1 , ..., φi−1 via the application of a rule
among R0, R1, R2 and R3.
N
Definition 6 (Derivable formula) A formula φ ∈ W F F is derivable in Θ
(in symbols, ⊢ φ) iff there is a derivation σ = φ1 , ..., φn where φn = φ.
4.2 Semantic validity
N
Definition 7 (Model) A model to interpret W F F -formulas is a tuple M =
⟨W, D, D , G, K, R□ , R⊞ , fx Oy , I⟩ s.t.:
∗
′ ′′
– W is a set of nodes, denoted by w, w , w , etc.;
′ ′′
– D is a domain of objects, denoted by d, d , d , etc.;
∗
– D ⊆ D is a domain of agents;
′ ′′
– G is a domain of refined action-types, denoted by g, g , g , etc.;
′ ′′
– K is a domain of configurations denoted by k, k , k , etc.;
– R□ and R⊞ are binary relations on W ;
N
– for each x, y ∈ AGE, fx Oy is a function mapping nodes to subsets of WFF ;
– I is an interpretation function mapping entity-labels to entities, namely:
∗
• I(x) ∈ D for any x ∈ OBJ (provided that I(y) ∈ D for any y ∈ AGE);
n
• I(α) ∈ G for any α ∈ ACT × OBJ ;
• I(c) ∈ K for any c ∈ CONF;
∗
• I(performs) ⊆ D × G × W ;
• I(is) ⊆ D × K × W .
N
Definition 8 (Truth-conditions) Formulas of L are evaluated at a node w
of a model M, according to the truth-conditions provided below:
– M, w ⊨ performs(x, α) iff (I(x), I(α), w) ∈ I(performs);
– M, w ⊨ is(x, S) iff (I(x), I(S), w) ∈ I(is);
– M, w ⊨ □φ iff for all v ∈ R□ (w), we have M, v ⊨ φ;
– M, w ⊨ ⊞φ iff for all v ∈ R⊞ (w), we have M, v ⊨ φ;
– M, w ⊨ x Oy φ iff φ ∈ fx Oy (w).
Definition 9 (Standard models) A standard model satisfies the properties:
PA R□ is an equivalence relation;
PB if φ ↔ ψ is derivable in Θ, then for all w ∈ W , φ ∈ fx Oy (w) iff ψ ∈ fx Oy (w).
PC R⊞ ◦ R□ ⊆ R□ ◦ R⊞
PD either (i) for all u ∈ R□ (w), R⊞ (u) = ∅
or (ii) for no u ∈ R□ (w), R⊞ (u) = ∅;
PE if φ ∈ fx Oy (w), then there is u ∈ R□ (w) and v ∈ R⊞ (u) s.t. M, v ⊨ φ.
Disentangling Deontic Positions and Abilities: a Modal Analysis 13
Property PA is a quite natural choice to characterize simultaneous alternatives
(since simultaneity is on its own an equivalence relation). Properties PB and PE
have been already discussed with reference to the corresponding axioms/rules
(R3 and A5). Property PC indicates that if we move one step forward in time
and look for simultaneous states, we find a subset of the states that are reachable
by first looking at simultaneous states and then —for each of these— moving
one step forward. Property PD indicates that the end of time is a global phe-
nomenon: it either affects all branches of a model or none. However, this has to
be distinguished from the end of change (i.e., the fact that formulas keep having
the same truth-value after some point), which may affect a proper subset of all
the branches.
N
Definition 10 (Valid formula) A formula φ ∈ WFF is valid in a model M
iff M, w ⊨ φ for all w ∈ W ; φ is valid in a class of models Cm iff it is valid in
all models of the class. If φ is valid in every standard model, we write ⊨ φ.
N
Theorem 1 (Soundness) For every φ ∈ WFF , if ⊢ φ, then ⊨ φ.
Proof. A standard induction on the length of derivations: every axiom of the
system is valid in all standard models and all rules of the system preserve validity
in standard models. For the sake of example, we show the validity of two axioms,
A4 and A5. In the case of A4, assume that there is a node w in a standard
model M s.t. M, w ⊨ ◊ ⊞ ⊥ and M, w ⊭ □ ⊞ ⊥. This means that there is a node
v ∈ R□ (w) s.t. M, v ⊨ ⊞⊥ and that it is not the case that for all u ∈ R□ (w),
we have M, u ⊨ ⊞⊥. Therefore, there is v ∈ R□ (w) s.t. M, v ⊭ ⊞⊥. From this
′ ′
one can infer R⊞ (v) = ∅ and R⊞ (v ) ≠ ∅, which contradicts PD.
′
In the case of A5, assume that there is a node w in a standard model M s.t.
M, w ⊨ x Oy φ but M, w ⊭ ◊ φ. Then for all u ∈ R□ (w) we have M, u ⊨ ⊞¬φ
and this means that for no such u there is a v ∈ R⊞ (u) s.t. M, v ⊨ φ, which
contradicts PE.
N
Theorem 2 (Completeness) For every φ ∈ WFF , if ⊨ φ, then ⊢ φ.
Proof. For the completeness proof we rely on the canonical model for Θ, using the
N
language L as its own interpretation. We will adopt the following abbreviations:
□ (w) = {φ ∶ □φ ∈ w} and ⊞ (w) = {φ ∶ ⊞φ ∈ w}. The canonical model for Θ
− −
is built in the following way:
– W contains precisely all maximal Θ-consistent sets of formulas;
∗
– D = OBJ, D = AGE;
– G = ⋃n∈N (ACT × OBJ );
n
– K = CON;
– R□ = {(w, v) ∶ □ (w) ⊆ v};
−
– R⊞ = {(w, v) ∶ ⊞ (w) ⊆ v};
−
– fx Oy = {(w, Γ ) ∶ Γ = {φ ∶ x Oy φ ∈ w}};
– I(performs) = {(I(x), I(α), w) ∶ performs(x, α) ∈ w};
– I(is) = {(I(x), I(S), w) ∶ is(x, S) ∈ w}.
14 G. Sileno and M. Pascucci
Relying on a straightforward adaptation of the truth-lemma for propositional
N
multimodal logic, we have that for every formula φ ∈ WFF and every maximal
Θ-consistent set (hereafter, m.c.s.) w, the following holds: M, w ⊨ φ iff φ ∈ w.
We need to show that the canonical model is a standard one, namely, that is
satisfies properties PA-PE. The case of PA follows from well-known results on
the completeness of system S5 and the definition of standard models.
In the case of PB, assume that φ ↔ ψ is derivable in Θ. Then, we can infer
that φ ↔ ψ belongs to every m.c.s., whence that (due to R3) x Oy φ ↔ x Oy ψ
belongs to every m.c.s. as well. By the truth-lemma, we can conclude that for
every m.c.s. w we have M, w ⊨ x Oy φ ↔ x Oy ψ, whence, by the truth-conditions,
that φ ∈ fx Oy (w) iff ψ ∈ fx Oy (w).
In the case of PC, assume that R⊞ (w) ◦ R□ (w) ⊆ / R□ (w) ◦ R⊞ (w) for some
m.c.s. w. Then, there is a m.c.s. v s.t. v ∈ R⊞ (w)◦R□ (w) and v ∉ R□ (w)◦R⊞ (w).
Let ψ be a formula which distinguishes v from any other m.c.s. (that is, for
every u ∈ W , we have ψ ∈ u iff v = u; there is always such a formula due to
the definition of a canonical model). By construction, ◊ψ ∈ w. Now, A3 is
provably equivalent with ◊φ → ◊ φ, whence, given that all instances of A3
are included in w, we have ◊ ψ ∈ w. But then there is z ∈ R□ (w) ◦ R⊞ (w) s.t.
ψ ∈ z. Yet, since ψ distinguishes v from any other m.c.s, we must have z = v.
In the case of PD, assume that there is some m.c.s. w s.t., for some u ∈ R□ (w),
we have R⊞ (u) = ∅. From this we can infer that ⊞⊥ ∈ u and ◊ ⊞ ⊥ ∈ w. Since
w contains all instances of A4, then □ ⊞ ⊥ ∈ w and, for any z ∈ R□ (w), we get
that ⊞⊥ ∈ z, whence R⊞ (z) = ∅.
In the case of PE, assume that φ ∈ fx Oy (w) for some m.c.s. w. Then, x Oy φ ∈
w and, since w contains all instances of A5, ◊ φ ∈ w, which entails that there
is u ∈ R□ (w) and v ∈ R□ (u) s.t. φ ∈ v; by the truth-lemma, we get M, v ⊨ φ.
5 Conclusion and Future Developments
The paper reports on a research effort unifying insights from modal logic and
normative systems, having in mind applications on complex cyber infrastruc-
tures. The key contribution of the paper is to make explicit the deep entrench-
ment between deontic and potestative categories, and how the second ones are
required to model complex coordination structures (e.g. delegation). Future de-
velopments will concern the completion of the analytical effort, focusing on the
mechanisms of enforcement, investigating the relations of powers with condi-
tional obligations, and extending those results introducing roles for objects and
agents and more complex forms of refined actions. Additionally, we started work-
ing on computational implementations of the proposed axiomatization (e.g. in
logic programming, proceeding similarly to [19]).
Acknowledgments Giovanni Sileno was supported by NWO for the DL4LD project
(Data Logistics for Logistics Data) (628.001.001). Matteo Pascucci was supported by
the tefan Schwarz Fund for the project “A fine-grained analysis of Hohfeldian concepts”
(2020-2022). Authors Contributions Sections 2 and 3 are mainly due to GS, Section
4 and 2.4 to MP. The authors contributed equally to 2.3 and 3.1.
Disentangling Deontic Positions and Abilities: a Modal Analysis 15
References
1. Åqvist, L.: Deontic logic. In: Gabbay, D., Guenthner, F. (eds.) Handbook of Philo-
sophical Logic, vol. 8, pp. 147–264 (2002)
2. van Binsbergen, L.T., Liu, L.C., van Doesburg, R., van Engers, T.: eFLINT: a
Domain-Specific Language for Executable Norm Specifications. In: GPCE 2020:
Proceedings of the 19th ACM SIGPLAN International Conference on Generative
Programming (2020)
3. Brown, M.A.: On the logic of ability. Journal of Philosophical Logic 17(1), 1–26
(1988)
4. Brown, M.A.: Normal bimodal logics of ability and action. Studia Logica 51(3-4),
519–532 (1992)
5. Chemero, A.: An Outline of a Theory of Affordances. Ecological Psychology 15(2),
181–195 (2003)
6. Gibson, J.: The ecological approach to visual perception. Houghton Mifflin, Boston
(1979)
7. Herrestad, H., Krogh, C.: Obligations directed from bearers to counterparties. Pro-
ceedings of the International Conference on Artificial Intelligence and Law (Jan-
uary 1995), 210–218 (1995)
8. Hohfeld, W.N.: Fundamental legal conceptions as applied in judicial reasoning.
The Yale Law Journal 26(8), 710–770 (1917)
9. Horty, J.F., Belnap, N.: The deliberative stit: a study of action, omission, ability,
and obligation. Journal of Philosophical Logic 24(6), 583–644 (1995)
10. Lindahl, L.: Position and Change: A Study in Law and Logic. Synthese Library,
Springer (1977)
11. Makinson, D.: On the formal representation of rights relations. Journal of philo-
sophical Logic 15 (1986)
12. Markovich, R.: Understanding Hohfeld and Formalizing Legal Rights: The Ho-
hfeldian Conceptions and Their Conditional Consequences. Studia Logica 108(1),
129–158 (2020)
13. Sahin, E., Cakmak, M., Dogar, M.R., Ugur, E., Ucoluk, G.: To Afford or Not
to Afford: A New Formalization of Affordances Toward Affordance-Based Robot
Control. Adaptive Behavior 15(4), 447–472 (2007)
14. Sartor, G.: Fundamental legal concepts: A formal and teleological characterisation.
Artificial Intelligence and Law 14(1), 101–142 (2006)
15. Sergot, M.J.: A computational theory of normative positions. ACM Transactions
on Computational Logic (TOCL) 2(4), 581–622 (2001)
16. Shanahan, M.: The event calculus explained. Artificial Intelligence Today pp. 409–
430 (1999)
17. Sharifi, S., Parvizimosaed, A., Amyot, D., Logrippo, L., Mylopoulos, J.: Symboleo:
Towards a Specification Language for Legal Contracts. In: IEEE International Re-
quirements Engineering Conference (RE’20), RE@Next! track (2020)
18. Sileno, G., Boer, A., van Engers, T.: On the Interactional Meaning of Fundamental
Legal Concepts. In: Proceedings of the 27th International Conference on Legal
Knowledge and Information Systems (JURIX 2014). vol. FAIA 271, pp. 39–48
(2014)
19. Sileno, G., Boer, A., van Engers, T.: Towards a Computational Theory of Action,
Causation and Power for Normative Reasoning. Proceedings of the 32nd Interna-
tional Conference on Legal Knowledge and Information Systems (JURIX 2019)
(2019)