A Map of Common Knowledge Logics^{∗}

(with M. Kaneko, T. Nagashima and Y. Tanaka)

Nobu-Yuki SUZUKI^{†}

                       smnsuzu@ipc.shizuoka.ac.jp

Department of Mathematics, Faculty of Science, Shizuoka University

Abstract

In order to capture the concept of common knowledge in the framework of multi-modal (epistemic) logics, various extensions of multi-modal epistemic logics, such as finitary ones and infinitary ones, have been proposed. The case of propositional epistemic logics, these extensions turn out to be all Kripke complete. F. Wolter showed that any finitary predicate common knowledge logic is Kripke incomplete. However, if we go further to an infinitary extension, the Kripke completeness would be recovered. Thus there is some gap in predicate case. The aim of this article is to give an overview of the finitary and infinitary approaches to common knowledge logics.

Introduction

Multi-agent epistemic logics have been developed for various investigations such as AI (see e.g. Meyer-van der Hoek [8]) and game theoretical problems (see e.g. Kaneko [3]). In such situations, common knowledge is important in discussing knowledge (or beliefs) shared among agents. Various extensions of multi-agent logics have been proposed in order to capture the concept of common knowledge in the framework of multi-modal (epistemic) logics. These extensions are divided into two types: the finitary approach such as Halpern-Moses’ fixed-point logics (Halpern-Moses [1]), and the infinitary approach such as Kaneko-Nagashima’s game logics (Kaneko-Nagashima [4, 5]). Some of them are given as propositional logics and some others as predicate logics. Also, some are considered from the model-theoretic viewpoint and some others from the proof-theoretic viewpoint. The aim of this article is to give an overview of finitary and infinitary approaches to common knowledge logics mainly from the viewpoint of Kripke completeness.

In the propositional case, these extensions turn out to be all Kripke complete, and are directly comparable in the sense that either two logics are deductively equivalent or if one is an extension of another, it is also a conservative extension. In contrast, F. Wolter [12] proved in the predicate case that the set of valid formulas in the Kripke semantics (with constant domain) is not recursively enumerable in the presence of common knowledge. This implies the Kripke-incompleteness theorem that any finitary predicate extension of the Halpern-Moses type common knowledge logic cannot capture the Kripke semantics with common knowledge. In other words, the latter has no finitary proof theory. Nevertheless, it is also known from Tanaka-Ono [10] and Tanaka [11] that this difficulty does not occur in the infinitary approach. Thus, the predicate case has some great difference between the finitary and infinitary approaches. In presenting our overview of common knowledge logics, we will focus especially on what this difference is.

Diagram 1 gives some extant extensions of multi-agent epistemic logics in proof theoretical setting. Since we discuss a variety of common knowledge extensions, we make a particular choice of basic epistemic axioms on knowledge operators. We adopt KD4-type axioms, starting with propositional multi-agent epistemic logic KD4^{n}, where n is the number of agents. The prefix Q means the predicate extension of a propositional logic together with the Barcan axiom. Logic HM is the fixed-point type extension of KD4^{n} due to Halpern-Moses [1], where the common knowledge of a formula is determined by adding one axiom and one inference rule to KD4^{n}. The game logic GL_{ω} is an infinitary extension of KD4^{n}, and QGL_{ω} is its predicate extension, due to Kaneko-Nagashima [4] and [5], where the common knowledge of a formula is expressed as an infinitary conjunctive formula.

∗This article is based on the author’s joint work [7] with M. Kaneko, T. Nagashima and Y. Tanaka.

†Department of Mathematics, Faculty of Science, Shizuoka University, Ohya 836, Shizuoka 422–8529, Japan. The author is supported in part by Grant-in-Aids for Scientific Research No. 13640111, Japan Society for the Promotion of Science.

Finitary Base Logic Finitary Infinitary
Propositional  KD4^{n}  HM  GL_{ω}
Predicate  QKD4^{n}  QHM  QGL_{ω}

Diagram 1

The Kripke completeness of KD4^{n} and that of QKD4^{n} are known as variants of the completeness results given in the modal logic literature (cf., Hughes-Cresswell [2]). It is also known from Halpern-Moses [1] that HM is Kripke complete. It follows from Tanaka-Ono [10] that GL_{ω} is also Kripke complete. These completeness results in the propositional case imply that if one logic is an extension of another, then it is a conservative extension.

On the other hand, it is known in the predicate case that there is a gap between QHM and QGL_{ω}. As already mentioned, the Kripke completeness of QKD4^{n} is known, and that of QGL_{ω} is proved in Tanaka [11]. However, we have Wolter’s Kripke-incompleteness theorem for QHM.

From the syntactical point of view, the distance between QHM and QGL_{ω} is large in that QGL_{ω} allows infinitary conjunctions and disjunctions as well as infinitary proofs. To consider the question of where the gap occurs, we provide two other logics, propositional CX and CY, and their predicate extensions QCX and QCY. These new logics are intermediate between HM, QHM and GL_{ω}, QGL_{ω} in that they have the set of finitary formulas in the same way as HM and QHM but admit infinitary proofs similar to GL_{ω} and QGL_{ω}.

In the propositional case, both CX and CY are shown to be deductively equivalent to HM. In the predicate case, QCY is Kripke complete, which is shown in Tanaka [11]. This result together with Wolter’s incompleteness theorem implies that QCY is deductively different from QHM. The completeness of QCX remains open, though QCX looks more natural as a common knowledge logic than QCY.

