In the literature, different axiomatizations of Public Announcement Logic (PAL) have been proposed. Most of these axiomatizations share a “core set” of the so-called “reduction axioms”. In this paper, by designing non-standard Kripke semantics for the language of PAL, we show that the proof system based on this core set of axioms does not completely axiomatize PAL without additional axioms and rules. In fact, many of the intuitive axioms and rules we took for granted could not be derived from the (...) core set. Moreover, we also propose and advocate an alternative yet meaningful axiomatization of PAL without the reduction axioms. The completeness is proved directly by a detour method using the canonical model where announcements are treated as merely labels for modalities as in normal modal logics. This new axiomatization and its completeness proof may sharpen our understanding of PAL and can be adapted to other dynamic epistemic logics. (shrink)
A proposition is noncontingent, if it is necessarily true or it is necessarily false. In an epistemic context, ‘a proposition is noncontingent’ means that you know whether the proposition is true. In this paper, we study contingency logic with the noncontingency operator? but without the necessity operator 2. This logic is not a normal modal logic, because?→ is not valid. Contingency logic cannot define many usual frame properties, and its expressive power is weaker than that of basic modal logic over (...) classes of models without reflexivity. These features make axiomatizing contingency logics nontrivial, especially for the axiomatization over symmetric frames. In this paper, we axiomatize contingency logics over various frame classes using a novel method other than the methods provided in the literature, based on the ‘almost-definability’ schema AD proposed in our previous work. We also present extensions of contingency logic with dynamic operators. Finally, we compare our work to the related work in the fields of contingency logic and ignorance logic, where the two research communities have similar results but are apparently unaware of each other’s work. One goal of our paper is to bridge this gap. (shrink)
When we say “I know why he was late”, we know not only the fact that he was late, but also an explanation of this fact. We propose a logical framework of “knowing why” inspired by the existing formal studies on why-questions, scientific explanation, and justification logic. We introduce the Kyi\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$${{\mathcal {K}}{}\textit{y}}_i$$\end{document} operator into the language of epistemic logic to express “agent i knows why φ\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} (...) \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$\varphi $$\end{document}” and propose a Kripke-style semantics of such expressions in terms of knowing an explanation of φ\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$\varphi $$\end{document}. We obtain two sound and complete axiomatizations w.r.t. two different model classes depending on different assumptions about introspection. Finally we connect our logic with justification logic technically by providing an alternative semantics and an in-depth comparison on various design choices. (shrink)
Epistemic logic has become a major field of philosophical logic ever since the groundbreaking work by Hintikka [58]. Despite its various successful applications in theoretical computer science, AI, and game theory, the technical development of the field has been mainly focusing on the propositional part, i.e., the propositional modal logics of “knowing that”. However, knowledge is expressed in everyday life by using various other locutions such as “knowing whether”, “knowing what”, “knowing how” and so on (knowing-wh hereafter). Such knowledge expressions (...) are better captured in quantified epistemic logic, as was already discussed by Hintikka [58] and his sequel works at length. This paper aims to draw the attention back again to such a fascinating but largely neglected topic. We first survey what Hintikka and others did in the literature of quantified epistemic logic, and then advocate a new quantifier-free approach to study the epistemic logics of knowing-wh, which we believe can balance expressivity and complexity, and capture the essential reasoning patterns about knowing-wh. We survey our recent line of work on the epistemic logics of ‘knowing whether”, “knowing what” and “knowing how” to demonstrate the use of this new approach. (shrink)
In this paper, we first propose a simple formal language to specify types of agents in terms of necessary conditions for their announcements. Based on this language, types of agents are treated as ‘first-class citizens’ and studied extensively in various dynamic epistemic frameworks which are suitable for reasoning about knowledge and agent types via announcements and questions. To demonstrate our approach, we discuss various versions of Smullyan’s Knights and Knaves puzzles, including the Hardest Logic Puzzle Ever (HLPE) proposed by Boolos (...) (in Harv Rev Philos 6:62–65, 1996). In particular, we formalize HLPE and verify a classic solution to it. Moreover, we propose a spectrum of new puzzles based on HLPE by considering subjective (knowledge-based) agent types and relaxing the implicit epistemic assumptions in the original puzzle. The new puzzles are harder than the previously proposed ones in the literature, in the sense that they require deeper epistemic reasoning. Surprisingly, we also show that a version of HLPE in which the agents do not know the others’ types does not have a solution at all. Our formalism paves the way for studying these new puzzles using automatic model checking techniques. (shrink)
In this paper, we propose a decidable single-agent modal logic for reasoning about goal-directed “knowing how”, based on ideas from linguistics, philosophy, modal logic, and automated planning in AI. We first define a modal language to express “I know how to guarantee \ given \” with a semantics based not on standard epistemic models but on labeled transition systems that represent the agent’s knowledge of his own abilities. The semantics is inspired by conformant planning in AI. A sound and complete (...) proof system is given to capture valid reasoning patterns, which highlights the compositional nature of “knowing how”. The logical language is further extended to handle knowing how to achieve a goal while maintaining other conditions. (shrink)
We look at lying as an act of communication, where (i) the proposition that is communicated is not true, (ii) the utterer of the lie knows that what she communicates is not true, and (iii) the utterer of the lie intends the lie to be taken as truth. Rather than dwell on the moral issues, we provide a sketch of what goes on logically when a lie is communicated. We present a complete logic of manipulative updating, to analyse the effects (...) of lying in public discourse. Next, we turn to the study of lying in games. First, a game-theoretical analysis is used to explain how the possibility of lying makes such games interesting, and how lying is put to use in optimal strategies for playing the game. Finally, we give a matching logical analysis. Our running example of lying in games in liar’s dice. (shrink)
In this article, we present an attempt to reconcile intellectualism and the anti-intellectualist ability account of knowledge-how by reducing “S knows how to F” to, roughly speaking, “S knows that she has the ability to F demonstrated by a concrete way w.” More precisely, “S has a certain ability” is further formalized as the proposition that S can guarantee a certain goal by a concrete way w of some method under some precondition. Having the knowledge of our own ability, we (...) can plan our future actions accordingly, which would not be possible by merely having the ability without knowing it, and this pinpoints the crucial difference between knowledge-how and ability. Our semi-formal account avoids most of the objections to both intellectualism and the anti-intellectualist ability account, and provides a multistage learning process of knowledge-how, which reveals various subtleties. (shrink)
A true lie is a lie that becomes true when announced. In a logic of announcements, where the announcing agent is not modelled, a true lie is a formula that becomes true when announced. We investigate true lies and other types of interaction between announced formulas, their preconditions and their postconditions, in the setting of Gerbrandy’s logic of believed announcements, wherein agents may have or obtain incorrect beliefs. Our results are on the satisfiability and validity of instantiations of these semantically (...) defined categories, on iterated announcements, including arbitrarily often iterated announcements, and on syntactic characterization. We close with results for iterated announcements in the logic of knowledge, and for lying as private announcements to different agents. Detailed examples illustrate our lying concepts. (shrink)
In this paper1, we develop an epistemic logic to specify and reason about the information flow on the underlying communication channels. By combining ideas from Dynamic Epistemic Logic (DEL) and Interpreted Systems (IS), our semantics offers a natural and neat way of modelling multi-agent communication scenarios with different assumptions about the observational power of agents. We relate our logic to the standard DEL and IS..
Security properties naturally combine temporal aspects of protocols with aspects of knowledge of the agents. Since BAN-logic, there have been several initiatives and attempts to incorpórate epistemics into the analysis of security protocols. In this paper, we give an overview of work in the field and present it in a unified perspective, with comparisons on technical subtleties that have been employed in different approaches. Also, we study to which degree the use of epistemics is essential for the analysis of security (...) protocols. We look for formal conditions under which knowledge modalities can bring extra expressive power to pure temporal languages. On the other hand, we discuss the cost of the epistemic operators in terms of model checking complexity. (shrink)
Recent years witnessed a growing interest in non-standard epistemic logics of knowing whether, knowing how, knowing what, knowing why and so on. The new epistemic modalities introduced in those logics all share, in their semantics, the general schema of ∃x◻φ, e.g., knowing how to achieve φ roughly means that there exists a way such that you know that it is a way to ensure that φ. Moreover, the resulting logics are decidable. Inspired by those particular logics, in this work, we (...) propose a very general and powerful framework based on quantifier-free predicate language extended by a new modality, which packs exactly ∃x◻ together. We show that the resulting language, though much more expressive, shares many good properties of the basic propositional modal logic over arbitrary models, such as finite-tree-model property and van Benthem-like characterization w.r.t.\ first-order modal logic. We axiomatize the logic over S5 frames with intuitive axioms to capture the interaction between the new modality and know-that operator in an epistemic setting. (shrink)
Epistemic protocols are communication protocols aiming at transfer of knowledge in a controlled way. Typically, the preconditions or goals for protocol actions depend on the knowledge of agents, often in nested form. Informal epistemic protocol descriptions for muddy children, coordinated attack, dining cryptographers, Russian cards, secret key exchange are well known. The contribution of this paper is a formal study of a natural requirement on epistemic protocols, that the contents of the protocol can be assumed to be common knowledge. By (...) formalizing this requirement we can prove that there can be no unbiased deterministic protocol for the Russian cards problem. For purposes of our formal analysis we introduce an epistemic protocol language, and we show that its model checking problem is decidable. (shrink)
In this paper, we give an alternative semantics to the non-normal logic of knowing how proposed by Fervari et al., based on a class of Kripke neighborhood models with both the epistemic relations and neighborhood structures. This alternative semantics is inspired by the same quantifier alternation pattern of \ in the semantics of the know-how modality and the neighborhood semantics for the standard modality. We show that this new semantics is equivalent to the original Kripke semantics in terms of the (...) validities. A key result is a representation theorem showing that the more abstract Kripke neighborhood models can be represented by the concrete Kripke models with action transitions modulo the valid formulas. We prove the completeness of the logic for the neighborhood semantics. The neighborhood semantics can be adapted to other variants of logics of knowing how. It provides us a powerful technical tool to study these logics while preserving the basic semantic intuition. (shrink)
Weakly Aggregative Modal Logic (WAML) is a collection of disguised polyadic modal logics with n-ary modalities whose arguments are all the same. WAML has some interesting applications on epistemic logic and logic of games, so we study some basic model theoretical aspects of WAML in this paper. Specifically, we give a van Benthem-Rosen characterization theorem of WAML based on an intuitive notion of bisimulation and show that each basic WAML system Kn lacks Craig Interpolation.
