# The Correspondence between Propositional Modal Logic with Axiom $\varphi \leftrightarrow \varphi$ and the Propositional Logic

Meiying Sun, Shaobo Deng, Yuefei Sui

► To cite this version:

Meiying Sun, Shaobo Deng, Yuefei Sui. The Correspondence between Propositional Modal Logic with Axiom $\varphi \leftrightarrow \varphi$ and the Propositional Logic. 8th International Conference on Intelligent Information Processing (IIP), Oct 2014, Hangzhou, China. pp.141-151, 10.1007/978-3-662-44980-6_16 . hal-01383327

HAL Id: hal-01383327

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

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_1.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
# The Correspondence Between Propositional Modal Logic with Axiom $\Box\varphi \leftrightarrow \Diamond\varphi$ and the Propositional Logic

Meiying Sun¹,², Shaobo Deng¹,² and Yuefei Sui¹

¹ Key Laboratory of Intelligent Information Processing,
Institute of Computing Technology, Chinese Academy of Sciences
Beijing China, 100190

² University of Chinese Academy of Sciences
Beijing China, 100049

sunmeiying07@mails.ucas.ac.cn

**Abstract.** The propositional modal logic is obtained by adding the necessity operator $\Box$ to the propositional logic. Each formula in the propositional logic is equivalent to a formula in the disjunctive normal form. In order to obtain the correspondence between the propositional modal logic and the propositional logic, we add the axiom $\Box\varphi \leftrightarrow \Diamond\varphi$ to K and get a new system $K^+$. Each formula in such a logic is equivalent to a formula in the disjunctive normal form, where $\Box^k(k \ge 0)$ only occurs before an atomic formula $p$, and $\neg$ only occurs before a pseudo-atomic formula of form $\Box^k p$. Maximally consistent sets of $K^+$ have a property holding in the propositional logic: a set of pseudo-atom-complete formulas uniquely determines a maximally consistent set. When a pseudo-atomic formula $\Box^k p_i(k, i \ge 0)$ is corresponding to a propositional variable $q_{ki}$, each formula in $K^+$ then can be corresponding to a formula in the propositional logic $P^+$. We can also get the correspondence of models between $K^+$ and $P^+$. Then we get correspondences of theorems and valid formulas between them. So, the soundness theorem and the completeness theorem of $K^+$ follow directly from those of $P^+$.

**Keywords:** propositional modal logic; propositional logic; disjunctive normal form; pseudo-atomic formula; pseudo-atom-complete; completeness

## 1 Introduction

Van Benthem gave the standard translation[1, 2] from the propositional modal logic into the first-order logic. The necessity operator $\Box$ corresponds to the universal quantifier $\forall$ via the standard translation and every modal formula corresponds to a first-order formula. Benthem discussed connections between modal axioms and first-order properties of the accessibility relation among worlds in the paper[3]. For example, the formula $\Box p \rightarrow p$ is valid on all reflexive frames. In order to solve the classical problems arising from the interplay between propositional attitudes, quantifiers and the notion of identity, Aloni proposed the conceptual covers semantics of the first-order modal logic[4, 5].

There are a number of systems of propositional modal logic, like K, D, T, S5, Triv and Ver. Trivially, K is a subsystem of all the others, and every normal
modal system<fnref n="1" /> is contained either in Triv or in Ver. We also have that every
consistent system which contains D is contained in Triv[7]. Each formula in S5
can be equivalent to a formula in the modal conjunctive normal form[7], and
each conjunct is the disjunction of φ or □φ or ◊φ, where φ is a formula of
the propositional logic. This makes the proof of the completeness of S5 much
easier and provides an effective procedure for determining whether or not a
formula is a theorem of S5 and S5-valid[7]. Similarly, Triv can collapse into
the propositional logic and Ver provides a different form of collapsing into the
propositional logic[7].

In the propositional logic, any formula is equivalent to a formula in the disjunctive normal form and each disjunct is the conjunction of atomic formula or its negation[8]. If there is a modal system S such that each formula can also be equivalent to a formula in the disjunctive normal form, then we can easily get a correspondence between S and the propositional logic. In K necessity can only be distributed over conjunction and possibility can only be distributed over disjunction. In order to distribute necessity over disjunction, we add the axiom □φ ↔ ◊φ to K and construct a new normal modal system K⁺.

