A non-distributive logic for semiconcepts of a context and its modal extension with semantics based on Kripke contexts

(R6) is derived using (R1), (R1)^{\prime} and (R4), while for (R7) one uses (R2), (R2)^{\prime} and (R4).

The proofs of 1-9 are obtained in a similar way as the proofs given in Theorem 25 in [howlader2021dbalogic] in case of CDBL. Nevertheless, we include the proofs in the appendix to make the paper self-contained.

5pt 10a is obtained using axiom 5a, Theorem 9(4a, 9a) and rules (R3), (R4). We get 10b by using the dual axiom and rules. The proof of 11a is given below. 11b is again obtained by using duals of axioms and rules that prove 11a. 5pt Proof of 11a:

\infer{\beta\vdash\alpha\vee\beta\mid\beta\sqcup\beta\vdash\beta~(R4)}{\infer{(Sp)~\beta\vdash\beta\sqcap\beta\mid\beta\sqcup\beta\vdash\beta~~~~\beta\sqcap\beta\vdash\alpha\vee\beta~(\mbox{using definition of} \vee \mbox{in previous step})}{\infer{\beta\sqcap\beta\vdash\neg(\neg\alpha\sqcap\neg\beta)~(R4)}{\infer{(\mbox{10a,~this~theorem)}~\beta\sqcap\beta\vdash\neg\neg\beta~~~~\neg\neg\beta\vdash\neg(\neg\alpha\sqcap\neg\beta)~~(R3~\mbox{on~previous~step})}{\infer{\neg\alpha\sqcap\neg\beta\vdash\neg\beta~(R4)}{\infer{(R1)~\neg\alpha\sqcap\neg\beta\vdash\neg\bot\sqcap\neg\beta~~~~\neg\bot\sqcap\neg\beta\vdash\neg\beta~(\mbox{axiom 3a})}{\infer{\neg\alpha\vdash\neg \bot~(R3)}{\infer{\bot\vdash\alpha~(\mbox{axiom 11a})}{}}}}}}}}

The proof that all the axioms of PDBL are valid in the class of all pdBas is straightforward and can be obtained using Proposition 3 and Definition 3. As examples, we give proofs for 15a and 15b. Let p\in\textbf{OV}, P\in\textbf{PV}, \textbf{D} be a pdBa and v be a valuation on \textbf{D}. As v(p)\in D_{\sqcap}, v(p)\sqcap v(p)=v(p). So v satisfies p\sqcap p\dashv\vdash p. Similarly as v(P)\in D_{\sqcup}, v(P)\sqcup v(P)=v(P), implying that v satisfies P\sqcup P\dashv\vdash P.

The validity of the inference rules then needs to be verified. The case for external rules is straightforward.

Using Proposition 3, one can show that (R1), (R2),(R1)^{\prime} and (R2)^{\prime} preserve validity. The cases for (R3) and (R3)^{\prime} follow from Proposition 4. For (R5), one uses Proposition 1 and Definition 3.

(Sp): Let \textbf{D} be a pdBa and v a valuation on \textbf{D}. Let \alpha\in \mathfrak{F}. Then either v(\alpha)=v(\alpha)\sqcap v(\alpha)=v(\alpha\sqcap\alpha) or v(\alpha)=v(\alpha)\sqcup v(\alpha)=v(\alpha\sqcup\alpha). In the former case v satisfies \alpha\vdash\alpha\sqcap\alpha and in the latter, v satisfies \alpha\sqcup\alpha\vdash\alpha.

1. Let p\in \textbf{OV}. By Lemma 4, F_{[p]}^{\prime}=I_{[p]_{\sqcap\sqcup}}=I_{[p]_{\sqcup}}, as [p]_{\sqcap}=[p] in \mathcal{L}(\mathfrak{F}). By Lemma 3, I_{[p]\sqcup [p]}=I_{[p]}, implying F_{[p]}^{\prime}= I_{[p]}. Similarly, we can show that for P\in\textbf{PV}, I_{[P]}^{\prime}=F_{[P]}. 4pt 2. In the following equations, we use Lemmas 4 and 3.

F^{\prime}_{[\phi]\sqcap [\sigma]}= I_{([\phi]\sqcap[\sigma])\sqcup ([\phi]\sqcap[\sigma])}=I_{([\phi]\sqcap[\sigma])}\cap I_{([\phi]\sqcap[\sigma])}=I_{([\phi]\sqcap[\sigma])}. 4pt I^{\prime}_{[\phi]\sqcup [\sigma]}= F_{([\phi]\sqcup[\sigma])\sqcap ([\phi]\sqcup[\sigma])}=F_{([\phi]\sqcup[\sigma])}\cap F_{([\phi]\sqcup[\sigma])}=F_{([\phi]\sqcup[\sigma])}. 4pt

F^{\prime}_{\neg [\phi]}= I_{\neg[\phi]\sqcap \neg[\phi]}=I_{\neg [\phi]}, as \neg[\phi]\sqcap \neg[\phi]=\neg [\phi] and I^{\prime}_{\lrcorner [\phi]}= F_{\lrcorner[\phi]\sqcup \lrcorner[\phi]}=F_{\lrcorner [\phi]}, as \lrcorner[\phi]\sqcup \lrcorner[\phi]=\lrcorner [\phi]

Let p\in \textbf{OV}, v_{0}(p)\sqcap v_{0}(p)=(F_{[p]}, I_{[p]})\sqcap (F_{[p]},I_{[p]})=(F_{[p]}\cap F_{[p]}, (F_{[p]}\cap F_{[p]})^{\prime})=(F_{[p]},F_{[p]}^{\prime})= (F_{[p]},I_{[p]})=v_{0}([p]), by Lemma 8(1). Similarly, for P\in \textbf{PV}, v_{0}(P)\sqcup v_{0}(P)= v_{0}(P). By Definition 11, v_{0}(\top)=(F_{[\top]}, I_{[\top]}). So v_{0}(\top)= (\mathcal{F}_{p}(\mathcal{L}(\mathfrak{F})),\emptyset)=\top_{\underline{\mathfrak{H}}(\mathbb{K}(\mathcal{L}(\mathfrak{F})))}. Similarly, we can show that v_{0}(\bot)= \bot_{\underline{\mathfrak{H}}(\mathbb{K}(\mathcal{L}(\mathfrak{F})))}. So v_{0} is a valuation on \underline{\mathfrak{H}}(\mathbb{K}(\mathcal{L}(\mathfrak{F}))).

