A new system of common knowledge predicate logic

Takashi Nagashima^{∗}

Private address: 351-76 Kohan 2-chōme, Higashiyamato-shi, 207-0002 Japan

                      nagasima-t@mta.biglobe.ne.jp
                   http://www2s.biglobe.ne.jp/~hotori/

Yoshihito Tanaka^{∗} Kyushu Sangyo University, 2-3-1 Matsukadai, Higashi-ku, Fukuoka 813-8503, Japan

                        ytanaka@ip.kyusan-u.ac.jp

January 12, 2000, at MLG meeting in Yuzawa

Abstract

We propose a Kripke complete sequent calculus for common knowledge predicate logic^{1}. Though the system is infinitary, it is finitary except for one inference rule.

Kaneko and Nagashima [KN96, KN97] proposed a system GL_{ω} for predicate common knowledge logic. The system GL_{ω} is infinitary in the following sense: (1) GL_{ω} allows conjunctions and disjunctions of countably many formulae. Common knowledge is defined as an infinite conjunction. (2) GL_{ω} has inference rules with countably many premises.

Halpern and Moses [HM92] proposed a finitary system for propositional common knowledge logic. In contrast to GL_{ω}, Halpern and Moses’ system has a symbol for common knowledge. The system has a set of an axiom and an inference rule which defines common knowledge as a fixed point.

A seemingly natural system for predicate common knowledge logic would be obtained by adding quantification rules to Halpern and Moses’ system. However, this cannot be Kripke complete. Indeed, any Kripke complete system for predicate common knowledge logic cannot be finitary because of the following: Fact. (Wolter [W99]) Any Kripke complete system for predicate common knowledge logic is not recursively enumerable.

Here we propose a Kripke complete sequent calculus CK for common knowledge predicate logic. Though the system CK is infinitary, it is finitary except for one inference rule. The system CK has a symbol for common knowledge, and the meaning of this symbol is determined with two inference rules.

The language L of CK consists of the following symbols. A positive integer n is fixed throughout this article. Free variables a_{0}, a_{1}, … (countably many). Bound variables x_{0}, x_{1}, … (countably many). Individual constants (at most finite). Predicate letters. Logical symbols ¬, ⊃, ∧, ∨, ∀, ∃. Epistemic symbols K_{1}, …, K_{n}, C.

∗Supported partially by Grant-in-Aid for Scientific Research, Ministry of Education, Science and Culture.The authors would like thank to Mamoru Kaneko and Nobu-Yuki Suzuki for their valuable comments.

1We consider common knowledge logics based upon KD4, but similar arguments may be carried out for some other modal logics such as K, S4 and so on.

N = {1, …, n} is the set of agents or players. K_{i} means that agent i knows (or believes) a proposition. C means that it is common knowledge among the agents in N.

Formulae are constructed as in the classical predicate logic with the additional rules: If A is a formula then K_{i}A is a formula (i = 1, …, n); If A is a formula then CA is a formula.

A sequent is an expression of the form Γ ⟶ Θ where Γ and Θ are finite sets of formulae.

Let N^{∗} be the set of all words i_{1} … i_{m} (i_{1} ∈ N, …, i_{m} ∈ N, m ≥ 0) on the alphabet N = {1, …, n}. The concatenation of words u ∈ N^{∗} and v ∈ N^{∗} is denoted as uv. The length of a word w ∈ N^{∗} is denoted as |w|. Let N^{⟨ω⟩} = {i_{1} … i_{m} | m ≥ 0, i_{1} ≠ i_{2} ≠ … ≠ i_{m}} ⊂ N^{∗}. For a word e = i_{1} … i_{m} ∈ N^{⟨ω⟩}, K_{i_{1}} ⋯ K_{i_{m}} is abbreviated as K_{e}. For e = i_{1}i_{2} … i_{m} ∈ N^{⟨ω⟩} and e′ = j_{1}j_{2} … j_{l} ∈ N^{⟨ω⟩}, e ∗ e′ is defined as

