STIT Based Deontic Logics for the Miners Puzzle

Abstract

In this paper we first develop two new STIT based deontic logics capable of solving the miners puzzle. The key idea is to use pessimistic lifting to lift the preference over worlds into the preference over sets of worlds. Then we also discuss a more general version of the miners puzzle in which plausibility is involved. In order to deal with the more general puzzle we add a modal operator representing plausibility to our logic. Lastly we present a sound and complete axiomatization.

Appendix

Proposition 5

If every consistent $\varGamma$ is satisfiable on some model $M$, then $\varGamma \vDash _{pudl^+_2} \phi$ implies $\varGamma \vdash \phi$.

Definition 14

(Maximal Consistent Set (MCS)). A set of formulas $\varGamma$ is maximally consistent if $\varGamma$ is consistent and any proper extension of $\varGamma$ is not consistent.

For every consistent $\varGamma$, $\varGamma$ can be extended to a MCS $\varGamma ^+$, we then construct a canonical model for $\varGamma ^+$.

Definition 15

(Canonical Model). The canonical model $\mathfrak {M}^0$ for $\varGamma ^+$ is a relational structure $(W^{0}, \{R^0_i\}_{i\in Agent}, \le ^0 <^0, \le ^0_p, <^0_p, V^0 )$ where:

• $W^{0}=\{w| w \text{ is } \text{ a } \text{ MCS } \text{ and } \text{ for } \text{ all } \square \phi \in \varGamma ^+, \phi \in w \}$;

• For every $i\in Agent$, $R^0_i$ is a binary relation on $W^0$ defined by $w R^0_i v$ iff for all $\phi$, $[i] \phi \in w$ implies $\phi \in v$;

• $\le ^0$ is a binary relation on $W^0$ defined by $w\le ^0 v$ iff for all $\phi$, $[\le ] \phi \in w$ implies $\phi \in v$;

• $<^0$ is a binary relation on $W^0$ defined by $w<^0 v$ iff for all $\phi$, $[<] \phi \in w$ implies $\phi \in v$;

• $\le ^0_p$ is a binary relation on $W^0$ defined by $w\le ^0_p v$ iff for all $\phi$, $[\le _p] \phi \in w$ implies $\phi \in v$;

• $<^0_p$ is a binary relation on $W^0$ defined by $w<^0_p v$ iff for all $\phi$, $[<_p] \phi \in w$ implies $\phi \in v$;

• $V^0$ is the valuation defined by $V^0(p)=\{w\in W^0\mid p\in w\}$.

Proposition 6

$\mathfrak {M}^0, \varGamma ^+ \vDash _{pudl^+_2} \varGamma$.

Proposition 7

$\mathfrak {M}^0$ has the following properties:

• (1) Both $\le ^0$ and $\le _p ^0$ are reflexive, transitive and connected relations.

• (2) If $w\le ^0 v$ and $v\nleq ^0 w$ then $w<^0 v$.

• (3) If $w\le ^0_p v$ and $v\nleq ^0_p w$ then $w<^0_p v$.

• (4) If $w<^0 v$ then $w\le ^0 v$.

• (5) If $w<^0_p v$ then $w\le ^0_p v$.

• (6) $R^0_i$ is an equivalence relation for each $i\in Agent$.

• (7) For every $w\in W^0$, $R^0_1(w)\cap \ldots \cap R^0_n(w) \not =\emptyset$.

Deleting $<$ -cluster. Note that converse of item (2) of Proposition 7 is not true because there may be two worlds $w$ and $v$ in $W^0$ such that $w <^0 v$ and $v <^0 w$. In this case we say that $w$ and $v$ are in the same $<^0$-clusters. To deal with this we follow Benthem [25] to use the technique called Bulldozing [21] to transform $\mathfrak {M}^0$ to a new model $\mathfrak {M}^1$ such that there is no $<$-cluster in $\mathfrak {M}^1$.

Definition 16

(Cluster). A $<$-cluster is an inclusion-maximal set of worlds $C$ such that $w< v$ for all worlds $w,v\in C$. Similarly for $\le _p$-cluster.

