A Postscript to a Completeness Proof for Johan

Wiebe van der Hoek and John-Jules Meyer

Abstract

We use our paper ‘A Complete Epistemic Logic for Multiple Agents’ ([7] as a demonstration of Johan’s influence on our work on epistemic logic: it uses several techniques and tools that in many ways go back to his early work on modal logic. We then end with two personal reflections

Contents

1 Introduction 2 2 Description of the paper [7] 2 3 Postscript to our Paper 4 4 John-Jules’ Postscript 5 5 Wiebe’s Postscript 5

1 Introduction

We like to elaborate a bit on the contents and the development of one of our papers, called ‘A Complete Epistemic Logic for Multiple Agents’ ([7]. We do so, since this paper is not only about a subject that is so close to Johan’s initial parade-horses (it deals with correspondence and completeness of a modal epistemic logic), but also since the development of the paper is very much inspired and influenced by Johan’s direct and indirect interference– in a way that may be typical for many work written under his influence.

2 Description of the paper [7]

In the field of AI and Computer Science, the modal system S5 is a familiar logic to model knowledge. Although the system on the one hand models an idealized notion of knowledge, its nice mathematical properties, on the other hand, often motivate researchers to adopt this system in their first exploration of the field. Then, for specific purposes, such as decision- and game-theoretic applications, some or many of these idealizations concerning introspective properties or logical omniscience are given up or, sometimes, replaced by weaker assumptions about knowledge.

It is a well-known fact that the idealized modal system S5 exactly describes the valid formulas of Kripke models in which the accessibility relation is an equivalence relation. In the case of one agent, one may use a result about preservation of truth under taking so-called generated sub-models (the formulas that are true in a word w in a Kripke model M are exactly those that are true in w and M′, where M′ is the restriction of M to only those worlds that are accessible from w—in any number of steps) to conclude that we may even assume this relation to be universal (cf. [9, 5, 6]). The latter fact guarantees many pleasant properties of the logic of knowledge, like the existence of small models and the superfluity of iteration of modal operators (cf. [11]). However, since the logic S5 was first used as an epistemic logic, many extensions and adaptions of it have been proposed.

A first extension satisfies the need to have a logic that describes the knowledge in a group of, say, m agents (the operator K_{i} expressing what is known by agent i). A shift from the bare system S5 to S5_{m} did not give rise to any logical complications, even though completeness with respect to universal models had to be sacrificed; the underlying accessibility relations R_{i} (i ≤ m) may still be taken to be equivalences. Later, researchers interested in the kinds of knowledge that emerge in a group of agents proposed enriching the language with operators E (‘Everybody knows’), C (‘it is Common knowledge that’) and D (‘it is Distributed knowledge that’) (cf. [5, 9]). Apart from these extensions, we may mention in passing various proposals for combining the notion of knowledge with that of belief ([8, 10]), time ([8]) or probability ([3]).

When they are treated as primitive operators, K_{1}, … K_{m}, C, D and E all are interpreted as necessity operators with respect to accessibility relations R_{1}, …, R_{m}, R_{C}, R_{D} and R_{E} in a Kripke model. The relations between the various kinds of knowledge, as expressed syntactically in the axioms of the logic, give rise to the enterprise of finding corresponding connections between the accessibility relations associated with these knowledge operators. The exact nature of the semantic counterparts of the modal axioms has been subject of folklore conjectures and assertions in the AI-community for some time now. It has also been claimed that several known results from the literature of modal logic apply. For instance, the relation between the operators E and C is much like a relation between some special modal operators studied in Dynamic Modal Logic by Goldblatt in [4]. His result concerning a semantical characterisation of these operators is often referred to when giving a completeness proof for S5_{m}(EC), which is our notation for an ‘S5-like’ modal logic for knowledge incorporating the operators E and C (such a completeness proof can be found in [6]). Claiming such a correspondence seems to invoke an implicit assumption of some ‘modularity’ principle, i.e. that the exact dependency between the E and K_{i}-operators does not undermine Goldblatt’s technique of manipulating Kripke models.

Another example regards the system S5_{m}(D), the logic that combines the knowledge of m agents with the notion of distributed knowledge. Halpern and Moses claimed ([5]) completeness with respect to models in which R_{D} = R_{1} ∩ R_{2} ∩ … ∩ R_{m}. Although, on the one hand, it turned out that this property was not modally definable (cf. [12]), on the other hand it appeared that the claim of Halpern and Moses could be proven using some non-standard techniques ([1, 12]).

However, where Goldblatt’s technique was essentially successful since he was able to build a finite model, the techniques used to prove completeness for the case of distributed knowledge yielded infinite models, so that a naive combination of the techniques will not do the trick. This, of course, raises the question of the completeness of S5_{m}(CDE) which, as far as we know, has not been stated—let alone solved—explicitly in the literature^{1}.

Taking into account the claims and partial proofs we mentioned above, the paper [7] is written to solve the following questions. Firstly, it does provide a completeness proof for S5_{m}(CDE), the epistemic logic that deals with Common, Distributed and Everybody’s Knowledge in a group of m agents. Secondly, it shows how the techniques used by Goldblatt can be applied in the S5 environment. Thirdly, as a consequence of the techniques we apply, we also obtain finite models for the cases in which distributed knowledge is involved, and from that, we easily get decidability of S5_{m}(D) and S5_{m}(CDE). Finally, we consider [7] as an application of the modular approach of [12], where it was claimed that one can use one uniform ‘unravelling-and-rewriting technique’ to transform models, keeping track of various properties of the relations in the underlying Kripke model (although, in [7], the rewrite technique is implicitly represented by an equivalence relation on paths, for reasons of space). It will appear, on the one hand, that this principle of modularity indeed takes care of keeping the models S5-like, but on the other hand, that to achieve the intended properties for the relations concerning the operators C, D and E, we have to make some additional decisions about how the equivalence relation is affected by the relations associated with those operators.

1We like to mention that Dimiter Vakarelov posed this question in a private communication, though.

Concerning the logic S5_{m}(D), we like to make one additional remark here. Halpern and Moses ([5]) defined R_{D} to be the intersection of the R_{i}’s. Completeness proofs of S5_{m}(D) with respect to the class of models satisfying this intersection property were independently given in [2] and [12]. Let us make one remark concerning this notion of distributed knowledge, though. Inspired by our work on agent systems, we asked ourselves the following question. Given a language with finitely many propositional atoms and a finite model M and a state s. Can we have a protocol of communication such that we can guarantee that every distributively known fact φ in s becomes known by every individual agent? Surprisingly, the answer here is no! In [13] we show that it is even possible to have a situation in which all agents know already the same (so that communication cannot increase the individual knowledge), while there can be facts φ for which Dφ holds, although none of the agents knows φ. Thus, in this sense, φ is hardly to be considered distributed among the agents!

3 Postscript to our Paper

The paper [7] shows in many aspects Johan’s influence on our work. First of all, we employ three techniques in our completeness proof: firstly, we show how a filtration technique of Goldblatt can be used to gain one of the desired properties of the models. Next, we unravel this finite filtration, following ideas that were introduced by Sahlqvist for the mono-modal case. Finally, we use an equivalence relation to identify unravelled paths, the equivalence classes of this relation becoming the worlds that together constitute a new model.

Johan was, no doubt, the first who introduced and encouraged the use of such logical tools in the field. We also learned from him that one first should come up with clear conceptual notions and natural definitions to work with, but that, at the same time, investigating the technical subtleties is a crucial aspect for understanding those notions completely. Johan’s work seems to find the perfect match between these two aspects, without exception. We hope to have contributed to the investigation in some of the subtleties of epistemic logic in [7], by exploiting the differences between correspondence and canonical properties, for instance. The same applies to [13], where we demonstrated that when making a common-sense notion of ‘distributed knowledge’ precise, one encouters various technical problems and counter-intuitive properties.

Our paper [7] appeared in the proceedings of the first LOFT conference, held in 1994, a conference on Epistemic Logic and Game Theory. Johan is one of the few people that was involved in both the ‘American’ conference that addressed this issue (TARK) and this ‘European’ LOFT. We know that he, as an enthousiastic bridge builder, has tried to combine the two conferences to one, but institutes move slow, so that, for the time being, it is up to people like Johan to make the distributed knowledge over this to conferences explicit.

4 John-Jules’ Postscript

Although I myself never have had the pleasure and privilege of being his student in a formal way, I nevertheless owe much to Johan. Very concretely, he provided the incentive to study modal epistemic logic. While being a lecturer at the Free University (VU) in Amsterdam, I followed a course of Johan on logic for AI at the University of Amsterdam (UvA). I was so enthusiastic about it that I decided to develop such a course at the VU as well. Together with Jan Willem Klop the course was set up: Jan Willem focused on logic programming and resolution, while I concentrated on epistemic logic. This eventually (after some seven years...) resulted in the book on epistemic logic [9] that I have written jointly with my former Ph.D. student and now staff member Wiebe van der Hoek. (By the way, I’m also indebted to Johan for ’educating’ a substantial part of my present staff in Utrecht. Besides Wiebe also Frank de Boer and Henry Prakken got their first lessons in logic from Johan.) Johan was one of the first who tested the material in the book in the class room (of the UvA)! Furthermore, the research on epistemic logic together with Wiebe was a direct spin-off of the interest in the subject raised by Johan, as was our joint effort (by Johan, Peter van Emde Boas, Wiebe and me) of organising the TARK conference in The Netherlands in 1996.

Apart from these concrete connections I’m also very grateful to Johan for the keen interest he has always shown in my work on deontic logic and the work on intelligent agents that we are undertaking at the present, and, above all of course, for his broad interest in the application of logic in computer science and AI. As such, he is an inspirer to the community, and myself in particular, without an equal!

5 Wiebe’s Postscript

I am indebted to Johan in many, many ways. First of all, he taught me logic in the mid-eighties in Groningen. We mentioned above the three techniques that we used in the paper [7]. They connect me to Johan, in several ways. The first technique mentioned, filtration, was a technique that Johan taught at a modal logic course. It is one of the main techniques that I investigate for graded modal logic in my masters’ thesis. While working on my thesis in Groningen, Johan, being my supervisor, wrote me twice a letter with comments and suggestions on my thesis: each letter provided me with ideas to work for months!

The second technique, unravelling, I read about in a three-volumed thesis by Segerberg, which had a special reserved place on a bookshelf at the Philosophy department in Groningen, and which I read there in its quiet and pleasant library. The third technique, which is in fact a kind of rewrite technique, was a technique I developed during writing my PhD-thesis, of which Johan was a referent.

Now Johan is not even my referent anymore. But still, every time when I am presenting some of my work on an occasion where Johan is in the audience (the last time was LOFT again, 1998!), he shows an interest and provides me with useful hints, comments and cross-references.

Finally, much more than the logical techniques I learned from Johan, I am indebted for his inspiring and enrapturing approach to logic, science, and, last but not least, his genuine interest in other people and their work.

References

[1] R. Fagin, J.Y. Halpern, and M.Y. Vardi. What can machines know? Research Report RJ 6250, IBM, 1988. to appear in JACM.

[2] R.F. Fagin and J.Y. Halpern. Belief, awareness, and limited reasoning. Artificial Intelligence, 34:39–76, 1988.

[3] R.F. Fagin, J.Y. Halpern, and N. Megiddo. A logic for reasoning about probabilities. Information and Computation, 87(1/2):78–128, 1990.

[4] R. Goldblatt. Logics of Time and Computation, volume 7 of CSLI Lecture Notes. CSLI, Stanford, 1992. Second edition.

[5] J.Y. Halpern and Y. Moses. A guide to the modal logics of knowledge and belief. In Proc. IJCAI-85, pages 480–490, Los Angeles, CA, 1985.

[6] J.Y. Halpern and Y. Moses. A guide to the completeness and complexity for modal logics of knowledge and belief. Artificial Intelligence, 54:319–379, 1992.

[7] W. van der Hoek and J.-J.Ch Meyer. A complete epistemic logic for multiple agents– combining distributed and common knowledge. In P. Mongin M.O.L. Bacharach, L.A. Gerard-Varet and H.S. Shin, editors, Epistemic Logic and the Theory of Games and Decisions, pages 35–68. Kluwer, Dordrecht, 1997.

[8] S. Kraus and D. Lehmann. Knowledge, belief and time. Theoretical Computer Science, 85:155–174, 1988.

[9] J.-J. Meyer and W. van der Hoek. Epistemic Logic for AI and Computer Science. Number 41 in Cambridge Tracks in Theoretical Computer Science. Cambridge University Press, 1995.

[10] W. van der Hoek. Systems for knowledge and beliefs. Journal of Logic and Computation, 3(2):173–195, 1993.

[11] W. van der Hoek and M. de Rijke. Generalized quantifiers and modal logic. Journal of Logic, Language and Information, 2(1):19–58, 1993.

[12] W. van der Hoek and J.-J. Ch Meyer. Making some issues of implicit knowledge explicit. International Journal of Foundations of Computer Science, 3(2):193–224, 1992.

[13] W. van der Hoek, B. van Linder, and J.-J.Ch. Meyer. Group knowledge isn’t always distributed. In Proceedings of the Bi-annual Israelian Symposium on the Foundations of AI ’95, pages 191–200, 1995.