##
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