Let $\mathfrak {M}^1 = (W^{1}, \{R^1_i\}_{i\in Agent}, \le ^1, <^1, \le ^1_p, <^1_p, V^1)$ where:

• $W^{1}= W^{0-}\cup \bigcup _{i\in I}C^{\prime }_i$, here $I$ is a set index of all $<$-clusters of $W^{0}$, $W^{0-}=W^0 - \bigcup _{i\in I}C_i$, $C^{\prime }_i = C_i\times \mathbb {Z}$, $\mathbb {Z}$ is the set of natural numbers.

• $R^1_i$ is defined by $wR^1_i v$ iff $\beta (w)R^0_i \beta (v)$, for every $i\in Agent$.

• $<^1$ is defined as follows: For each $C_i$, choose an arbitrary linear order $<^{1,i}$. Define a map $\beta : W^1\rightarrow W^0$ by $\beta (x)=x$ if $x\in W^{0-}$ and $\beta (x)=w$ if $x$ is a pair $(w,n)$ for some world $w$ and integer $n$. We define $<^1$ via the following cases:

  • Case 1: $x$ or $y$ is in $W^{0-}$. In this case we let $x <^1 y$ iff $\beta (x) <^0 \beta (y)$.

  • Case 2: $x\in C'_i$ and $y\in C'_j$, $i\ne j$. In this case we let $x <^1 y$ iff $\beta (x) <^0 \beta (y)$.

  • Case 3: $x\in C'_i$ and $y\in C'_i$. In this case, $x=(w,m)$ and $y=(v,n)$. There are two sub-cases:

    • * Case 3.1: If $m\ne n$, we use the natural ordering on $\mathbb {Z}$: $(w,m) <^1 (v,n)$ iff $m<n$.

    • * Case 3.2: If $m=n$, we use the linear ordering $<^{1,i}$: $(w,m) <^1 (v,m)$ iff $w<^{1,i} v$.

• $\le ^1$ is defined via the following cases:

  • Case 1: $x$ or $y$ is in $W^{0-}$. In this case we let $x \le ^1 y$ iff $\beta (x) \le ^0 \beta (y)$.

  • Case 2: Otherwise, we take the reflexive closure of $<^1$: $x \le ^1 y$ iff $x <^1 y$ or $x=y$.

• $\le ^1_p$ is defined by $w\le ^1_p v$ iff $\beta (w)\le ^0_p \beta (v)$.

• $<^1_p$ is defined by $w<^1_p v$ iff $\beta (w)<^0_p \beta (v)$.

• $V^1$ is defined by $w\in V^1(p)$ iff $\beta (w)\in V^0(p)$.

Definition 17

(Bounded Morphism). A mapping $f: M=(W,\{R_i\}_{i\in Agent},\le , <, \le _p,<_p,V) \rightarrow M'=(W, \{R'_i\}_{i\in Agent},\le ', <', \le '_p,<'_p,V')$ is a bounded morphism if it satisfies the following conditions:

• $w$ and $f(w)$ satisfy the same proposition letters.

• if $w\le v$ then $f(w)\le ' f(v)$. And similarly for $<, \le _p,<_p, R_i$.

• if $f(w)\le ' v'$ then there exists $v$ such that $w\le v$ and $f(v)=v'$. And similarly for $<', \le '_p,<'_p, R_i$.

Lemma 1

If $f$ is a bounded morphism from $M$ to $M'$, then for all $\phi$, for all $w\in M$, $M,w \vDash _{pudl^+_2} \phi$ iff $M',f(w) \vDash _{pudl^+_2} \phi$.

Proposition 8

For every consistent set $\varPhi$, if $\mathfrak {M}^0, \varGamma \vDash _{pudl^+_2} \varPhi$, then there exists $\varGamma '$ such that $\mathfrak {M}^1, \varGamma ' \vDash _{pudl^+_2} \varPhi$.

Proposition 9

$\mathfrak {M}^1$ has the following properties:

• (1) Both $\le ^1$ and $\le _p ^1$ are reflexive, transitive and connected relations.

• (2) $w<^1 v$ iff $w\le ^1 v$ and $v\nleq ^1 w$

