Kanazawa Workshop for Epistemic Logic and its Dynamic Extensions

Duality theory for modal logic was developed to describe the interaction between Kripke structures and modal algebras. Public announcement logic is an extension of modal logic by adding public announcement operators. It was designed first by Plaza to model the change of epistemic information by making observable action. Nowadays it becomes a simple but very useful tool for modeling various social scenarios. In this talk, I will use duality toolkit to develop algebraic semantics for public announcement logic. The resulting mechanism is the following: first we construct a quotient algebra which is obtained from the given modal algebra and an equivalence relation w.r.t a chosen ‘announced’ element. Then we get a `projection' from the quotient algebra into the original algebra. It is in this way we give an interpretation for public announcement operators over algebraic models. Moreover, we generalize public announcements to subframe operations and show some more duality results. The algebraic semantics for PAL is a joint work with Alessandra Palmigiano (Delft University of Technology) and Mehrnoosh Sadrzadehc (Queen Mary University of London) in [1].

References
[1] M. Ma, A. Palmigiano, M. Sadrzadeh. Algebraic semantics and model completeness for Intuitionistic Public Announcement Logic. Annals of Pure and Applied Logic, 165(4): 963-995, 2014.
[2] Minghui Ma. Mathematics of Public Announcements. Proceedings of the third International Workshop on Logic, Rationality and Interaction (LORI-III), LNAI 6953, pp. 193–205, Springer-Verlag, 2011.
[3] J. van Benthem. Logical dynamics of information and interaction. Cambridge University Press, Cambridge MA, 2011.

One of the main criticisms to epistemic logic is the logical omniscience problem: under relational models, the knowledge of any epistemic logic agent is closed under modus ponens and contains every validity, thus making it closed under logical consequence. Among the proposals to solve this problem, an important one has been to distinguish between an agent’s explicit knowledge and her implicit knowledge: this have allowed many approaches that differ on what each one of then considers to be the 'missing' ingredient that makes explicit something that so far is only implicit.

In this work the missing ingredient is that of 'awareness of': in order for an implicitly known formula to be explicitly know, the agent needs to be aware of it. We start by recalling the awareness logic (Fagin and Halpern, 1988) framework, focussing in the particular case in which awareness is generated by atomic propositions. Then we discuss what the notion of awareness means in terms of how an agent sees a model, formalising the discussion with the notion of awareness bisimulation. We conclude presenting an extension of the well-known action models (Baltag, Moss, Solecki, 1999) with which we can represent actions that modify the agent's knowledge and awareness.

The presentation is a summary of work developed across different publications by Johan van Benthem, Hans van Ditmarsch, Tim French, Fernando R. Velázquez-Quesada and Yi Wang.

A lie is a statement that is false, or at least believed to be false, when it is announced. But the world after the lie is not the same as the world before the lie, so is the statement necessarily still false after the lie is announced - is the lie still a lie? This talk is about true lies. These are "self-fulfilling" lies that become true when they are made. The analysis is based on formal modal epistemic logic. True lies are conceptually related to Moore sentences, sentences that are true but become false when they are announced, but the exact relationship between the two types of sentences is not trivial. I will also discuss impossible lies (lies that stay false when announced) as well as the relationships to successful formulas (truths that stay truths when announced) and self-refuting truths (truths that become false when announced). The talk is based on joint work with Hans van Ditmarsch (Nancy) and Yanjing Wang (Beijing).

One and the same sentence of natural language can be used to perform more than one illocutionary act. Although the securing of uptake is necessary for the successful performance of illocutionary acts, the illocutionary force of an utterance can be underdetermined even if the addressee knows the context of the utterance and the status of the utterer very well. If we combine dynamic logic of illocutionary acts with simple static epistemic logic, however, a surprising result holds. Namely, the securing of uptake will be gained for free. In spite of the fact that only the static epistemic logic is added, the epistemic states of the agents involved are dynamically updated by acts of commanding, promising, requesting, etc. This happens because we are not able to model the uncertainties among the agents involved as regards what has happened. We will examine how the product update introduced in Dynamic Epistemic Logic can be used to represent such uncertainties of the uptake.

In this talk, I will implement simultaneous belief changes of multiple agents. In order to manage so many indices, e.g., agent ID's, time stamps, and informed propositions, we introduce the notation of vectors and matrices for the simultaneous informing action. By this, we show that a matrix can represent a public announcement and/or a consecutive message passing, in accordance with time sequence of belief change properly. A collective belief state multiplied by a communication matrix, including matrices of accessibility in Kripke semantics, becomes a hypercuboid.

We consider multi-agent scenarios where each agent controls a surveillance camera positioned in the plane, with fixed position and angle of view, but rotating freely. The agents can thus observe the surroundings and each other. They can also reason about each other's observation abilities and knowledge derived from these observations. We introduce suitable logical languages for reasoning about such scenarios which involve atomic formulae stating what agents can see, multi-agent epistemic operators for individual, distributed and common knowledge, as well as dynamic operators reflecting the ability of cameras to turn around in order to reach positions satisfying formulae in the language.

We introduce semantics of our basic logic BBL and its extensions on natural geometric models, as well as formal Kripke semantics for them in vision-based finite abstractions of the geometric models. We discuss the expressiveness of our logical languages and provide their translations in PDL style. Using these translations we develop algorithms and obtain complexity results for model checking and satisfiability testing for BBL and its extensions. Notably, we show that even for the extension with common knowledge, model checking remains in PSPACE. Finally, we discuss some further extensions: by adding obstacles, positioning the cameras in 3D or enabling them to change positions.

In this talk, we discuss proof systems for logics combining Artemov's logic of proofs (LP) and the logic of provability (GL) (and strong provability (Grz)). The logic of proofs has been introduced to explore a combinatorial structure of proofs and also taken to be an ``explicit'' version of epistemic logic. GL (Grz) has been studied as a logic of formal provability (provability and truth) in arithmetic. These combined logics themselves have already existed in the literature for a while. The logic combining LP and GL is called GLA, and the logic combining LP and Grz is called GrzA. Hilbert-style axiomatizations of the logics have already been given; however, neither tableau systems nor Gentzen- style proof systems for the logics with nice proof-theoretic properties have been proposed so far. In the talk, we first give some motivating discussions for the logic of proofs. Then, we introduce both Fitting-style prefixed tableau systems and hypersequent calculi for GLA and GrzA. As technical results, we present the following. The first one is the admissibility of cut for the prefixed tableau systems via semantic completeness for the cut-free prefixed tableau systems for GLA and GrzA. The second one is the admissibility of cut for the hypersequent calculi for GLA and GrzA. We show this by constructing a translation from the prefixed tableau systems to the hypersequent calculi.

I will present a logic for reasoning about evidence-based knowledge and beliefs and the evidential dynamics of non-logically-omniscient agents. I will adapt the key tools and techniques from Dynamic Epistemic Logic, Justification Logic, and Belief Revision in order to provide a lightweight, yet fine-grained approach that characterizes well-known epistemic and doxastic attitudes in the terms of the evidential reasoning that justifies these attitudes. As a result, I will argue that this approach can serve as a lynchpin in the formal analysis of complex dynamic epistemological reasoning scenarios, such as e.g. in various Gettier-type cases. This presentation is based on joint work with A. Baltag and B. Renne.

Epistemic Logic of Friendship (EFL) is a version of two-dimensional modal logic proposed by Seligman, Girard and Liu (2013). Compared to the ordinary epistemic logic, one of the main features of their logic is to encode the information of agents into the object language by a technique of hybrid logic. Then, a propositional variable p can be read as an indexical proposition such as `I am p' and we may formalize the sentences like `I know that all of my friend is p' or `All of my friends know that he/she is p'. Moreover, they provide a dynamic mechanism for capturing public announcements, announcements to all the friends, and private announcements and established a relative completeness result. This talk focuses on the problem of axiomatizaing EFL, i.e., the static part of their framework. First, we provided a labelled sequent calculus LEFL for EFL and establish the completeness result of LEFL. Second, we translate each sequent of LEFL into an ordinary formula and specify a Hilbert-style axiomatization HEFL of EFL and establish a semantic completeness result for HEFL.

In order to study infinite regresses arising from prediction/decision making in an 2-person game, we present a logic called the infinite regress logic IR². It extends finitary epistemic logic KD² for two players, by incorporating the two operators expressing infinite regresses. Here, an infinite regress arises from the interactive thinking of a player about the other's subjective thinking and vice versa. If we add the Truth Axiom for the belief operators to the KD², the infinite regresses collapse into the common knowledge. Hover, we keep the subjective nature of the concept, avoiding the Truth Axiom, Positive Introspection Axiom (4) as well as the Negative Introspection Axiom (5). We prove the completeness theorem with respect to Kripke semantics and a certain restricted class of Kripke models. These lead to various meta-theorems useful for considerations of prediction decision making in games. Indeed, we will show that the players may keep different understandings about the game situation even after the actual play of the game.

Epistemic logics of shallow depths are developed in various papers by Kaneko-Suzuki to aim to study game theoretical decision making, where by ``shallow depths'' we mean players' bounded interpersonal inferences. The key idea for designing our formal system is separation of epistemic and non-epistemic inferences by means of thought-sequents. Based on this formalism, we give consideration to decision and prediction criteria in game situations.

We also discuss feasibility of player's decision in a certain game from the viewpoint of constructive reasoning. In our previous approach, classical logic is adopted as the base logic, which implies that the players' logical abilities are also described by classical logic. Classical logic has some non-constructive feature, but decision making typically requires constructive reasoning. To capture the constructive nature, we adopt intuitionistic logic as the base logic rather than classical logic. The resulting epistemic logical system is based on first-order intuisionistic logic, and is complete with respect to Kripke-type semantics. Some meta-theorems are proved by making use of this semantics, and assure the equivalence between existence of decisions and feasibility of those decisions in our framework.

You are a secret agent with a secret $S$ that you would like to transmit to a fellow agent $a$ unobtrusively using a very public network like Twitter. Any information you tweet will be received by your followers on the network. You correctly assume that they will send the message on to their followers (retweet it) if and only if it does not conflict with any information they already possess. With luck, your message will be tweeted through the network until it eventually reachers $a$. Under what conditions is it possible for you to convey $S$ to $a$ in this way, without other agents in the network learning this information? Clearly, you cannot tweet $S$ itself, but if, for example, $a$ is the only agent to knows that $K$ then the message `if $K$ then $S$’ may work, if there is a suitable path from you to $a$. To know whether you can succeed or not and what to tweet, you need to know something about the network and the information already possessed by the other agents. But you can learn something about this with a test tweet. If, for example, you know that you have two followers $b$ and $c$ and only $b$ believes $P$ and then you tweet the message $\neg P$ then if, after a certain length of time, someone tweets $P$ to you, you know that there is a loop back to you via $c$. This talk will report on recent joint work on these and similar questions with Mostafa Raziebrahimsaraei.