The second part of the lemma is proved by induction on the number of connectives in \alpha, and using Definition 9 and Lemma 8(2), one gets the result in each case.

1 \Longrightarrow 2: Let G:= \alpha_{1}\vdash\beta_{1}|\alpha_{2}\vdash\beta_{2}|\ldots|\alpha_{n}\vdash\beta_{n} be provable in \textbf{PDBL}. If possible, let us assume that for all i\in\{1,2,\ldots,n\}, \alpha_{i}\vdash \beta_{i} is not provable in \textbf{PDBL}. By Proposition 8, for all i\in\{1,2,\ldots,n\}, [\alpha_{i}]\not\sqsubseteq [\beta_{i}] in \mathcal{L}(\mathfrak{F}). By Proposition 2, either [\alpha_{i}]\sqcap[\alpha_{i}]\not\sqsubseteq_{\sqcap}[\beta_{i}]\sqcap[\beta_{i}] or [\alpha_{i}]\sqcup[\alpha_{i}]\not\sqsubseteq_{\sqcap}[\beta_{i}]\sqcup[\beta_{i}] for all i\in\{1,2,\ldots,n\}. Now, we consider the valuation v_{0}. By Lemma 9, v_{0}(\alpha_{i})=(F_{[\alpha_{i}]}, I_{[\alpha_{i}]}) for all i\in \{1,2,\ldots, n\}. Let [\alpha_{i}]\sqcap[\alpha_{i}]\not\sqsubseteq_{\sqcap}[\beta_{i}]\sqcap[\beta_{i}] for some i. Then there exists a prime filter F_{0i} in \mathcal{L}(\mathfrak{F})_{\sqcap} such that [\alpha_{i}]\sqcap[\alpha_{i}]\in F_{0i} and [\beta_{i}]\sqcap[\beta_{i}]\notin F_{0i}. Therefore by Lemma 2 there exists a filter F_{i} in \mathcal{L}(\mathfrak{F}) such that F_{i}\cap\mathcal{L}(\mathfrak{F})_{\sqcap}=F_{0i}. As F_{0i} is a prime filter in \mathcal{L}(\mathfrak{F})_{\sqcap}, F_{i}\in\mathcal{F}_{p}(\mathcal{L}(\mathfrak{F})) such that [\alpha_{i}]\sqcap[\alpha_{i}]\in F_{i} and [\beta_{i}]\sqcap[\beta_{i}]\notin F_{i}. So [\alpha_{i}]\in F_{i}, as [\alpha_{i}]\sqcap[\alpha_{i}]\sqsubseteq[\alpha_{i}] and [\beta_{i}]\notin F_{i} otherwise [\beta_{i}]\sqcap[\beta_{i}]\in F_{i}. Therefore F_{[\alpha_{i}]} \cancel{\subseteq} F_{[\beta_{i}]}.

If [\alpha_{i}]\sqcup[\alpha_{i}]\not\sqsubseteq_{\sqcap}[\beta_{i}]\sqcup[\beta_{i}], then dually, we can show that there exists I_{i}\in \mathcal{I}_{p}(\mathcal{L}(\mathfrak{F})) such that [\alpha_{i}]\notin I_{i} and [\beta_{i}]\in I_{i}, which implies that I_{[\beta_{i}]} \cancel{\subseteq} I_{[\alpha_{i}]}.

So in either case, v_{0}(\alpha_{i})\cancel{\sqsubseteq} v_{0}(\beta_{i}) for all i\in \{1,2,3,\ldots, n\}, which is not possible, as G is valid in the class all pdBas by Theorem 10. So there exists i\in \{1,2,3,\ldots, n\} such that \alpha_{i}\vdash \beta_{i} is provable in \textbf{PDBL}.

2 \Longrightarrow 1: Let \alpha_{i}\vdash\beta_{i} be provable for some i\in \{1, 2,\ldots, n\}.

The s-hypersequent G is then proved by repeatedly applying the external rules EW and EE.

By Propositions 9, 8 and (Sp), it follows that [\alpha]\sqsubseteq [\alpha\sqcap\alpha] or [\alpha\sqcup\alpha]\sqsubseteq [\alpha] in \mathcal{L}(\mathfrak{F}). By Proposition 3(5), [\alpha]\sqcap[\alpha]\sqsubseteq [\alpha] and [\alpha]\sqsubseteq [\alpha]\sqcup[\alpha]. So [\alpha]=[\alpha]\sqcap [\alpha]=[\alpha\sqcup\alpha] or [\alpha]=[\alpha]\sqcup [\alpha]=[\alpha\sqcup\alpha], which implies that \mathcal{L}(\mathfrak{F}) is a pdBa.

Suppose if possible, G is not provable. Then \alpha_{i}\vdash\beta_{i} are not provable for all i\in\{1,2,\ldots, n\} by Proposition 9. Rest of the proof is similar to the proof of 1 \Longrightarrow 2 part of Proposition 9.

As all the axioms of PDBL are also axioms of MPDBL and the rules of inference of PDBL are also rules of inference of MPDBL, a proof for the s-hypersequent G in PDBL is also a proof for G in MPDBL.

To complete the proof it is sufficient to show that all axioms of \textbf{MPDBL}\Sigma are valid in V_{\Sigma} and rules of inference preserve validity. The propositional cases follow from Theorem 10. Here, we check the validity of axioms 16a, 17a, 18a, 16b, 17b and 18b in V_{\Sigma}, and show that rules of inference (R9) and (R10) preserve validity. Let \mathfrak{O} be a pdBao belonging to the class V_{\Sigma} and v be a valuation on \mathfrak{O}. Let \alpha,\beta\in \mathfrak{F}. Then v(\square(\alpha\sqcap\beta))=\textbf{I}(v(\alpha\sqcap\beta))=\textbf{I}(v(\alpha)\sqcap v(\beta))= \textbf{I}(v(\alpha))\sqcap\textbf{I}(v(\beta))=v(\square\alpha)\sqcap v(\square\beta)=v(\square\alpha\sqcap\square\beta). Now v(\square(\alpha\sqcap\alpha))=\textbf{I}(v(\alpha\sqcap\alpha))=\textbf{I}(v(\alpha)\sqcap v(\alpha))=\textbf{I}(v(\alpha))=v(\square\alpha). Therefore the axioms 16a and 18a are true in \mathfrak{O}, which implies that 16a and 18a are valid in the class V_{\Sigma}. Dually, we can show that the axioms 16b and 18b are valid in the class V_{\Sigma}. Now v(\square(\neg \bot))=\textbf{I}(v(\neg\bot))=\textbf{I}(\neg v(\bot))=\textbf{I}(\neg\bot_{D})=\neg\bot_{D} and v(\blacksquare(\lrcorner\top) )= \textbf{C}(v(\lrcorner\top))=\textbf{C}(\lrcorner v(\top))= \textbf{C}(\lrcorner\top_{D})=\lrcorner\top_{D}. Therefore axioms 17a and 17b are true in \mathfrak{O}, which implies that 17a and 17b are valid in the class V_{\Sigma}.