• (3) If $w\le ^1_p v$ and $v\nleq ^1_p w$ then $w<^1_p v$.

• (4) If $w<^1_p v$ then $w\le ^1_p v$.

• (5) $R^1_i$ is an equivalence relation for each $i\in Agent$.

• (6) For every $w\in W^1$, $R^1_1(w)\cap \ldots \cap R^1_n(w) \not =\emptyset$.

Deleting $<_p$ -cluster. Now we use Bulldozing again to delete $<_G$clusters.

Let $\mathfrak {M}^2 = (W^{2}, \{R^2_i\}_{i\in Agent},\le ^2, <^2, \le ^2_p, <^2_p, V^2)$ where:

• $W^{2}= W^{1-}\cup \bigcup _{i\in I}C^{\prime }_i$, here $I$ is a set index of all $<_G$-clusters of $W^{1}$, $W^{1-}=W^1- \bigcup _{i\in I}C_i$, $C^{\prime }_i = C_i\times \mathbb {Z}$, $\mathbb {Z}$ is the set of natural numbers.

• $R^2_i$ is defined by $wR^2_i v$ iff $\sigma (w)R^1_i \sigma (v)$, for every $i\in Agent$.

• $<^2_p$ is defined as follows: For each $C_i$, choose an arbitrary linear order $<^{2,i}_p$. Define a map $\sigma : W^2\rightarrow W^1$ by $\sigma (x)=x$ if $x\in W^{1-}$ and $\sigma (x)=w$ if $x$ is a pair $(w,n)$ for some world $w$ and integer $n$. We define $<^2_p$ via the following cases:

  • Case 1: $x$ or $y$ is in $W^{1-}$. In this case we let $x <^2_p y$ iff $\sigma (x) <^1_p \sigma (y)$.

  • Case 2: $x\in C_i$ and $y\in C_j$, $i\ne j$. In this case we let $x <^3_p y$ iff $\sigma (x) <^2_p\sigma (y)$.

  • Case 3: $x\in C_i$ and $y\in C_i$. In this case , $x=(w,m)$ and $y=(v,n)$. There are two sub-cases:

    • * Case 3.1: If $m\ne n$, we use the natural ordering on $\mathbb {Z}$: $(w,m) <^2_p (v,n)$ iff $m<n$.

    • * Case 3.2: If $m=n$, we use the linear ordering $<^{2,i}_p$: $(w,m) <^2_p (v,m)$ iff $w<^{2,i}_p v$.

• $\le ^2_p$ is defined via the following cases:

  • Case 1: $x$ or $y$ is in $W^{1-}$. In this case we let $x \le ^2_p y$ iff $\sigma (x) \le ^1_p \sigma (y)$.

  • Case 2: Otherwise, we take the reflexive closure of $<^2_p$: $x \le ^2_p y$ iff $x <^2_p y$ or $x=y$.

• $\le ^2$ is defined by $w\le ^2 v$ iff $\sigma (w)\le ^1 \sigma (v)$.

• $<^2$ is defined by $w<^2 v$ iff $\sigma (w)<^1 \sigma (v)$.

• $V^2$ is defined by $w\in V^2(p)$ iff $\sigma (w)\in V^1(p)$.

Proposition 10

For every consistent set $\varPhi$, if $\mathfrak {M}^1, \varGamma \vDash _{pudl^+_2} \varPhi$, then there exists $\varGamma '$ such that $\mathfrak {M}^2, \varGamma ' \vDash _{pudl^+_2} \varPhi$.

Proposition 11

$\mathfrak {M}^2$ has the following properties:

• (1) Both $\le ^2$ and $\le _p ^2$ are reflexive, transitive and connected relations.

• (2) $w<^2 v$ iff $w\le ^2 v$ and $v\nleq ^2 w$

• (3) $w<^2_p v$ iff $w\le ^2_p v$ and $v\nleq ^2_p w$

• (4) $R^2_i$ is an equivalence relation for each $i\in Agent$.

• (5) For every $w\in W^2$, $R^2_1(w)\cap \ldots \cap R^2_n(w) \not =\emptyset$.