<figure><img src="image_1.png" /></figure>

HAL
open science

A Sound and Complete Axiomatic System for Modality

$$ \phi \equiv \_1\phi \wedge \_2\phi $$

Shaobo Deng, Meiying Sun, Cungen Cao, Yuefei Sui

► To cite this version:

Shaobo Deng, Meiying Sun, Cungen Cao, Yuefei Sui. A Sound and Complete Axiomatic System for Modality $\phi \equiv \_1\phi \wedge \_2\phi$. 8th International Conference on Intelligent Information Processing (IIP), Oct 2014, Hangzhou, China. pp.152-160, 10.1007/978-3-662-44980-6_17. hal-01383328

HAL Id: hal-01383328

https://inria.hal.science/hal-01383328

Submitted on 18 Oct 2016

**HAL** is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_2.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
A Sound And Complete Axiomatic System For
Modality □φ ≡ □₁φ ∧ □₂φ

Shaobo Deng*,**, Meiying Sun*,**, Cungen Cao*, Yuefei Sui*

*Key Laboratory of Intelligent Information Processing,
Institute of Computing Technology,
Chinese Academy of Science,
Beijing,
100190,
China
houjiyuan2002@163.com

**University of Chinese Academy of Sciences,
Beijing,
100049,
China

**Abstract:** An axiomatic system is presented in this paper, which has a modal operator □ such that □φ ≡ □₁φ ∧ □₂φ, where □₁ and □₂ are the modal operators of the language for the axiom system S5. The axiomatic system for □ is proved to be sound and complete.

**Keywords:** Modal logic, Axiomatic system S5, Soundness, Completeness, Canonical model

# 1 Introduction

The modal logic has many axiomatic systems, such as K, T, D, B, S4 and S5 ([1]). The axiom system S5 is characterized by all equivalence frames([1]). The approximation spaces for Rough sets can be used as the possible-world semantics for S5. Let an approximate space (U, R) be an equivalence frame (W, R) for S5, i.e., U = W. Then for any formula φ, if the interpretation of φ corresponds to a subset X of U, then the lower and upper approximations of X correspond to the interpretations of □φ and ◊φ, respectively, and the equivalence relation R corresponds to the accessibility relation for □([2]).

Given two approximation spaces (U, R₁) and (U, R₂), R₁ ∪ R₂ may not be an equivalence relation. Given two modal operators □₁ and □₂, let R₁ and R₂ be the accessibility relations for □₁ and □₂, respectively. Let □ be a modal operator such that R₁ ∪ R₂ is the accessibility relation for □, that is, M, w ⊧ □φ iff for any w' ∈ W if (w, w') ∈ R₁ ∪ R₂ then M, w' ⊧ φ, which implies and is implied by that for any w' ∈ W if (w, w') ∈ R₁ then M, w' ⊧ φ and for any w' ∈ W if (w, w') ∈ R₂ then M, w' ⊧ φ, i.e., M, w ⊧ □₁φ and M, w ⊧ □₂φ if and only if M, w ⊧ □φ.
Let $\Box$ be a modal operator such that for any possible world $w, M, w \models \Box\varphi$
iff $M, w \models \Box_1\varphi$ and $M, w \models \Box_2\varphi$, i.e., for any formula $\varphi$, $\Box\varphi \equiv \Box_1\varphi \wedge \Box_2\varphi$. In
this paper, we consider the modal operator $\Box\varphi \equiv \Box_1\varphi \wedge \Box_2\varphi$. We shall give
the language, the syntax and the semantics for the modal logic with modal
operator $\Box\varphi \equiv \Box_1\varphi \wedge \Box_2\varphi$. The axiomatic system for $\Box$ will be given and
proved to be sound and complete.

The main contribution of this paper is that a propositional modal logic with a modal operator $\Box\varphi \equiv \Box_1\varphi \wedge \Box_2\varphi$. The axiomatic system for $\Box$ is sound, and complete with respect to the class of all reflective and symmetric frames, where the accessibility relation $R$ for $\Box$ is equivalent to $R_1 \cup R_2$, where $R_i$ is the equivalence relation for $\Box_i$ and $i = 1, 2$.

If $R_1 = R_2$, then the axiomatic system for $\Box$ turns out to be $S_5$.