To show that (R9) preserves validity, let B~|~\alpha\vdash\beta~|~C be valid in V_{\Sigma}. Let \mathfrak{O}\in V_{\Sigma} and v be a valuation on \mathfrak{O}. Now B~|~\alpha\vdash\beta~|~C is true in \mathfrak{O}, as B~|~\alpha\vdash\beta~|~C is valid in V_{\Sigma}. So v satisfies the s-hypersequent B~|~\alpha\vdash\beta~|~C. Now there are two possibilities. (1) v satisfies a component from B or C. (2) v satisfies the component \alpha\vdash\beta. Now if (1) holds then v also satisfies the s-hypersequent B~|~\square\alpha\vdash\square\beta~|~C, and if (2) holds then v(\alpha)\sqsubseteq v(\beta) in \mathfrak{O}, which implies that \textbf{I}(v(\alpha))\sqsubseteq \textbf{I}(v(\beta)), by the monotonicity of \textbf{I}. So v(\square\alpha)\sqsubseteq v(\square\beta), which implies that v satisfies the s-hypersequent B~|~\square\alpha\vdash\square\beta~|~C. So (R9) preserves validity in V_{\Sigma}.

Showing (R10) preserves validity is similar to the above.

Let [\alpha]\sqsubseteq [\beta]. \alpha\vdash\beta by Proposition 10. So \square\alpha\vdash\square\beta and \blacksquare\alpha\vdash\blacksquare\beta by (R9) and (R10). Again using Proposition 10, [\square\alpha]\sqsubseteq [\square\beta] and [\blacksquare\alpha]\sqsubseteq [\blacksquare\beta]. Hence f_{\square}([\alpha])\sqsubseteq f_{\square}([\beta]) and f_{\blacksquare}([\alpha])\sqsubseteq f_{\blacksquare}([\beta]).

By Propositions 10 and 11, (\mathfrak{F}_{1}/\equiv_{\vdash}, \sqcup,\sqcap,\neg,\lrcorner,[\top],[\bot]) is a pdBa. Lemma 11 implies that the operators f_{\square}, f_{\blacksquare} are monotonic. Now let [\alpha],[\beta]\in\mathfrak{F}_{1}/\equiv_{\vdash}. Then f_{\square}([\alpha]\sqcap[\beta])=f_{\square}([\alpha\sqcap\beta])=[\square(\alpha\sqcap\beta)]=[\square\alpha\sqcap\square\beta]=[\square\alpha]\sqcap [\square\beta] by axiom 16a, which implies that f_{\square}([\alpha]\sqcap[\beta])=[\square\alpha]\sqcap[\square\beta]=f_{\square}([\alpha])\sqcap f_{\square}([\beta]). Dually, we can show that f_{\blacksquare}([\alpha]\sqcup [\beta])= f_{\blacksquare}([\alpha])\sqcup f_{\blacksquare}([\beta]). The others axioms can be proved directly using axioms 17a, 17b, 18a, and 18b, which implies that \mathcal{L}_{\Sigma}(\mathfrak{F}_{1}) is a pdBao.

For any p\in \textbf{OV}, v_{+}(p):=[p]\in \mathcal{L}_{\Sigma}(\mathfrak{F}_{1})_{\sqcap}, using axiom 15a. Similarly, using axiom 15b, for any P\in \textbf{PV}, v_{+}(P):=[P]\in \mathcal{L}_{\Sigma}(\mathfrak{F}_{1})_{\sqcup}. By definition of v_{+}, v_{+}(\top)=[\top]=\top_{\mathcal{L}_{\Sigma}(\mathfrak{F}_{1})}. Similarly, v_{+}(\bot)=\bot_{\mathcal{L}_{\Sigma}(\mathfrak{F}_{1})}. So v_{+} is a valuation on \mathcal{L}_{\Sigma}(\mathfrak{F}_{1}).

The second part of the lemma is proved by

mathematical induction on the number of connectives in \alpha; using the definition of v_{+} and the induction hypothesis, the cases are obtained.

Let G:\alpha_{1}\vdash\beta_{1}\mid\alpha_{2}\vdash\beta_{2}\mid\ldots\mid\alpha_{n}\vdash\beta_{n} be not provable in \textbf{MPDBL}\Sigma. By Proposition 11, for all i\in \{1,2,\ldots, n\}, \alpha_{i}\vdash\beta_{i} is not provable in \textbf{MPDBL}\Sigma. By Proposition 10, for all i\in \{1,2,\ldots, n\}, [\alpha_{i}]\cancel{\sqsubseteq}[\beta_{i}], which implies that for all i\in \{1,2,\ldots, n\}, v_{+}(\alpha_{i})\cancel{\sqsubseteq} v_{+}(\beta_{i}). So G is not true in \mathcal{L}_{\Sigma}(\mathfrak{F}_{1}), which is not possible, as G is valid in V_{\Sigma}. So G is provable in \textbf{MPDBL}\Sigma.

We given the proofs of 1 and 3. 2 and 4 follow dually. 5 and 6 follow directly from Definition 15.

The result is obtained by using mathematical induction on the number of connectives that occur in

\alpha. Let \mathbb{M}:=(\mathbb{K},v) be a model, where v:\textbf{OV}\cup\textbf{PV}\cup \{\top, \bot\}\rightarrow\mathfrak{H}(\mathbb{K}) is the valuation.

For the base case let the number of connectives in \alpha, n=0. Then either \alpha belongs to \textbf{OV}\cup\textbf{PV} or \alpha is a propositional constant.

Let \alpha=p. Then v_{1}(p)=\{g\in G~|~ \mathbb{M},g\models p\}=ext(v(p)) and v_{2}(p)=\{m\in M~ |~ \mathbb{M},m\succ p\}= int(v(p)) by the definition of satisfaction and co-satisfaction. So (v_{1}(p),v_{2}(p))=(ext(v(p)), int(v(p)))=v(p)\in \mathfrak{H}(\mathbb{K}).

