Belief Re-Revision in Chivalry Case

Abstract

We propose a formalization of legal judgment revision in terms of dynamic epistemic logic, with two dynamic operators; commitment and permission. Each of these operations changes the accessibility to possible worlds, restricting to personal belief as local announcement. The commitment operator removes some accessible links for an agent to come to believe an announced proposition, while the permission operator restores them to tolerate former belief state. In order to demonstrate our formalization, we analyze judge’s belief change in Chivalry Case in which a self-defense causes a misconception. Furthermore, we show an implementation of our logical formalization to demonstrate that it can be used in a practical way.

A Complete Axiomatization of Dynamic Logic with Commitment and Permission Operators

In this section, we give an axiomatization of our dynamic logic with two operators and sketch its completeness proof.

Table 4. Axiomatization of static logic in $\mathcal {L}$

Theorem 1

The set of all the valid formulas of $\mathcal {L}$ is completely axiomatized by all the axioms and the rules of Table 4.

Proof

(Sketch) Soundness is easy to establish. So, let us concentrate on the completeness proof. We can regard our syntax $\mathcal {L}$ as a syntax $\mathcal {H}(\mathsf {E})$ of hybrid logic [12, p.72] by the following identification: $\mathsf {n}$ as a nominal and $\mathsf {E}$ as the global modality, where a ‘nominal’ means a new sort of propositional variable which is true at exactly one state. Our axiomatization of Table 4 is the equivalent axiomatization of hybrid logic with nominals and the global modality in [12, p.72], provided the set of nominals consists of $\mathsf {n}$ alone. Then, [12, Theorem 5.4.2] implies that our axiomatization is strongly complete with respect to the class of all models, since the proof of [12, Theorem 5.4.2] does not depend on the number of nominals in the syntax (in fact, we could obtain the stronger result to cover the additional axioms for $\mathop {\mathsf {B}_{i}}$ called Sahlqvist axioms [12, p.87, Theorem 5.4.2]).    $\square$

Theorem 2

The set of all the valid formulas of $\mathcal {L}^{+}$ is completely axiomatized by all the axioms and the rules of Table 4 and 3 as well as the necessitation rules for $[\mathsf {com}_{{i}}({\varphi })]$ and $[\mathsf {per}_{{i}}({{\varphi })}]$: from $\psi$, we may infer $[\mathsf {com}_{{i}}({\varphi })] \psi$ and $[\mathsf {com}_{{i}}({\varphi })] \psi$.

Proof

(Sketch) By $\vdash \psi$ (or $\vdash ^{+} \psi$), we mean that $\psi$ is a theorem of the axiomatization for $\mathcal {L}$ (or, $\mathcal {L}^{+}$, respectively.) The soundness part is mainly due to Proposition 1. One can also check that the necessitation rules for $[\mathsf {com}_{{i}}({\varphi })]$ and $[\mathsf {per}_{{i}}({{\varphi })}]$ preserve the validity on the class of all models. As for the completeness part, we can reduce the completeness of our dynamic extension to the static counterpart (i.e., Theorem 1) as follows. With the help of the reduction axioms of Table 3, we can define a mapping $t$ sending a formula $\psi$ of $\mathcal {L}^{+}$ to a formula $t(\psi )$ of $\mathcal {L}$, where we start rewriting the innermost occurrences of $[\mathsf {com}_{{i}}({\varphi })]$ and $[\mathsf {per}_{{i}}({{\varphi })}]$. We can define this mapping $t$ such that $\psi \leftrightarrow t(\psi )$ is valid on all models and $\vdash ^{+} \psi \leftrightarrow t(\psi )$. Then, we can proceed as follows. Fix any formula $\psi$ of $\mathcal {L}^{+}$ such that $\psi$ is valid on all models. By the validity of $\psi \leftrightarrow t(\psi )$ on all models, we obtain $t(\psi )$ is valid on all models. By Theorem 1, $\vdash t(\psi )$, which implies $\vdash ^{+} t(\psi )$. Finally, it follows from $\vdash ^{+} \psi \leftrightarrow t(\psi )$ that $\vdash ^{+} \psi$, as desired.    $\square$