This paper is organized as follows: the propositional modal logic with modal operator $\Box\varphi \equiv \Box_1\varphi \wedge \Box_2\varphi$ is described in section 2, including the language, the syntax and the semantics for the logic. Then we shall give the axiomatic system for $\Box$ and prove the soundness theorem and the completeness theorem. Section 3 summarizes results of the paper and discusses some possible extension of the logic.

## 2 The propositional modal logic with modal operator $\Box\varphi \equiv \Box_1\varphi \wedge \Box_2\varphi$

In this section, we shall give the language, the syntax and the semantics for the propositional modal logic with the modality $\Box\varphi \equiv \Box_1\varphi \wedge \Box_2\varphi$. The axiomatic system for $\Box$ is denoted by $S_{51} \wedge S_{52}$, then we prove that $S_{51} \wedge S_{52}$ is sound and complete.

### 2.1 The language, syntax and semantics for the logic

The language for $S_{51} \wedge S_{52}$ contains the following symbols:

* propositional variables: $p_0, p_1, \dots$;

* logical connectives: $\neg, \rightarrow$;

* modalities: $\Box, \Box_1, \Box_2$;

* auxiliary symbols: $(,)$.

Formulas:

$$ \varphi := p|\varphi_1 \rightarrow \varphi_2|\neg\varphi_1|\Box\varphi_1; $$

$$ \Box\varphi := \Box_1\varphi_1 \wedge \Box_2\varphi_1. $$

Other operators:

$$ (\alpha \vee \beta) =_{\text{def}} (\neg\alpha \rightarrow \beta); $$

$$ (\alpha \wedge \beta) =_{\text{def}} \neg(\alpha \rightarrow \neg\beta); $$

$$ (\alpha \leftrightarrow \beta) =_{\text{def}} ((\alpha \rightarrow \beta) \wedge (\beta \rightarrow \alpha)); $$

$$ (\diamond\alpha) =_{\text{def}} (\neg\Box\neg\alpha). $$
**Definition 2.1.** A frame $F$ is a triple $\langle W, R_1, R_2 \rangle$, where $W$ is a non-empty set of possible worlds, and $R_1 \subseteq W^2$ and $R_2 \subseteq W^2$ are the equivalence relations defined over the members of $W$ and the accessibility relations for $\square_1$ and $\square_2$, respectively.

**Definition 2.2.** A model $M$ is a quadruple $\langle W, R_1, R_2, I \rangle$, where $\langle W, R_1, R_2 \rangle$ is a frame and $I$ is an interpretation such that for any propositional variable $p$ $I(p) \subseteq W$ and for any $w \in I(p)$ $p$ is true in $w$.

A satisfaction relation $\vdash$, between any formula $\varphi$ and any possible world $w$, is defined as follows:

**Definition 2.3.** Given any model $M$, any possible world $w \in W$ and any formula $\varphi$,