If \alpha=P then similar to the above, (v_{1}(\alpha),v_{2}(\alpha))=(ext(v(P)), int(v(P)))=v(P)\in \mathfrak{H}(\mathbb{K}).

For \alpha=\top, v_{1}(\top)=G and v_{2}(\top)=\emptyset. So (v_{1}(\top),v_{2}(\top))=(G,\emptyset)\in \mathfrak{H}(\mathbb{K}), and if \alpha=\bot then v_{1}(\bot)=\emptyset and v_{2}(\bot)=M. So (v_{1}(\bot),v_{2}(\bot))=(\emptyset, M)\in \mathfrak{H}(\mathbb{K}).

Now, we assume that the result is true for all formulae with number of connectives less or equal to n. Let \alpha be a formula with n+1 connectives. Then \alpha is of one of the forms \beta\sqcap\delta, \beta\sqcup\delta, \neg\beta, or \lrcorner\beta, where \beta, \delta are formulae with number of connectives less or equal to n. By induction hypothesis (v_{1}(\beta),v_{2}(\beta)) and (v_{1}(\delta),v_{2}(\delta)) belong to \mathfrak{H}(\mathbb{K}). Therefore (v_{1}(\beta),v_{2}(\beta))\sqcap (v_{1}(\delta),v_{2}(\delta)), (v_{1}(\beta),v_{2}(\beta))\sqcup (v_{1}(\delta),v_{2}(\delta)), \neg(v_{1}(\beta),v_{2}(\beta)) and \lrcorner (v_{1}(\beta),v_{2}(\beta)) all belong to \mathfrak{H}(\mathbb{K}), as \mathfrak{H}(\mathbb{K}) is closed under \sqcap,\sqcup, \neg, \lrcorner.

By Proposition 12 it follows that

(v_{1}(\beta\sqcap\delta),v_{2}(\beta\sqcap\delta)) =(v_{1}(\beta)\cap v_{1}(\delta),(v_{1}(\beta)\cap v_{1}(\delta))^{\prime})=(v_{1}(\beta),v_{2}(\beta))\sqcap (v_{1}(\delta),v_{2}(\delta)),

(v_{1}(\beta\sqcup\delta),v_{2}(\beta\sqcup\delta))=((v_{2}(\beta)\cap v_{2}(\delta))^{\prime},v_{2}(\beta)\cap v_{2}(\delta))=(v_{1}(\beta),v_{2}(\beta))\sqcup (v_{1}(\delta),v_{2}(\delta)),

(v_{1}(\neg\beta),v_{2}(\neg\beta))=(v_{1}(\beta)^{c},(v_{1}(\beta))^{c\prime})=\neg (v_{1}(\beta),v_{2}(\beta)),

(v_{1}(\lrcorner \beta),v_{2}(\lrcorner \beta))=((v_{2}(\beta))^{c\prime},v_{2}(\beta)^{c})=\lrcorner (v_{1}(\beta),v_{2}(\beta)).

So (v_{1}(\alpha), v_{2}(\alpha))\in \mathfrak{H}(\mathbb{K}).

The proof follows from Proposition 12, Corollary 2 and the definitions of the operations \sqcap, \sqcup, \neg, \lrcorner on \mathfrak{H}(\mathbb{K}) as given in Section ?.

Follows by induction on the number of connectives that occur in a formula, using definition of extension of a valuation and Corollary 3. Note that v(p)=(ext(v(p)), int(v(p)))=(v_{1}(p), v_{2}(p)) and similarly, v(P)=(v_{1}(P), v_{2}(P)). v(\top)=(G, \emptyset)=(v_{1}(\top), v_{2}(\top)) by Proposition 12. Similarly, v(\bot)=(v_{1}(\bot), v_{2}(\bot)).

Let \alpha\vdash\beta be satisfied in the model \mathbb{M}. Let g\in v_{1}(\alpha). Then \mathbb{M}, g\models \alpha, which implies that \mathbb{M}, g\models \beta. So g\in v_{1}(\beta), whence v_{1}(\alpha)\subseteq v_{1}(\beta). Let m\in v_{2}(\beta). Then \mathbb{M}, m\succ\beta, which implies that \mathbb{M}, m\succ\alpha. So m\in v_{2}(\alpha), which implies that v_{2}(\beta)\subseteq v_{2}(\alpha). Therefore v(\alpha)\sqsubseteq v(\beta).

Conversely, let v(\alpha)\sqsubseteq v(\beta). Then v_{1}(\alpha)\subseteq v_{1}(\beta) and v_{2}(\beta)\subseteq v_{2}(\alpha). Let \mathbb{M},g\models \alpha. Then g\in v_{1}(\alpha), which implies that g\in v_{1}(\beta). So \mathbb{M}, g\models\beta. Similar to the above, we can show that \mathbb{M}, m\succ\beta implies that \mathbb{M}, m\succ\alpha. Therefore \alpha\vdash\beta is satisfied in the model \mathbb{M}.

Proof follows from Definition 10 and Proposition 13.

Let \mathbb{M}:=(\mathbb{K}, v) be a model based on \mathbb{K}. Theorem 10 and Proposition 14 ensure that G is satisfied in \mathbb{M}, as v is also a valuation on the pdBa \underline{\mathfrak{H}}(\mathbb{K}).

Let G:= \alpha_{1}\vdash\beta_{1}|\alpha_{2}\vdash\beta_{2}|\ldots|\alpha_{n}\vdash\beta_{n} be valid in \mathcal{K}. If possible, let us assume that G is not provable in \textbf{PDBL}. By Proposition 9, for all i\in\{1,2,\ldots,n\}, \alpha_{i}\vdash \beta_{i} is not provable in \textbf{PDBL}. By Proposition 8 [\alpha_{i}]\not\sqsubseteq [\beta_{i}] in \mathcal{L}(\mathfrak{F}), for all i\in\{1,2,\ldots,n\}. Now, we consider the model \mathbb{M}(\mathfrak{F}):=(\mathbb{K}(\mathcal{L}(\mathfrak{F})),v_{0}). Using the same argument as the proof of part 1\implies 2 of Proposition 9, we can show that

v_{0}(\alpha_{i})\cancel{\sqsubseteq} v_{0}(\beta_{i}) for all i\in \{1,2,3\cdots n\}, which is not possible, as G is valid in the class \mathcal{K}. So G is provable in \textbf{PDBL}.

