1 Introduction

Among ‘fundamental legal conceptions’ proposed by Hohfeld (1913) right and duty form the first pair of several correlating notions.Footnote 1 Hohfeldian right-duty relation encounters a situation in which one agent has a right correlated with another agent’s duty to realise that right. A dynamic aspect of normative positions, i.e. changes of rights and duties, is captured with the use of the notion of power.Footnote 2 An agent that has power can create new rights and duties of other agents.

Usually, it is clear who the proper addressee of power is and, consequently, who is bound by the new duty. However, sometimes it is not so. This problem occurs, for instance, when rights of a general nature are involved and are connected with the type or position of an agent rather than with the relation of the agent with another person.

We shall start with two examples. The first one concerns abortion regulations in Polish law. Under certain circumstances abortion is permitted and should be carried on within a public healthcare system. However, there exists the conscience clause which allows doctors to refuse to provide such a service. In the paper we try to determine when a doctor is obliged to provide the abortion service. The other example concerns a clash between freedom of expression and freedom of enterprise. In particular, we analyse a situation where a print shop owner refused to print a poster because he did not agree with the content of the poster. We are interested in determining the circumstances in which there exists an obligation to take on such a job. The examples will be further analysed and formalised.

We want to provide a precise formulation of a certain solution to the problem of pointing out the addressee of an obligation in a multi-agent setting. For that purpose we shall use a formal model based on a labelled transition system, namely the action language with normativity \(n\mathcal {C}+\) introduced by Sergot and Craven (2006) and Craven and Sergot (2008). An essential feature of the formalism is that, unlike most approaches to deontic logic, it allows us to discuss the normative features of both states of affairs and the agent’s actions. In our investigations, we make use of this feature and utilise the interactions between the deontic assessments concerning states of affairs and actions.

Two main difficulties will be tackled. The first one is to model rights within a labelled transition system. The other one is to determine, within a model, actions that are obligatory for particular agents.

Ultimately, creating a formal model facilitates the analysis, either for the purpose of interpretation and disambiguation of existing norms and regulations, or in the design and specification of a new set of norms. In particular, we want to provide a precise interpretation of the norms in our examples and show that this interpretation is consistent.

Moreover the formalisation will allow us to see which features of \(n\mathcal {C}+\) are needed to express the scenarios under consideration and which constraints imposed on a model are useful.

The rest of the paper has the following structure: in Sect. 2 we analyse our examples, in Sect. 3 we introduce the formal tools, in Sect. 4 we apply the formalism to our examples, and finally in Sect. 5 we present conclusions and further research perspectives.

2 The problem on examples and an intuitive solution

2.1 Abortion: Polish regulations and their implementation

Let us start with a presentation of Polish law concerning abortion. The regulations are meant to balance between the right to life of human beings in their prenatal phase, the well-being of a pregnant women and the freedom of conscience of medical personnel. There are two general acts that are relevant here: Act on family planning, protection of the human fetus and conditions for the admissibility of termination of pregnancy and Act on the professions of a doctor and a dentist. The first one focuses on the admissibility of abortion.

Art. 1. The right to life is protected, also in the prenatal phase, within the limits set out in the Act. [...]

Art. 4a. 1. The termination of pregnancy can only be conducted by a physician when:

1) pregnancy is a threat to the life or health of a pregnant woman,

2) prenatal tests or other medical premises indicate a high probability of severe and irreversible impairment of the fetus or an incurable disease threatening their life,

3) there is a reasonable suspicion that the pregnancy arose as a result of a prohibited act,

2. In the cases specified in paragraph 1 pt. 2 abortion is allowed until the fetus is able to live independently outside the body of a pregnant woman; in the case referred to in paragraph 1 point 3, if no more than 12 weeks have passed since the beginning of pregnancy.

3. In the cases referred to in paragraph 1 point 1 and 2, the pregnancy is terminated by a doctor in hospital.

A more detailed regulation placed in another act states that the fact mentioned in Art. 4a. 1. 3) is confirmed by a public prosecutor. The act further states that the allowed abortion cases are included into the state medical care system.

Art. 4b. Persons covered by social insurance and persons entitled under the provisions for free medical care are entitled to a free termination of pregnancy in a public health care facility.

The Act on the professions of a doctor and a dentist introduces conscience clause for doctors, its limitations and the way it can be used.

Art 30. A doctor is obliged to provide medical assistance in any case when the delay in granting it could lead to the risk of a loss of life, serious injury or serious health disorder, and in other urgent cases. [...]

Art 39. A doctor may refrain from providing health services inconsistent with his conscience, subject to the provisions of art. 30, however they are obliged to indicate real possibilities of obtaining this benefit from another doctor or another medical institution, and to justify and record this fact in the medical documentation. A physician practising his profession on the basis of an employment contract or as a part of a service has moreover the obligation of prior notification in writing to the manager.

Let us now trace how these regulations may work in a particular case. Let us think of a woman whose pregnancy is a result of a rape, who decides to have an abortion in the 11th week of pregnancy. Having a proper document from a public persecutor she can ask for a free abortion in a public clinic. Then a physician in the clinic, let us call her Dr. A, will have two options: either perform the abortion or make use of her conscience clause. The former option finishes the case. When Dr. A chooses the latter option she is obliged to make an appropriate note in the the patient’s medical record and provide the information about real possibilities of obtaining abortion from another doctor or another medical institution.

What does it mean in practice? Since there is no institution coordinating abortion services nor any official list of institutions and specialists willing to perform an abortion the only thing Dr. A can really do is to point out some other physician, let’s say Dr. B. However, Dr B. may also make use of the conscience clause. This is possible even if Dr. A justifiably believes that Dr. B will perform the abortion. It may be the case that Dr. B. has just recently changed his mind about abortion.