$$ M, w \models \varphi \text{ iff } \left\{ \begin{array}{ll} w \in I(p) & \text{if } \varphi = p \\ M, w \not\models \varphi_1 & \text{if } \varphi = \neg \varphi_1 \\ M, w \models \varphi_1 \Rightarrow M, w \models \varphi_2 & \text{if } \varphi = \varphi_1 \rightarrow \varphi_2 \\ \text{for all } w' \in W \text{ if } wR_1w' \text{ then } M, w' \models \varphi_1, \text{ and} \\ \text{for all } w' \in W \text{ if } wR_2w' \text{ then } M, w' \models \varphi_1 & \text{if } \varphi = \square \varphi_1 \end{array} \right. $$

By the definition of the satisfaction relation, we can give the following definition:

**Definition 2.4.** A formula $\varphi$ is valid in a model $M$, denoted by $M \models \varphi$, iff for any $w \in W$, $M, w \models \varphi$; a formula $\varphi$ is valid in a frame $F$, denoted by $F \models \varphi$, iff for any model $M$ based on $F$, $M \models \varphi$; let $C$ be a class of frames. A formula $\varphi$ is valid in $C$ iff for any $F \in C$, $F \models \varphi$; $\Sigma \models_C \varphi$ iff for any frame $F \in C$ if $F \models \Sigma$ then $F \models \varphi$. If $\Sigma = \emptyset$ then $\models_C \varphi$.

Now we give the following axiom schemas and inference rules for $^{S5_1} \wedge ^{S5_2}$:

* **Axiom schemas:**

$$ L1 \quad \varphi \rightarrow (\psi \rightarrow \varphi) $$

$$ L2 \quad (\varphi \rightarrow (\psi \rightarrow \mu)) \rightarrow ((\varphi \rightarrow \psi) \rightarrow (\varphi \rightarrow \mu)) $$

$$ L3 \quad (\neg\psi \rightarrow \neg\varphi) \rightarrow (\varphi \rightarrow \psi) $$

$$ L4 \quad \Box(\varphi \rightarrow \psi) \rightarrow (\Box\varphi \rightarrow \Box\psi) $$

$$ L5 \quad \Box\varphi \rightarrow \varphi $$

$$ L6 \quad \varphi \rightarrow \Box\Diamond\varphi $$

$$ L7_1 \quad \Box_1\varphi \rightarrow \Box_1\Box_1\varphi $$

$$ L7_2 \quad \Box_2\varphi \rightarrow \Box_2\Box_2\varphi $$

* **Inference rules:**

$$ (MP) \quad \frac{\varphi, \varphi \rightarrow \psi}{\psi} $$

$$ (N) \quad \frac{\varphi}{\Box\varphi} $$
**Definition 2.5.** A formula $\varphi$ is provable from $\Gamma$, denoted by $\Gamma \vdash \varphi$, if there is a sequence of formulas $\varphi_1, \dots, \varphi_n$ such that $\varphi = \varphi_n$, and for each $1 \le i \le n$, either $\varphi_i$ is an axiom or a formula in $\Gamma$, or is deduced from the previous formulas via one of the deduction rules.

## 2.2 The Soundness Theorem

This section is to prove the soundness theorem by induction on the length of proofs. Before giving the proof, we give the following lemmas:

**Lemma2.1.** Each axiom schema is valid.

*Proof*. As for the axiom schema $L_1, L_2, L_3$, we do not check their validity and two references are [1] and [3].

(L5) By the definition 2.3, it is easy to prove it.

(L6) By the definition 2.3, it is easy to prove it.

(L7₁) Since the accessibility relation $R_1$ for $\Box_1$ is an equivalence relation, it follows that $\Box_1\varphi \to \Box_1\Box_1\varphi$ is valid.

(L7₂) Since the accessibility relation $R_2$ for $\Box_2$ is an equivalence relation, it follows that $\Box_2\varphi \to \Box_2\Box_2\varphi$ is valid.

□

**Lemma2.2.** The deduction rules preserve validity.

*Proof*. We prove that $(N)$ preserves the validity. Since for any model $\langle W, R_1, R_2, I \rangle$ based on any frame $\langle W, R_1, R_2 \rangle$ and any $w \in W$, $M, w \models \varphi$.

Let $w_1$ be any possible world. Since $R_1$ and $R_2$ are the equivalence relations on $W$, we can obtain that for any $w'_1 \in W$ if $w_1 R_1 w'_1$ then $M, w'_1 \models \varphi$, and for any $w''_1 \in W$ if $w_1 R_2 w''_1$ then $M, w''_1 \models \varphi$. It follows that $M, w_1 \models \Box\varphi$. Since for any $w_1 \in W$, $M, w_1 \models \Box\varphi$, it follows that $\models \Box\varphi$.

□

**Theorem 2.1(The Soundness Theorem).** For any set of formulas $\Gamma$ and formula $\varphi$, if $\Gamma \vdash \varphi$, then $\Gamma \models \varphi$.

*Proof*. For any set of formulas $\Gamma$ and formula $\varphi$, since $\Gamma \vdash \varphi$, $\varphi$ is the last member of a sequence which is a deduction from $\Gamma$. So we can use induction on the number of the sequence to prove this theorem as follows:

For the base step, the sequence has only one formula, namely $\varphi$. Then $\varphi$ must be an axiom of $S^{51} \wedge S^{52}$ or a member of $\Gamma$, and then $\Gamma \models \varphi$.

Now suppose that the sequence contains $n$ formulas, where $n>1$, and suppose as induction hypothesis that $\Gamma \models \alpha$ follows from $\Gamma \vdash \alpha$, which sequence is fewer than $n$ members. There are the following cases:

**Case a.** $\varphi$ is an axiom of $S^{51} \wedge S^{52}$ or a member of $\Gamma$, then we have $\Gamma \models \varphi$.

**Case b.** $\varphi$ is obtained by modus ponens rule from a formula $\psi$ and a formula $\psi \to \varphi$ in the sequence. So by induction hypothesis, it obtains that $\Gamma \models \psi$ and $\Gamma \models \psi \to \varphi$, then it follows that $\Gamma \models \varphi$.

**Case c.** $\varphi = \Box\psi$ is obtained by the inference rule $N$ from $\psi$. So by induction hypothesis, it follows that $\Gamma \models \psi$. Since if for any model $\langle W, R_1, R_2, I \rangle$
based on any frame $\langle W, R_1, R_2 \rangle$ and any $w \in W M, w \models \psi$ then for any model $\langle W, R_1, R_2, I \rangle$ based on any frame $\langle W, R_1, R_2 \rangle$ and any $w \in W M, w \models \Box \psi$, it follows that $\Gamma \models \Box \psi$.

## 2.3 The completeness theorem

The completeness theorem is to be proved in this section. The proof method of the complete theorem is similar to the classical canonical model method ([1]). We shall construct two relations on W and prove whether the two relations are equivalence relations or not. And one relation corresponds to the accessibility relation for $\Box_1$, while the other corresponds to the accessibility relation for $\Box_2$.

**Definition 2.6.** $\Gamma$ is consistent iff there is no finite set $\{\varphi_1, ..., \varphi_n\} \subseteq \Gamma$ such that:

$$ \vdash \neg(\varphi_1 \wedge \dots \wedge \varphi_n). $$

By definition 2.6, we can prove that $\Gamma$ is inconsistent iff there is some formula $\varphi$ such that $\Gamma \vdash \varphi$ and $\Gamma \vdash \neg \varphi$.

**Lemma 2.3.** Suppose that $\Sigma$ is a consistent set of formulas. Then there is a maximal consistent set of formulas $\Sigma^*$ such that $\Sigma \subseteq \Sigma^*$.

In constructing a model in which the possible worlds are maximal consistent sets of formulas we will have to specify when one world is accessible from another(that model, in this paper, is also called canonical model). Thereby, the accessibility relation $R_1$ and $R_2$, in the canonical model, is defined as follows:

**Definition 2.7.** For any two distinct maximal consistent sets $\Sigma_1^*, \Sigma_2^*$, we define two binary relations $R_1$ and $R_2$ on W as follows:

(1) We shall say that $\Sigma_1^* R_1 \Sigma_2^*$ iff $\Sigma_1^*$ and $\Sigma_2^*$ satisfy the following condition: For any formula $\varphi$ if $\Box \varphi \in \Sigma_1^*$ then $\varphi \in \Sigma_2^*$ (written: $S^-(\Sigma_1^*) = \{\varphi : \Box \varphi \in \Sigma_1^*\}$).

(2) We shall say that $\Sigma_1^* R_2 \Sigma_2^*$ iff $\Sigma_1^*$ and $\Sigma_2^*$ satisfy the following condition: For any formula $\varphi$ if $\Box \varphi \in \Sigma_1^*$ then $\varphi \in \Sigma_2^*$ (written: $S(\Sigma_1^*) = \{\Box \varphi : \Box \varphi \in \Sigma_1^*\}$).

**Lemma 2.4.** Let $\Gamma^* = \{\Sigma_0^*, \Sigma_1^*, ...\}$ be the set of all maximal consistent sets. If for any $i, j \in N$ we define $\Sigma_i^* R_1 \Sigma_j^*$ iff $S^-(\Sigma_i^*) \subseteq \Sigma_j^*$, and $\Sigma_i^* R_2 \Sigma_j^*$ iff $S(\Sigma_i^*) \subseteq \Sigma_j^*$, then both the relation $R_1$ and $R_2$ are equivalence relations on W.

*Proof.* (1) In order to prove that $R_1$ is an equivalence relation, we shall prove the following three conditions:

1) For any $i \in N$, if $\Sigma_i^* \in \Gamma^*$ then $\Sigma_i^* R_1 \Sigma_i^*$.