For any model \mathbb{M}:=(\mathbb{K}, v), \top\sqcap\top\dashv\vdash\bot\sqcup\bot is satisfied in \mathbb{M} if and only if v(\top\sqcap\top)=v(\bot\sqcup\bot), i.e if and only if (G, G^{\prime})=(M^{\prime},M), i.e. if and only if G^{\prime}=M and G=M^{\prime}, which is equivalent to R=G\times M.

1. Let g\in G. Then \mathbb{M},g\models\lozenge\alpha if and only if \mathbb{M},g\models\neg\square\neg\alpha, which is equivalent to \mathbb{M},g\not\models\square\neg\alpha. Now \mathbb{M},g\not\models\square\neg\alpha if and only if there exists g_{1}\in G such that gRg_{1} and \mathbb{M},g_{1}\not\models\neg\alpha, which is equivalent to say that there exists g_{1}\in G such that gRg_{1} and \mathbb{M},g_{1}\models\alpha.

2. Let m\in M. Then \mathbb{M},m\succ\lozenge\alpha if and only if \mathbb{M},m\succ\neg\square\neg\alpha, which is equivalent to say that for all g\in G(\mathbb{M},g\not\models\square\neg\alpha~\mbox{implies}~gIm). Now \mathbb{M},g\not\models\square\neg\alpha if and only if there exists g_{1}\in G such that gR g_{1} and \mathbb{M},g_{1}\not\models\neg\alpha. So \mathbb{M},m\succ\lozenge\alpha if and only if for all g\in G ((there exists g_{1}\in G such that gRg_{1} and \mathbb{M},g_{1}\models\alpha) \Longrightarrow gIm).

3. Let m\in M. Then \mathbb{M},m\succ\blacklozenge\alpha if and only if \mathbb{M},m\succ\lrcorner\blacksquare\lrcorner\alpha, which is equivalent to \mathbb{M},m\not\succ\blacksquare\lrcorner\alpha if and only if there exists a m_{1}\in M such that mSm_{1} and \mathbb{M},m_{1}\succ\alpha.

4. Let g\in G. Then \mathbb{M},g\models\blacklozenge\alpha if and only if \mathbb{M},g\models\lrcorner\blacksquare\lrcorner\alpha, which is equivalent to say that for all m\in M (\mathbb{M},m\not\succ\blacksquare\lrcorner\alpha implies that gIm). Now \mathbb{M},m\cancel{\succ}\blacksquare\lrcorner\alpha if and only if there exists m_{1}\in M such that m S m_{1} and \mathbb{M},m_{1}\succ\alpha. So \mathbb{M},g\models\blacklozenge\alpha if and only if for all m\in M((there exists m_{1}\in M such that mSm_{1} and \mathbb{M},m_{1}\succ\alpha) \Longrightarrow gIm).

1. Let \alpha=\square\phi. Then v_{1}(\alpha)=\{g\in G:\mathbb{M},g\models\square\phi\}=\{g\in G:~\mbox{for all}~g_{1}\in G, (Rgg_{1} \Longrightarrow \mathbb{M},g_{1}\models \phi)\}=\{g\in G:g\in \underline{v_{1}(\phi)}_{R}\}=\underline{v_{1}(\phi)}_{R}.

v_{2}(\alpha)=\{m\in M: \mathbb{M},m\succ\square\phi\}=\{m\in M:~\mbox{for all}~g,g_{1}\in G, ((Rgg_{1} \Longrightarrow\mathbb{M},g_{1}\models\phi) \Longrightarrow gIm)\}=(\underline{v_{1}(\phi)}_{R})^{\prime}.

2. Let \alpha=\blacksquare\phi. Then v_{2}(\alpha)=\{m\in M:~\mathbb{M},m\succ\blacksquare\phi\}=\{m\in M: ~ \mbox{for all}~ m_{1}\in M( Smm_{1} \Longrightarrow \mathbb{M},m_{1}\succ\phi)\}=\underline{v_{2}(\phi)}_{S}.

v_{1}(\alpha)=\{g\in G: \mathbb{M},g\models \blacksquare\phi\}=\{g\in G: ~\mbox{for all}~m,m_{1}\in M(( Smm_{1} \Longrightarrow\mathbb{M},m_{1}\succ\phi) \Longrightarrow gIm)\}=(\underline{v_{2}(\phi)}_{S})^{\prime}.

3. Let \alpha= \lozenge\phi. Then by Lemma 13(1), 13(2), v_{1}(\alpha)=\overline{v_{1}(\neg\neg\phi)}^{R} and v_{2}(\alpha)=(\overline{v_{1}(\neg\neg\phi)}^{R})^{\prime}, which implies that v_{1}(\alpha)=\overline{v_{1}(\neg\neg\phi)}^{R}=\overline{v_{1}(\phi)^{cc}}^{R}=\overline{v_{1}(\phi)}^{R} and v_{2}(\alpha)=(\overline{v_{1}(\neg\neg\phi)}^{R})^{\prime}=(\overline{v_{1}(\phi)}^{R})^{\prime}.

4. The proof is similar to that of 3.

The corollary is proved using mathematical induction on the number of connectives in \alpha, and the cases are obtained using Corollary 2, Proposition 15 and the induction hypothesis.

The proof follows from the definition of extension of a valuation, Proposition 15 and Corollary 5.

The proof follows from the definition of extension of a valuation, Corollaries 5 and 6.

Let \mathbb{M}:=(\mathbb{KC}, v) be a model based on \mathbb{KC}. By Theorem 16(1), G is satisfied by the valuation v on the pdBao \underline{\mathfrak{H}}^{+}(\mathbb{KC}). So by Proposition 17, G is satisfied in \mathbb{M}.

We will use mathematical induction on the number of connectives in \alpha to prove this lemma. The base case follows from the definition of v_{0}. Let the claim be true for all formulae \alpha with number of connectives less or equal to n.

Let \alpha be a formula with n+1 connectives . Then \alpha\in \{\beta\sqcup\gamma, \beta\sqcap\gamma,\neg\beta,\lrcorner\gamma\} or \alpha\in \{\square\beta,\blacksquare\beta\}, where \beta and \gamma are formulae with number of connectives less or equal to n. Proof for the propositional cases is similar to the proof of Lemma 9. To complete the proof it is sufficient to show that v_{0}(\alpha)=(F_{[\alpha]}, I_{[\alpha]}), for \alpha\in \{\square\beta,\blacksquare\beta\}. 4pt Case I: Let \alpha=\square\beta. By Proposition 15, v_{1}(\alpha)=\underline{v_{1}(\beta)}_{R}. By induction hypotheses v_{1}(\beta)=F_{[\beta]}. Therefore v_{1}(\alpha)=\underline{F_{[\beta]}}_{R}. By Lemma 7(1), v_{1}(\alpha)= \underline{F_{[\beta]}}_{R}=F_{f_{\square}([\beta])}=F_{[\square\beta]}=F_{[\alpha]}.