In K<sup>+</sup> necessity can be distributed over conjunction and disjunction. And it is easy to prove that the formula □¬φ ↔ ¬□φ is a theorem of K<sup>+</sup>. Therefore the system K<sup>+</sup> has a remarkable property that any formula can be equivalent to a formula in the disjunctive normal form and each disjunct is the conjunction of pseudo-atomic formulas □<sup>k</sup>p(k ≥ 0) or the negation of a pseudo-atomic formula. Then discussions of logical properties of K<sup>+</sup> reduce to discussions of logical properties of the propositional logic.

We have the concept of atom-completeness in the propositional logic, and in K⁺ we correspondingly give the definition of pseudo-atom-completeness. In K⁺ for any pseudo-atom-complete set A of formulas, if we delete one □ from each φ in A then the new set □⁻A is also pseudo-atom-complete. Each atom-complete set of formulas in the propositional logic determines a maximally consistent set in a unique way. Similarly, each pseudo-atom-complete set of formulas in K⁺ uniquely determines a maximally consistent set. So the accessibility relation in the canonical model[7] of K⁺ can be simply given by eliminating one □ from each pseudo-atomic formula in a possible world.

Assume that $P^+ = \{q_{ki} : k, i \ge 0\}$ is a language of the propositional logic. When a pseudo-atomic formula $\Box^k p_i(k, i \ge 0)$ is corresponding to a propositional variable $q_{ki}$, each formula in $K^+$ then can be corresponding to a formula in $P^+$. Then we can prove that any theorem of $K^+$ can be corresponding to a theorem of $P^+$, and vice versa. The semantics of $K^+$ is the possible world semantics, which is a set of models of $P^+$. For any model $M$ of $K^+$ and any possible world $w$ in $M$ we can construct an assignement $v_w$ of $P^+$ such that for any formula $\varphi$ of $K^+$, $M, w \models \varphi$ if and only if $v_w \models \varphi'$, where $\varphi'$ is the cor-

<footnote n="1">¹A normal modal system is a consistent extension of the system K which retains the rules MP and N. And the definition can be found in [6, 7].</footnote>
responding formula of $\varphi$. Then we can prove that any valid formula of $K^+$ can be corresponding to a valid formula of $P^+$, and vice versa. So, the soundness theorem and the completeness theorem of $K^+$ follow directly from those of $P^+$.

This paper is organized as follows: the next section gives the basic definition of the propositional modal logic K; the third section defines the propositional modal logic $K^+$ and gives the disjunctive normal form of formulas in $K^+$; the fourth section defines pseudo-atom-complete, and proves that each maximally consistent set of formulas is uniquely generated by a pseudo-atom-complete set of formulas; the fifth section gives correspondences between $K^+$ and the propositional logic $P^+$, and get the soundness and completeness of $K^+$; and the last section concludes the whole paper.

## 2 The propositional modal logic K

This section gives the basic definitions of the propositional modal logic K, including the language, the syntax and the semantics, where the syntax gives the definitions of formulas, axioms and inference rules; and the semantics defines the models, satisfaction and validity. K is sound and complete, and proofs can be found in [7, 9].

Let the logical language $L$ of the propositional modal logic contain the following symbols:

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

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

* the necessary modality: $\square$;

* auxiliary symbols: $(,)$.

A formula of the propositional modal logic is defined as follows<fnref n="2" />:

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

The possible modality $\Diamond$ and the necessary modality $\Box$ are dual. For any formula $\varphi$,

$$ \Diamond\varphi =_{df} \neg\Box\neg\varphi. $$

**Definition 1** A frame $F$ of the propositional modal logic is an ordered pair $(W, R)$, where $W$ is a non-empty set of possible worlds, and $R \subseteq W^2$ is a dyadic relation defined over the members of $W$.

For any possible worlds $w, w' \in W$, $(w, w') \in R$ is usually denoted by $wRw'$. Frames can be classified by the relation $R$, and details of the classification can be found in [7, 9].

**Definition 2** A model $M$ is an ordered triple $(W, R, I)$, where $(W, R)$ is a frame; and $I$ is an interpretation such that for any propositional variable $p, I(p) \subseteq W$.