2) For any $\Sigma_i^*, \Sigma_j^* \in \Gamma^*$, if $\Sigma_i^* R_1 \Sigma_j^*$ then $\Sigma_j^* R_1 \Sigma_i^*$.

3) For any $\Sigma_1^*, \Sigma_2^*, \Sigma_3^* \in \Gamma^*$, if $\Sigma_1^* R_1 \Sigma_2^*$ and $\Sigma_2^* R_1 \Sigma_3^*$ then $\Sigma_1^* R_1 \Sigma_3^*$.

1). For any $i \in N$, we shall prove $S^-(\Sigma_i^*) \subseteq \Sigma_i^*$. For any formula $\varphi$, if $\Box \varphi \in \Sigma_i^*$ then $\varphi \in S^-(\Sigma_i^*)$. Since $\Box \varphi \rightarrow \varphi(L_5)$ and $\Box \varphi \in \Sigma_i^*$, $\varphi \in \Sigma_i^*$. It follows that $S^-(\Sigma_i^*) \subseteq \Sigma_i^*$.
2). We shall prove that if $S^-(\Sigma_i^*) \subseteq \Sigma_j^*$ then $S^-(\Sigma_j^*) \subseteq \Sigma_i^*$, that is to say, we shall prove that for any formula $\beta$ if $\Box\beta \in \Sigma_j^*$ then $\beta \in \Sigma_i^*$. Suppose $\beta \notin \Sigma_i^*$. $\neg\beta \in \Sigma_i^*$. By $L_6$ and $\neg\beta \in \Sigma_i^*$ it follows that $\Box\Diamond\neg\beta \in \Sigma_i^*$.

