The question of whether knowledge is definable in terms of belief, which has played an important role in epistemology for the last 50 years, is studied here in the framework of epistemic and doxastic logics. Three notions of definability are considered: explicit definability, implicit definability, and reducibility, where explicit definability is equivalent to the combination of implicit definability and reducibility. It is shown that if knowledge satisfies any set of axioms contained in S5, then it cannot be explicitly defined in (...) terms of belief. S5 knowledge can be implicitly defined by belief, but not reduced to it. On the other hand, S4.4 knowledge and weaker notions of knowledge cannot be implicitly defined by belief, but can be reduced to it by defining knowledge as true belief. It is also shown that S5 knowledge cannot be reduced to belief and justification, provided that there are no axioms that involve both belief and justification. (shrink)

This paper provides a logic framework for investigations of game theoretical problems. We adopt an infinitary extension of classical predicate logic as the base logic of the framework. The reason for an infinitary extension is to express the common knowledge concept explicitly. Depending upon the choice of axioms on the knowledge operators, there is a hierarchy of logics. The limit case is an infinitary predicate extension of modal propositional logic KD4, and is of special interest in applications. In Part I, (...) we develop the basic framework, and show some applications: an epistemic axiomatization of Nash equilibrium and formal undecidability on the playability of a game. To show the formal undecidability, we use a term existence theorem, which will be proved in Part II. (shrink)

This paper provides a Genzten style formulation of the game logic framework GLm (0 m ), and proves the cut-elimination theorem for GLm. As its application, we prove the term existence theorem for GL used in Part I.

Kaneko-Suzuki developed epistemic logics of shallow depths with multiple players for investigations of game theoretical problems. By shallow depth, we mean that nested occurrences of belief operators of players in formulae are restricted, typically to be of finite depths, by a given epistemic structure. In this paper, we develop various methods of surgical operations (cut and paste) of epistemic world models. An example is a bouquet-making, i.e., tying several models into a bouquet. Another example is to engraft a model to (...) some branches of another model. By these methods, we obtain various meta-theorems on semantics and syntax on epistemic logics. To illustrate possible uses of our meta-theorems, we present one game theoretical theorem, which is also a meta-theorem in the sense of logic. (shrink)

Buchholz’s Ω μ+1-rules provide a major tool for the proof-theoretic analysis of arithmetical inductive definitions. The aim of this paper is to put this approach into the new context of modal fixed point logic. We introduce a deductive system based on an Ω-rule tailored for modal fixed point logic and develop the basic techniques for establishing soundness and completeness of the corresponding system. In the concluding section we prove a cut elimination and collapsing result similar to that of Buchholz (Iterated (...) inductive definitions and subsystems of analysis: recent proof theoretic studies. Lecture notes in mathematics, vol. 897, pp. 189–233, Springer, Berlin, 1981). (shrink)

We define infinitary extensions to classical epistemic logic systems, and add also a common belief modality, axiomatized in a finitary, fixed-point manner. In the infinitary K system, common belief turns to be provably equivalent to the conjunction of all the finite levels of mutual belief. In contrast, in the infinitary monotonic system, common belief implies every transfinite level of mutual belief but is never implied by it. We conclude that the fixed-point notion of common belief is more powerful than the (...) iterative notion of common belief. (shrink)

The question of whether knowledge is definable in terms of belief, which has played an important role in epistemology for the last 50 years, is studied here in the framework of epistemic and doxastic logics. Three notions of definability are considered: explicit definability, implicit definability, and reducibility, where explicit definability is equivalent to the combination of implicit definability and reducibility. It is shown that if knowledge satisfies any set of axioms contained in S5, then it cannot be explicitly defined in (...) terms of belief. S5 knowledge can be implicitly defined by belief, but not reduced to it. On the other hand, S4.4 knowledge and weaker notions of knowledge cannot be implicitly defined by belief, but can be reduced to it by defining knowledge as true belief. It is also shown that S5 knowledge cannot be reduced to belief and justification, provided that there are no axioms that involve both belief and justification. (shrink)

For some modal fixed point logics, there are deductive systems that enjoy syntactic cut-elimination. An early example is the system in Pliuskevicius [15] for LTL. More recent examples are the systems by the authors of this paper for the logic of common knowledge [5] and by Hill and Poggiolesi for PDL[8], which are based on a form of deep inference. These logics can be seen as fragments of the modal mu-calculus. Here we are interested in how far this approach can (...) be pushed in general. To this end, we introduce a nested sequent system with syntactic cut-elimination which is incomplete for the modal mu-calculus, but complete with respect to a restricted language that allows only fixed points of a certain form. This restricted language includes the logic of common knowledge and PDL. There is also a traditional sequent system for the modal mu-calculus by Jäger et al. [9], without a syntactic cut-elimination procedure. We embed that system into ours and vice versa, thus establishing cut-elimination also for the shallow system, when only the restricted language is considered. (shrink)