We presentArrow Update Logic, a theory of epistemic access elimination that can be used to reason about multi-agent belief change. While the belief-changing “arrow updates” of Arrow Update Logic can be transformed into equivalent belief-changing “action models” from the popular Dynamic Epistemic Logic approach, we prove that arrow updates are sometimes exponentially more succinct than action models. Further, since many examples of belief change are naturally thought of from Arrow Update Logic’s perspective of eliminating access to epistemic possibilities, Arrow Update Logic is a valuable addition to the repertoire of logics of information change. In addition to proving basic results about Arrow Update Logic, we introduce a new notion of common knowledge that generalizes both ordinary common knowledge and the “relativized” common knowledge familiar from the Dynamic Epistemic Logic literature.
Two groups of agents, \(\mathcal{G}_{1}\) and \({\mathcal{G}}_{2}\) , face a moral conflict if \(\mathcal{G}_{1}\) has a moral obligation and \(\mathcal{G}_{2}\) has a moral obligation, such that these obligations cannot both be fulfilled. We study moral conflicts using a multi-agent deontic logic devised to represent reasoning about sentences like ‘In the interest of group \(\mathcal{F}\) of agents, group \(\mathcal{G}\) of agents ought to see to it that \(\phi\) .’ We provide a formal language and a consequentialist semantics. An illustration of our semantics with an analysis of the Prisoner’s Dilemma follows. Next, necessary and sufficient conditions are given for (1) the possibility that a single group of agents faces a moral conflict, for (2) the possibility that two groups of agents face a moral conflict within a single moral code, and for (3) the possibility that two groups of agents face a moral conflict.
Taking our inspiration from modal correspondence theory, we present the idea of correspondence analysis for many-valued logics. As a benchmark case, we study truth-functional extensions of the Logic of Paradox (LP). First, we characterize each of the possible truth table entries for unary and binary operators that could be added to LP by an inference scheme. Second, we define a class of natural deduction systems on the basis of these characterizing inference schemes and a natural deduction system for LP. Third, we show that each of the resulting natural deduction systems is sound and complete with respect to its particular semantics.
Every truth-functional three-valued propositional logic can be conservatively translated into the modal logic S5. We prove this claim constructively in two steps. First, we define a Translation Manual that converts any propositional formula of any three-valued logic into a modal formula. Second, we show that for every S5-model there is an equivalent three-valued valuation and vice versa. In general, our Translation Manual gives rise to translations that are exponentially longer than their originals. This fact raises the question whether there are three-valued logics for which there is a shorter translation into S5. The answer is affirmative: we present an elegant linear translation of the Logic of Paradox and of Strong Three-valued Logic into S5.
29 September 2007 in Journal of Logic, Language and Information
Propositional dynamic logic ( \(\mathsf{PDL}\) ) is complete but not compact. As a consequence, strong completeness (the property \(\Gamma \models \varphi \Rightarrow \Gamma \vdash \varphi\) ) requires an infinitary proof system. In this paper, we present a short proof for strong completeness of \(\mathsf{PDL}\) relative to an infinitary proof system containing the rule from [α; βn]φ for all \(n \in {\mathbb{N}}\) , conclude \([\alpha;\beta^*] \varphi\) . The proof uses a universal canonical model, and it is generalized to other modal logics with infinitary proof rules, such as epistemic knowledge with common knowledge. Also, we show that the universal canonical model of \(\mathsf{PDL}\) lacks the property of modal harmony, the analogue of the Truth lemma for modal operators.