We see a systematic set of cut-free axiomatisations for all the basic normal modal logics formed by some combination the axioms d, t, b, 4, 5. They employ a form of deep inference but otherwise stay very close to Gentzen’s sequent calculus, in particular they enjoy a subformula property in the literal sense. No semantic notions are used inside the proof systems, in particular there is no use of labels. All their rules are invertible and the rules cut, weakening and (...) contraction are admissible. All systems admit a straightforward terminating proof search procedure as well as a syntactic cut elimination procedure. (shrink)

Epistemic logic has grown from its philosophical beginnings to find diverse applications in computer science, and as a means of reasoning about the knowledge and belief of agents. This book provides a broad introduction to the subject, along with many exercises and their solutions. The authors begin by presenting the necessary apparatus from mathematics and logic, including Kripke semantics and the well-known modal logics K, T, S4 and S5. Then they turn to applications in the context of distributed systems and (...) artificial intelligence. These include the notions of common knowledge, distributed knowledge, explicit and implicit belief, the interplays between knowledge and time, and knowledge and action, as well as a graded (or numerical) variant of the epistemic operators. The authors also discuss extensively the problem of logical omniscience. They cover Halpern & Moses' theory of honest formulas, and they make a digression into the realm of nonmonotonic reasoning and preferential entailment. They discuss Moore's autoepistemic logic, together with Levesque's related logic of "all I know". Furthermore, they show how one can base default and counterfactual reasoning on epistemic logic. Graduate students in philosophy or in computer science, especially those with an interest in AI, will find this book useful. (shrink)

Common knowledge logic is a multi-modal epistemic logic with a modal operator which describes common knowledge condition. In this paper, we discuss some proof systems for the logic $\ckpl$, the predicate common knowledge logic characterized by the class of all Kripke frames with constant domains. Various systems for $\ckpl$ and other related logics are surveyed by Kaneko-Nagashima-Suzuki-Tanaka, however, they did not give a proof of the completeness theorem of their main system for $\ckpl$. We first give a proof of their (...) completeness theorem by an algebraic method. Next, we give a cut-free system for $\ckpl$, and show that the class of formulas in $\ckpl$ which have some positive occurrences of the common knowledge operator and some occurrences of knowledge operators and quantifiers is not recursively axiomatizable and its complement is recursively axiomatizable. As a corollary, we obtain a cut-free system for the predicate modal logic $\logick$ with the Barcan formula $\barcan$. (shrink)