<footnote n="2">²The logical connectives $\wedge$, $\vee$ and $\leftrightarrow$ can be defined by $\neg$ and $\rightarrow$. For example, $\varphi \wedge \psi =_{df} \neg(\varphi \rightarrow \neg\psi)$, where$_{df}$ is read as “be defined as”.</footnote>
A model $\langle W, R, I \rangle$ is said to be based on the frame $\langle W, R \rangle$.

A model we define here is called a standard model, which is different from a Kripke model [10]. You can see the difference between them in [6] and any standard model can be transformed into a Kripke model[6].

**Definition 3** Given a model $M$, for any possible world $w$,

$$ M, w \models \varphi \text{ if and only if } \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, \\ \mathbf{A}w'((w, w') \in R \Rightarrow M, w' \models \varphi_1) & \text{if } \varphi = \Box \varphi_1, \end{array} \right. $$

where $\mathbf{A}w'$ means “for any possible world $w'$”. We will give definitions of validity of formulas in a model, a frame and a class of frames.

**Definition 4** A formula $\varphi$ is valid in a model $M$, denoted by $M \models \varphi$, if $\varphi$ is true at every world in $M$. A formula $\varphi$ is valid on a frame $F$, denoted by $F \models \varphi$, if $\varphi$ is valid in every model based on $F$. Given a class of frames $C$, a formula $\varphi$ is valid with respect to $C$, if $\varphi$ is valid on every frame in $C$.

Given a set $\Gamma$ of formulas and a formula $\varphi$, and $C$ is a class of frames, $\varphi$ is a logical consequence of $\Gamma$ in $C$, denoted by

$$ \Gamma \models_C \varphi, $$

if for any frame $F \in C$ and model $M$ based on $F$, $M \models \Gamma$ implies $M \models \varphi$. In this section we mainly talk about the system K, which is characterized by all frames. So we will use $\Gamma \models \varphi$ to denote $\Gamma \models_C \varphi$.

In the following we will give the axiom system of the propositional modal logic K.

Axioms:

$$ \begin{array}{l} \varphi_1 \rightarrow (\varphi_2 \rightarrow \varphi_1), \\ (\varphi_1 \rightarrow (\varphi_2 \rightarrow \varphi_3)) \rightarrow ((\varphi_1 \rightarrow \varphi_2) \rightarrow (\varphi_1 \rightarrow \varphi_3)), \\ (\varphi_1 \rightarrow \varphi_2) \rightarrow (\neg \varphi_2 \rightarrow \neg \varphi_1), \\ \Box (\varphi_1 \rightarrow \varphi_2) \rightarrow (\Box \varphi_1 \rightarrow \Box \varphi_2). \end{array} $$

Inference rules:

$$ (\text{MP}) \quad \frac{\varphi_1, \varphi_1 \rightarrow \varphi_2}{\varphi_2}, $$

$$ (\text{N}) \quad \frac{\varphi_1}{\Box \varphi_1}. $$

The last axiom is called the axiom K. The system we given above is called the system K of the propositional modal logic. It is sound and complete. We will only give the soundness theorem and the completeness theorem here, and the details of their proofs can be found in [7] and [9].

**Theorem 1.** (Soundness theorem of K) For any formula $\varphi$, if $\vdash \varphi$ then $\models \varphi$.
**Theorem 2.** (Completeness theorem of K) For any formula $\varphi$, if $\models \varphi$ then
$\vdash \varphi$.

**3 The new system K<sup>+</sup> and the disjunctive normal form**

Let K<sup>+</sup> be the propositional modal system obtained by adding to K the fol-
lowing axiom:

$$
K^+ \quad \Box \varphi \leftrightarrow \Diamond \varphi.
$$

Then the necessary modality ☐ is equivalent to the possible modality ♦. In K
we have the theorems about the distributivity of ☐ over ∧ and the distributivity
of ♦ over ∨[7]. So in K<sup>+</sup> we can easily get the following theorems about the
distributivity of ☐ over ∧ and ∨.

**Proposition 1.**

$$
(i) \vdash \Box (\varphi \wedge \psi) \leftrightarrow (\Box \varphi \wedge \Box \psi);
$$

$$
(ii) \vdash \Box (\varphi \lor \psi) \leftrightarrow (\Box \varphi \lor \Box \psi).
$$

□