By Proposition 15, v_{2}(\alpha)=(\underline{v_{1}(\beta)}_{R})^{\prime}=(F_{[\alpha]})^{\prime}. By Lemmas 4, 3, and axiom 17a, v_{2}(\alpha)=(F_{[\alpha]})^{\prime}=I_{[\alpha]_{\sqcap \sqcup}}=I_{[\alpha]_{\sqcap}}=I_{[\alpha]}. Therefore v_{0}(\alpha)=(F_{[\alpha]}, I_{[\alpha]}). 4pt Case II: Let \alpha=\blacksquare\phi. Then similar to the above, we can show that v_{2}(\alpha)=I_{[\alpha]} and v_{1}(\alpha)=(v_{2}(\alpha))^{\prime}=F_{[\alpha]}. In this case we use Lemmas 4, 3, and axiom 17b. Therefore v_{0}(\alpha)=(F_{[\alpha]},I_{[\alpha]}).

Let the s-hypersequent G:\alpha_{1}\vdash\beta_{1}~|~\ldots~|~\alpha_{n}\vdash\beta_{n} be valid in \mathcal{KC}. If possible, assume that G is not provable in MPDBL. By Propositions 10 and 11, [\alpha_{i}]\not\sqsubseteq [\beta_{i}] for all i\in \{1,2,3,\ldots, n\}. The rest of the proof is similar to the proof of Theorem 18.

The proof is a consequence of Theorem 16(2) and Proposition 17, as for a model \mathbb{M}:=(\mathbb{KC}, v), v is also a valuation on the tpdBa \underline{\mathfrak{H}}^{+}(\mathbb{KC}).

In case of MPDBL4, \mathcal{L}_{\Sigma}(\mathfrak{F}_{1}) forms a tpdBa. By Theorem 7 it follows that \mathbb{KC}(\mathcal{L}(\mathfrak{F}_{1})) is reflexive and transitive. Rest of the proof is similar to the proof of Theorem 21.

To complete the proof it is sufficient to show that 21a and 21b are valid in \mathcal{KC}_{RST}. To show 21a is valid in \mathcal{KC}_{RST}, let \mathbb{KC}\in\mathcal{KC}_{RST} and \mathbb{M}:=(\mathbb{KC}, v) be a model based on \mathbb{KC}.

By Corollary 6 and 7, v(\square\lozenge\alpha)=f_{R}f^{\delta}_{R}((v_{1}(\alpha), v_{2}(\alpha)))=f_{R}((\overline{v_{1}(\alpha)}^{R}, (\overline{v_{1}(\alpha)}^{R})^{\prime}))=(\underline{(\overline{v_{1}(\alpha)}^{R})}_{R}, (\underline{(\overline{v_{1}(\alpha)}^{R})}_{R})^{\prime} ). Let x\in \overline{v_{1}(\alpha)}^{R}. Then R(x)\cap v_{1}(\alpha)\neq\emptyset. Let z_{0}\in R(x)\cap v_{1}(\alpha) for some z_{0}\in G. Then xRz_{0}. Let y\in R(x). Then xRy, which implies that yRx, as R is symmetric. So yRz_{0}, as R is transitive, which implies that R(y)\cap v_{1}(\alpha)\neq\emptyset. So y\in \overline{v_{1}(\alpha)}^{R}, whence R(x)\subseteq \overline{v_{1}(\alpha)}^{R}. So x\in \underline{(\overline{v_{1}(\alpha)}^{R})}_{R}, which implies that \overline{v_{1}(\alpha)}^{R}\subseteq \underline{(\overline{v_{1}(\alpha)}^{R})}_{R}. So (\underline{(\overline{v_{1}(\alpha)}^{R})}_{R})^{\prime}\subseteq (\overline{v_{1}(\alpha)}^{R})^{\prime}, whence (\overline{v_{1}(\alpha)}^{R}, (\overline{v_{1}(\alpha)}^{R})^{\prime})\sqsubseteq (\underline{(\overline{v_{1}(\alpha)}^{R})}_{R}, (\underline{(\overline{v_{1}(\alpha)}^{R})}_{R})^{\prime}). So v(\lozenge\alpha)\sqsubseteq v(\square\lozenge\alpha).

By Proposition 16, \lozenge\alpha\vdash\square\lozenge\alpha is satisfied in \mathbb{M}, which implies that \lozenge\alpha\vdash\square\lozenge\alpha is true in \mathbb{KC}. So \lozenge\alpha\vdash\square\lozenge\alpha is valid in \mathcal{KC}_{RST}.

Similar to the above proof, we can show that \blacksquare\blacklozenge\alpha\vdash\blacklozenge\alpha is valid in \mathcal{KC}_{RST}.

We show that \mathbb{KC}(\mathcal{L}_{\Sigma}(\mathfrak{F}_{1})) is a symmetric Kripke context and rest of the proof is similar to the proof of Theorems 21 and 23.

To show R is symmetric, let F, F_{1}\in \mathcal{F}_{p}(\mathcal{L}_{\Sigma}(\mathfrak{F}_{1})) and FRF_{1}. Then for all [\alpha]\in F_{1}, f_{\lozenge}([\alpha])=[\lozenge\alpha]\in F. By axiom 21a and Proposition 10, f_{\lozenge}([\alpha])=[\lozenge\alpha]\sqsubseteq [\square\lozenge\alpha]=f_{\square}f_{\lozenge}([\alpha]). By Lemma 5(2), [\alpha]\sqcap [\alpha]\sqsubseteq f_{\lozenge}([\alpha]), as \mathcal{L}_{\Sigma}(\mathfrak{F}_{1}) is a pdBao. So [\alpha]\sqcap [\alpha]\sqsubseteq f_{\square}f_{\lozenge}([\alpha]). Let [\alpha]\in F. Then [\alpha]\sqcap [\alpha]\in F, as F is a filter. So f_{\square}f_{\lozenge}([\alpha])\in F, as F is a filter. By Lemma 6(1), f_{\lozenge}([\alpha])\in F_{1}, which implies that RF_{1}F. So R is symmetric.

Similar to the above, we can show that S is also symmetric.