Such a situation may even recur several times. However, at some point Art. 30 of the Act on the professions of a doctor and a dentist enters into the scenario. Since abortion in our case is allowed until the 12th week of the pregnancy the case becomes urgent because of the passage of time. Thus the doctor who is asked at the last moment, say Dr. T, cannot make use of the conscience clause and is obliged to perform the abortion.

Alternatively, at some point there may be no more doctors available. Each doctor that refrains from performing abortion has to introduce that information into the patient’s medical record. Thus, each subsequent doctor has the access to the list of the ones that have previously refused. The Act on the professions of a doctor and a dentist mentions the real possibilities of obtaining abortion. We assume that such a provision entails that the woman should not be forced to travel a long way etc. Thus, a doctor that is last on the list of doctors in the neighbourhood, say Dr. Z, not being able to point out a real alternative, should provide the abortion service by herself.

This scenario may seem awkward because of the requirement imposed on a woman to repeat her claim for abortion iteratively. There is no efficient and reliable procedure of executing the right to get the abortion service.Footnote 3 Still, in our opinion, the existing laws do not provide any better solution. We will be interested in the formalisation of the as-is situation rather than showing how to improve it.

2.2 Print shop and the discrimination problem

Another example we want to discuss is based on a real-life situation in which balance between freedom of speech and preventing discrimination on the one hand, and freedom of enterprise and conscience on the other hand, is to be found.

An LGBT organisation wanted to get a roll-up poster printed. Certainly freedom of expression allows for it and even more: makes it a protected right if only the content is not illegal. A print shop owner, initially interested in doing the job, after getting to know the content of the poster refused to print it because of his conservative views. He informed the organisation of his refusal to print the poster with the received graphics on the grounds that his company does not contribute to the promotion of LGBT movements.

The LGBT organisation claimed that it is a case of discrimination. The print shop owner’s defence was based on the argument that he could rightfully do so because of freedom of enterprise and freedom of conscience.

Formally the accusation was based on article 138 of the Polish Code of offences:

Whoever, when dealing professionally in the provision of services, demands and charges for a payment higher than the one in force or intentionally without a valid reason, refuses the service to which he is obliged is subject to a fine.

Court of first instance sentenced the print shop owner to a fine of 200 Polish Zloty (approx. 50 Euro) for refusing the service. The appeal court upheld the decision—recognising the printer’s responsibility for the offence. The court, however, annulled the fine.

The final verdict of the court did not stop the discussion. Where should be the demarcation line between the lawful freedom allowing to choose business partners and clients in accordance with personal preferences on the one hand and discrimination on the other hand?Footnote 4

We want to find a solution that is balanced and satisfying for both parties involved. Thus, the solution should enable the organisation to have the poster printed and, if possible, nobody should be forced to provide services against his or her will. Thus, if there is another easily available print shop, the organisation should approach it.Footnote 5

2.3 An informal outline of a solution

We shall now look for the common content of the two examples and generalise it. In both examples we want to protect a right to have an abortion under certain circumstances in one case, and on freedom of expression in the other one. In both cases the subject cannot realise their right without the contribution of other parties: in this case a physician or print shop.

Our understanding of rights follows Mill (1979, p. 309), who claims that “[w]hen we call anything a person’s right, we mean that he has a valid claim on society to protect him in the possession of it, either by the force of law, or by that of education and opinion.” Nowadays, such protection is commonly extended to include not only interference against one’s enjoyment of a right but also enabling this enjoyment. Thus, we expect that in the case of rights there must be a way in which a person or organisation possessing a right is able to exercise it with the contribution of other members of the society when such a contribution is necessary.

We can even go further and reduce rights to procedures. Then, we can state that a person has a right to something if and only if there is a procedure based on legal or conventional norms that allows him or her to obtain it. We will use this equivalence to define rights in Sect. 3.

There are many subjects (physicians and print shops) that can be helpful and any of them individually may have reasons to refuse co-operation. However, this refusal cannot prevent a party from fulfilling their rights. Moreover, the subjects are independent and do not form a coordinated structure.

How can we now derive an individual obligation from rights in this context? Our basic intuition is that if a right of an agent cannot be upheld without an action of another agent, then that action is obligatory for that agent. Who and when exactly is obliged to contribute to the realisation of justified claims towards society in our examples? We propose the solution in which the last available potential contributor is obliged to help when all the others refuse. There may be many intuitive objections to this solution. We may, for example, ask why one’s obligation should depend on a somehow random sequence of choices of the agent exercising their right or why this agent should be forced to perform an extra effort to ask for assistance many times in order to fulfil their right in the situation with many refusals. Nonetheless, we believe that the solution is worth discussing and formalisation is a good way to explore its details and consequences.

We can express this solution in terms of Hohfeldian power. If, in our example, the client requests a service from a printer company, normally the client does not have legal power to create a duty. However, if that printer company is the only one (or the last one to ask) that can satisfy the request of the client, then the client has the power to create the duty. Thus, power plays a fundamental role here, although we will not introduce it explicitly to our logical language sticking to the notions of obligation usual for deontic logic.Footnote 6

Since, in our opinion, both our examples have the same structure, in Sect. 4 we will limit ourselves to the latter one. The transfer of the solution to the former one is straightforward.

2.4 Expected features of the formalism

Now let us consider the features of the modelling tools needed for the formalisation of our subject. In order to formalise our scenarios and proposed solutions we would like to be able to express:

  1. (i)

    how the world changes: situations (states of affairs, actual and possible worlds at different moments of time) and transition between situations;

  2. (ii)

    which situations and transitions are good and which are bad;

  3. (iii)

    what agents do and how actions of different agents contribute to the occurrence of a transition;

  4. (iv)

    which rights are to be protected by the normative system;

  5. (v)

    which acts of the agents are obligatory.