Each formula in the propositional logic is equivalent to a formula in the disjunctive normal form[8]. Similarly, each formula in the system K<sup>+</sup> can also be equivalent to a formula in the disjunctive normal form, where □<sup>i</sup>(i ≥ 0) only occurs before an atomic formula, and ¬ only occurs before a pseudo-atomic formula of form □<sup>i</sup>p, where p is an atomic formula. In the following we will first give the definitions of pseudo-atomic formula and the disjunctive normal form, and then prove that each formula in K<sup>+</sup> is equivalent to a formula in the disjunctive normal form.

**Definition 5.** A formula $\varphi$ is pseudo-atomic if $\varphi = \Box^k p$, where $k \ge 0$ and $p$ is a propositional variable.

**Definition 6.** A formula $\varphi$ is in the *disjunctive normal form* if

$$
\varphi = \varphi_1 \lor \varphi_2 \lor \cdots \lor \varphi_n,
$$

where for each $1 \le i \le n$,

$$
\varphi_i = \psi_{i1} \wedge \dots \wedge \psi_{im_i},
$$

where for each $1 \le j \le m_i$,

$$
\psi_{ij} = \sim^{l_{ij}} \Box^{k_{ij}} p_{ij},
$$

$k_{ij}$-many □s

$$
\text{where } \Box^{k_{ij}} = \text{\(\overbrace{\Box \dots \Box}^{k_{ij}}\)} ;
$$

$$
\sim^{l_{ij}} = \begin{cases} \neg & \text{if } l_{ij} = 1, \\ \lambda & \text{if } l_{ij} = 0, \end{cases}
$$
and $p_{ij}$ is a propositional variable, where $\lambda$ is the empty string.

Similarly, we can define the conjunctive normal form. In this paper we will use the disjunctive normal form only. For simplicity, we call it the normal form. Since the propositional modal logic is obtained by adding $\Box$ to the propositional logic, and $\Box$ can be distributed over $\wedge$ and $\vee$ in $K^+$, we can get the conclusion that for any formula $\psi$ of $K^+$, we have a formula $\varphi$ in the normal form which is equivalent to $\psi$.

**Proposition 2.** For any formula $\psi$, there is a formula $\varphi$ in the normal form such that

$$ \vdash \psi \leftrightarrow \varphi. $$

*Proof.* By induction on the construction of the formula $\psi$. $\square$

# 4 Pseudo-atom-complete set of formulas

In this section we give the definition of pseudo-atom-complete. In the propositional logic an atom-complete set determines a maximally consistent set in a unique way. Similarly, in $K^+$ a pseudo-atom-complete set determines a maximally consistent set in a unique way. In $K^+$ for any pseudo-atom-complete set $A$ of formulas, if we delete one $\Box$ from each $\varphi$ in $A$ then the new set $\Box^-A$ is also pseudo-atom-complete. And the accessibility relation in the canonical model of $K^+$ can be simply given by eliminating one $\Box$ from each pseudo-atomic formula in a possible world.

Let $A$ be a maximally consistent set of formulas in the propositional logic. For any propositional variable $p$, exactly one member of $\{p, \neg p\}$ is in $A$.

**Definition 7.** A set $A$ of atomic formulas or the negation of atomic formulas is *atom-complete* if for any atomic formula $p$, exactly one member of $\{p, \neg p\}$ is in $A$.

**Proposition 3.** An atom-complete set $A$ determines a maximally consistent set in a unique way.

Let $B$ be a maximally consistent set of formulas of $K^+$. For any pseudo-atomic formula $\Box^k p$, exactly one member of $\{\Box^k p, \neg \Box^k p\}$ is in $B$.

**Definition 8.** A set $A$ of pseudo-atomic formulas or the negation of pseudo-atomic formulas is *pseudo-atom-complete* if for any pseudo-atomic formula $\Box^k p$, exactly one member of $\{\Box^k p, \neg \Box^k p\}$ is in $A$.

For any maximally consistent set $B$ of formulas, let

$$ \sigma(B) = \{\sim^l \Box^k p : \sim^l \Box^k p \in B\}. $$

Then, $\sigma(B)$ is pseudo-atom-complete.

**Proposition 4.** For any pseudo-atom-complete set $B$ of formulas, there is a unique maximally consistent set $C$ of formulas such that