Let \mathbb{K}:=(G, M, I) and A\subseteq G, B\subseteq M. Now observe that the pair (A,B) is a concept of \mathbb{K} if and only if (A,B)\sqcup (A,B)=(A,B)\sqcap (A,B)=(A, B). As v is a valuation, v preserve \sqcap, \sqcup and in \mathfrak{H}(\mathbb{K}) \sqsubseteq is partial order. The proof is a consequence of the observations.

1. Let (A, B) be a concept of \mathbb{K}, which implies that B=A^{\prime}=M and A=B^{\prime}=G. So (A, B)=(G, M), which implies that \mathcal{B}(\mathbb{K})=\{(G, M)\}.

2. v(\top\sqcap\top)=v(\top)\sqcap v(\top)=(G, \emptyset)\sqcap (G,\emptyset)=(G, G^{\prime})=(G, M)\in \mathcal{B}(\mathbb{K}). So \top\sqcap \top\in \mathfrak{F}_{\mathbb{M}}.

3. Let \alpha, \beta \in \mathfrak{F}_{\mathbb{M}}. Then v(\alpha) and v(\beta) are concepts of \mathbb{K}, which implies that v(\alpha)=(G, M)=v(\beta). So \beta\dashv\vdash\alpha is satisfied in the model \mathbb{M}.

Conversely, let \alpha\in \mathfrak{F}, and take \beta\in \mathfrak{F}_{\mathbb{M}} such that \beta \dashv\vdash\alpha is satisfied in the model \mathbb{M}. Then v(\alpha)=v(\beta)=(G, M)\in \mathcal{B}(\mathbb{K}). So \alpha\in \mathfrak{F}_{\mathbb{M}}.

Let

\mathbb{K}:=(\{g_{1},\ldots g_{n}\}, \{m_{1}\ldots m_{n}\}, I), and (A, B):=(\{g_{r_{1}}\ldots, g_{r_{k}}\}, \{m_{r_{1}},\ldots, m_{r_{k}}\} ) be a concept of \mathbb{K}. Then (A, B)=(\{g_{r_{1}}\ldots, g_{r_{k}}\}, \{m_{r_{1}},\ldots, m_{r_{k}}\} )=(B^{\prime}, B^{\prime\prime})= \sqcap_{i=1}^{k}(\{m_{r_{i}}\}^{\prime}, \{m_{r_{i}}\}). So there are some P_{i}, i=1,2,\ldots k, such that v(P_{i})=(\{m_{r_{i}}\}^{\prime}, \{m_{r_{i}}\}) in the model \mathbb{M}. The required formula is \alpha:=\sqcap_{i=1}^{k} P_{i}.

The proof of (R11) is similar to that of (R10) and we only prove (R10).
Note that from Proposition 3 and Theorem 11, one obtains in PDBL,
\alpha\sqcap\bot\vdash \bot and \bot\vdash\alpha\sqcap\bot (*)

Then we have:

Let \mathcal{K} be the class of all clarified contexts and p\sqcup p\vdash q\sqcup q, q\sqcup q\vdash p\sqcup p be valid in the class \mathcal{K}. To show p\vdash q and q\vdash p are valid in the class \mathcal{K}, let \mathbb{M}:=(\mathbb{K}, v) be a named model based on \mathbb{K}:=(G,M, R)\in\mathcal{K}. Then v(p)=(\{g\}, \{g\}^{\prime}) and v(q)=(\{g_{1}\}, \{g_{1}\}^{\prime} ) for some g,g_{1}\in G, and v(P)=(\{m\}^{\prime}, \{m\}), v(Q)=(\{m_{1}\}^{\prime}, \{m_{1}\}) for some m, m_{1}\in M. By Corollary 3, v(p\sqcup p)=v(p)\sqcup v(p)=(\{g\}, \{g\}^{\prime})\sqcup (\{g\}, \{g\}^{\prime} )=( \{g\}^{\prime\prime}, \{g\}^{\prime}). Similarly v(q\sqcup q)=( \{g_{1}\}^{\prime\prime}, \{g_{1}\}^{\prime}). Then ( \{g\}^{\prime\prime}, \{g\}^{\prime})=v(p\sqcup p)\sqsubseteq v(q\sqcup q)=( \{g_{1}\}^{\prime\prime}, \{g_{1}\}^{\prime}) and ( \{g_{1}\}^{\prime\prime}, \{g_{1}\}^{\prime})=v(q\sqcup q)\sqsubseteq v(p\sqcup p)=( \{g\}^{\prime\prime}, \{g\}^{\prime}), which implies that ( \{g\}^{\prime\prime}, \{g\}^{\prime})=( \{g_{1}\}^{\prime\prime}, \{g_{1}\}^{\prime}). So \{g\}^{\prime}=\{g_{1}\}^{\prime}, which implies that g=g_{1}, as \mathbb{K} is a clarified context. So v(p)=v(q), which implies that v(p)\sqsubseteq v(q) and v(q)\sqsubseteq v(p). So p\vdash q and q\vdash p are satisfied in \mathbb{M}, which implies that p\vdash q and q\vdash p are true in \mathbb{K}. So p\vdash q and q\vdash p are valid in the class \mathcal{K}, which implies that (1) and (2) are valid in \mathcal{K}.
Similar to the above proof we can show that (3) and (4) are valid in the class \mathcal{K}.
Conversely, let (1)-(4) be valid in the class \mathcal{K}. To show \mathcal{K} is the class of all clarified contexts, let \mathbb{K}:=(G,M,R)\in \mathcal{K}, and g, g_{1}\in G , m,m_{1}\in M such that \{g\}^{\prime}=\{g_{1}\}^{\prime} and \{m\}^{\prime}=\{m_{1}\}^{\prime}. Let \mathbb{M}:=(\mathbb{K}, v) be a named model such that v(p):=(\{g\}, \{g\}^{\prime}), v(q):=(\{g_{1}\}, \{g_{1}\}^{\prime}) and v(P):=(\{m\}^{\prime}, \{m\}), v(Q):=(\{m_{1}\}^{\prime}, \{m_{1}\}). Then p\sqcup p\dashv\vdash q\sqcup q and P\sqcap P\dashv\vdash Q\sqcap Q are satisfied in \mathbb{M}, as v(p\sqcup p)=v(q\sqcup q) and v(P\sqcap P)=v(Q\sqcap Q). So p\dashv\vdash q and P\dashv\vdash Q are satisfied in \mathbb{M}, which implies that v(p)=v(q) and v(P)=v(Q). So g=g_{1} and m=m_{1}, which implies that \mathbb{K} is a clarified context. Hence \mathcal{K} is the class of all clarified contexts.