Ad (i) At each step of our scenarios we deal with a certain situation. We need to represent the features of those situations. Moreover, we need to represent how the scenarios can develop, i.e. how the world can evolve and change when moving from one situation to another, especially which transitions are possible.

Ad (ii) In the modelling we cannot limit ourselves to the purely descriptive aspect of reality and its changes. The important aspect that we need to capture is their evaluation. Good (acceptable, desired) states and transitions have to be distinguished from bad (unacceptable, undesired) ones.

Ad (iii) Another important element of our scenarios is the behaviour of agents. We need to be able to name the actions they undertake and to record their effects: trace the results of particular actions or the way how actions of different agents compose to cause a transition. A poster is printed because somebody ordered to print it and somebody else actually did the job. These two activities contribute to the transition between two situations.

Ad (iv) We have already mentioned in the introductory section that modelling rights is one of the main challenges, especially because we want to understand these notions in terms of actions and transitions between states of affairs. In those terms we need to express the fact that a woman is permitted to obtain the abortion service or that an organisation has the right to have posters printed.

Ad (v) Representing action guiding obligations is the other difficulty mentioned in the introductory section. We need such obligations to answer the main questions in our examples: which doctor is obliged to provide the abortion service or is the printer obliged to print the poster.

3 Formal account

This section describes the formal framework that will be used in the modelling of the examples described above. The framework fulfils all the requirements listed in the previous section. It has been introduced by Sergot and Craven in the series of papers (Sergot and Craven 2006; Sergot 2008; Craven and Sergot 2008; Sergot 2014) under the name \(n\mathcal {C}+\). In the following subsections, we describe the features of \(n\mathcal {C}+\) that are needed to express our scenarios: a labelled transition system and a language that allows us to talk about states and transitions within that system, global norms, agent-specific norms some other features concerning agency and finally the deontic notions of obligation and prohibition. In this section we do not go beyond Sergot and Craven’s formalism. Further, in Sects. 4.2 and 4.3, we extend \(n\mathcal {C}+\) by introducing definitions of right and procedure.

3.1 A label transition system and its language

The basic element of the model is a labelled transition (see Fig. 1).

Fig. 1
figure 1

