24.01.2017  Foundations  Ausgabe 3/2018 Open Access
Deontic STIT logic, from logical paradox to security policy
 Zeitschrift:
 Soft Computing > Ausgabe 3/2018
1 Introduction
2 The miners paradox
There are 10 miners trapped in either shaft A or shaft B, but we don’t know which one. Water threatens to flood the shafts. We have sandbags to block only one shaft. If one shaft is blocked, all water will flood into the other shaft, killing all miners inside. If we block neither shaft, both will be flooded partially, killing 1 miner.
3 Deontic STIT logic

strong lifting: Let \(U_1\) and \( U_2\) be two sets of worlds, \(U_1\) is strongly at least as good as \( U_2\) iff \(\forall w\in U_1\), \(\forall v\in U_2\), w is at least as good as v.

optimistic lifting: \(U_1\) is optimistically at least as good as \( U_2\) iff \(\exists w\in U_1\), \(\forall v\in U_2\), w is at least as good as v.

pessimistic lifting: \(U_1\) pessimistically at least as good as \( U_2\) iff \(\forall w\in U_1\), \(\exists v\in U_2\), w is at least as good as v.

\(Optimal^s_{H}\) = {\(T \in Choice(H):\) there is no \(T'\in Choice(H)\) such that \(T\prec ^s_{H} T'\)}.

\(Optimal^s_{H/Y}\) = {\(T \in Choice(H/Y):\) there’s no \(T'\in Choice(H/Y)\) such that \(T\prec ^s_{H/Y}T'\)}.
3.1 Utilitarian deontic logic via pessimistic lifting
3.1.1 Language

pessimistic lifting: \(\psi \preceq ^{p} \phi {::=} \square (\phi \Rightarrow \langle \succeq \rangle \psi ) \). Informally, the formula \(\square (\phi \Rightarrow \langle \succeq \rangle \phi ) \) says that every \(\phi \)world is weakly better than some \(\psi \)world.

\(\bigcirc _i \psi {::=} (\lnot \psi \prec ^p [i]\psi ) \wedge \lozenge [i]\psi \). That is to say, agent i ought to STIT \(\psi \) if and only if in the pessimistic sense STIT \(\psi \) is strictly better than \(\lnot \psi \) and it is possible for i to STIT \(\psi \).

\(\bigcirc _i (\psi /\phi ) {::=} \lozenge [i]\psi \wedge ((\lnot \psi \wedge \phi ) \prec ^p ([i] \phi \wedge \psi ))\).
3.1.2 Semantics
3.1.3 Solving the miners paradox
3.1.4 Bonus 1: solving the contrary to duty paradox
3.1.5 Bonus 2: solving Ross’ paradox
In UDL, the formula \(\bigcirc _{H} \phi \Rightarrow \bigcirc _{H} (\phi \vee \psi )\) is valid, which means UDL cannot solve Ross’ paradox. On the other hand, PUDL solves Ross’ paradox, as the following proposition shows.Suppose John should send a letter. Since sending the letter implies sending it or burning it, John should send the letter or burn it.
3.1.6 Axiomatization of PUDL
3.2 Multiauthority deontic STIT logic
3.2.1 Language

\(\bigcirc ^{j}_i \psi {::=} (\lnot \psi \prec ^j [i]\psi ) \wedge \lozenge [i]\psi \). Intuitively, this formula means that agent i ought to see to it that \(\psi \) according to the normative value of authority j iff \(\lnot \psi \) is strictly worse than seeing to it that \(\psi \) according to the normative value of authority j and it is possible for i to see to it that \(\psi \).

\(\bigcirc ^{j}_i (\psi /\phi ) {::=} ((\lnot \psi \wedge \phi ) \prec ^j ([i]\psi \wedge \phi )) \wedge \lozenge [i]\psi \).

\(F ^{j}_i \psi {::=} \bigcirc ^{j}_i \lnot \psi \). This means according to the normative value of authority j, agent i is forbidden to STIT \(\psi \) iff i is obliged to STIT \(\lnot \psi \).

\(F^{j}_i (\psi /\phi ) {::=} \bigcirc ^{j}_i (\lnot \psi /\phi ) \).

\(P ^{j}_i \psi {::=} \lnot F ^{j}_i \psi \). This means according to the normative value of authority j, agent i is permitted to see to it that \(\psi \) iff i is not forbidden to see to it that \( \psi \).

\(P ^{j}_i(\psi /\phi ) {::=} \lnot F ^{j}_i (\psi /\phi ) \).