$$ \sigma(C) = B. $$
*Proof.* It is easy to see that $B$ is consistent. So by the theorem of Lin-denbaum we can extend $B$ to a maximally consistent set $C$ of formulas and it satisfies the condition that $\sigma(C) = B$. Then we can prove that $C$ is unique by contraposition. $\square$

**Theorem 3.** For any pseudo-atom-complete set $A$, $\Box^{-}A = \{\sim^{l} \Box^{n-1}p : \sim^{l} \Box^{n}p \in A \text{ and } n \geq 1\}$ is pseudo-atom-complete.

*Proof.* By the definition of pseudo-atom-complete. $\square$

For any set $B$ of formulas, let

$$ \Box^{-}(B) = \{\varphi : \Box \varphi \in B\}. $$

Let $W$ be the set of all maximally consistent sets, and $R_{\square}$ be the binary relation on $W$. For any possible worlds $w, w' \in W$, $(w, w') \in R_{\square}$ if and only if $\Box^{-}(w) \subseteq w'$.

**Corollary 1.** Given a pseudo-atom-complete set $A$, let $\tau(A)$ be the unique maximally consistent set such that $\sigma(\tau(A)) = A$. Then,

$$ \{\tau(A), \tau(\Box^{-}A), \dots, \tau(\Box^{-n}A), \dots\} $$

is a set of possible worlds such that

(i) $(\tau(A), \tau(\Box^{-}A)) \in R_{\square}$, and

(ii) for any $n \geq 1$, $(\tau(\Box^{-n+1}A), \tau(\Box^{-n}A)) \in R_{\square}$.

*Proof.* We can prove (i) by contraposition. From the theorem 3 and the proposition 4 we can also prove (ii) with the same method of (i). $\square$

# 5 Correspondences between $K^{+}$ and the propositional logic

In this section we build correspondences between $K^{+}$ and the propositional logic $P^{+}$. When a pseudo-atomic formula $\Box^{k}p_{i}(k, i \geq 0)$ is corresponding to a propositional variable $q_{ki}$, each formula in $K^{+}$ then can be corresponding to a formula in the propositional logic $P^{+}$. We also get the correspondence of models between $K^{+}$ and $P^{+}$. Then we get correspondences of theorems and valid formulas between them. So, the soundness theorem and the completeness theorem of $K^{+}$ follow directly from those of $P^{+}$.

Suppose that $P^{+} = \{q_{ki} : k, i \geq 0\}$ is a language of the propositional logic. In order to give the correspondence between $K^{+}$ and $P^{+}$, we firstly redefine a formula $\varphi$ in the normal form of $K^{+}$.

$$ \theta ::= \Box^{k}p_{i} \mid \neg \Box^{k}p_{i}; $$

$$ \psi ::= \theta | \psi_{1} \wedge \psi_{2}; $$

$$ \varphi ::= \psi | \varphi_{1} \vee \varphi_{2}. $$

where $k, i \geq 0$ and $p_i$ is a propositional variable of $K^{+}$.

Then we define a mapping $\sigma$ of formulas from $K^{+}$ to $P^{+}$. And $\sigma$ is defined as follows:
$$
\begin{align*}
\sigma(\theta) &= \begin{cases} q_{ki} & \text{if } \theta = \Box^k p_i \\ \neg q_{ki} & \text{if } \theta = \neg \Box^k p_i \end{cases} \\
\sigma(\psi) &= \begin{cases} \sigma(\theta) & \text{if } \psi = \theta \\ \sigma(\psi_1) \wedge \sigma(\psi_2) & \text{if } \psi = \psi_1 \wedge \psi_2 \end{cases} \\
\sigma(\varphi) &= \begin{cases} \sigma(\psi) & \text{if } \varphi = \psi \\ \sigma(\varphi_1) \vee \sigma(\varphi_2) & \text{if } \varphi = \varphi_1 \vee \varphi_2 \end{cases}
\end{align*}
$$

It is easy to see that each formula $\varphi$ in the normal form in $K^+$ can be
corresponding to a formula $\sigma(\varphi)$ in the normal form in $P^+$. Since each formula
$\varphi$ in $K^+$ can be equivalent to a formula in the normal form in $K^+$, each formula
$\varphi$ in $K^+$ can be corresponding to a formula in the normal form in $P^+$. For
simplicity, we will only consider formulas in the normal form in $K^+$ and formulas
in the normal form in $P^+$. Then it is easy to prove that $\sigma$ is a bijective function.
And we can also get that for any formula $\varphi$ of $K^+$, $\sigma(\neg\varphi) = \neg\sigma(\varphi)$.