Since $S^-(\Sigma_i^*) \subseteq \Sigma_j^*$, it follows that $\Diamond\neg\beta \in \Sigma_j^*$, that is, $\neg\Box\beta \in \Sigma_j^*$. Since $\neg\Box\beta \in \Sigma_j^*$ and $\Box\beta \in \Sigma_j^*$, $\Sigma_j^*$ is not consistent, which is a contradiction to the hypothesis of this lemma.

3). We need to prove that if $S^-(\Sigma_1^*) \subseteq \Sigma_2^*$ and $S^-(\Sigma_2^*) \subseteq \Sigma_3^*$ then $S^-(\Sigma_1^*) \subseteq \Sigma_3^*$, that is to say, for any formula $\beta$, if $\Box\beta \in \Sigma_1^*$ then $\beta \in \Sigma_3^*$. We can prove it by $L_5$ and $L_7$.

What we need to explain is that $R_1$ is the accessibility relation for $\Box_1$ and in this case for any formula $\varphi$ $\Box\varphi \equiv \Box_1\varphi$. Thereby, we can use the axiom schema $L_7$.

(2) Now, we prove that the relation $R_2$ is an equivalence relation. the following three conditions shall be proved:

1) For any $i \in N$, if $\Sigma_i^* \in \Gamma^*$ then $\Sigma_i^* R_2 \Sigma_i^*$.

2) For any $\Sigma_i^*, \Sigma_j^* \in \Gamma^*$, if $\Sigma_i^* R_2 \Sigma_j^*$ then $\Sigma_j^* R_2 \Sigma_i^*$.

3) For any $\Sigma_1^*, \Sigma_2^*, \Sigma_3^* \in \Gamma^*$, if $\Sigma_1^* R_2 \Sigma_2^*$ and $\Sigma_2^* R_2 \Sigma_3^*$ then $\Sigma_1^* R_2 \Sigma_3^*$.

It is easy to prove the item 1)-3). We omit the proof procedures.

□

**Lemma 2.5.** Let $\Gamma$ be any consistent set of formulas containing $\neg\Box\psi$, then $S^-(\Gamma) \cup \{\neg\psi\}$ is consistent and $S(\Gamma) \cup \{\neg\psi\}$ is consistent, where $S^-(\Gamma) = \{\varphi : \Box\varphi \in \Gamma\}$ and $S(\Gamma) = \{\Box\varphi : \Box\varphi \in \Gamma\}$.

*Proof.* (1) We shall prove that $S^-(\Gamma) \cup \{\neg\psi\}$ is consistent as follows:

Suppose that $S^-(\Gamma) \cup \{\neg\psi\}$ is not consistent. Then there exists some finite subset $\{\varphi_1, \dots, \varphi_n\} \cup \{\neg\psi\}$ of $S^-(\Gamma) \cup \{\neg\psi\}$ such that $\vdash \neg(\varphi_1 \wedge \dots \wedge \varphi_n \wedge \neg\psi)$.

Then

$$ 
\begin{array}{lclcl}
\vdash (\varphi_1 \wedge \dots \wedge \varphi_n) \rightarrow \neg\psi & \text{iff} & \vdash \Box (\varphi_1 \wedge \dots \wedge \varphi_n) \rightarrow \psi \\
& & \text{iff} & \vdash \Box (\varphi_1 \wedge \dots \wedge \varphi_n) \rightarrow \Box\psi \\
& & \text{iff} & \vdash (\Box\varphi_1 \wedge \dots \wedge \Box\varphi_n) \rightarrow \Box\psi \\
& & \text{iff} & \vdash \neg(\Box\varphi_1 \wedge \dots \wedge \Box\varphi_n \wedge \neg\Box\psi)
\end{array}
$$