The deductive equivalence of HM, CX and CY to GL_{ω}, as far as relevant formulas are concerned, is shown by proving that HM, CX and CY are faithfully embedded into GL_{ω}. In the predicate case, only QCY is faithfully embedded into to QGL_{ω}. The faithful embedding of QCX into QGL_{ω} remains open.

Concluding Remarks

1. From our considerations, we draw Diagram 2. The map has four rows: The above two give the logics considered in the propositional and predicate cases. The two additional rows explain the characteristics of each logic, e.g., QHM has finitary formulae and finitary proofs, while QCX has finitary formulae but infinitary proofs. The arrow → denotes the relationship of deductive strength and ⇝ that of being faithfully embedded.

KD4^{n} → HM ⟷ CX ⟷ CY ⇝ GL_{ω}
↓ ↓ ↓ ↓ ↓
QKD4^{n} → QHM → QCX → QCY ⇝ QGL_{ω}
formulae finitary  finitary  finitary  infinitary
proofs  finitary  finitary  infinitary  infinitary

Diagram 2

No serious problems remain in the propositional case. All the logics from KD4^{n} to GL_{ω} are Kripke complete, and HM, CX, CY are deductively equivalent. They can be faithfully embedded into GL_{ω}. Also, GL_{ω} is a conservative extension of KD4^{n}. On the other hand, we have met various problems in the predicate case. The logics QKD4^{n}, QCY, and QGL_{ω} are Kripke complete, but QHM is Kripke incomplete. The Kripke completeness of QCX remains open. The logic QCY is faithfully embedded into QGL_{ω}, and QGL_{ω} is a conservative extension of QKD4^{n}. Though faithfulness of embedding of QHM into QGL_{ω} fails to hold. The faithful embedding problem of QCX into QGL_{ω} remains still open.

In Diagram 2, the gap exists around QHM and QCX. There is a formula that is valid in the Kripke semantics but is not provable in QHM. However it is also an open problem to find a concrete one.

2. Recall that MH is Kripke complete but QHM is not. We may see the difference between the above facts from two points of view.

First, let us see the above theorems from the finitary point of view. It is well-known that both KD4^{n} and QKD4^{n} are Kripke complete and have recursively enumerable sets of provable formulas. In the propositional case, HM is complete and {A |A is propositional and ⊧ A} is also recursively enumerable, while in the predicate case, F. Wolter [12] proved that QHM is incomplete and {A |A is predicate and ⊧ A} is not recursively enumerable. Although HM and QHM are obtained from KD4^{n} and QKD4^{n}, respectively, by adding both finitary axiom schema and inference rule, only the logic QHM turns out to be incomplete. In this sense, this incompleteness of QHM seems to be an unexpected jump.

Second, let us see the above two theorems from the infinitary point of view. In the infinitary approach, completeness results are known. Indeed, Kripke completeness is recovered in the sense that the strengthened provability in an infinitary approach captures {A | A is predicate and ⊧ A}. In the propositional case, Kaneko [6] proved that HM can be regarded as a fragment of infinitary propositional epistemic logics. Hence we can regard HM as well as QHM as having already an infinitary aspect in part. The non-recursive-enumerability of {A | A is predicate and ⊧ A} is better understood from this point of view. In this sense, from the infinitary point of view, we may regard the completeness of HM as an unexpected result, rather than the incompleteness of QHM.

3. We have been focussed on extensions of QHM rather than on its fragments. On the other hand, Sturm-Wolter-Zakharyaschev [9] considered the monodic fragment of QHM. They proved the Kripke completeness of the monodic fragment of QHM. This fragment is located between HM and QHM. The gap between QHM and QCY occurs after the monodic fragment of QHM.

References

[1] Halpern, J. Y., and Y. Moses, A guide to completeness and complexity for modal logics of knowledge and beliefs, Artificial Intelligence 54 (1992), 319–379.

[2] Hughes, G. E., and M. J. Cresswell, A Companion to Modal Logic, Methuen &Co. London.

[3] Kaneko, M., Epistemic logics and their applictions: Introduction, to appear in the special issue “Logic and Economics” of Economic Theory.

[4] Kaneko, M., and T. Nagashima, Game logic and its applications I, Studia Logica 57 (1996), 325– 354.

[5] Kaneko, M., and T. Nagashima, Game logic and its applications II, Studia Logica 58 (1997), 273–303.

[6] Kaneko, M., Common knowledge logic and game logic, Journal of Symbolic Logic 64 (1999), 685–700.

[7] Kaneko, M., T. Nagashima, N.-Y. Suzuki and Y. Tanaka, A map of common knowledge logics, to appear in Studia Logica.

[8] Meyer, J.-J. Ch. and W. van der Hoek, Epistemic Logic for AI and Computer Science, Cambridge University Press, 1995.

[9] Sturm, H., F. Wolter and M. Zakharyaschev, Monodic epistemic predicate logic, to appear in the special issue “Logic and Economics” of Economic Theory.

[10] Tanaka, Y., and H. Ono, The Rasiowa-Sikorski lemma and Kripke completeness of predicate and infinitary modal logics, Advances in Modal Logics Vol.2 (2001), CSLI Publications, pp.401–419.

[11] Tanaka, Y., Some proof systems for common knowledge predicate logic, Mimeo.

[12] Wolter, F., First order common knowledge logics, Studia Logica 65 (2000), 249–271.