By induction on the number of formulas in the sequence forming the deduction of $\varphi$ from $K^+$, we can get that if $\varphi$ is a theorem of $K^+$ then $\sigma(\varphi)$ is a theorem of $P^+$. For example, if $\varphi$ is a theorem of $K^+$ and we get it by an application of the N rule from the theorem $\varphi_1(p_0, p_1, \dots, p_n)$, then $\sigma(\varphi)$ is also a theorem of the propositional logic. Since we can distribute $\Box$ over $\wedge$ and $\vee$, we get that $\varphi = \varphi_1(\Box p_0, \Box p_1, \dots, \Box p_n)$. By induction hypothesis we know that $\sigma(\varphi_1) = \varphi'_1(q_{k_00}, q_{k_{11}}, \dots, q_{k_n n}) (0 \le i \le n, k_i \ge 0)$ is a theorem of $P^+$, when we use $q_{(k_i+1)i}$ to substitute for $q_{k_i}$ we get a formula $\varphi'_1(q_{(k_0+1)0}, q_{(k_1+1)1}, \dots, q_{(k_n+1)n}) (0 \le i \le n, k_i \ge 0)$ of $P^+$, which is $\sigma(\varphi)$ and also a theorem of $P^+$. We know that each axiom of the propositional logic is an axiom of $K^+$, by using the rule MP each theorem of $P^+$ we get is also a theorem of $K^+$. So we get the following proposition.

**Proposition 5.** For any formula $\varphi$ of $K^+$, $\varphi$ is a theorem of $K^+$ if and only if $\sigma(\varphi)$ is a theorem of $P^+$.

$\square$

Suppose that $A$ is a set of formulas in $K^+$, and $A' = \{\sigma(\varphi) : \varphi \in A\}$ is a set of formulas of $P^+$. Then we have the following propositions.

**Proposition 6.** *A* is consistent if and only if *A'* is consistent. □

**Proposition 7.** *A* is maximally consistent if and only if *A'* is maximally consistent. □

For any model $M = (W, R, I)$ of $K^+$ and any possible world $w \in W$, there is an assignment $v_w$ of $P^+$ such that for any pseudo-atomic formula $\Box^k p_i$,

$M, w \models \Box^k p_i \text{ if and only if } v_w \models q_{ki}.$

Then we have the following proposition.

**Proposition 8.** For any formula $\varphi$ of $K^+$, $M, w \models \varphi$ if and only if $v_w \models \sigma(\varphi)$.

*Proof.* Suppose that $\varphi$ is in the normal form, and

$$
\begin{align*}
\varphi &= \varphi_1 \vee \dots \vee \varphi_n \\
&= (\psi_{11} \wedge \dots \wedge \psi_{1m_1}) \vee \dots \vee (\psi_{n1} \wedge \dots \wedge \psi_{nm_n}),
\end{align*}
$$
where $\psi_{ij} = \mathop{\sim}^{l_{ij}} \Box^{k_{ij}} p_{ij}$, $1 \le i \le n$, $1 \le j \le m_i$ and $k_{ij} \ge 0$. Then

$$ \begin{aligned} \sigma(\varphi) &= \sigma(\varphi_1) \lor \dots \lor \sigma(\varphi_n) \\ &= (\sigma(\psi_{11}) \land \dots \land \sigma(\psi_{1m_1})) \lor \dots \lor (\sigma(\psi_{n1}) \land \dots \land \sigma(\psi_{nm_n})). \end{aligned} $$

Obviously, $M, w \models \psi_{ij}$ if and only if $v_w \models \sigma(\psi_{ij})$.

$v_w \models \sigma(\varphi)$ if and only if there is an $i$ such that $v_w \models \sigma(\varphi_i)$; if and only if there is an $i$ and for any $j$, $v_w \models \sigma(\psi_{ij})$; if and only if there is an $i$ and for any $j$, $M, w \models \psi_{ij}$; if and only if there is an $i$ such that $M, w \models \varphi_i$; if and only if $M, w \models \varphi$. $\square$