Let (A, B) be a concept of \mathbb{K}. Then A^{\prime\prime}=A and B^{\prime\prime}=B. Let g\in A and g_{1}\in E_{1}(g). By definition of E_1, this means I(g)=I(g_{1}). As g \in A, g I m for any m \in A^\prime. So g_{1}Im for all such m, and thereby, g_1 \in A^{\prime\prime}=A.

Thus E_{1}(g)\subseteq A, which gives g\in \underline{A}. So \underline{A}=A, by Proposition 6(v), and by Proposition 6(vii), A is a category in (G, E_{1}). Similarly, we can show that B is a category in (M, E_{2}). Therefore, (A, B) is a definable semiconcept.

1. By Proposition 6(v), \underline{(\underline{A}_{E_{1}})^{\prime}}_{E_{2}}\subseteq (\underline{A}_{E_{1}})^{\prime}. Let m\in (\underline{A}_{E_{1}})^{\prime}. Then gIm for all g\in\underline{A}_{E_{1}}, which implies that gIm for all g\in G such that E_{1}(g)\subseteq A. Let m_{1}\in E_{2}(m), which implies that gIm if and only if gIm_{1} for all g\in G. So gIm_{1} for all g\in G, E_{1}(g)\subseteq A, which implies that gIm_{1} for all g\in \underline{A}_{E_{1}}. So m_{1}\in (\underline{A}_{E_{1}})^{\prime}, which implies that E_{2}(m)\subseteq (\underline{A}_{E_{1}})^{\prime}. So m\in \underline{(\underline{A}_{E_{1}})^{\prime}}_{E_{2}}, whence (\underline{A}_{E_{1}})^{\prime}\subseteq \underline{(\underline{A}_{E_{1}})^{\prime}}_{E_{2}}. So \underline{(\underline{A}_{E_{1}})^{\prime}}_{E_{2}}= (\underline{A}_{E_{1}})^{\prime}. By Proposition 6(v), (\overline{A}^{E_{1}})^{\prime}\subseteq \overline{(\overline{A}^{E_{1}})^{\prime}}^{E_{2}}. Let m\in \overline{(\overline{A}^{E_{1}})^{\prime}}^{E_{2}}. Then E_{2}(m)\cap (\overline{A}^{E_{1}})^{\prime}\neq\emptyset, which implies that there exists m_{1}\in (\overline{A}^{E_{1}})^{\prime} such that m_{1}\in E_{2}(m). Now for all g\in \overline{A}^{E_{1}}, gIm_{1}, which implies that for all g\in \overline{A}^{E_{1}}, gIm , as m_{1}\in E_{2}(m). So m\in (\overline{A}^{E_{1}})^{\prime}, whence \overline{(\overline{A}^{E_{1}})^{\prime}}^{E_{2}}\subseteq (\overline{A}^{E_{1}})^{\prime}. So \overline{(\overline{A}^{E_{1}})^{\prime}}^{E_{2}}=(\overline{A}^{E_{1}})^{\prime}. 3pt 2. The proof is similar to that of 1.

1. The proof follows from Propositions 21, 22 and 6(vii and viii).

2. Let (A, B) be a definable semiconcept. If (A, B) \in \mathcal{B}(\mathbb{K}), the proof follows from Definition 26(a).

Let (A, B)\in\mathfrak{H}(\mathbb{K})_{\sqcap}\setminus \mathcal{B}(\mathbb{K}). Then \underline{(A, B)}=(\underline{A}_{E_{1}}, (\underline{A}_{E_{1}})^{\prime})=(A, A^{\prime}), as A is a category in (G, E_{1}). So \underline{(A, B)}= (A, A^{\prime})=(A, B). Similarly, one gets the result for the case when (A, B)\in\mathfrak{H}(\mathbb{K})_{\sqcup}\setminus \mathcal{B}(\mathbb{K}).

Similar to the above proof, we can show that \overline{(A,B)}=(A, B).

3. The proof follows from 1 and 2.

4. Let (A, B) be a left semiconcept, so that (A, B)=(A, A^{\prime}).

If A is a category then by Proposition 22(1) it follows that A^{\prime} is a category. So (A, B) is definable semiconcept. The other direction follows from the definition of definability of semiconcepts.

5. The proof is similar to that of 4.

We give the proof for (1). The proof of (2) is similar.

(1)

Let (A, B)\in \mathfrak{H}(\mathbb{K}). If (A, B) \in \mathcal{B}(\mathbb{K}), the results are trivially true.

Case I: Let (A, B)\in\mathfrak{H}(\mathbb{K})_{\sqcap}\setminus \mathcal{B}(\mathbb{K}). We consider a model \mathbb{M}:=(\mathbb{KC}_{SD}, v) and p\in \textbf{OV} such that v(p)=(A, B). As \square p\vdash p is a valid sequent of \textbf{MPDBL5}, v(\square p)\sqsubseteq v(p), by Proposition 16. Using Proposition 15 and Definition 26(b), v(\Box p)= (\underline{A}_{E_{1}},(\underline{A}_{E_{1}})^{\prime})= \underline{v(p)}. So we get \underline{v(p)}\sqsubseteq v(p), which implies that \underline{(A, B)}\sqsubseteq (A, B). 3pt Case II: Let (A, B)\in\mathfrak{H}(\mathbb{K})_{\sqcup}\setminus \mathcal{B}(\mathbb{K}). We consider a model \mathbb{M}:=(\mathbb{KC}_{SD}, v) and P\in \textbf{PV} such that v(P)=(A, B). By Proposition 23(1), \blacklozenge P\vdash P\sqcup P. v(\blacklozenge P)\sqsubseteq v(P\sqcup P), by Proposition 16. Using Proposition 15 and Definition 26(c), v(\blacklozenge P)= ((\overline{B}^{E_{2}})^{\prime}, \overline{B}^{E_{2}})=\underline{v(P)}. Hence \underline{v(P)}\sqsubseteq v(P\sqcup P)=v(P)\sqcup v(P)= v(P), as v(P) \in \mathfrak{H}(\mathbb{K})_{\sqcup} which implies that \underline{(A, B)}\sqsubseteq (A, B). 3pt

3pt

Similar to the above derivations, using the valid sequents P\vdash\blacksquare P and p\sqcap p\vdash\lozenge p of \textbf{MPDBL5} (the last from Proposition 23(2), we get the property (A, B)\sqsubseteq \overline{(A, B)} in \mathfrak{H}(\mathbb{K}).