A labelled transition \(\tau = (s, \varepsilon , s')\)

Full size image

From the formal point of view, transitions are triples of the form “\((s, \varepsilon , s')\)”, where s and \(s'\) belong to a (non-empty) set of states S and \(\varepsilon\) is an element of A, i.e. a set of event (action) types also called “labels”. All transitions belong to the set \(R \subseteq S\times A \times S\). Following Sergot and Craven we shall use Greek letter \(\tau\) (sometimes with numerical indexes) to refer to the transitions.

In order to refer to the elements of a transition \(\tau = (s, \varepsilon , s')\) the following two functions are defined: \(prev(\tau )\) that returns the initial state of the transition \(\tau\), so \(prev(\tau )=s\), and \(post(\tau )\) that returns the resulting state of the transition \(\tau\), so \(post(\tau )=s'\)

Structure

$$\begin{aligned} \langle S, A, R, prev, post \rangle \end{aligned}$$

is called a labelled transition system (LTS).

A two-sorted language of \(n\mathcal {C}+\) allows us to talk both about the properties of states and the properties of transitions. We have the following two sets of atomic propositions:

  • \(P_f\)—a set of propositional atoms for expressing properties of states (e.g. the poster is printed),

  • \(P_a\)—a set of propositional atoms for expressing properties of transitions (e.g. client asks for printing the poster).

Below we introduce logical operators that will allow us to create compound formulas expressing some chosen properties of states and transitions. Thus we have

  • formulas to describe states:

    $$\begin{aligned} F \;\; {::}= \;\; \text{ any } \text{ atom } p \text{ of } P_f \mid \lnot F\mid F\wedge F \mid \underset{\rightarrow }{\Box }\varphi \end{aligned}$$

  • formulas to describe transitions:

    $$\begin{aligned} \varphi \;\; {::}= \;\; \text{ any } \text{ atom } \alpha \text{ of } P_a \mid \lnot \varphi \mid \varphi \wedge \varphi \mid \text{0: }F\mid 1:F\mid \Box \varphi \end{aligned}$$

In both sorts negation ‘\(\lnot\)’ and conjunction ‘\(\wedge\)’ are understood classically. The operators: ‘\(\underset{\rightarrow }{\Box }\)’, ‘\(\text{0: }\)’ and ‘1 : ’ play the role of bridges between the two sorts. Intuitively, ‘\(\underset{\rightarrow }{\Box }\varphi\)’ says that all transitions from the given state are \(\varphi\). ‘\(\text{0: }F\)’ is satisfied by transitions whose initial state satisfies F and ‘1 : G’ by transitions whose resulting state satisfies G. For a given transition \(\tau\), ‘\(\Box \varphi\)’ says that all transitions that initiate in the same state as \(\tau\) are \(\varphi\) (so the meaning of \(\Box \varphi\) is essentially the same as \(\underset{\rightarrow }{\Box }\varphi\)—they differ in the evaluation point—the first one is evaluated in the transitions, whereas the other one in the states).

The remaining classical operators of disjunction (\(\vee\)), implication (\(\rightarrow\)) and equivalence (\(\equiv\)), as well as modal operators \(\underrightarrow{\Diamond }\) and \(\Diamond\) dual respectively to \(\underset{\rightarrow }{\Box }\) and \(\Box\) are defined in the standard way.

The meaning of the \(n\mathcal {C}+\) formulas is provided formally by reference to the following model:

$$\begin{aligned} \mathcal M= \langle LTS, h^f, h^a\rangle , \end{aligned}$$

where \(h^f\) and \(h^a\) are assignment functions such that \(h^f: P_f\longrightarrow 2^S\) and \(h^a: P_a\longrightarrow 2^R\). Satisfaction conditions are defined as follows:

$$\begin{aligned} \begin{array}{lcl} \mathcal M, s \models p &{} \iff &{} s\in h^f(p)\\ \mathcal M, s \models \underset{\rightarrow }{\Box }\varphi &{} \iff &{} \mathcal M, \tau \models \varphi for every \tau \in R s.t. prev(\tau ) = s\\ \mathcal M, \tau \models \alpha &{} \iff &{} \tau \in h^a(\alpha )\\ \mathcal M, \tau \models \text{0: }F &{} \iff &{} \mathcal M, prev(\tau ) \models F\\ \mathcal M, \tau \models 1: F &{} \iff &{} \mathcal M, post(\tau ) \models F\\ \mathcal M, \tau \models \Box \varphi &{} \iff &{} \mathcal M, \tau ' \models \varphi for every \tau ' s.t. prev(\tau ) = prev(\tau ')\\ \end{array} \end{aligned}$$

Figures 2 and 3 illustrate the meaning of operators characterised by the satisfaction conditions above.

Fig. 2
figure 2

If \(\mathcal M, s\models F\) and \(\mathcal M, s'\models G\), then \(\mathcal M, \tau \models \text{0: }F \wedge 1: G\), providing \(\tau = (s, \varepsilon , s')\)

Full size image
Fig. 3
figure 3

\(\mathcal M, s\models \underset{\rightarrow }{\Box }\varphi\) and \(\mathcal M, \tau \models \Box \varphi\) providing \(prev(\tau ) = s\)

Full size image

We say a state formula F is valid in a model \(\mathcal M\), written \(\mathcal M\models F\) , when \(\mathcal M, s \models F\) for every state s in S, and a transition formula \(\varphi\) is valid in a model \(\mathcal M\), written \(\mathcal M\models \varphi\), when \(\mathcal M,\tau \models \varphi\) for every transition \(\tau\) in R.

We shall also use truth sets for transitions and states. For a given model \(\mathcal M\), a transition formula \(\varphi\) and a state formula F, the truth set \(\left\| \varphi \right\|^{\mathcal{M}}\) is the set of transitions where \(\varphi\) is satisfied and \(\left\| F \right\|^{\mathcal{M}}\) is the set of states where F is satisfied:

$$\begin{aligned}&\Vert \varphi \Vert ^{{\mathcal{M}}}={_{def} }\{ \tau \in R\; | \; \mathcal M, \tau \models \varphi \} \end{aligned}$$
(1)
$$\begin{aligned}&\Vert F\Vert ^{{\mathcal{M}}}={_{def} }\{ s \in S\; | \; \mathcal M, s \models F\} \end{aligned}$$
(2)

Any subset of R, so any truth set \(\left\| \varphi \right\|^{\mathcal{M}}\), we shall call an action type and any subset of S, so any truth set \(\left\| F \right\|^{\mathcal{M}}\)—a description of a state of affairs.

3.2 Global norms in LTS

By global norms we understand those norms which do not refer to any specific agent and just assess some states or transitions as good or bad in general. To talk about them the labelled transition system has been extended with two sets—one for states and another one for transitions: \(S_{red}\) and \(R_{red}\), respectively. \(S_{red}\subseteq S\) is a set of forbidden (‘red’) states of the system and \(R_{red}\subseteq R\) is a set of forbidden (‘red’) transitions of the system. States or transitions that are not red are permitted (‘green’). The sets of green states and transitions are denoted by \(S_g\) and \(R_g\), respectively.

The sequence in which we introduce colours is not random. It is prohibition that introduces norms and permission is just the absence of prohibition. Thus, if there is a reason for a state or transition to be forbidden it is coloured red and in the opposite case it is assumed green. We may also interpret this way of colouring as encoding a liberal attitude towards normative system: whatever is not forbidden is permitted.Footnote 7

To refer to the normative sets, Sergot and Craven introduced four normative atoms: \(status = green, status = red\in P_f\) and \(trans = green, trans = red\in P_a\). They have the following interpretation:

$$\begin{aligned} \begin{array}{lcl} {\mathcal{M}}, s \models {{ status=red}} &{} \iff &{} h^f( {{ status=red}})=S_{red}\\ {\mathcal{M}}, s \models {{ status=green}} &{} \iff &{} h^f( {{ status=red}})=S_{g}\\ {\mathcal{M}}, \tau \models {{ trans=red}} &{} \iff &{} h^a({{ trans=red}})=R_{red}\\ {\mathcal{M}}, \tau \models {{ trans=green}} &{} \iff &{} h^a({{ trans=red}})=R_{g}\\ \end{array} \end{aligned}$$
$$\begin{aligned}&\Vert trans = green\Vert ^{{\mathcal{M}}} = R_g \end{aligned}$$
(3)
$$\begin{aligned}&\Vert trans = red\Vert ^{{\mathcal{M}}} = R_{red} \end{aligned}$$
(4)
$$\begin{aligned}&\Vert status = green\Vert ^{{\mathcal{M}}} = S_g \end{aligned}$$
(5)
$$\begin{aligned}&\Vert status = red\Vert ^{{\mathcal{M}}}= S_{red} \end{aligned}$$
(6)

Thus for a given model \({\mathcal{M}}\), \(\Vert trans = green\Vert ^{{\mathcal{M}}}\) is the most general green action type and \(\Vert trans = red\Vert ^{{\mathcal{M}}}\)—the most general red one. \(\Vert status = green\Vert ^{{\mathcal{M}}}\) is the most general description of all green states of affairs and \(\Vert status = red\Vert ^{{\mathcal{M}}}\)—the most general description of all red states of affairs.

Consistency and closedness of the normative colouring of states and transitions is guaranteed:

$$\begin{aligned}&{\mathcal{M}}\models \lnot status = red \equiv status = green \end{aligned}$$
(7)
$$\begin{aligned}&{\mathcal{M}}\models \lnot trans = red \equiv trans = green \end{aligned}$$
(8)

The normative sets for states and transitions are related by ggg constraint (well-formedness principle)Footnote 8 stating that a green (permitted, acceptable, legal) transition in a green state always leads to a green state:

$$\begin{aligned} \text{ if } \tau \in R_g \text{ and } prev(\tau )\in S_g \text{, } \text{ then } post(\tau )\in S_g \end{aligned}$$
(9)

On the level of language the ggg principle is represented by the following transition formula:

$$\begin{aligned} {\mathcal{M}}\models trans = green \wedge \text{0: }status = green \rightarrow 1: status = green \end{aligned}.$$
(10)

3.3 Agent specific norms in LTS

Agents have been introduced into the picture by a finite set of agents Ag. For every agent \(x \in Ag\), \(R^x_{red}\) (where \(R^x_{red}\subseteq R\)) is a set of (red/illegal) transitions, i.e. the transitions that do not comply with the agent-specific norms that govern x’s individual actions.

$$\begin{aligned} R^x_{g} = R\setminus R^x_{red} \end{aligned}$$
(11)

To refer to the the agent-specific normative sets, for each agent \(x\in Ag\), Sergot and Craven introduced two normative atoms: \(green(x), red(x)\in P_a\). They have the following interpretation:

$$\begin{aligned}&\Vert green(x)\Vert ^{{\mathcal{M}}}= R^x_{g} \end{aligned}$$
(12)
$$\begin{aligned}&\Vert red(x)\Vert ^{{\mathcal{M}}}= R^x_{red} \end{aligned}$$
(13)

Normative consistency of the agent-specific norms is valid in the model:

$$\begin{aligned} {\mathcal{M}}\models \lnot (green(x)\wedge red(x)) \end{aligned}$$
(14)

Sergot and Craven assumed the local-global coherence constraint stating that if any of the agents fails to satisfy its standards of legality then so does the system as a whole (in other words, if a transition is red for some agent x then it is also globally red), formally:

$$\begin{aligned} \text{ for } \text{ all } \text{ agents } x\in Ag\text{, } R^x_{red}\subseteq R_{red} \end{aligned}$$
(15)

It is worth noting that the constraint allows, for a given transition \(\tau \in R\), that \(\tau\) is globally red, whereas it is green for all agents x from Ag, i.e., it it possible that at the same time \(\tau \in R_{red}\) and \(\tau \in R^x_{g}\) for every agent \(x\in Ag\).

On the level of language the constraint is represented by the following formula:

$$\begin{aligned} {\mathcal{M}}\models red(x) \rightarrow trans = red \end{aligned}$$
(16)

For the modelling of the examples described above, we will need a stronger version of that principle, absent in the original \(n\mathcal {C}+\), stating (in addition to the principle 15) that the global assessment of the system is dependant only on the assessment of the acting agents. It is a modification of \(n\mathcal {C}+\) appropriate for the applications in which, like in our examples, everything that is relevant to the normative evaluation is connected with agents. In other words the principle means that if \(\tau \in R_{red}\), then there must exist \(x\in Ag\) s.t. \(\tau \in R^x_{red}\) (i.e. if there is something wrong with a transition there must be someone who has spoilt it):

$$\begin{aligned} \text{ for } \text{ all } \text{ agents } x\in Ag\text{, } R_{red} \subseteq \bigcup _{x\in Ag} R^x_{red} \end{aligned}$$
(17)

On the level of language we can express this constraint as follows:

$$\begin{aligned} {\mathcal{M}}\models trans = red \rightarrow red(a_1) \vee \dots \vee red(a_n), \text{ where } \{a_1,\dots , a_n\} = Ag \end{aligned}$$
(18)

3.4 Agency

Since LTS might be a nondeterministic structure, Sergot in Sergot (2014) introduced relation \(\sim _x\) defined as follows:Footnote 9

$$\begin{aligned} \begin{aligned} \sim _x \;=_{def}\; \{(\tau ,\tau ') \;|\, prev(\tau )=prev(\tau ') \text{ and } x \text{ performs } \text{ the } \text{ same } \text{ action } \text{ in } \tau ' \text{ as } \text{ it } \text{ does } \text{ in } \tau .\} \end{aligned} \end{aligned}$$
(19)

This relation is used to define STIT-like choices (Belnap 2001) (i.e. the groups of transitions initiating in the same moment where the agent performs the same action):

$$\begin{aligned} alt_x(\tau )\,=\,_{def} \{\tau ' | \tau \sim _x\tau '\} \end{aligned}$$
(20)

Then it is possible to define agency STIT-like operators in the language. By ‘\([x]\varphi\)’ we shall mean an agency operator that is evaluated in the transitions. It is true at a give transition iff \(\varphi\) is necessary for how the agent x acts in the transition. Its satisfaction condition is defined as follows:

$$\begin{aligned} \begin{array}{lcl} {\mathcal{M}}, \tau \models [x]\varphi \quad &{} \iff &{}\quad alt_x(\tau )\subseteq \Vert \varphi \Vert ^{{\mathcal{M}}}\\ \end{array} \end{aligned}$$

Expressing agency and possible agent’s choices in a given situation is the key to modelling the examples we’ve introduced above. We need to know and be able to express what an agent can bring about and what she or he is responsible for. It is worth noting that STIT operators and the concept of choice introduced by Sergot and Craven differ from the concepts described by Belnap in Belnap (2001). \(n\mathcal {C}+\) choices group transitions, not histories, and \(n\mathcal {C}+\) STIT operators express agent’s responsibility for carrying out actions, whereas standard STIT operators describe the responsibility of agents for the states of affairs.

For modelling of the examples we will also need to refer to joint actions of groups of agents. For that purpose, following Sergot (2014), we define the set \(alt_G(\tau )\) of transitions initiating in the same state in which every agent in G performs the same action as it does in \(\tau\):

$$\begin{aligned} alt_G(\tau ) =\,_{def} \bigcap _{x\in G} alt_x(\tau ), G\subseteq Ag \end{aligned}$$
(21)

\(alt_G(\tau )\) is a representation of the joint action performed by the group G in the transition \(\tau\). On the level of language the joint action is represented by the transition formula “\([G]\varphi\)”. \([G]\varphi\) is true at \(\tau\) iff \(\varphi\) is necessary for how the agents G collectively act in \(\tau\):

$$\begin{aligned} \begin{array}{lcl} {\mathcal{M}}, \tau \models [G]\varphi \quad &{} \iff &{} \quad alt_G(\tau )\subseteq \Vert \varphi \Vert ^{{\mathcal{M}}}and alt_G(\tau ) \not =\emptyset \\ \end{array} \end{aligned}$$

Following Horty we will use agency operators that have “the negative condition—which enforces the idea that an agent cannot be said to see to it that A if he really has no choice in the matter, if the truth of A is guaranteed no matter which action he performs” (John 2001, p. 16). So we shall have two operators of agency that imply that “\(\varphi\)” is not necessary:

$$\begin{aligned}&E_x\varphi\,\equiv\,_{def} [x]\varphi \wedge \lnot \Box \varphi \end{aligned}$$
(22)
$$\begin{aligned}&E_G\varphi\,\equiv \,_{def} [G]\varphi \wedge \lnot \Box \varphi \end{aligned}$$
(23)

By the operators we are able to express the fact that \(\varphi\) is necessary for how the agent x (or the group of agents G) act(s) but at the same time we ensure that \(\varphi\) is not necessary (in the non-agentive sense), i.e. if x (or the group of agents G) had acted differently, \(\varphi\) might not have happened.

3.5 Agency and norms

The final step in our preparatory phase concerns moral responsibility. We shall assume absence of ‘moral luck’ (see Craven and Sergot 2008). Formally the principle has the following shape:

$$\begin{aligned} \text{ if } \tau \sim _x \tau ' \text{, } \text{ then } (\tau \in R^x_g \text{ iff } \tau ' \in R^x_g). \end{aligned}$$
(24)

The principle says that the moral value of the agent x’s action depends only on the type of action she/he carries out. Factors independent of the agent’s action are not taken into account since the colour of a transition is the same for transitions to which the agent contributes in the same way.Footnote 10

Absence of moral luck on the language level is expressed by the formula below:

$$\begin{aligned} {\mathcal{M}}\models green(x) \rightarrow [x]green(x) \end{aligned}$$
(25)

If \(\tau\) is a green transition from a state s, then every transition \(\tau '\) from state s in which agent x behaves in the same way as it does in \(\tau\) must also be green.

All of these steps led us to definitions of deontic operators. Obligation and prohibition are defined in the Andersonian–Kangarian style as follows:

$$\begin{aligned}&\mathsf O_x(\varphi )\,\equiv\,_{def} \underset{\rightarrow }{\Box }(green(x)\rightarrow \varphi ) \end{aligned}$$
(26)
$$\begin{aligned}&\mathsf F_x(\varphi )\,\equiv\,_{def} \underset{\rightarrow }{\Box }(\varphi \rightarrow red(x)) \end{aligned}$$
(27)

Technically both operators forms state formulas: some actions are obligatory or forbidden in a certain state and this is a property of that state. We say that \(\varphi\) is obligatory for x in a state s iff all transitions that take their beginning in s and are green for x are \(\varphi\) and \(\varphi\) is forbidden for x in a state s iff all \(\varphi\)-transitions that take their beginning in s are red. In other words the action \(\varphi\) is obligatory if its extension contains all allowed (green) transitions and the action \(\varphi\) is forbidden if its extension does contains no green transitions—cannot be performed in an acceptable (green) way. Such definitions make our deontic operators similar to the ones of standard deontic logic (SDL). Although such an interpretation of obligation and prohibition has been criticised, for our purposes it is sufficient and suitable.

4 Examples formalised

4.1 Non-normative description

The two examples in the interpretation presented in Sect. 2.3 share the same structure. Thus we will just present the formal account of one of them: the one concerning print shop owners. For the sake of simplicity we assume that there are only two print shops available. Figure 4 depicts the possible course of actions. The same situation can be described by a STIT-like model (see Fig. 5).

Fig. 4
figure 4

Labelled transition system for the print shop example limited to two available print shops: a purely descriptive account

Full size image
Fig. 5
figure 5

STIT-like model for the print shop example limited to two available print shops

Full size image

In the initial state \(s_1\) the poster is not printed:

$$\begin{aligned} {\mathcal{M}}, s_1 \models \lnot printed \end{aligned}$$
(28)

Client c in \(s_1\) has two choices: he can ask the printer \(p_1\) to carry out printing or can ask the printer \(p_2\) to carry out printing but he cannot ensure that the poster is printed in the next states:

$$\begin{aligned}&\{\tau _5,\tau _4\} = \Vert \text{0:}\,\lnot printed \wedge E_c (c \text{ asks } p_2)\wedge \lnot E_c (1{:}\,printed)\Vert ^{{\mathcal{M}}}\end{aligned}$$
(29)
$$\begin{aligned}&\{\tau _0,\tau _1\} = \Vert \text{0:}\,\lnot printed \wedge E_c (c \text{ asks } p_1)\wedge \lnot E_c (1{:}\,printed)\Vert ^{{\mathcal{M}}}\end{aligned}$$
(30)

So there is no transition from \(s_1\) where it is true that \(E_{c} (1{:}\,printed)\), i.e. agent c himself cannot make sure that the poster is printed:

$$\begin{aligned} {\mathcal{M}}, s_1 \models \lnot \underrightarrow{\Diamond }E_{c} (1{:}printed) \end{aligned}$$
(31)

But there are transitions in which a group of agents including agent c can make it happen. For instance, c and \(p_2\) can make sure in \(s_1\) that the poster is printed:

$$\begin{aligned} {\mathcal{M}}, s_1 \models \underrightarrow{\Diamond }E_{\{c,p_2\}} (1{:}\,printed) \end{aligned}$$
(32)

Agents c and \(p_1\) in states \(s_1\) and \(s_3\) can make sure that the poster is printed (though in \(s_1\) two steps are needed for this):

$$\begin{aligned}&{\mathcal{M}}, s_3 \models \underrightarrow{\Diamond }E_{\{c,p_1\}} (1{:}\,printed) \end{aligned}$$
(33)
$$\begin{aligned}&{\mathcal{M}}, s_1 \models \underrightarrow{\Diamond } 1: \underrightarrow{\Diamond }E_{\{c,p_1\}} (1{:}\,printed) \end{aligned}$$
(34)

4.2 Rights

To model rights there must be a way in which a person or organisation possessing the right is able to exercise it with the contribution of other members of the society when such a contribution is necessary. Thus, in the case of our example, the dependency of a LGBT organisation c possessing the right from the owners of the printing shops (\(p_1\) and \(p_2\)) can be modelled by the formula that guarantees that in any circumstances c together with one of the printers can bring about that the poster is printed in the next step or n-number of steps, formally:

$$\begin{aligned} \begin{aligned}&\underrightarrow{\Diamond }E_{\{c,p_{1}\}} (1{:}\,printed) \;\vee \underrightarrow{\Diamond }E_{\{c,p_{2}\}} (1{:}\,printed) \;\vee \\&\underrightarrow{\Diamond } 1: \underrightarrow{\Diamond }E_{\{c,p_{1}\}} (1{:}\,printed) \;\vee \underrightarrow{\Diamond } 1: \underrightarrow{\Diamond }E_{\{c,p_{2}\}} (1{:}printed) \;\vee \\&\underrightarrow{\Diamond } 1: \underrightarrow{\Diamond } 1: \underrightarrow{\Diamond }E_{\{c,p_{1}\}} (1{:}\,printed) \;\vee \underrightarrow{\Diamond } 1: \underrightarrow{\Diamond } 1: \underrightarrow{\Diamond }E_{\{c,p_{2}\}} (1{:}\,printed) \;\vee \\&\dots \\&\underrightarrow{\Diamond } 1: \dots \underrightarrow{\Diamond }E_{\{c,p_{1}\}} (1{:}\,printed) \;\vee \underrightarrow{\Diamond } 1: \dots \underrightarrow{\Diamond }E_{\{c,p_{2}\}} (1{:}\,printed) \end{aligned} \end{aligned}$$
(35)

We can generalize it for n printers:

$$\begin{aligned} \begin{aligned}&\underrightarrow{\Diamond }E_{\{c,p_{1}\}} (1{:}\,printed) \;\vee \dots \;\vee \underrightarrow{\Diamond }E_{\{c,p_{n}\}} (1{:}printed) \;\vee \\&\underrightarrow{\Diamond } 1: \underrightarrow{\Diamond }E_{\{c,p_{1}\}} (1{:}\,printed) \;\vee \dots \;\vee \underrightarrow{\Diamond } 1: \underrightarrow{\Diamond }E_{\{c,p_{n}\}} (1{:}\,printed) \;\vee \\&\underrightarrow{\Diamond } 1: \underrightarrow{\Diamond } 1: \underrightarrow{\Diamond }E_{\{c,p_{1}\}} (1{:}\,printed) \;\vee \dots \;\vee \underrightarrow{\Diamond } 1: \underrightarrow{\Diamond } 1: \underrightarrow{\Diamond }E_{\{c,p_{n}\}} (1{:}\,printed) \;\vee \\&\dots \\&\underrightarrow{\Diamond } 1: \dots \underrightarrow{\Diamond }E_{\{c,p_{1}\}} (1{:}\,printed) \;\vee \dots \;\vee \underrightarrow{\Diamond } 1: \dots \underrightarrow{\Diamond }E_{\{c,p_{n}\}} (1{:}\,printed) \end{aligned} \end{aligned}$$
(36)

To simplify the formulas introduced above we shall define n-step-can operator:

$$\begin{aligned}&Can_G^{1} \varphi \equiv _{def} \underrightarrow{\Diamond } E_{G} \varphi \end{aligned}$$
(37)
$$\begin{aligned}&Can_G^n \varphi \equiv _{def} \underrightarrow{\Diamond } 1{:}Can_G^{n-1} \varphi \end{aligned}$$
(38)

So for two printers the formula below expresses the same as the formula (36):

$$\begin{aligned} Can_{\{c,p_{1}\}}^n 1\text{: }printed \vee Can_{\{c,p_{2}\}}^n 1\text{: }printed \end{aligned}$$
(39)

We define a state formula “\(PROCED_c^{\{p_1,\dots , p_k\}} (F)\)” stating that c has procedure that guarantees that F by collective act with agents from \(\{p_1,\dots , p_k\}\):

$$\begin{aligned} PROCED_c^{\{p_1,\dots , p_k\}} (F) \equiv _{def} F \vee Can_{\{c,p_{1}\}}^n 1\text{: }F \vee \dots \vee Can_{\{c,p_{k}\}}^n 1\text{: }F \end{aligned}$$
(40)

The fact that F being true is enough for \(PROCED_c^{\{p_1,\dots , p_k\}} (F)\) can be treated as a border case.

The existence of a procedure of bringing about F can be a necessary or even sufficient condition (if there is only one norm) for states to be legally acceptable. In our printing shop example all states where \(PROCED_c^G (printed)\) is true should be green:

$$\begin{aligned} {\mathcal{M}}\models state = green\equiv PROCED_c^G (printed) \end{aligned}$$
(41)

A weaker version of the formula (41) with (left to right) implication can be understood as definiens of the procedural definition of right proposed in Sect. 2.3. c has a right that agents from G will guarantee that F is/will be the case iff a state is green providing c has a procedure that guarantees that F by collective act with agents from G:

$$\begin{aligned} RIGHT_c^G (F) \equiv _{def} state = green\rightarrow PROCED_c^G (F) \end{aligned}$$
(42)

4.3 From rights to obligation

In this section we shall reconstruct step by step how the obligation to print a poster arises from the rights of the LGBT organization. The model without normative aspects is depicted in Fig. 4.

We shall start from assuming that the right to print a poster should be valid in the model:

$$\begin{aligned} {\mathcal{M}}\models RIGHT_c^{\{p_1,p_2\}} (printed) \end{aligned}$$
(43)

As far as the procedure to print the poster is concerned we have:

  • \(\{s_1,s_2,s_3,s_4\} = \Vert PROCED_c^{\{p_1,p_2\}} (printed)\Vert ^{{\mathcal{M}}}\)

  • \(\{s_5\} = \Vert \lnot PROCED_c^{\{p_1,p_2\}} (printed)\Vert ^{{\mathcal{M}}}\)

Thus because of (41) we have

  • \(\{s_1,s_2,s_3,s_4\} = \Vert state = green\Vert ^{{\mathcal{M}}}\)

  • \(\{s_5\} = \Vert state = red\Vert ^{{\mathcal{M}}}\)

That gives the labelled transition system with state colouring presented in Fig. 6.

Fig. 6
figure 6

Printers with colours

Full size image

Because of ggg principle (formula 10) we have:

  • \(\{\tau _3,\tau _7\} = \Vert trans = red\Vert ^{{\mathcal{M}}}\)

And because of formula (8)

  • \(\{\tau _0,\tau _1,\tau _2,\tau _4,\tau _5,\tau _6\} = \Vert trans = green\Vert ^{{\mathcal{M}}}\)

Thus (from 16) in the globally green transitions it is true that all agent-specific norms are green:

  • \(\{\tau _0,\tau _1,\tau _2,\tau _4,\tau _5,\tau _6\} = \Vert green(c)\wedge green(p_1) \wedge green(p_2)\Vert ^{{\mathcal{M}}}\)

In \(\tau _3\) and \(\tau _7\) where it is true that \(trans = red\), because of absence of moral luck (formula 25) we have:

  • \({\mathcal{M}}, \tau _3\models green(c)\wedge green(p_1)\)

  • \({\mathcal{M}}, \tau _7\models green(c)\wedge green(p_2)\)

and because of strong local-global coherence (formula 18):

  • \({\mathcal{M}}, \tau _3\models red(p_2)\)

  • \({\mathcal{M}}, \tau _7\models red(p_1)\)

And finally by definition (26) we have that:

  • \({\mathcal{M}}, s_3 \models \mathsf O_{p_1}(p_1 \text{ prints})\)

  • \({\mathcal{M}}, s_2 \models \mathsf O_{p_2}(p_2 \text{ prints})\)

5 Conclusions and future work

We presented important, controversial and evoking public interest normative systems concerning abortion and prevention from discrimination in the context of freedom of conscience. In order to better understand and interpret them we represented their core issues within a formal system. We used the labelled transition system \(n\mathcal {C}+\).

We introduced a representation of rights of one agent and a representation of obligations of other agents induced by those rights. We believe that this is an important contribution of this paper since the complex formal representation of these phenomena is not common in the literature. Rights are introduced to the system as procedures allowing for their fulfilment. Obligations are based on the requirement of cooperation in the realisation of goals of the agent that has a right. If a right of an agent cannot be fulfilled without an action of another agent, then that action is obligatory for that agent. If there are many potential contributors who are individually allowed to refuse, then the last of them is obliged to help when all the others have already refused. Our intuitive solution proves to be consistent and to lead to the notion of obligation that can have an action-guiding interpretation.

Another lesson learned from the formalisation is that \(n\mathcal {C}+\) proves to be a convenient tool for our task, as it was for the formalisation of different simpler examples of normative situations discussed in Sergot (2014). Which features of \(n\mathcal {C}+\) are important and make it suitable for scenarios like our example? The most important one is that it allows us to discuss the properties of both states of affairs and actions, normative saturation of both of them and mutual relations between them. That allowed us to gradually build a model of a complex normative situation and introduce the notion of right into it.

It would be interesting to compare the formalisation proposed in this paper with the ones using other popular logical frameworks, especially STIT. Classical STIT does not allow talking about an action directly. That would make it difficult to formalise the search for obligatory actions of the type found in our examples. However, there are several extensions of STIT that include actions like (Broersen 2008; Horty and Pacuit 2017; Lorini and Schwarzentruber 2017) and they should be expressive enough for the needs of our task.

Another interesting question concerns the limitations of the approach. The computation complexity of the reasoning we conduct seems to be high. Is it a serious limitation of an application of the approach in a realistic situation? Is it possible to limit the formalism to avoid this risk?