e ∗ e′ = \{ \begin{matrix}i_{1}i_{2} … i_{m}j_{2} … j_{l} & if e ≠ ε, e′ ≠ ε and i_{m} = j_{1}, \\ i_{1}i_{2} … i_{m}j_{1}j_{2} … j_{l} = ee′ & otherwise. \end{matrix}

N^{⟨ω⟩} is closed under this operation. Now we introduce a notation K[u; Δ; A] where A is a formula, u ∈ N^{∗}, and Δ is a sequence of formulae such that |u| = |Δ|. K[i_{1}i_{2} … i_{k}; D_{1}, D_{2}, …, D_{k}; A] means

K_{i_{1}}(D_{1} ⊃ K_{i_{2}}(D_{2} ⊃ … ⊃ K_{i_{k}}(D_{k} ⊃ A) …)).

The notation K[u; Δ; A] is meaningful only when |u| = |Δ|.

The system CK has the following schemas for initial sequents and inference rules. The only infinitary rule is (→ C), which has countably many premises.

Initial Sequent: A ⟶ A Inference rules:

{Γ ⟶ Θ \atop Γ, Δ ⟶ Θ, Λ} (set)
\begin{matrix}Γ ⟶ Θ, A & A, Δ ⟶ Λ \\ Γ, Δ ⟶ Θ, Λ \end{matrix} (cut)
{Γ ⟶ Θ, A \atop ¬A, Γ ⟶ Θ} (¬ →)  {A, Γ ⟶ Θ \atop Γ ⟶ Θ, ¬A} (→ ¬)
\begin{matrix}Γ ⟶ Θ, A & B, Δ ⟶ Λ \\ A ⊃ B, Γ, Δ ⟶ Θ, Λ \end{matrix} (⊃ →)  {A, Γ ⟶ Θ, B \atop Γ ⟶ Θ, A ⊃ B} (→ ⊃)

\begin{matrix}{B, Γ ⟶ Θ \atop A ∧ B, Γ ⟶ Θ} & (∧ →) \\ {A, Γ ⟶ Θ \atop A ∧ B, Γ ⟶ Θ} & (∧ →) \end{matrix}  \begin{matrix}Γ ⟶ Θ, A & Γ ⟶ Θ, B \\ Γ ⟶ Θ, A ∧ B \end{matrix} (→ ∧)

\begin{matrix}A, Γ ⟶ Θ & B, Γ ⟶ Θ \\ A ∨ B, Γ ⟶ Θ \end{matrix} (∨ →)  \begin{matrix}{Γ ⟶ Θ, A \atop Γ ⟶ Θ, A ∨ B} & (→ ∨) \\ {Γ ⟶ Θ, B \atop Γ ⟶ Θ, A ∨ B} & (→ ∨) \end{matrix}

{F (t), Γ ⟶ Θ \atop ∀x F (x), Γ ⟶ Θ} (∀ →)  {Γ ⟶ Θ, K[u; Δ; F (a)] \atop Γ ⟶ Θ, K[u; Δ; ∀x F (x)]} (→ ∀) (u ∈ N^{∗})
{F (a), Γ ⟶ Θ \atop ∃x F (x), Γ ⟶ Θ} (∃ →)  {Γ ⟶ Θ, F (t) \atop Γ ⟶ Θ, ∃x F (x)} (→ ∃)
{Γ, K_{i}Δ ⟶ Θ \atop K_{i}Γ, K_{i}Δ ⟶ K_{i}Θ} (K_{i}) (i ∈ N , |Θ| ≤ 1)

{K_{e}A, Γ ⟶ Θ \atop CA, Γ ⟶ Θ} (C →) (e ∈ N^{⟨ω⟩})  \{Γ ⟶ Θ, K[u; Δ; K_{e}A] | e ∈ N^{⟨ω⟩}\} ; Γ ⟶ Θ, K[u; Δ; CA] (→ C) (u ∈ N^{∗})

Condition on variables: In the rules (→ ∀) and (∃ →), the free variable a should not occur in the lower sequent.

We define the fixed-point systems HM^{2}, QHM and QHM + BF as follows. The language L′ of HM is the propositional fragment of L. The system HM is Hilbert style calculus for propositional multimodal KD4_{n} with an additional axiom

2Slightly different from the original systems in [HM92] but the difference is not essential.

CA ⊃ A ∧ K_{1}CA ∧ … ∧ K_{n}CA

and an additional inference rule

{B ⊃ A ∧ K_{1}B ∧ … ∧ K_{n}B \atop B ⊃ CA} .

The quantificational extension QHM is a system over L, and it has additional quantification rules same as in classical predicate logic. The system QHM + BF is QHM with additional Barcan axiom BF:

∀x K_{i}F (x) ⊃ K_{i}∀x F (x).

Theorem 1. CK is Kripke complete.

Proof will be reported at proof 2000 meeting^{3}.

Lemma 2. ⊢_{CK} K_{u}A ⟶ K[u; Δ; A] and ⊢_{CK} K[u; ⊤, …, ⊤; A] ⟶ K_{u}A, where ⊤ is A_{0} ⊃ A_{0} and A_{0} is any closed atomic formula.

Theorem 3. [Barcan rule] ⊢_{CK} ∀x K_{i}F (x) ⟶ K_{i}∀x F (x). Proof. By Lemma 2,

\begin{matrix}\begin{matrix}{K_{i}F (a) ⟶ K_{i}(⊤ ⊃ F (a)) \atop ∀x K_{i}F (x) ⟶ K_{i}(⊤ ⊃ F (a))} & (∀ →) \\ ∀x K_{i}F (x) ⟶ K_{i}(⊤ ⊃ ∀x F (x)) \end{matrix} ; (→ ∀) & K_{i}(⊤ ⊃ ∀x F (x)) ⟶ K_{i}∀x F (x) \\ ∀x K_{i}F (x) ⟶ K_{i}∀x F (x) \end{matrix} (cut)

Lemma 4. If ⊢_{CK} K_{e_{1}}A_{1}, …, K_{e_{m}}A_{m} ⟶ Θ and if |Θ| ≤ 1 then ⊢_{CK} K_{e∗e_{1}}A_{1}, …, K_{e∗e_{m}}A_{m} ⟶ K_{e}Θ.

Lemma 5. [Barcan rule for K_{e}] ⊢_{CK} ∀x K_{e}F (x) ⟶ K_{e}∀x F (x).

Theorem 6. [Barcan rule for C] ⊢_{CK} ∀x CF (x) ⟶ C∀x F (x).

Theorem 7. [Conservativeness] If A contains none of K_{1}, …, K_{n}, C then ⊢_{CK} A ⟺ ⊢_{LK} A. Proof. Similarly as in proof of Proposition 4.1 of [KN96], the result of eliminating all occurrences of K_{1}, …, K_{n}, C from a CK-proof can be easily transformed into an LK-proof.

Theorem 8. [Conservativeness] If A contains no C then ⊢_{CK} A if and only if A is provable in QKD4_{n} + BF, where QKD4_{n} is the quantificational extension of multimodal KD4_{n}.

Conjecture. If no C occurs positively in a CK-provable formula A then there exists a CK-proof of A without (→ C).

Lemma 9. (1) ⊢_{CK} CA ⟶ A.  (2) ⊢_{CK} CA ⟶ K_{i}CA.  (3) ⊢_{CK} CA ⟶ CCA.

(4) If ⊢_{CK} Γ ⟶ A then ⊢_{CK} CΓ ⟶ CA.

Theorem 10. A CK-provable formula containing none of K_{1}, …, K_{n} is provable in S4 if we regard C as the box symbol . Conversely, a S4-provable formula is provable in CK if we regard as C. Proof. First we replace all occurrences of K_{1}, …, K_{n}, C by in a given CK-proof. The result of this replacement can be easily converted into an S4-proof. The converse follows from Lemma 9.

Theorem 11. [Conservativeness] If a quantifier-free sequent Γ ⟶ Θ is provable in CK then there exists a CK-proof of Γ ⟶ Θ without quantifier rules. Corollary 12. If a quantifier-free formula is provable in CK, then it is provable in HM.^{4}

Theorem 13. [Fixed point] ⊢_{CK} CA ⟶ A ∧ K_{1}CA ∧ … ∧ K_{n}CA and ⊢_{CK} A, K_{1}CA, …, K_{n}CA ⟶ CA.

3“Shōmeiron kenkyūshūkai”, January 18–20, Tokyo University, Komaba, Tokyo

4Cf. Kaneko’s Theorem 3.4 in [K99]

Theorem 14. If ⊢_{CK} B ⟶ A ∧ K_{1}B ∧ … K_{n}B then ⊢_{CK} B ⟶ CA.

Definition. [K99] A formula in GL_{ω} is a cc-formula if it satisfies the following conditions.

(1) It contains no infinitary disjunction.

(2) If it contains an infinitary conjunction then the conjunction has the form ∧{K_{e}B | e ∈ N^{⟨ω⟩}} for some B.

Definition. [K99] We define a mapping ψ which transforms a L-formula into a cc-formula. Definition is by induction on the structure of formula.

(1) If no C occurs in A, then ψ(A) is A.

(2) ψ(A ⊃ B) is ψ(A) ⊃ ψ(B) and similarly for the other logical symbols.

(3) ψ(K_{i}A) is K_{i}(ψ(A)).

(4) ψ(CA) is ∧{K_{e}(ψ(A)) | e ∈ N^{⟨ω⟩}}.

Kaneko [K99] proved that ψ is a bijection from the set of L-formulae to the set of cc-formulae. Theorem 15. If a formula A is provable in CK, then ψ(A) is provable in GL_{ω}.

Theorem 16. If a cc-formula A is provable in GL_{ω}, then ψ^{−1}(A) is provable in CK.

For a certain propositional fragment of GL_{ω}, a corresponding theorem is proved by Kaneko [K99]. Proof. If a cc-formula A is provable in GL_{ω}, then ψ^{−1}(A) is valid in every Kripke model of CK, hence provable.

Any formula provable in QHM + BF is provable in CK, but not conversely. Open problems. (1) Find a formula that is CK-provable but not provable in QHM + BF. (2) [Hiroakira Ono] What X makes QHM + BF + X equivalent to CK?

References

[HM92] Halpern, Joseph Y. and Moses, Yoram:

A guide to completeness and complexity for modal logics of knowledge and belief .

Artificial Intelligence, 54 (1992), pp. 319–379.

[K99] Kaneko, Mamoru: Common knowledge logic and game logic.

J. Symbolic Logic, 64, No. 2 (1999), pp.685–700.

[KN96] Kaneko, Mamoru and Nagashima, Takashi: Game logic and its applications I . Studia Logica, Vol.57 (1996), pp.325–354.

[KN97] Kaneko, Mamoru and Nagashima, Takashi: Game logic and its applications II . Studia Logica, Vol.58 (1997), pp.273–303.

[W98] Wolter, Frank: Fragments of common knowledge logics.

Invited talk at LOFT3, to appear in Studia Logica.

     Manuscript available at http://www.informatik.uni-leipzig.de/~wolter/.