Yoshihito TANAKA:
Some proof systems for predicate common knowledge logic
A b s t r a c t. 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$.