Thereby, $\{\Box\varphi_1, \dots, \Box\varphi_n\} \cup \{\neg\Box\psi\}$ is not consistent. By the definition of $S^-(\Gamma)$ it follows that $\{\Box\varphi_1, \dots, \Box\varphi_n\} \cup \{\neg\Box\psi\}$ is a subset of $\Gamma$. Thereby, $\Gamma$ is not consistent, which is a contradiction to the hypothesis of this lemma.

(2) We shall prove that $S(\Gamma) \cup \{\neg\psi\}$ is consistent as follows. Suppose that $S(\Gamma) \cup \{\neg\psi\}$ is not consistent. Then there exists some finite subset $\{\Box\varphi_1, \dots, \Box\varphi_n\} \cup \{\neg\psi\}$ of $S(\Gamma) \cup \{\neg\psi\}$ such that $\vdash \neg(\Box\varphi_1 \wedge \dots \wedge \Box\varphi_n \wedge \neg\psi)$. Then

$$ 
\begin{array}{lclcl}
\vdash (\Box\varphi_1 \wedge \dots \wedge \Box\varphi_n) \rightarrow \neg\psi & \text{iff} & \vdash \Box(\Box\varphi_1 \wedge \dots \wedge \Box\varphi_n) \rightarrow \psi \\
& & \text{iff} & \vdash \Box(\Box\varphi_1 \wedge \dots \wedge \Box\varphi_n) \rightarrow \Box\psi \\
& & \text{iff} & \vdash (\Box\varphi_1 \wedge \dots \wedge \Box\varphi_n) \rightarrow \Box\psi \\
& & \text{iff} & \vdash \neg(\Box\Box\varphi_1 \wedge \dots \wedge \Box\Box\varphi_n \wedge \neg\Box\psi)
\end{array}
$$
Thereby, {$\Box\Box\varphi_1, ..., \Box\Box\varphi_n$} $\cup$ {$\neg\Box\psi$} is not consistent. For any $\Box\varphi_i$, by $L_7(\Box\varphi \equiv \Box_2\varphi)$ it follows that $\Box\Box\varphi \in \Gamma$, where $i=1,...,n$. Thereby, {$\Box\Box\varphi_1, ..., \Box\Box\varphi_n$} $\cup$ {$\neg\Box\psi$} is a subset of $\Gamma$. Then $\Gamma$ is not consistent, which is a contradiction to the hypothesis of this lemma.

What we need to explain is that $R_2$ is the accessibility relation for $\Box_2$ and in this case for any formula $\varphi$ $\Box\varphi \equiv \Box_2\varphi$. Thereby, we can use the axiom schema $L_7_2$.

□

The canonical model for $^{S5_1} \wedge ^{S5_2}$, $M$, is like any other model, a quadruple $(W, R_1, R_2, I)$. $W$ is the set of all sets of maximal consistent sets of formulas. I.e. $w \in W$ iff $w$ is a maximal consistent set of formulas. If $w$ and $w'$ are both in $W$, then $wR_1w'$ iff $S^-(w) \subseteq w'$. And if $w$ and $w'$ are both in $W$, then $wR_2w'$ iff $S(w) \subseteq w'$. For any propositional variable $p$ $I(p) \subseteq W$, and for any $w \in I(p)$ $p$ is true in $w$ iff $p \in w$. For any other formula this has to be proved as follows:

**Lemma 2.6.** Let $M = (W, R_1, R_2, I)$ be the canonical model for $^{S5_1} \wedge ^{S5_2}$. Then for any formula $\varphi$ and any world $w$, $M, w \models \varphi$ iff $\varphi \in w$.

*Proof.* We prove the lemma by induction on the structure of formulas.

**Case a.** $\varphi := p$: By definition, this lemma holds.

**Case b.** $\varphi := \neg\alpha$:

$$M, w \models \neg\alpha \quad \begin{array}{l} \text{iff } M, w \not\models \alpha \\ \text{iff } \alpha \notin w \\ \text{iff } \neg\alpha \in w \end{array}$$

**Case c.** $\varphi := \alpha \rightarrow \beta$:

$$\alpha \rightarrow \beta \notin w \quad \begin{array}{l} \text{iff } \neg(\alpha \rightarrow \beta) \in w \\ \text{iff } \alpha \in w \text{ and } \neg\beta \in w \\ \text{iff } M, w \models \alpha \text{ and } M, w \not\models \beta \\ \text{iff } M, w \not\models \alpha \rightarrow \beta \end{array}$$

**Case d.** $\varphi := \Box\alpha$:

(=$\Box$) **Subcase d.1.** $\Box\alpha \in w$: By the definition of $R_1, R_2$, we have the following two cases:

(1) For any $w' \in W$, if $wR_1w'$ then $\alpha \in w'$. $\alpha \in w'$ iff $M, w' \models \alpha$ by induction hypothesis. Then $M, w' \models \Box\alpha$ because for any $w'$ if $wR_1w'$ and $M, w' \models \alpha$.

(2) For any $w' \in W$, if $wR_2w'$ then $\Box\alpha \in w'$. Since $\Box\alpha \in w'$ and $\Box\alpha \rightarrow \alpha$, $\alpha \in w'$. $\alpha \in w'$ iff $M, w' \models \alpha$ by induction hypothesis. Then $M, w' \models \Box\alpha$ because for any $w'$ if $wR_2w'$ and $M, w' \models \alpha$.

**Subcase d.2.** $\neg\Box\alpha \in w$: By the lemma 2.5, both $S^-(w) \cup \{\neg\alpha\}$ and $S(w) \cup \{\neg\alpha\}$ are consistent. By the lemma 2.3, we can enlarge $S^-(w) \cup \{\neg\alpha\}$ and $S(w) \cup \{\neg\alpha\}$ into maximal consistent sets of formulas $w_1$ and $w_2$, respectively. Thereby, there exist $w_1, w_2$ such that $S^-(w) \subseteq w_1$ and $S(w) \subseteq w_2$.
Since $S^-(w) \subseteq w_1$ and $S(w) \subseteq w_2$, by the definition of $R_1$ and $R_2$, it
follows that $wR_1w_1$ and $wR_2w_2$. For $\neg\alpha \in w_1$ and $\neg\alpha \in w_2$, it follows that
$M, w_1 \models \neg\alpha$ and $M, w_2 \models \neg\alpha$ by induction hypothesis. So there exist $w_1, w_2$
such that $wR_1w_1$ and $wR_2w_2$ and $M, w_1 \models \neg\alpha$ and $M, w_2 \models \neg\alpha$. Therefore,
by the definition 2.3, it follows that $M, w \not\models \Box\alpha$.

(⇒) **Subcase d.3.** $M, w \models \Box\alpha$: By the definition 2.3, we have:

(1) For any $w' \in W$, if $wR_1w'$ then $M, w' \models \alpha$; and

(2) For any $w' \in W$, if $wR_2w'$ then $M, w' \models \alpha$.

From (1), we have:

(3) For any $w' \in W$, if $wR_1w'$ then $\alpha \in w'$ by induction hypothesis.

From (2), we have:

(4) For any $w' \in W$, if $wR_2w'$ then $\alpha \in w'$ by induction hypothesis.

Assume $\neg\Box\alpha \in w$. Since $w$ is a maximal consistent set of formulas, it follows
that there exists $w_1, w_2 \in W$ such that $wR_1w_1$ and $wR_2w_2$ and $\neg\alpha \in w_1$
and $\neg\alpha \in w_2$ by the lemma 2.5. So $\neg\alpha \in w_1$ is a contradiction to (3), and
$\neg\alpha \in w_1$ and $\neg\alpha \in w_2$ is also a contradiction to (4). Thereby, $\Box\alpha \in w$ for $w$ is
a maximal consistent set of formulas.

**Subcase d.4.** $M, w \not\models \Box\alpha$: By the definition 2.3, we have:

(1) There exists $w_1 \in W$ such that $wR_1w_1$ and $M, w_1 \not\models \alpha$; or

(2) There exists $w_2 \in W$ such that $wR_2w_2$ and $M, w_2 \not\models \alpha$.

From (1), by induction hypothesis, $\neg\alpha \in w_1$; and from (2), $\neg\alpha \in w_2$. Suppose $\Box\alpha \in w$, by the definition of $R_1$ and $R_2$, it follows that:

(3) For any $w' \in W$ if $wR_1w'$ then $\alpha \in w'$; and

(4) For any $w' \in W$ if $wR_2w'$ then $\Box\alpha \in w'$.

From (4) and L5, we have:

(5) For any $w' \in W$ if $wR_2w'$ then $\alpha \in w'$.

It follows that (3) is in contradiction with $wR_1w_1$ and $\neg\alpha \in w_1$. And (5) also
is in contradiction with $wR_2w_2$ and $\alpha \in w_2$. Thereby, $\neg\Box\alpha \in w$ for that $w$ is
a maximal consistent set of formulas.

<figure><img src="image_3.png" /></figure>

**Theorem 2.2(The Completeness Theorem):** For any set of formulas
$\Gamma$ and formula_3ϕ, if Γ ⊢ ϕ, then Γ ⊢ ϕ.

*Proof*. Suppose $\Gamma \not\vdash \varphi$, so $\Gamma \cup \{\neg\varphi\}$ is consistent. Then there is a maximal consistent set of formulas $w$ such that $\Gamma \cup \{\neg\varphi\} \subseteq w$ by the lemma 2.3.

Let $M = (W, R_1, R_2, I)$ be a canonical model, where $W$ is the set of all sets of maximal consistent sets of formulas. I.e. $w \in W$ iff $w$ is a maximal consistent set of formulas. If $w$ and $w'$ are both in $W$, then $wR_1w'$ iff $S^-(w) \subseteq w'$. And if $w$ and $w'$ are both in $W$, then $wR_2w'$ iff $S(w) \subseteq w'$. By the lemma 2.4 it follows that $R_1$ and $R_2$ are the equivalence relations on $W$.

For any formula $\alpha \in \Gamma \cup \{\neg\varphi\}$, $\alpha \in w$. By the theorem 2.6, $M, w \models \alpha$. So $M, w \models \Sigma$ and $v \models \neg\varphi$, which is a contradiction to $\Sigma \models \varphi$.

So for any set of formulas $\Gamma$ and formula_3\varphi, if $\Gamma \models \varphi$, then $\Gamma \vdash \varphi$.

<figure><img src="image_4.png" /></figure>
## 3 Conclusion

In this paper, we present an axiomatic system for a modality $\Box\varphi \equiv \Box_1\varphi \wedge \Box_2\varphi$, and prove that the axiomatic system for $\Box$ is sound and complete. The axiomatic system for $\Box$ is different from S5. What we need to point out is that $L7_1$ and $L7_2$ are not the axiom schemas for $\Box$, which is needed when proving the completeness theorem. An interesting problem is to give a sound and complete axiomatic system for the modality corresponding to the accessibility relation $R = R_1 \cap R_2$, where the equivalence relation $R_i$ is the accessibility relation for $\Box_i, i = 1, 2$.

## Acknowledgement:

This work is supported by National Natural Science Foundation of China under grant No. 91224006, 61035004, 61173063, 61203284, 61363047, and the ministry of science and technology project under grant No. 201303107.

## References

[1] George Edward Hughes and Maxwell John Cresswell. *A new introduction to modal logic*. Burns & Oates, 1996.

[2] Tsau Young Lin and Qing Liu. First-order rough logic i: approximate reasoning via rough sets. *Fundamenta Informaticae*, 27(2):137–153, 1996.

[3] H-D Ebbinghaus, Jörg Flum, and Wolfgang Thomas. *Mathematical logic*. Springer Verlag, 1994.

[4] Walter A Carnielli, Claudio Pizzi, and Juliana Bueno-Soler. *Modalities and multimodalities*, volume 12. Springer, 2008.

[5] Giovanna Corsi and Eugenio Orlandelli. Free quantified epistemic logics. *Studia Logica*, 101(6):1159–1183, 2013.

[6] Roberto Blanco, Gregorio de Miguel Casado, José Ignacio Requeno, and José Manuel Colom. Temporal logics for phylogenetic analysis via model checking. In *Bioinformatics and Biomedicine Workshops (BIBMW), 2010 IEEE International Conference on*, pages 152–157. IEEE, 2010.

[7] Carlo Proietti. Intuitionistic epistemic logic, kripke models and fitchs paradox. *Journal of philosophical logic*, 41(5):877–900, 2012.

[8] Johan Van Benthem and Ştefan Minică. Toward a dynamic logic of questions. In *Logic, Rationality, and Interaction*, pages 27–41. Springer, 2009.
[9] Floor Sietsma and Jan van Eijck. Action emulation between canonical models. In *Proceedings of the 10th Conference on Logic and the Foundations of Game and Decision Theory*, page 6, 2012.