For any assignment $v$ of $P^+$ we can construct a model of $K^+$.

Let $W = \{v_0, v_1, v_2, \dots\}$ be a set of assignments such that for any propositional variable $p_i$ ($i \ge 0$) of $K^+$,

$v_0(p_i) = 1$ if and only if $v(q_{0i}) = 1$;

$v_1(p_i) = 1$ if and only if $v(q_{1i}) = 1$;

...

$v_k(p_i) = 1$ if and only if $v(q_{ki}) = 1$;

...

Let $M = (W, R, I)$, where $R = \{(v_n, v_{n+1}) : n \ge 0\}$; for any propositional variable $p_i$ ($i \ge 0$) and any $k \ge 0$, $v_k \in I(p_i)$ if and only if $v_k(p_i) = 1$. Then we have the following proposition.

**Proposition 9.** For any formula $\varphi$ of $K^+$, $M, v_0 \models \varphi$ if and only if $v \models \sigma(\varphi)$. $\square$

It is easy to get the following proposition.

**Proposition 10.** For any formula $\varphi$ of $K^+$, $\models \varphi$ if and only if $\models \sigma(\varphi)$. $\square$

*Proof.* The proof is by contraposition. $\square$

Let $C$ be the class of frames in which each world can only see one world, itself or another. We should prove that $K^+$ is sound and complete with respect to $C$. And theorems of $K^+$ are also theorems of $P^+$, and vice versa; valid formulas of $K^+$ are also valid formulas of $P^+$, and vice versa. So we can easily get the following theorems from the soundness and completeness of $P^+$.

**Theorem 4.** (Soundness of $K^+$) For any formula $\varphi$ of $K^+$, if $\vdash \varphi$ then $\models_C \varphi$.

**Theorem 5.** (Completeness of $K^+$) For any formula $\varphi$ of $K^+$, if $\models_C \varphi$ then $\vdash \varphi$.

# 6 Conclusions

In this paper we construct a new propositional modal system $K^+$, in which maximally consistent sets have a property holding in the propositional logic: a maximally consistent set is uniquely determined by a set of pseudo-atom-complete formulas. Each formula in such a logic is equivalent to a formula in the disjunctive normal form, where each disjunct is the conjunction of pseudo-atomic formula or the negation of pseudo-atomic formula. The accessibility
relation in the canonical model of $K^+$ can be simply given by eliminating one
☐ from each pseudo-atomic formula or its negation in a possible world. We
also build correspondences of formulas, theorems and valid formulas between
$K^+$ and the propositional logic $P^+$. So, the soundness theorem and the com-
pleteness theorem of $K^+$ follow directly from those of $P^+$.

## Acknowledgements

This work is supported by National Natural Science Foundation of China under
grant No. 60573064, 91224006, 61203284, and 61173063.

## References

1. Van Benthem,J.: Modal correspondence theory [Ph.D. Thesis]. University of Amsterdam, Netherlands(1976)

2. Blackburn,P., Van Benthem,J., Wolter,F.: Handbook of Modal Logic. Elsevier Science Ltd(2006)

3. Van Benthem,J.: Correspondence Theory. In: Gabbay D, Guenthner F, eds. Handbook of Philosophical Logic. Kluwer Academic Publishers. 325-408(2001)

4. Aloni,M.: Quantification under Conceptual Covers [Ph.D. Thesis]. University of Amsterdam, Amsterdam(2001)

5. Aloni,M.: Individual Concepts in Modal Predicate Logic. Journal of Philosophical Logic. 34(1),1-64(2005)

6. Hazen,A., Rin,B., Wehmeier,K.: Actuality in Propositional Modal Logic. STUDIA LOGICA. 101(3),487-503(2013)

7. Hughes,GE., Cresswell,MJ.: A New introduction to Modal Logic. Lodon, Routledge(1996)

8. Hamilton,AG.: Logic for Mathematicians. Cambridge University Press(1988)

9. Fitting,M., Mendelsohn,R.: First-order Modal Logic. Kluwer Academic Publishers, The Netherlands(1998)

10. Kripke,S.: Semantical analysis of modal logic I: Normal modal propositional calculi. Zeitschrift fr Mathematische Logik und Grundlagen der Mathematik. 9,67-96(1963)