Reports on Mathematical Logic

No. 37

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$. 

Back to Main Menu