| Sbornik: Mathematics |
|
|
|
|
|
On the quantified version of the Belnap–Dunn modal logic A. V. Grefenshtein, S. O. Speranski Steklov Mathematical Institute of Russian Academy of Sciences, Moscow, Russia
Bibliographic databases:
     § 1. IntroductionQuantified intuitionistic logic, $\mathsf{QInt}$, plays a key role in constructive mathematics. Among its interpretations, a special place is occupied by Kleene’s realizability semantics and the informal Brouwer–Heyting–Kolmogorov interpretation; see [1] and, say, [2], Ch. 1. However, $\mathsf{QInt}$ has a certain drawback: although from each derivation of $\Phi$ in intuitionistic number theory one can extract a way to verify $\Phi$, a derivation of $\neg \Phi$ does not give a direct way to falsify $\Phi$, but only reduces the assumption that $\Phi$ is verifiable to absurdity; see [3] and [4].1 In particular, this implies the failure of the ‘negative disjunction property’: from the derivability of $\neg (\Phi \wedge \Psi)$ we cannot in general obtain the derivability of $\neg \Phi$ or $\neg \Psi$. In order to eliminate the drawback mentioned above, Nelson proposed to enrich the language of $\mathsf{QInt}$ by adding a ‘strong negation’, $\mathord{\sim}$, which is directly responsible for falsification, and expand the realizability semantics to the new language; see [4], and also [5]. This is how the logic $\mathsf{QN3}$ arose. Then its useful generalization $\mathsf{QN4}$ was described, which allows one to deal with inconsistent data; see [6]. Here $\mathsf{QN3}$ extends $\mathsf{QN4}$ by adding the scheme In what follows, for every quantified logic $\mathsf{Q}L$ we denote its propositional version by $L$.2 Notice that if we exclude intuitionistic implication, then $\mathsf{N3}$ turns to Kleene’s strong three-valued logic, which has an algorithmic interpretation, and $\mathsf{N4}$ turns to the well-known Belnap–Dunn four-valued logic; see [8], § 64, [9] and [10].A very important role in understanding $\mathsf{QInt}$ is played by the Gödel–McKinsey–Tarski translation from $\mathsf{QInt}$ into the modal logic $\mathsf{QS4}$, that is, the reflexive-transitive extension of the modal logic $\mathsf{QK}$. We would like to have a similar understanding of the logics $\mathsf{QN3}$ and $\mathsf{QN4}$. In the propositional case this problem was solved by Odintsov and Wansing in [11]:
However, so far nothing has been known about the situation in the quantifier case, despite the fact that constructive theories are formulated exactly in a quantified language. Our aim is to develop a quantified version of $\mathsf{BK}$, prove the strong completeness theorems for it and some of its extensions with respect to a suitable possible worlds semantics, and also generalize the result about faithful embeddings to $\mathsf{QN3}$ and $\mathsf{QN4}$. We will consider semantics with expanding domains as well as with constant domains. Furthermore, we will discuss interpolation properties for $\mathsf{QBK}$-extensions. § 2. SyntaxFor simplicity we restrict ourselves to signatures without equality and without function symbols.4 Let $\sigma$ be a signature. We denote by $\mathrm{Pred}_{\sigma}$ and $\mathrm{Const}_{\sigma}$ the sets of all of its predicate and constant symbols, respectively. Here and elsewhere we assume that $\mathrm{Pred}_{\sigma} \ne \varnothing$. Fix a countable set $\mathrm{Var}$, whose elements will be called variables. We denote by $\mathrm{Term}_{\sigma}$ the set of all $\sigma$-terms. Thus, $\mathrm{Term}_{\sigma} = \mathrm{Var} \cup \mathrm{Const}_{\sigma}$. Our logical vocabulary consists of:
We denote by $\mathrm{Form}_{\sigma}$ the set of all $\sigma$-formulae. For each $\Phi \in \mathrm{Form}_{\sigma}$ set
$$
\begin{equation*}
\mathrm{FV}(\Phi):= \{x \in \mathrm{Var} \mid x\ \text{is free in}\ \Phi\}.
\end{equation*}
\notag
$$
By $\sigma$-substitutions we mean functions from $\mathrm{Var}$ to $\mathrm{Term}_\sigma$. If $\mathrm{FV} (\Phi) \subseteq \{x_1, \dots, x_n\}$, then for each $\sigma$-substitution $\lambda$ we denote by $\lambda \Phi$ the result of replacing (simultaneously) all the free occurrences of $x_1$, …, $x_n$ in $\Phi$ by $\lambda(x_1)$, …, $\lambda(x_n)$, respectively. In the case when
$$
\begin{equation*}
\lambda=\{(x, t)\} \cup \{(y, y) \mid y \in \mathrm{Var}\text{ and }y \ne x\},
\end{equation*}
\notag
$$
where $x \in \mathrm{Var}$ and $t \in \mathrm{Term}_{\sigma}$, we often write $\Phi(x/t)$ instead of $\lambda\Phi$. Finally, a $\sigma$-substitution $\lambda$ is said to be ground if $\lambda(x) \in \mathrm{Const}_{\sigma}$ for all $x \in \mathrm{Var}$. For convenience we introduce the following abbreviations:
We denote by $\mathrm{Sent}_{\sigma}$ the set of all $\sigma$-sentences, that is, $\sigma$-formulae without free variables. Arbitrary subsets of $\mathrm{Sent}_{\sigma}$ are called $\sigma$-theories. As usual, by $\sigma$-structures we mean nonempty sets augmented with interpretations for the symbols of $\sigma$ over them. Let $\mathfrak{A}$ be an arbitrary $\sigma$-structure and $A$ be its domain. For each $\varepsilon \in \sigma$ set
$$
\begin{equation*}
\varepsilon^{\mathfrak{A}}:=\text{the interpretation of }\varepsilon\ \text{in}\ \mathfrak{A}.
\end{equation*}
\notag
$$
If we expand $\sigma$ to the signature
$$
\begin{equation*}
\sigma_A:=\sigma \cup \{\underline{a} \mid a \in A\},
\end{equation*}
\notag
$$
where the $\underline{a}$ are new constant symbols, then we can pass from $\mathfrak{A}$ to its $\sigma_A$-expansion $\mathfrak{A}^{\ast}$ such that
$$
\begin{equation*}
\underline{a}^{\mathfrak{A}^{\ast}}:=a \quad \text{for every } a\in A.
\end{equation*}
\notag
$$
In this case $\sigma_A$-formulae are also called $A$-formulae, and $\sigma_A$-substitutions are called $A$-substitutions. If $\Phi$ is a $A$-sentence, then we will often write $\mathfrak{A} \Vdash \Phi$ instead of $\mathfrak{A}^{\ast} \Vdash \Phi$.
§ 3. Hilbert-style calculusOur calculus for a quantified version of $\mathsf{BK}$ extends the deductive system for $\mathsf{BK}$ from [11]. It employs the following axiom schemes.
It also employs the following inference rules:
We denote by $\mathsf{QBK}_{\sigma}$ the least set of $\sigma$-formulae containing all axioms of our calculus (in the signature $\sigma$) and closed under all of its inference rules. In what follows, when the choice of $\sigma$ is not of significant importance or the whole logic is meant (with no reference to a specific signature), the lower index $\sigma$ will often be dropped. Proposition 3.1. $\mathsf{QBK}$ includes the Kripke scheme Furthermore, $\mathsf{QBK}$ is closed under the normalization rule Proof. The Kripke scheme is obtained in a standard way:
$$
\begin{equation*}
\begin{array}{ l| l|l} 1& (\Phi \to \Psi) \wedge \Phi \to \Psi &\text{classical logic} \\ 2& \Box ((\Phi \to \Psi) \wedge \Phi) \to \Box \Psi &\text{from 1 by MB} \\ 3& \Box (\Phi \to \Psi) \wedge \Box \Phi \to \Box ((\Phi \to \Psi) \wedge \Phi) &\mathrm{\Box 1} \\ 4& \Box (\Phi \to \Psi) \wedge \Box \Phi \to \Box \Psi &\text{from 3, 2} \\ 5& \Box (\Phi \to \Psi) \to (\Box \Phi \to \Box \Psi) &\text{from 4} \end{array}
\end{equation*}
\notag
$$
Now let us check the closedness of $\mathsf{QBK}$ under the normalization rule. Suppose that $\Phi$ belongs to $\mathsf{QBK}$. Then $\Box \Phi$ also belongs to $\mathsf{QBK}$:
$$
\begin{equation*}
\begin{array}{ l| l|l} 1& \Phi &\text{by hypothesis} \\ 2& (\Phi \to \Phi) \to \Phi&\text{from 1} \\ 3& \Box (\Phi \to \Phi) \to \Box \Phi&\text{from 2 by MB} \\ 4&\Box (\Phi \to \Phi)&\Box 2 \\ 5&\Box \Phi &\text{from 4, 3} \end{array}
\end{equation*}
\notag
$$
The proposition is proved. For each $\Gamma \subseteq \mathrm{Form}_{\sigma}$ we define
$$
\begin{equation*}
\operatorname{Disj} (\Gamma):=\{\Phi_1 \vee \dots \vee \Phi_n \mid n \in \mathbb{N}\ \text{and}\ \{\Phi_1, \dots, \Phi_n\} \subseteq \Gamma\}.
\end{equation*}
\notag
$$
Here the empty disjunction is identified with $\bot$. Given $\Gamma \subseteq \mathrm{Sent}_{\sigma}$ and $\Delta \subseteq \mathrm{Form}_{\sigma}$, we write $\Gamma \vdash \Delta$ if and only if some element of $\mathrm{Disj}(\Delta)$ can be obtained from elements of $\Gamma \cup \mathsf{QBK}_{\sigma}$ by means of $\mathrm{MP}$, $\mathrm{BR1}$ and $\mathrm{BR2}$.5 Since the modal rules ($\mathrm{MB}$ and $\mathrm{MD}$) are not used here, the derivability relation $\vdash$ has a local character, in the sense that it is intended to preserve truth in specific worlds (see the definition of the semantical consequence relation in § 4); at the same time $\mathrm{MB}$ and $\mathrm{MD}$ will apply globally, that is, preserve truth in models, but not in specific worlds of these models. Of course, when $\Delta = \{\Phi\}$, we usually write $\Gamma \vdash \Phi$ instead of $\Gamma \vdash \{\Phi\}$. Theorem 3.2 (deduction). For any $\Gamma \cup \{\Phi\} \subseteq \mathrm{Sent}_{\sigma}$ and $\Psi \in \mathrm{Form}_{\sigma}$,6 The proof is similar to the case of classical first-order logic. Like other logics with strong negation, $\mathsf{BK}$ is not closed under the usual replacement rule; see [11]. Of course, the same holds for $\mathsf{QBK}$, but to justify this fact formally, we need a suitable possible world semantics, which appears only in § 4. Nevertheless, the ‘positive’ and ‘weak’ replacement rules from [11] can be generalized, without much effort, to the quantifier case. Theorem 3.3 (positive replacement rule). Let $\{\Phi, \Psi, \Theta\} \subseteq \mathrm{Form}_{\sigma}$. Suppose that $\Phi'$ is obtained from $\Phi$ by replacing some occurrences of $\Psi$ by $\Theta$, and none of these occurrences are in the scope of $\mathord{\sim}$. Then $\vdash \Psi \leftrightarrow \Theta$ implies that $\vdash \Phi \leftrightarrow \Phi'$. Proof. We restrict ourselves to the cases when $\Phi$ begins with $\forall$ or $\exists$, because the remaining cases have actually been considered by Odintsov and Wansing. Furthermore, we may assume that $\Psi \ne \Phi$, since otherwise the statement is trivial.
Suppose $\Phi = \forall\,x\ \Omega$. Clearly, the part $\Omega$ corresponds to $\Omega'$ such that $\Phi' = \forall\,x\ \Omega'$. Then $\Phi \leftrightarrow \Phi'$ is derived in a standard way:
$$
\begin{equation*}
\begin{array}{ c| l|l} 1& \Omega \leftrightarrow \Omega' &\text{inductive hypothesis} \\ 2&\forall\,x\ \Omega \to \Omega &\text{Q1} \\ 3&\forall\,x\ \Omega \to \Omega' &\text{from 2, 1} \\ 4&\forall\,x\ \Omega \to \forall\,x\ \Omega' &\text{from 3 by BR1} \\ 5&\forall\,x\ \Omega' \to \forall\,x\ \Omega &\text{by analogy with 4} \\ 6&\forall\,x\ \Omega \leftrightarrow \forall\,x\ \Omega' &\text{from 4, 5} \end{array}
\end{equation*}
\notag
$$
For $\Phi = \exists\,x\ \Omega$ the argument is similar. The theorem is proved. For convenience, in what follows we will denote applications of Theorem 3.3 by $\mathrm{PR}$, from ‘positive replacement’. Theorem 3.4 (weak replacement rule). Let $\{\Phi, \Psi, \Theta\} \subseteq \mathrm{Form}_{\sigma}$. Suppose that $\Phi'$ is obtained from $\Phi$ by replacing some occurrences of $\Psi$ by $\Theta$. Then $\vdash \Psi \Leftrightarrow \Theta$ implies that $\vdash \Phi \Leftrightarrow \Phi'$. Proof. We restrict ourselves to the cases when $\Phi$ begins with $\mathord{\sim}$, $\forall$ or $\exists$. Furthermore, we may assume that $\Psi \ne \Phi$.
Suppose $\Phi = \mathord{\sim} \Omega$. Clearly, the part $\Omega$ corresponds to $\Omega'$ such that $\Phi' = \mathord{\sim} \Omega'$. Then $\Phi \Leftrightarrow \Phi'$ can easily be derived:
$$
\begin{equation*}
\begin{array}{ c| l|l} 1 &\Omega \Leftrightarrow \Omega' &\text{inductive hypothesis} \\ 2&\Omega \leftrightarrow \Omega' &\text{from 1} \\ 3&\mathord{\sim} \mathord{\sim} \Omega \leftrightarrow \Omega &\text{SN1} \\ 4&\Omega'\leftrightarrow \mathord{\sim} \mathord{\sim} \Omega' &\text{SN1} \\ 5&\mathord{\sim} \mathord{\sim} \Omega \leftrightarrow \mathord{\sim} \mathord{\sim} \Omega' &\text{from 3, 2, 4} \\ 6&\mathord{\sim} \Omega \leftrightarrow \mathord{\sim} \Omega' &\text{from 1}\\ 7&\mathord{\sim} \Omega \Leftrightarrow \mathord{\sim} \Omega' &\text{from 6, 5} \end{array}
\end{equation*}
\notag
$$
Suppose $\Phi = \forall\,x\ \Omega$. So the part $\Omega$ corresponds to $\Omega'$ such that $\Phi' = \forall\,x\ \Omega'$. Then $\Phi \Leftrightarrow \Phi'$ can be derived in the following way:
$$
\begin{equation*}
\begin{array}{ c| l|l} 1&\Omega \Leftrightarrow \Omega' &\text{inductive hypothesis} \\ 2&\Omega \leftrightarrow \Omega' &\text{from 1} \\ 3&\forall\,x\ \Omega \leftrightarrow \forall\,x\ \Omega' &\text{from 2 by PR} \\ 4 &\mathord{\sim} \Omega \leftrightarrow \mathord{\sim} \Omega' &\text{from 1} \\ 5&\exists\,x\ \mathord{\sim} \Omega \leftrightarrow \exists\,x\ \mathord{\sim} \Omega' &\text{from 4 by PR} \\ 6&\mathord{\sim} \forall\,x\ \Omega \leftrightarrow \exists\,x\ \mathord{\sim} \Omega &\text{SN6} \\ 7&\exists\,x\ \mathord{\sim} \Omega' \leftrightarrow \mathord{\sim} \forall\,x\ \Omega' &\text{SN6} \\ 8&\mathord{\sim}\forall\,x\ \Omega \leftrightarrow \mathord{\sim} \forall\,x\ \Omega' &\text{from 6, 5, 7} \\ 9&\forall\,x\ \Omega \Leftrightarrow \forall\,x\ \Omega' &\text{from 3, 8} \end{array}
\end{equation*}
\notag
$$
For $\Phi = \exists\,x\ \Omega$ the argument is similar. The theorem is proved. For convenience, in what follows we will denote applications of Theorem 3.4 by $\mathrm{WR}$, from ‘weak replacement’. We say that a $\sigma$-formula $\Phi$ is a negation normal form, or an n.n.f. for short, if each occurrence of $\mathord{\sim}$ in $\Phi$ immediately precedes some atomic subformula.7 Our next aim is to prove a strong version of the n.n.f. theorem for $\mathsf{QBK}$. Here ‘strong’ indicates that we do use not $\leftrightarrow$ (as in [13], for example), but $\Leftrightarrow$ (cf. Proposition 3.1 in [16]). On this path the following result turns out to be useful. Proposition 3.5. The following schemes are derivable8 in $\mathsf{QBK}$: Proof. $\mathrm{A1}$. First we derive $\mathord{\sim}\neg\Phi \to \neg\neg\Phi$:
$$
\begin{equation*}
\begin{array}{ c| l|l} 1&\mathord{\sim}(\Phi \to \bot) \leftrightarrow (\Phi \wedge \mathord{\sim}\bot) &\text{SN3} \\ 2&\mathord{\sim}(\Phi \to \bot) \to (\Phi \wedge \mathord{\sim}\bot) &\text{from 1} \\ 3&\mathord{\sim}(\Phi \to \bot) \to \Phi &\text{from 2} \\ 4&\Phi \to \neg \neg \Phi &\text{classical logic} \\ 5&\mathord{\sim}(\Phi \to \bot) \to \neg \neg \Phi &\text{from 3, 4} \end{array}
\end{equation*}
\notag
$$
(recall that $\neg \Phi$ is an abbreviation for $\Phi \to \bot$). Now we derive $\neg\neg\Phi \to \mathord{\sim} \neg\Phi$:
$$
\begin{equation*}
\begin{array}{ c| l|l} 1&\neg \neg \Phi \to \Phi &\text{classical logic} \\ 2&\mathord{\sim}\bot &\text{SN5} \\ 3&\neg \neg \Phi \to (\Phi \wedge \mathord{\sim}\bot) &\text{from 1, 2} \\ 4&(\Phi \wedge \mathord{\sim}\bot) \leftrightarrow \mathord{\sim}(\Phi \to \bot) &\text{SN3} \\ 5&\neg\neg \Phi \to \mathord{\sim}(\Phi \to \bot) &\text{from 3, 4} \end{array}
\end{equation*}
\notag
$$
Thus, $\mathord{\vdash} \mathord{\sim} \neg \Phi \leftrightarrow \neg\neg\Phi$ for all $\Phi \in \mathrm{Form}_{\sigma}$. Finally, note that:
$$
\begin{equation*}
\begin{array}{ c| l|l} 1&\mathord{\sim}\mathord{\sim}\neg \Phi \leftrightarrow \neg \Phi &\text{SN4} \\ 2&\neg \Phi \leftrightarrow \neg \neg \neg \Phi &\text{classical logic} \\ 3&\neg \neg \neg \Phi \leftrightarrow \mathord{\sim}\neg \neg \Phi &\text{by what has already been proved} \\ 4&\mathord{\sim}\mathord{\sim}\neg \Phi \leftrightarrow \mathord{\sim}\neg \neg \Phi &\text{from 1, 2, 3} \end{array}
\end{equation*}
\notag
$$
Hence $\mathord{\vdash}\mathord{\sim}\neg\Phi \Leftrightarrow \neg\neg\Phi$ for every $\Phi\in \mathrm{Form}_{\sigma}$.
$\mathrm{A2}$. Clearly, $(\Phi \to \Psi) \leftrightarrow (\neg\Phi\vee\Psi)$ can be derived as in classical logic. Let us show the derivability of $\mathord{\sim}(\Phi \to \Psi) \leftrightarrow \mathord{\sim}(\neg\Phi\vee \Psi)$:
$$
\begin{equation*}
\begin{array}{ c| l|l} 1&\mathord{\sim}(\Phi \to \Psi) \leftrightarrow (\Phi \wedge \mathord{\sim}\Psi) &\text{SN3} \\ 2&\Phi \leftrightarrow {\neg \neg \Phi} &\text{classical logic} \\ 3&\neg \neg \Phi \Leftrightarrow \mathord{\sim}\neg \Phi &\text{A1} \\ 4&\Phi \leftrightarrow \mathord{\sim}\neg \Phi &\text{from 3, 4} \\ 5&(\Phi \wedge \mathord{\sim}\Psi) \leftrightarrow (\mathord{\sim}\neg \Phi \wedge \mathord{\sim} \Psi) &\text{from 4 by PR} \\ 6&({\mathord{\sim}\neg \Phi} \wedge \mathord{\sim}\Psi) \leftrightarrow {\mathord{\sim}(\neg \Phi \vee \Psi)} &\text{SN3} \\ 7&{\mathord{\sim}(\Phi \to \Psi)} \leftrightarrow {\mathord{\sim}(\neg \Phi \vee \Psi)} &\text{from 1, 5, 6} \end{array}
\end{equation*}
\notag
$$
The proposition is proved. For each $\mathrm{S} \in \{\mathrm{SN1}, \mathrm{SN2}, \mathrm{SN3}, \mathrm{SN6}, \mathrm{SN7}, \mathrm{M1}, \mathrm{M2}\}$ we denote by $\mathrm{S}^{\ast}$ the scheme obtained from $\mathrm{S}$ by replacing $\leftrightarrow$ by $\Leftrightarrow$. Lemma 3.6. $\mathrm{SN1}^{\ast}$, $\mathrm{SN2}^{\ast}$, $\mathrm{SN3}^{\ast}$, $\mathrm{M1}^{\ast}$ and $\mathrm{M2}^{\ast}$ are derivable in $\mathsf{QBK}$.9 Proof. $\mathrm{SN1}^{\ast}$. Obviously, $\mathord{\sim} \mathord{\sim} \mathord{\sim} \Phi \leftrightarrow \mathord{\sim} \Phi$ belongs to $\mathsf{QBK}$ (as a special case of $\mathrm{SN1}$).
$\mathrm{SN2}^{\ast}$. Let us show that $\mathord{\sim} \mathord{\sim} (\Phi \wedge \Psi) \leftrightarrow \mathord{\sim} (\mathord{\sim} \Phi \vee \mathord{\sim} \Psi)$ belongs to $\mathsf{QBK}$:
$$
\begin{equation*}
\begin{array}{ c| l|l} 1 &{\mathord{\sim}\mathord{\sim}(\Phi \wedge \Psi)} \leftrightarrow (\Phi \wedge \Psi) &\text{SN1} \\ 2 &\Phi \leftrightarrow {\mathord{\sim}\mathord{\sim}\Phi} &\text{SN1} \\ 3& (\Phi \wedge \Psi) \leftrightarrow ({\mathord{\sim}\mathord{\sim}\Phi} \wedge \Psi) &\text{from 2 by PR} \\ 4 & \Psi \leftrightarrow {\mathord{\sim}\mathord{\sim}\Psi} &\text{SN1} \\ 5 & ({\mathord{\sim}\mathord{\sim}\Phi} \wedge \Psi) \leftrightarrow ({\mathord{\sim}\mathord{\sim}\Phi} \wedge {\mathord{\sim}\mathord{\sim}\Psi}) &\text{from 4 by PR} \\ 6 & ({\mathord{\sim}\mathord{\sim}\Phi} \wedge {\mathord{\sim}\mathord{\sim}\Psi}) \leftrightarrow {\mathord{\sim}(\mathord{\sim}\Phi \vee \mathord{\sim}\Psi)} &\text{SN3} \\ 7 & \mathord{\sim}\mathord{\sim}(\Phi \vee \Psi) \leftrightarrow \mathord{\sim}(\mathord{\sim}\Phi \wedge \mathord{\sim}\Psi) &\text{from 1, 3, 5, 6} \end{array}
\end{equation*}
\notag
$$
$\mathrm{SN3}^{\ast}$. This case is similar to $\mathrm{SN2}^{\ast}$. $\mathrm{M1}^{\ast}$. Let us show that $\mathord{\sim} \neg\Box\Phi \leftrightarrow \mathord{\sim} \Diamond \neg \Phi$ belongs to $\mathsf{QBK}$:
$$
\begin{equation*}
\begin{array}{ c| l|l} 1&{\mathord{\sim}{\neg \Box \Phi}} \leftrightarrow {\neg {\neg \Box \Phi}} &\text{A1} \\ 2&{\neg \Box \Phi} \leftrightarrow {\Diamond \neg \Phi} &\text{M1} \\ 3&{\neg {\neg \Box \Phi}} \leftrightarrow {\neg {\Diamond \neg \Phi}} &\text{from 1 by PR} \\ 4&{\neg {\Diamond \neg \Phi}} \leftrightarrow {\Box {\neg \neg \Phi}} &\text{M2} \\ 5&{\neg \neg \Phi} \leftrightarrow {\mathord{\sim}\neg \Phi} &\text{A1} \\ 6&{\Box {\neg \neg \Phi}} \leftrightarrow {\Box {\mathord{\sim}\neg \Phi}} &\text{from 5 by PR} \\ 7&{\Box {\mathord{\sim}\neg \Phi}} \leftrightarrow {\mathord{\sim}{\mathord{\sim}{\Box {\mathord{\sim}\neg \Phi}}}} &\text{SN1} \\ 8& {\mathord{\sim}{\Box {\mathord{\sim}\neg \Phi}}} \Leftrightarrow {\Diamond \neg \Phi} &\text{M4} \\ 9& {\mathord{\sim}{\mathord{\sim}{\Box {\mathord{\sim}\neg \Phi}}}} \leftrightarrow {\mathord{\sim}{\Diamond \neg \Phi}} &\text{from 8} \\ 10& {\mathord{\sim}{\neg \Box \Phi}} \leftrightarrow {\mathord{\sim}{\Diamond \neg \Phi}} &\text{from 1, 3, 4, 6, 7, 9} \end{array}
\end{equation*}
\notag
$$
$\mathrm{M2}^{\ast}$. This case is similar to $\mathrm{M1}^{\ast}$. The lemma is proved. Proof. $\mathrm{SN6}^{\ast}$. Let us show that $\mathord{\sim} \mathord{\sim} \forall\,x\ \Phi \leftrightarrow \mathord{\sim} \exists\,x\ \mathord{\sim} \Phi$ belongs to $\mathsf{QBK}$:
$$
\begin{equation*}
\begin{array}{ c| l|l} 1&{\mathord{\sim}{\mathord{\sim}\forall\,x\ \Phi}} \leftrightarrow \forall\,x\ \Phi &\text{SN1} \\ 2& \Phi \leftrightarrow {\mathord{\sim}\mathord{\sim}\Phi} &\text{SN1} \\ 3& \forall\,x\ \Phi \leftrightarrow \forall\,x\ {\mathord{\sim}\mathord{\sim}\Phi} &\text{from 2 by PR} \\ 4& \forall\,x\ {\mathord{\sim}\mathord{\sim}\Phi} \leftrightarrow {\mathord{\sim}\exists\,x\ \mathord{\sim}\Phi} &\text{SN7} \\ 5& {\mathord{\sim}{\mathord{\sim}\forall\,x\ \Phi}} \leftrightarrow {\mathord{\sim} \exists\,x\ \mathord{\sim}\Phi} &\text{from 1, 3, 4} \end{array}
\end{equation*}
\notag
$$
$\mathrm{SN7}^{\ast}$. This case is similar to $\mathrm{SN6}^{\ast}$. The lemma is proved. At the same time we cannot replace $\leftrightarrow$ in $\mathrm{SN4}$ by $\Leftrightarrow$ (this can formally be justified by means of a suitable possible world semantics). However, instead of $\mathrm{SN4}$ one can employ the formula scheme
$$
\begin{equation}
{\mathord{\sim}(\Phi \to \Psi)} \Leftrightarrow ({\neg \neg \Phi} \wedge \mathord{\sim} \Psi),
\end{equation}
\tag{SN4$'$}
$$
which is not hard to obtain by using the above results:
$$
\begin{equation*}
\begin{array}{ c| c|l} 1&(\Phi \to \Psi) \Leftrightarrow (\neg \Phi \vee \Psi) &\text{A2} \\ 2&{\mathord{\sim}(\Phi \to \Psi)} \Leftrightarrow {\mathord{\sim}(\neg \Phi \vee \Psi)} &\text{from 1 by WR} \\ 3&{\mathord{\sim}(\neg \Phi \vee \Psi)} \Leftrightarrow ({\mathord{\sim}\neg \Phi} \wedge \mathord{\sim}\Psi) &\text{SN3}^{\ast} \\ 4&{\mathord{\sim}\neg \Phi} \Leftrightarrow {\neg \neg \Phi} &\text{A1} \\ 5&({\mathord{\sim}\neg \Phi} \wedge \mathord{\sim}\Psi) \Leftrightarrow ({\neg \neg \Phi} \wedge \mathord{\sim}\Psi) &\text{from 4 by WR} \\ 6&{\mathord{\sim}(\Phi \to \Psi)} \Leftrightarrow ({\neg \neg \Phi} \wedge \mathord{\sim} \Psi) &\text{from 2, 3, 5} \end{array}
\end{equation*}
\notag
$$
Now we are ready to establish the following. Theorem 3.8 (on negation normal form, strong version). For every $\sigma$-formula $\Phi$ there exists an n.n.f. $\overline{\Phi}$ such that $\Phi \Leftrightarrow \overline{\Phi} \in \mathsf{QBK}_{\sigma}$. Moreover, there is an algorithm that, given a $\sigma$-formula $\Phi$, constructs a suitable n.n.f. $\overline{\Phi}$. Proof. This goes by easy induction on the complexity of $\Phi$, where we use the rule $\mathrm{WR}$ and the schemes $\mathrm{SN1}^{\ast}$, $\mathrm{SN2}^{\ast}$, $\mathrm{SN3}^{\ast}$, $\mathrm{SN4}'$, $\mathrm{SN6}^{\ast}$, $\mathrm{SN7}^{\ast}$, $\mathrm{M3}$ and $\mathrm{M4}$. Here it is convenient to rewrite $\mathrm{M3}$ and $\mathrm{M4}$ as follows:
$\mathrm{M3}'$. $\mathord{\sim}\Box\Phi \Leftrightarrow \Diamond\mathord{\sim}\Phi$; $\mathrm{M4}'$. $\mathord{\sim}\Diamond\Phi \Leftrightarrow \Box\mathord{\sim}\Phi$. The theorem is proved. Remark 3.9. For Nelson’s constructive logics (propositional or quantified) the analogue of Theorem 3.8 does not hold: there the implication connective has a much more complex, intuitionistic character, and we can obtain only a weak version of the n.n.f. theorem. Finally, by $\mathsf{QBK}$-extensions we mean supersets of $\mathsf{QBK}$ closed under formula substitutions and all the inference rules (including the modal ones).10 Given a $\mathsf{QBK}$-extension $L$, we define
$$
\begin{equation*}
\Gamma \vdash_{L} \Delta \quad :\Longleftrightarrow \quad L \cup \Gamma \vdash \Delta.
\end{equation*}
\notag
$$
If $L$ is a $\mathsf{QBK}$-extension and $\mathrm{S}_1,\dots,\mathrm{S}_n$ are formula schemes, then we denote by $L + \{\mathrm{S}_1, \dots, \mathrm{S}_n\}$ the least $\mathsf{QBK}$-extension containing $L$ and all the substitution instances of $\mathrm{S}_1, \dots, \mathrm{S}_n$. In fact, all these notions depend formally on the choice of $\sigma$, but it will always be clear from the context which signature we are talking about, or we will explicitly write $L_{\sigma}$ instead of $L$. It is not hard to see that the results of the present section remain true if we replace $\mathsf{QBK}$ by an arbitrary $\mathsf{QBK}$-extension in their formulations. § 4. Possible world semanticsAs usual, by a frame we mean an ordered pair of the form $\mathcal{W} = \langle W, R \rangle$, where $W$ is a nonempty set, whose elements are called possible worlds, and $R$ is a binary relation on $W$. Given a frame $\mathcal{W}$ and two families of $\sigma$-structures
$$
\begin{equation*}
\mathscr{A}^+=\langle \mathfrak{A}_w^+\colon w \in W \rangle \quad\text{and}\quad \mathscr{A}^-=\langle \mathfrak{A}_w^-\colon w \in W \rangle,
\end{equation*}
\notag
$$
the corresponding triple
$$
\begin{equation*}
\mathcal{M}=\langle \mathcal{W}, \mathscr{A}^+, \mathscr{A}^- \rangle
\end{equation*}
\notag
$$
is called a $\mathsf{QBK}_{\sigma}$-model if for any $u, v \in W$:
Let $\mathcal{M}$ be a $\mathsf{QBK}_\sigma$-model. In what follows $R(u)$ will denote $\{v \in W \mid u \mathbin{R} v\}$, that is, the image of $\{u\}$ under $R$. For any $w \in W$ and $A_w$-sentence $\Phi$ we define
$$
\begin{equation*}
\mathcal{M}, w \Vdash^+ \Phi \quad\text{and}\quad \mathcal{M}, w \Vdash^- \Phi
\end{equation*}
\notag
$$
by recursion on the complexity of $\Phi$:
$$
\begin{equation*}
\begin{aligned} \, \mathcal{M}, w \Vdash^+ P (t_1, \dots, t_n) \quad&\Longleftrightarrow \quad \mathfrak{A}^+_w \Vdash P (t_1, \dots, t_n); \\ \mathcal{M}, w \Vdash^- P (t_1, \dots,t_n) \quad &\Longleftrightarrow \quad \mathfrak{A}^-_w \Vdash P (t_1, \dots,t_n); \\ \mathcal{M}, w \Vdash^+ \Psi \wedge \Theta \quad&\Longleftrightarrow \quad \mathcal{M}, w \Vdash^+ \Psi \quad \text{and} \quad \mathcal{M}, w \Vdash^+ \Theta; \\ \mathcal{M}, w \Vdash^- \Psi \wedge \Theta \quad&\Longleftrightarrow \quad \mathcal{M}, w \Vdash^- \Psi \quad \text{or} \quad \mathcal{M}, w \Vdash^- \Theta; \\ \mathcal{M}, w \Vdash^+ \Psi \vee \Theta \quad&\Longleftrightarrow \quad \mathcal{M}, w \Vdash^+ \Psi \quad \text{or} \quad \mathcal{M}, w \Vdash^+ \Theta; \\ \mathcal{M}, w \Vdash^- \Psi \vee \Theta \quad&\Longleftrightarrow \quad \mathcal{M}, w \Vdash^- \Psi \quad \text{and} \quad \mathcal{M}, w \Vdash^- \Theta; \\ \mathcal{M}, w \Vdash^+ \Psi \to \Theta \quad&\Longleftrightarrow \quad \mathcal{M}, w \nVdash^+ \Psi \quad \text{or} \quad \mathcal{M}, w \Vdash^+ \Theta; \\ \mathcal{M}, w \Vdash^- \Psi \to \Theta \quad&\Longleftrightarrow \quad \mathcal{M}, w \Vdash^+ \Psi \quad \text{and} \quad \mathcal{M}, w \Vdash^- \Theta; \\ \mathcal{M}, w \Vdash^+ \bot \quad&\Longleftrightarrow \quad 0 \not= 0; \\ \mathcal{M}, w \Vdash^- \bot \quad&\Longleftrightarrow \quad 0 = 0; \\ \mathcal{M}, w \Vdash^+ \mathord{\sim}\Psi \quad&\Longleftrightarrow \quad \mathcal{M},w \Vdash^- \Psi; \\ \mathcal{M}, w \Vdash^- \mathord{\sim}\Psi \quad&\Longleftrightarrow \quad \mathcal{M},w \Vdash^+ \Psi; \\ \mathcal{M}, w \Vdash^+ {\Box \Psi} \quad&\Longleftrightarrow \quad \mathcal{M}, w \Vdash^+ \Psi \quad \text{for all} \ {u \in R (w)}; \\ \mathcal{M},w \Vdash^- \Box \Psi \quad&\Longleftrightarrow \quad \mathcal{M}, w \Vdash^- \Psi \quad \text{for some} \ {u \in R (w)}; \\ \mathcal{M}, w \Vdash^+ \Diamond \Psi \quad&\Longleftrightarrow \quad \mathcal{M}, w \Vdash^+ \Psi \quad \text{for some} \ {u \in R (w)}; \\ \mathcal{M}, w \Vdash^- \Diamond \Psi \quad&\Longleftrightarrow \quad \mathcal{M}, w \Vdash^- \Psi \quad \text{for all} \ {u \in R (w)}; \\ \mathcal{M}, w \Vdash^+ \forall\,x\ \Psi \quad&\Longleftrightarrow \quad \mathcal{M}, w \Vdash^+ {\Psi (x / \underline{a})} \quad \text{for all} \ a \in A_w; \\ \mathcal{M},w \Vdash^- \forall\,x\ \Psi \quad&\Longleftrightarrow \quad \mathcal{M}, w \Vdash^- {\Psi (x / \underline{a})} \quad \text{for some} \ a \in A_w; \\ \mathcal{M}, w \Vdash^+ \exists\,x\ \Psi \quad&\Longleftrightarrow \quad \mathcal{M}, w \Vdash^+ {\Psi (x / \underline{a})} \quad \text{for some} \ a \in A_w; \\ \mathcal{M},w \Vdash^- \exists\,x\ \Phi \quad&\Longleftrightarrow \quad \mathcal{M}, w \Vdash^- {\Psi (x / \underline{a})} \quad \text{for all} \ a \in A_w. \end{aligned}
\end{equation*}
\notag
$$
In particular, we always have $\mathcal{M}, w \nVdash^+ \bot$ and $\mathcal{M}, w \Vdash^- \bot$. Informally, $\Vdash^+$ is responsible for verifiability, and $\Vdash^-$ is for falsifiability. When the model $\mathcal{M}$ we are talking about is clear from the context, we write $w \Vdash^{\circ} \Phi$ instead of $\mathcal{M}, w \Vdash^{\circ} \Phi$, where ${\circ} \in \{+, -\}$. Finally, the notation $\mathcal{W} \Vdash \Phi$ means that $\mathcal{M}, w \Vdash^+ \lambda \Phi$ for any $\mathsf{QBK}_{\sigma}$-model $\mathcal{M}$ based on $\mathcal{W}$, $w \in W$ and $A_w$-substitution $\lambda$. The semantics for $\mathsf{QBK}$, as well as its propositional version from [17], is locally four-valued. More precisely, four situations are potentially possible:
Remark 4.1. Models for $\mathsf{QBK}$ can be viewed as ‘modalized’ versions of models for the quantified Belpan–Dunn logic; cf. [18]. Although the language of the latter does not contain $\bot$ and $\to$, they can easily be added; see [17], § 4. Let $\Gamma \subseteq \mathrm{Sent}_{\sigma}$ and $\Delta \subseteq \mathrm{Form}_{\sigma}$. We say that $\Delta$ follows semantically from $\Gamma$, and write $\Gamma \vDash \Delta$, if for any $\mathsf{QBK}_{\sigma}$-model $\mathcal{M} = \langle \mathcal{W}, \mathscr{A}^+, \mathscr{A}^- \rangle$, $w \in W$ and ground $A_w$-substitution $\lambda$,
$$
\begin{equation*}
{\mathcal{M}, w \Vdash^+ \Phi} \quad \text{for all} \ {\Phi \in \Gamma} \quad \Longrightarrow \quad {\mathcal{M}, w \Vdash^+ \lambda \Psi} \quad \text{for some} \ {\Psi \in \Delta}.
\end{equation*}
\notag
$$
By analogy with $\vdash$, when $\Delta = \{\Phi\}$, we usually write $\Gamma \vDash \Phi$ instead of $\Gamma \vDash \{\Phi\}$. We call a $\sigma$-formula $\Phi$ valid if $\vDash \Phi$. As is easily verified, the following semantic analogue of the deduction theorem holds. Theorem 4.2. For any $\Gamma \cup \{\Phi\} \subseteq \mathrm{Sent}_{\sigma}$ and $\Psi \in \mathrm{Form}_{\sigma}$, Our next goal is to show that $\mathsf{QBK}$ is sound with respect to the above semantics. Lemma 4.3. For every $\Phi \in \mathrm{Form}_{\sigma}$, In other words, the derivability of a $\sigma$-formula implies its validity. Proof. Suppose that $\vdash \Phi$, that is, there exists a finite sequence of $\sigma$-formulae such that for each $i \in \{0, \dots, n\}$ one of the following conditions is satisfied:
If $\Phi_i$ is an axiom of classical logic, then we can argue as in classical first-order logic. If $\Phi_i$ is a ‘propositional’ axiom for strong negation, then we can argue as in $\mathsf{BK}$: see [11], § 4. For example, let $\Phi_i$ be an axiom of type $\mathrm{SN4}$, that is, of the form
$$
\begin{equation*}
{\mathord{\sim}(\Psi \to \Theta) \leftrightarrow (\Psi \wedge {\mathord{\sim}\Theta})}.
\end{equation*}
\notag
$$
We need to show that for any $w \in W$ and ground $A_w$-substitution $\lambda$,
$$
\begin{equation*}
w \Vdash^+ \lambda \mathord{\sim}(\Psi \to \Theta) \quad \Longleftrightarrow \quad w \Vdash^+ {\lambda (\Psi \wedge {\mathord{\sim}\Theta})}.
\end{equation*}
\notag
$$
This is done as follows:
$$
\begin{equation*}
\begin{aligned} \, w \Vdash^+ \lambda \mathord{\sim}(\Psi \to \Theta) \quad &\Longleftrightarrow \quad w \Vdash^+ {\mathord{\sim}({\lambda \Psi} \to {\lambda \Theta})} \\ \quad &\Longleftrightarrow \quad w \Vdash^- {\lambda \Psi} \to {\lambda \Theta} \\ \quad &\Longleftrightarrow \quad w \Vdash^+ {\lambda \Psi} \quad \text{and} \quad w \Vdash^- {\lambda \Theta} \\ \quad &\Longleftrightarrow \quad w \Vdash^+ {\lambda \Psi} \quad \text{and} \quad w \Vdash^+ {\mathord{\sim}\lambda \Theta} \\ \quad &\Longleftrightarrow \quad w \Vdash^+ {\lambda \Psi} \wedge {\mathord{\sim}{\lambda \Theta}} \\ \quad &\Longleftrightarrow \quad w \Vdash^+ {\lambda (\Psi \wedge {\mathord{\sim}\Theta})}. \end{aligned}
\end{equation*}
\notag
$$
Next, consider the ‘quantifier’ axioms for strong negation. Let $\Phi_i$ be an axiom of type $\mathrm{SN6}$, that is, of the form
$$
\begin{equation*}
{\mathord{\sim}\forall\,x\ \Psi} \leftrightarrow \exists\,x\ \mathord{\sim}\Psi.
\end{equation*}
\notag
$$
We need to show that for any $w \in W$ and ground $A_w$-substitution $\lambda$,
$$
\begin{equation*}
w \Vdash {\lambda \mathord{\sim}\forall\,x\ \Psi} \quad \Longleftrightarrow \quad w \Vdash {\lambda\, \exists\,x\ \mathord{\sim}\Psi}.
\end{equation*}
\notag
$$
This is done as follows:
$$
\begin{equation*}
\begin{aligned} \, w \vDash \lambda \mathord{\sim}\forall\,x\ \Psi \quad &\Longleftrightarrow \quad w \Vdash^+ {\mathord{\sim}\forall\,x\ {\lambda^x_x \Phi}} \\ \quad &\Longleftrightarrow \quad w \Vdash^- \forall\,x\ {\lambda^x_x \Phi} \\ \quad &\Longleftrightarrow \quad w \Vdash^- {(\lambda^x_x \Phi) (x / \underline{a})} \quad \text{for some} \ a \in A_w \\ \quad &\Longleftrightarrow \quad w \Vdash^+ {\mathord{\sim}(\lambda^x_x \Phi) (x / \underline{a})} \quad \text{for some} \ a \in A_w \\ \quad &\Longleftrightarrow \quad w \Vdash^+ \exists\,x\ {\mathord{\sim}{\lambda^x_x \Phi}} \\ \quad &\Longleftrightarrow \quad w \Vdash^+ \lambda \, \exists\,x\ \mathord{\sim}\Psi, \end{aligned}
\end{equation*}
\notag
$$
where $\lambda^x_x$ denotes $(\lambda \setminus \{(x, {\lambda(x)})\}) \cup \{(x, x)\}$. For $\mathrm{SN7}$ the argument is similar.
If $\Phi_i$ is either an axiom for $\Box$ or a modal interaction axiom, then we can argue as in $\mathsf{BK}$. If $\Phi_i$ is obtained from previous formulae $\Phi_j$ and $\Phi_k$ by $\mathrm{MP}$, $\mathrm{BR1}$ or $\mathrm{BR2}$, then we can argue as in classical predicate logic, and if $\Phi_i$ is obtained from a previous formula $\Phi_j$ by $\mathrm{MB}$ or $\mathrm{MD}$, then we can argue as in $\mathsf{BK}$. The lemma is proved. Theorem 4.4 (soundness of $\mathsf{QBK}$). For any $\Gamma \subseteq \mathrm{Sent}_{\sigma}$ and $\Delta \subseteq \mathrm{Form}_{\sigma}$, Proof. Suppose that $\Gamma \vdash \Delta$. So there are a finite set $\Lambda \subseteq \Gamma$ and $\Phi \in \mathrm{Disj}(\Delta)$ such that $\Lambda \vdash \Phi$. We consider two cases separately.
$\bullet$ Assume that $\Lambda = \varnothing$. Then $\vDash \Phi$ by Lemma 4.3, hence $\Gamma \vDash \Delta$. $\bullet$ Assume that $\Lambda = \{\Psi_0, \dots, \Psi_n\}$. So $\Psi_0 \wedge \dots \wedge \Psi_n \vdash \Phi$, which is equivalent to by Theorem 3.2. Then $\vDash {\Psi_0 \wedge \dots \wedge \Psi_n} \to \Phi$ by Lemma 4.3, which is equivalent to by Theorem 4.2. Hence $\Gamma \vDash \Delta$.The theorem is proved. Let $L$ be a $\mathsf{QBK}$-extension. We denote by $\vDash_{L}$ the relativization of $\vDash$ to the class of frames
$$
\begin{equation*}
\mathcal{K}_L:= {\{\mathcal{W} \mid \mathcal{W} \Vdash \Phi\ \text{for all}\ \Phi \in L\}}.
\end{equation*}
\notag
$$
It is easy to see that the results of the present section remain true if we replace $\vdash$ by $\vdash_L$ and $\vDash$ by $\vDash_L$ in their formulations, where $L$ is an arbitrary $\mathsf{QBK}$-extension.
§ 5. Strong completeness theoremWe call a $\sigma$-theory $\Gamma$ saturated if:
The proof is similar to the case of classical first-order logic. For any set $S$, let
$$
\begin{equation*}
\sigma_S:= \sigma \cup \{\underline{s} \mid s \in S\},
\end{equation*}
\notag
$$
where all the $\underline{s}$ are new constant symbols. Lemma 5.2. Let $\Gamma \subseteq \mathrm{Sent}_{\sigma}$ and $\Delta \subseteq \mathrm{Form}_{\sigma}$ be such that $\Gamma \nvdash \Delta$. Then for each set $S$ of cardinality $|\mathrm{Sent}_{\sigma}|$ there exists a saturated $\sigma_S$-theory $\Gamma' \supseteq \Gamma$ such that $\Gamma' \nvdash \Delta$. The proof is similar to the case of classical first-order logic. Now fix some set $S^{\star}$ of cardinality $|\mathrm{Sent}_{\sigma}|$. It will play the role of a ‘potential’ universe in our canonical model for $\mathsf{QBK}_{\sigma}$. We call $S \subseteq S^{\star}$ admissible if ${|S^{\star} \setminus S|=|S^{\star}|}$. Lemma 5.3. Let $S \subseteq S^{\star}$ be admissible, and let $\Gamma \subseteq \mathrm{Sent}_{\sigma_S}$ and $\Delta \subseteq \mathrm{Form}_{\sigma_S}$ be such that $\Gamma \nvdash \Delta$. Then there exist an admissible set $S' \supseteq S$ and a saturated $\sigma_{S'}$-theory $\Gamma' \supseteq \Gamma$ such that $\Gamma' \nvdash \Delta$. Proof. Since $|S^{\star} \setminus S|=|\mathrm{Sent}_{\sigma}|$, we can find admissible $S' \supseteq S$ such that Moreover, we have $|\mathrm{Sent}_{\sigma}|=|\mathrm{Sent}_{\sigma_S}|$, because $|S|\leqslant|\mathrm{Sent}_{\sigma}|$. It remains to apply Lemma 5.2 for $\sigma := \sigma_S$ and $S := S' \setminus S$.
The lemma is proved. Lemma 5.4. Let $S \subseteq S^{\star}$ be admissible, and let $\Gamma \subseteq \mathrm{Sent}_{\sigma_S}$ and $\Delta \subseteq \mathrm{Form}_{\sigma_S}$ be such that $\Gamma \nvdash \Delta$. Then there exists a saturated $\sigma_{S^{\star}}$-theory $\Gamma' \supseteq \Gamma$ such that $\Gamma' \nvdash \Delta$. To prove the lemma, we just need to apply Lemma 5.2 for $\sigma := \sigma_S$ and $S = S^{\star} \setminus S$. Finally, we are ready to adapt the method of canonical models for $\mathsf{QBK}$ and its extensions. Informally speaking, we need to combine the canonical model for $\mathsf{BK}$ from [11], § 4, and the canonical model for classical quantified modal logic (see [15], § 6) in a natural way. We will sometimes drop the index $\sigma$, but it will always be clear from the context which signature we are talking about. For any set $S$, let
$$
\begin{equation*}
\mathrm{Sat}_S:= \text{the collection of all saturated}\ \sigma_S \text{-theories}.
\end{equation*}
\notag
$$
In addition, for an arbitrary set $\Gamma$ of formulae, we denote by $\mathrm{Const}(\Gamma)$ the collection of all constant symbols that occur in elements of $\Gamma$. Note that for each $\Gamma$ in $\mathrm{Sat}_S$ we have $\mathrm{Const} (\Gamma) = \mathrm{Const}_{\sigma_S}$: obviously, $\mathrm{Const}_{\sigma_{S}}$ includes $\mathrm{Const} (\Gamma)$; on the other hand, for every $c \in \mathrm{Const}_{\sigma_{S}}$ we can easily construct $\Psi_c \in \mathsf{QBK}_{\sigma_S} \cap \mathrm{Sent}_{\sigma_S}$ such that $c$ occurs in $\Psi_c$, and therefore $\mathrm{Const}_{\sigma_{S}} \subseteq \mathrm{Const} (\Gamma)$ (in view of the inclusion $\mathsf{QBK}_{\sigma_S} \subseteq \Gamma$). Next, with any saturated $\sigma_S$-theory $\Gamma$ we associate two $\sigma_S$-structures ${(\mathfrak{A}_{\Gamma}^S)}^+$ and ${(\mathfrak{A}_{\Gamma}^S)}^-$ with the same domain such that all constant symbols of $\sigma_S$ are interpreted as themselves in these structures, and for every atomic $\sigma_S$-sentence $\Phi$,
$$
\begin{equation*}
\begin{aligned} \, {(\mathfrak{A}_{\Gamma}^S)}^+ \Vdash \Phi \quad &:\Longleftrightarrow \quad {\Phi\in \Gamma}, \\ {(\mathfrak{A}_{\Gamma}^S)}^- \Vdash \Phi \quad &:\Longleftrightarrow \quad {\mathord{\sim}\Phi\in \Gamma}. \end{aligned}
\end{equation*}
\notag
$$
We denote by $\mathfrak{A}_{\Gamma}^+$ and $ \mathfrak{A}_{\Gamma}^-$ the $\sigma$-reducts of ${(\mathfrak{A}_{\Gamma}^S)}^+ $ and ${( \mathfrak{A}_{\Gamma}^S)}^-$, respectively. Clearly, every $A_{\Gamma}$-sentence has the form
$$
\begin{equation*}
{\Phi (x_1/\underline{c_1}, \dots, x_n/\underline{c_n})},
\end{equation*}
\notag
$$
where $\{c_1, \dots, c_n\} \subseteq \mathrm{Const} (\Gamma)$; therefore, for convenience we will often identify it with the $\sigma_S$-sentence $\Phi (x_1/c_1, \dots, x_n/c_n)$. Now consider
$$
\begin{equation*}
W^{\mathsf{QBK}}:= \bigcup\, \{\mathrm{Sat}_S \mid S\ \text{is an admissible subset of}\ S^{\star}\}.
\end{equation*}
\notag
$$
By the canonical frame for $\mathsf{QBK}$ we mean a frame $\mathcal{W}^{\mathsf{QBK}} = \langle W^{\mathsf{QBK}}, R^{\mathsf{QBK}} \rangle$, where the relation $R^{\mathsf{QBK}}$ is defined in a standard way:11
$$
\begin{equation*}
R^{\mathsf{QBK}}:= {\{(\Gamma, \Delta) \in W^{\mathsf{QBK}} \times W^{\mathsf{QBK}} \mid \Gamma_{\Box} \subseteq \Delta\}}.
\end{equation*}
\notag
$$
The canonical model for $\mathsf{QBK}$ is
$$
\begin{equation*}
\mathcal{M}^{\mathsf{QBK}}=\langle \mathcal{W}^{\mathsf{QBK}}, {( \mathscr{A}^{\mathsf{QBK}})}^+, {(\mathscr{A}^{\mathsf{QBK}})}^- \rangle,
\end{equation*}
\notag
$$
where
$$
\begin{equation*}
{(\mathscr{A}^{\mathsf{QBK}})}^+ :=\langle \mathfrak{A}_{\Gamma}^+ : \Gamma \in W^{\mathsf{QBK}} \rangle
\end{equation*}
\notag
$$
and
$$
\begin{equation*}
{(\mathscr{A}^{\mathsf{QBK}})}^- :=\langle \mathfrak{A}_{\Gamma}^- : \Gamma \in W^{\mathsf{QBK}} \rangle.
\end{equation*}
\notag
$$
As we will verify shortly, this construction is well defined. Proof. Suppose that $\Gamma R^{\mathsf{QBK}} \Delta$. Let $\sigma_S$ be the signature of $\Gamma$. Clearly, for every $c \in \mathrm{Const}_{\sigma_S}$ we can construct $\Psi_c \in \mathsf{QBK}_{\sigma_S} \cap \mathrm{Sent}_{\sigma_S}$ such that $c$ occurs in $\Psi_c$; then $\Box \Psi_c \in \mathsf{QBK}_{\sigma_S} \cap \mathrm{Sent}_{\sigma_S}$ (by $\mathrm{RN}$), and therefore $\Box \Psi_c \in \Gamma$, hence ${\Psi_c \in \Delta}$. As a consequence, $\mathrm{Const} (\Delta)$ includes $\mathrm{Const} (\Gamma)$, which coincides with $\mathrm{Const}_{\sigma_S}$. Furthermore, the interpretation of the symbols of $\mathrm{Const}_{\sigma}$ is obviously preserved when we pass from $\mathfrak{A}_{\Gamma}^+$ to $\mathfrak{A}_{\Delta}^+$.
The lemma is proved. A key role in the proof of the strong completeness theorem is played by the following result. Lemma 5.6 (canonical model for $\mathsf{QBK}$). For any $\Gamma \!\in\! W^{\mathsf{QBK}}$ and $A_{\Gamma}$-sentence $\Phi$: Proof. This goes by induction on the complexity of $\Phi$.
The case when $\Phi$ is atomic is trivial. Suppose $\Phi = \exists\,x\ \Psi$. Let us look at verification first:
$$
\begin{equation*}
\begin{aligned} \, \mathcal{M}^{\mathsf{QBK}}, \Gamma \Vdash^+ \exists\,x\ \Psi \quad &\Longleftrightarrow \quad {\mathcal{M}^{\mathsf{QBK}}, \Gamma \Vdash^+ \Psi (x/\underline{a})} \quad \text{for some} \ {a \in \mathrm{Const} (\Gamma)}\\ \quad &\Longleftrightarrow \quad {\Psi (x / \underline{a}) \in \Gamma} \quad \text{for some} \ {a \in \mathrm{Const} (\Gamma)}\\ &\Longleftrightarrow \quad {\exists\,x\ \Psi} \in \Gamma. \end{aligned}
\end{equation*}
\notag
$$
Here the last equivalence requires explanation: the direct implication is obtained by using $\mathrm{Q2}$, and the converse employs the existential property. Now let us look at falsification:
$$
\begin{equation*}
\begin{aligned} \, \mathcal{M}^{\mathsf{QBK}}, \Gamma \Vdash^- \exists\,x\ \Psi \quad &\Longleftrightarrow \quad \mathcal{M}^{\mathsf{QBK}}, \Gamma \Vdash^- {\Psi (x / \underline{a})} \quad \text{for all} \ {a \in \mathrm{Const} (\Gamma)} \\ \quad &\Longleftrightarrow \quad {{\mathord{\sim}\Psi (x/\underline{a})} \in \Gamma} \quad \text{for all} \ {a \in \mathrm{Const} (\Gamma)} \\ &\Longleftrightarrow \quad {\forall\,x\ \mathord{\sim}\Psi} \in \Gamma \\ &\Longleftrightarrow \quad {\mathord{\sim}\exists\,x\ \Psi} \in \Gamma. \end{aligned}
\end{equation*}
\notag
$$
In the third equivalence the direct implication is obtained by using $\mathrm{Q1}$, and the converse uses Proposition 5.1 (ii); the last equivalence is guaranteed by $\mathrm{SN7}$.
For $\Phi = \forall\,x\ \Psi$ the argument is similar. The remaining cases are handled as in $\mathsf{BK}$ (see [11], § 4, or [17], § 2), although we need to use Lemma 5.3 instead of the propositional version of the extension lemma. The lemma is proved. Theorem 5.7 (strong completeness of $\mathsf{QBK}$). For any $\Gamma \subseteq \mathrm{Sent}_{\sigma}$ and $\Delta \subseteq \mathrm{Form}_{\sigma}$, Proof. $\Longrightarrow$. See Theorem 4.4.
$\Longleftarrow$. Suppose that $\Gamma \nvdash \Delta$. Fix some admissible $S \subseteq S^{\star}$ of cardinality $\aleph_0$ (thus, $|S|=|\mathrm{Var}|$). Let $\lambda$ be a one-to-one function from $\mathrm{Var}$ onto $\{\underline{s} \mid s \in S\}$. Set It is easy to verify that $\Gamma \nvdash \Delta'$. By Lemma 5.3 (for $\sigma := \sigma_S$ and $S: = S^{\star} \setminus S$) there exists $\Gamma' \in W^{\mathsf{QBK}}$ such that $\Gamma \subseteq \Gamma'$ and $\Gamma' \nvdash \Delta'$. Clearly, $\lambda$ can be viewed as a ground $A_{\Gamma'}$-substitution. So by Lemma 5.6 we have $\mathcal{M}^{\mathsf{QBK}}, \Gamma' \Vdash \Phi$ for all $\Phi \in \Gamma$ and also $\mathcal{M}^{\mathsf{QBK}}, \Gamma' \nVdash \lambda \Psi$ for all $\Psi \in \Delta$. Hence $\Gamma \nvDash \Delta$.The theorem is proved. Let $L$ be a $\mathsf{QBK}$-extension. Then the canonical frame for $L$ and the canonical model for $L$, denoted by $\mathcal{W}^L$ and $\mathcal{M}^L$, respectively, can be defined in the same way as for $\mathsf{QBK}$, but with $\mathrm{Sat}_S$ replaced by
$$
\begin{equation*}
\mathrm{Sat}_S^L:=\{ \Gamma \in \mathrm{Sat}_S \mid L \cap \mathrm{Sent}_{\sigma_S} \subseteq \Gamma \}.
\end{equation*}
\notag
$$
Further, as is easy to understand, the analogue of Lemma 5.6 holds for $L$. However, the analogue of Theorem 5.7 can fail if there are non-canonical models based on $\mathcal{W}^L$ in which formulae from $L$ are refuted, that is, when $\mathcal{W}^L$ does not belong to $\mathcal{K}_L$.
§ 6. Some natural extensionsUsing a variant of the canonical model method from the previous section, it is not difficult to establish the strong completeness of some natural $\mathsf{QBK}$-extensions (cf. [11], § 4). Here we consider two basic types of such extensions:
We start with extensions of type (i). At the axiomatic level, the following axiom schemes correspond to excluding ‘overdefined’ or ‘undefined’: $\mathrm{Exp}$. ${\mathord{\sim} \Phi} \to (\Phi \to \Psi)$; $\mathrm{ExM}$. ${\Phi} \vee {\mathord{\sim} \Phi}$. Here $\mathrm{Exp}$ is an abbreviation for ‘explosion’, and $\mathrm{ExM}$ is for ‘excluded middle’. In fact, it suffices to have $\mathrm{Exp}$ and $\mathrm{ExM}$ for all atomic $\Phi$ and $\Psi$; furthermore, $\mathrm{Exp}$ is equivalent to the scheme ‘$\mathord{\sim} \Phi \to \neg \Phi$’. Let
$$
\begin{equation*}
\mathsf{QBK}^{\circ}:={\mathsf{QBK} + \{\mathrm{ExM}\}} \quad\text{and}\quad \mathsf{QB3K}:={\mathsf{QBK} + \{\mathrm{Exp}\}}.
\end{equation*}
\notag
$$
A $\mathsf{QBK}_{\sigma}$-model $\mathcal{M} = \langle \mathcal{W}, \mathscr{A}^+, \mathscr{A}^- \rangle$ is called:
Theorem 6.1. For any $\Gamma \subseteq \mathrm{Sent}_{\sigma}$ and $\Delta \subseteq \mathrm{Form}_{\sigma}$, Proof. $\Longrightarrow$. Here the argument is similar to the proof of Theorem 4.4. In the present case the verifiability of $\mathrm{Exp}$ in all $\mathsf{QB3K}_{\sigma}$-models is established by easy induction on the complexity of $\Phi$.
$\Longleftarrow$. First we check that $\mathcal{M}^{\mathsf{QB3K}}$ is a $\mathsf{QB3K}_{\sigma}$-model. Let $\Gamma \in W^{\mathsf{QB3K}}$ and $\sigma_S$ be the signature of $\Gamma$. Consider an arbitrary atomic $A_\Gamma$-sentence $\Phi$; it can also be viewed as a $\sigma_S$-sentence. Assume, by way of contradiction, that $\mathfrak{A}_{\Gamma}^+ \Vdash \Phi$ and $\mathfrak{A}_{\Gamma}^- \Vdash \Phi$, that is,
$$
\begin{equation*}
\mathcal{M}^{\mathsf{QB3K}}, \Gamma \Vdash^+ \Phi \quad\text{and}\quad \mathcal{M}^{\mathsf{QB3K}}, \Gamma \Vdash^- \Phi.
\end{equation*}
\notag
$$
By the analogue of Lemma 5.6 for ${\mathsf{QB3K}}$, this is equivalent to $\Phi \in \Gamma$ and $\mathord{\sim} \Phi \in \Gamma$. At the same time we have $\mathord{\sim} \Phi \to (\Phi \to \Psi) \in \Gamma$ for all $\Psi \in \mathrm{Sent}_{\sigma_S}$. Hence we easily obtain $\Gamma = \mathrm{Sent}_{\sigma_S}$, which is a contradiction. Then we can argue as in the proof of Theorem 5.7.
The theorem is proved. Theorem 6.2. For any $\Gamma \subseteq \mathrm{Sent}_{\sigma}$ and $\Delta \subseteq \mathrm{Form}_{\sigma}$, The proof is similar to the proof of Theorem 6.1. Now we turn to extensions of type (ii). For each such extension $L$ we assume that:
$$
\begin{equation*}
\begin{gathered} \, \mathsf{QBD}:={\mathsf{QBK} + \{\mathrm{D}\}}, \qquad \mathsf{QBT}:={\mathsf{QBK} + \{\mathrm{T}\}}, \qquad \mathsf{QBK4}:={\mathsf{QBK} + \{\mathrm{4}\}}, \\ \mathsf{QBD4}:={\mathsf{QBK} + \{\mathrm{D}, \mathrm{4}\}}, \qquad \mathsf{QBS4}:={\mathsf{QBK} + \{\mathrm{T}, \mathrm{4}\}}. \end{gathered}
\end{equation*}
\notag
$$
In addition, for convenience we denote the collection of all these logics by $\mathscr{L}$. Theorem 6.3. Let $L \in \mathscr{L}$. Then for any $\Gamma \subseteq \mathrm{Sent}_{\sigma}$ and $\Delta \subseteq \mathrm{Form}_{\sigma}$, The proof is similar to the proof of Theorem 5.7 (taking the above remarks into account). Of course, the two types of extension can be combined. For example, set Hence ‘undefined’ must be excluded in $\mathsf{QB3S4}$-models (as in $\mathsf{QB3K}$), and the accessibility relations must be preorderings (as in $\mathsf{QBS4}$). We denote by $\vDash_{\mathsf{QBS4}}^3$ the relativization of $\vDash$ to the models of this kind. Clearly, $\mathcal{M}^{\mathsf{QB3S4}}$ turns out to be a $\mathsf{QB3S4}$-model. So $\vdash_{\mathsf{QB3S4}}$ coincides with $\vDash_{\mathsf{QBS4}}^3$, that is, the completeness theorem holds for $\mathsf{QB3S4}$.The logics $\mathsf{QBS4}$ and $\mathsf{QB3S4}$ play an important role in § 8, which is devoted to faithful embeddings of Nelson’s quantified logics. § 7. Constant domain variantConsider the following two variants of the Barcan scheme: $\mathrm{Ba}^{\Box}$. $\forall\,x\ {\Box \Phi} \to {\Box \forall\,x\ \Phi}$; $\mathrm{Ba}^{\Diamond}$. ${\Diamond \exists\,x\ \Phi} \to \exists\,x\ {\Diamond \Phi}$. Note that the scheme corresponding to the converse to $\mathrm{Ba}^{\Box}$ is derivable in $\mathsf{QBK}$:
$$
\begin{equation*}
\begin{array}{ c| l|l} 1&\forall\,x\ \Phi \to \Phi &\text{Q1} \\ 2& \Box \forall\,x\ \Phi \to \Box \Phi &\text{from 1 by MD} \\ 3& \Box \forall\,x\ \Phi \to \forall\,x\ \Box \Phi &\text{from 2 by BR1} \end{array}
\end{equation*}
\notag
$$
The converse scheme for $\mathrm{Ba}^{\Diamond}$ is obtained similarly. Set
$$
\begin{equation*}
\mathsf{QBK}^{\sharp}_{\Box}:=\mathsf{QBK} + \{\mathrm{Ba}^{\Box}\} \quad\text{and}\quad \mathsf{QBK}^{\sharp}_{\Diamond}:=\mathsf{QBK} + \{\mathrm{Ba}^{\Diamond}\}.
\end{equation*}
\notag
$$
Although the proof of the proposition below is exactly similar to the case of classical quantified modal logic, we provide it for expository purposes. Proof. We show that $\mathrm{Ba}^{\Diamond}$ is derivable in $\mathsf{QBK}^{\sharp}_{\Box}$:
$$
\begin{equation*}
\begin{array}{ c| l|l} 1&\forall\,x\ \Box \neg \Phi \to \Box \forall\,x\ \neg \Phi &\text{Ba}^{\Box} \\ 2&\neg \Box \forall\,x\ \neg \Phi \to \neg \forall\,x\ \Box \neg \Phi &\text{from 1} \\ 3&\Diamond \neg \forall\,x\ \neg \Phi \leftrightarrow \neg \Box \forall\,x\ \neg \Phi &\text{M1} \\ 4&\exists\,x\ \Phi \leftrightarrow \neg \forall\,x\ \neg \Phi &\text{classical logic} \\ 5&\Diamond \exists\,x\ \Phi \leftrightarrow \Diamond \neg \forall\,x\ \neg \Phi &\text{from 4 by PR} \\ 6&\neg \forall\,x\ \Box \neg \Phi \leftrightarrow \exists\,x\ \neg \Box \neg \Phi &\text{classical logic} \\ 7&\neg \Box \neg \Phi \leftrightarrow \Diamond \neg \neg \Phi &\text{M1} \\ 8&\neg \neg \Phi \leftrightarrow \Phi &\text{classical logic} \\ 9&\Diamond \neg \neg \Phi \leftrightarrow \Diamond \Phi &\text{from 8 by PR} \\ 10&\neg \Box \neg \Phi \leftrightarrow \Diamond \Phi &\text{from 7, 9} \\ 11&\exists\,x\ \neg \Box \neg \Phi \leftrightarrow \exists\,x\ \Diamond \Phi &\text{from 10 by PR} \\ 12&\Diamond \exists\,x\ \Phi \to \exists\,x\ \Diamond \Phi &\text{from 5, 3, 2, 6, 11} \end{array}
\end{equation*}
\notag
$$
In a similar way one can show that $\mathrm{Ba}^{\Box}$ is derivable in $\mathsf{QBK}^{\sharp}_{\Diamond}$. The proposition is proved. In what follows we will write $\mathsf{QBK}^{\sharp}$ instead of $\mathsf{QBK}^{\sharp}_{\Box}$ and $\mathsf{QBK}^{\sharp}_{\Diamond}$, and also $\vdash^{\sharp}$ instead of $\vdash_{\mathsf{QBK}^{\sharp}}$. Furthermore, we restrict ourselves to at most countable signatures, since dealing with uncountable signatures gives rise to some problems even for the variant of $\mathsf{QK}$ with constant domains; cf. Lemma 7.1.2 in [15], where the proof makes significant use of the countability of the signature. We call a $\mathsf{QBK}_{\sigma}$-model $\mathcal{M}=\langle \mathcal{W}, \mathscr{A}^+, \mathscr{A}^- \rangle$ a $\mathsf{QBK}^{\sharp}_{\sigma}$-model if $A_u = A_v$ for all $u, v \in W$. In other words, $\mathsf{QBK}^{\sharp}_{\sigma}$-models are $\mathsf{QBK}_{\sigma}$-models with constant domains. In fact, the Barcan scheme only guarantees that for any $u, v \in W$, However, this is not crucial, since for a given world $u \in W$ one can always pass to the generated submodel whose set of worlds is $R(u)$. We denote by $\vDash^{\sharp}$ the relativization of $\vDash$ to the class of all $\mathsf{QBK}^{\sharp}_{\sigma}$-models.Theorem 7.2 (soundness of ${\mathsf{QBK}}^{\sharp}_{\sigma}$). For any $\Gamma \subseteq \mathrm{Sent}_{\sigma}$ and $\Delta \subseteq \mathrm{Form}_{\sigma}$, The proof is similar to the proof of Theorem 4.4. In the present case the verifiability of $\mathrm{Ba}^{\Box}$ (or $\mathrm{Ba}^{\Diamond}$) in all $\mathsf{QBK}^{\sharp}_{\sigma}$-models is established as in classical quantified modal logic. As in § 5, fix some set $S^{\star}$ of cardinality $|\mathrm{Sent}_{\sigma}|$. For brevity we write $\sigma_{\star}$ instead of $\sigma_{S^{\star}}$. Set
$$
\begin{equation*}
W^{\sharp}:= \text{the collection of all saturated}\ \sigma_{\star} \text{-theories}.
\end{equation*}
\notag
$$
Obviously, $\mathrm{Const} (\Gamma) = \mathrm{Const}_{\sigma_{\star}}$ for all $\Gamma \in W^{\sharp}$. By the canonical frame for $\mathsf{QBK}^{\sharp}$ and the canonical model for $\mathsf{QBK}^{\sharp}$ we mean
$$
\begin{equation*}
\mathcal{W}^{\sharp}=\langle W^{\sharp}, R^{\sharp} \rangle \quad\text{and}\quad \mathcal{M}^{\sharp}=\langle \mathcal{W}^{\sharp}, {(\mathscr{A}^{\sharp})}^+, {(\mathscr{A}^{\sharp})}^- \rangle,
\end{equation*}
\notag
$$
where the components $R^{\sharp}$, $(\mathscr{A}^{\sharp})^+$ and $(\mathscr{A}^{\sharp})^-$ are defined in the same way as $R^{\mathsf{QBK}}$, $(\mathscr{A}^{\mathsf{QBK}})^+$ and $(\mathscr{A}^{\mathsf{QBK}})^-$, but with $W^{\mathsf{QBK}}$ replaced by $W^{\sharp}$. Lemma 7.3. For any $\Gamma \in W^{\sharp}$ and $\Phi \in \mathrm{Sent}_{\sigma^{\star}}$: The proof is exactly similar to the case of classical quantified modal logic; see, for example, [15], Lemma 7.1.2. From this we easily obtain the following result. Lemma 7.4 (canonical model for $\mathsf{QBK}^{\sharp}$). For any $\Gamma \in W^{\sharp}$ and $A_{\Gamma}$-sentence $\Phi$: Proof. This goes by induction on the complexity of $\Phi$.
Of course, since all worlds deal with the same domain $\mathrm{Const}_{\sigma_{\star}}$, we cannot use Lemma 5.3. However, the cases when $\Phi$ does not begin with $\Box$ or $\Diamond$ are handled as in the proof of Lemma 5.6 (because they do not require Lemma 5.3). Suppose $\Phi = \Box \Psi$. Obviously, the equivalence for $\Vdash^+$ follows from Lemma 7.3 (and the inductive hypothesis). Let us now look at falsification:
$$
\begin{equation*}
\begin{aligned} \, \mathcal{M}^{\sharp}, \Gamma \Vdash^- {\Box \Psi} \quad \Longleftrightarrow& \quad \text{there exists} \ \Delta \in W^\sharp \ \text{such that}\ \Gamma_{\Box} \subseteq \Delta \text{ and } \mathcal{M}^{\sharp}, \Delta \Vdash^- \Psi \\ \quad\Longleftrightarrow& \quad \text{there exists} \ \Delta \in W^\sharp \ \text{such that}\ \Gamma_{\Box} \subseteq \Delta \text{ and } \mathord{\sim} \Psi \in \Delta \\ \quad \Longleftrightarrow& \quad {\Diamond \mathord{\sim} \Psi}\in \Gamma \\ \quad \Longleftrightarrow& \quad {\mathord{\sim} {\Box \Psi}}\in \Gamma. \end{aligned}
\end{equation*}
\notag
$$
Here the third equivalence is guaranteed by Lemma 7.3, and the last one follows from the fact that $\Diamond {\mathord{\sim} \Psi} \Leftrightarrow \mathord{\sim} \Box\Psi$ is derivable in $\mathsf{QBK}$:
$$
\begin{equation*}
\begin{array}{ c| l|l} 1&{\Diamond \mathord{\sim} \Psi} \Leftrightarrow {\mathord{\sim} {\Box {\mathord{\sim} \mathord{\sim} \Psi}}} &\text{M4} \\ 2&{\mathord{\sim} \mathord{\sim} \Psi} \Leftrightarrow \Psi &\text{SN1}^{\ast} \\ 3&{\mathord{\sim} {\Box {\mathord{\sim} \mathord{\sim} \Psi}}} \Leftrightarrow {\mathord{\sim} {\Box \Psi}} &\text{from 2 by WR} \\ 4&{\Diamond \mathord{\sim} \Psi} \Leftrightarrow {\mathord{\sim} {\Box \Psi}} &\text{from 1, 3} \end{array}
\end{equation*}
\notag
$$
Similarly for $\Phi = \Diamond \Psi$. The lemma is proved. Theorem 7.5 (strong completeness of $\mathsf{QBK}^{\sharp}$). For any $\Gamma \subseteq \mathrm{Sent}_{\sigma}$ and $\Delta \subseteq \mathrm{Form}_{\sigma}$, Proof. $\Longrightarrow$. See Theorem 7.2.
$\Longleftarrow$. Suppose that $\Gamma \nvdash^{\sharp} \Delta$. Fix some admissible $S \subseteq S^{\star}$ of cardinality $\aleph_0$. Let $\lambda$ be a one-to-one function from $\mathrm{Var}$ onto $\{\underline{s} \mid s \in S\}$. Set Clearly, $\Gamma \nvdash^{\sharp} \Delta'$. By Lemma 5.4 there exists $\Gamma' \in W^{\sharp}$ such that $\Gamma \subseteq \Gamma'$ and $\Gamma' \nvdash^{\sharp} \Delta'$. Obviously, $\lambda$ can be viewed as a ground $A_{\Gamma'}$-substitution. So by Lemma 7.4 we have $\mathcal{M}^{\sharp}, \Gamma' \Vdash \Phi$ for all $\Phi \in \Gamma$ and also $\mathcal{M}^{\sharp}, \Gamma' \nVdash \lambda \Psi$ for all $\Psi \in \Delta$. Hence $\Gamma \nvDash^{\sharp} \Delta$.The theorem is proved. Of course, by analogy with $\mathsf{QBK}$ we can consider various natural extensions of $\mathsf{QBK}^{\sharp}$. In particular, as is easily verified, for extensions obtained from logics in $\mathscr{L}$, $\mathsf{QB3K}$ or $\mathsf{QBK}^{\circ}$ by adding $\mathrm{Ba}^{\Box}$, the corresponding strong completeness theorems hold. § 8. Faithful embedding of quantified Nelson’s logicsLet $\mathsf{QN4}$ be the quantified version of Nelson’s constructive logic and $\mathsf{QN3}$ be its extension obtained by excluding ‘overdefined’, that is, by adding the relativization of the scheme $\mathrm{Exp}$ to the language of $\mathsf{QN4}$; see [4] and [6], and also [19] and [20]. Recall that syntactically, the language of $\mathsf{QN4}$ is simply the non-modal fragment of the language of $\mathsf{QBK}$. However, there are fundamental differences between $\mathsf{QN4}$ and $\mathsf{QBK}$ at the semantic level: $\to$ and $\forall$ are verified in $\mathsf{QN4}$ by analogy with intuitionistic logic, and not by analogy with classical logic as in $\mathsf{QBK}$. Intuitively, $\mathsf{QN4}$ enriches quantified intuitionistic logic, $\mathsf{QInt}$, by adding strong negation. Below, by constructive $\sigma$-formulae we mean $\sigma$-formulae in the language of $\mathsf{QN4}$, that is, those containing no occurrences of $\Box$ and $\Diamond$. Negation normal forms in the language of $\mathsf{QN4}$ are defined in the same way as in $\mathsf{QBK}$. It is well known that a result similar to Theorem 3.8 holds for $\mathsf{QN4}$, but with weak equivalence instead of strong equivalence. Theorem 8.1 (see, for example, [20]). For every constructive $\sigma$-formula $\Phi$ there exists an n.n.f. $\overline{\Phi}$ such that $\Phi \leftrightarrow \overline{\Phi} \in \mathsf{QN4}_{\sigma}$. Moreover, there is an algorithm that, given any constructive $\sigma$-formula $\Phi$, constructs a suitable n.n.f. $\overline{\Phi}$.12 Next, we define a translation $\tau$ that associates with each n.n.f. in the language of $\mathsf{QN4}_{\sigma}$ a formula in the language of $\mathsf{QBK}_{\sigma}$:
$$
\begin{equation*}
\begin{aligned} \, \tau (P (t_1, \dots, t_n))&:= \Box P (t_1, \dots, t_n); \\ \tau (\mathord{\sim} P (t_1, \dots, t_n))&:= \mathord{\sim} \Diamond P (t_1, \dots, t_n); \\ \tau (\Phi \wedge \Psi)&:= \tau (\Phi) \wedge \tau (\Psi); \\ \tau (\Phi \vee \Psi)&:= \tau (\Phi) \vee \tau (\Psi); \\ \tau (\Phi \to \Psi)&:= \Box (\tau (\Phi) \to \tau (\Psi)); \\ \tau (\bot)&:= \bot; \\ \tau (\mathord{\sim} \bot)&:= \bot \to \bot; \\ \tau (\forall\,x\ \Phi)&:= \Box \forall\,x\ {\tau (\Phi)}; \\ \tau (\exists\,x\ \Phi)&:= \exists\,x\ {\tau (\Phi)}. \end{aligned}
\end{equation*}
\notag
$$
The mapping $\tau$ can naturally be extended to the set of all constructive $\sigma$-formulae: if $\Phi$ is not an n.n.f., then take Formally, we should write $\tau_{\sigma}$ instead of $\tau$, but it will always be clear from the context which signature we are talking about. Clearly, the restriction of $\tau$ to formulae not containing $\mathord{\sim}$ coincides with the Gödel–McKinsey–Tarski translation, which faithfully embeds $\mathsf{QInt}$ into the modal logic $\mathsf{QS4}$. Furthermore, $\tau$ can be viewed as a (quantified) extension of the propositional translation proposed earlier in [11], § 7.1. Remark 8.2. If we fix the usual algorithm for reducing constructive $\sigma$-formulae to n.n.f., then the mapping $\tau$ can be described as follows: We say that a $\mathsf{QBK}_{\sigma}$-model $\mathcal{M} = \langle \mathcal{W}, \mathscr{A}^+, \mathscr{A}^- \rangle$ is a $\mathsf{QN4}_{\sigma}$-model if $R$ is a preordering on $W$ and for any $u, v \in W$,
$$
\begin{equation*}
u \mathbin{R} v \quad \Longrightarrow \quad {P^{\mathfrak{A}^{\pm}_{u}} \subseteq P^{\mathfrak{A}^{\pm}_{v}}} \quad \text{for all} \ {P \in \mathrm{Pred}_{\sigma}}.
\end{equation*}
\notag
$$
Further, a $\mathsf{QN4}_{\sigma}$-model $\mathcal{M}$ is called a $\mathsf{QN3}_{\sigma}$-model if for every $w \in W$,
$$
\begin{equation*}
P^{\mathfrak{A}^{+}_{w}} \cap P^{\mathfrak{A}^{-}_{w}}=\varnothing \quad \text{for all} \ {P \in \mathrm{Pred}_{\sigma}}.
\end{equation*}
\notag
$$
The verifiability and falsifiability relations for $\mathsf{QN4}_{\sigma}$ are defined in the natural way:
$$
\begin{equation*}
\begin{aligned} \, \mathcal{M}, w \Vdash^+ {P (t_1, \dots, t_n)} \quad\Longleftrightarrow& \quad \mathfrak{A}^+_{w} \Vdash {P (t_1, \dots, t_n)}; \\ \mathcal{M}, w \Vdash^- {P (t_1, \dots,t_n)} \quad\Longleftrightarrow& \quad \mathfrak{A}^-_{w} \Vdash {P (t_1, \dots,t_n)}; \\ \mathcal{M},w \Vdash^+ \Phi \wedge \Psi \quad\Longleftrightarrow& \quad \mathcal{M}, w \Vdash^+ \Phi \quad \text{and} \quad \mathcal{M}, w \Vdash^+ \Psi; \\ \mathcal{M},w \Vdash^- \Phi \wedge \Psi \quad\Longleftrightarrow& \quad \mathcal{M},w \Vdash^- \Phi \quad \text{or} \quad \mathcal{M}, w \Vdash^- \Psi; \\ \mathcal{M}, w \Vdash^+ \Phi \vee \Psi \quad\Longleftrightarrow& \quad \mathcal{M}, w \Vdash^+ \Phi \quad \text{or} \quad \mathcal{M}, w \Vdash^+ \Psi; \\ \mathcal{M}, w \Vdash^- \Phi \vee \Psi \quad\Longleftrightarrow& \quad \mathcal{M}, w \Vdash^- \Phi \quad \text{and} \quad \mathcal{M}, w \Vdash^- \Psi; \\ \mathcal{M},w \Vdash^+ \Phi \to \Psi \quad\Longleftrightarrow& \quad \text{for every} \ {u \in R (w)}, \text{ if} \ \mathcal{M}, u \Vdash^+ \Phi, \\ &\quad\text{then} \ \mathcal{M},u \Vdash^+ \Psi; \\ \mathcal{M},w \Vdash^- \Phi \to \Psi \quad\Longleftrightarrow& \quad \mathcal{M}, w \Vdash^+ \Phi \quad \text{and} \quad \mathcal{M}, w \Vdash^- \Psi; \\ \mathcal{M}, w \Vdash^+ \bot \quad\Longleftrightarrow& \quad 0 \ne 0; \\ \mathcal{M}, w \Vdash^- \bot \quad\Longleftrightarrow& \quad 0 = 0; \\ \mathcal{M}, w \Vdash^+ \mathord{\sim}\Phi \quad\Longleftrightarrow& \quad \mathcal{M}, w \Vdash^- \Phi; \\ \mathcal{M}, w \Vdash^- \mathord{\sim}\Phi \quad\Longleftrightarrow& \quad \mathcal{M}, w \Vdash^+ \Phi; \\ \mathcal{M}, w \Vdash^+ \forall\,x\ \Phi \quad\Longleftrightarrow& \quad {\mathcal{M}, u \Vdash^+ \Phi (x / \underline{a})} \quad \text{for all} \ {u \in R (w)} \ \text{and} \ {a \in A_u}; \\ \mathcal{M},w \Vdash^- \forall\,x\ \Phi \quad\Longleftrightarrow& \quad {\mathcal{M}, w \Vdash^- \Phi (x / \underline{a})} \quad \text{for some} \ {a \in A_w}; \\ \mathcal{M},w \Vdash^+ \exists\,x\ \Phi \quad\Longleftrightarrow& \quad {\mathcal{M}, w \Vdash^+ \Phi (x / \underline{a})} \quad \text{for some} \ {a \in A_w}; \\ \mathcal{M},w \Vdash^- \exists\,x\ \Phi \quad\Longleftrightarrow& \quad {\mathcal{M}, u \Vdash^- \Phi (x / \underline{a})} \quad \text{for all} \ {u \in R (w)} \ \text{and} \ {a \in A_u}. \end{aligned}
\end{equation*}
\notag
$$
Here, instead of $\Vdash^+$ and $\Vdash^-$, it would be more accurate to write $\Vdash^+_{\mathsf{QN4}}$ and $\Vdash^-_{\mathsf{QN4}}$, but in what follows it will always be clear from the context what kind of logic we are talking about. Note that $\mathcal{M}$ is a $\mathsf{QN3}_{\sigma}$-model if and only if there are no $w \in W$ and no atomic $A_w$-sentence $\Phi$ such that $\mathfrak{A}^+_w \Vdash \Phi$ and $\mathfrak{A}^-_w \Vdash \Phi$; cf. the definition of $\mathsf{QB3K}_{\sigma}$-model in § 6. The semantical consequence relations for $\mathsf{QN4}$ and $\mathsf{QN3}$ are defined by analogy with $\vDash_\mathsf{QBK}$ and $\vDash_\mathsf{QBK}^3$; we denote them by $\vDash_{\mathsf{QN4}}$ and $\vDash_{\mathsf{QN4}}^3$, respectively. Theorem 8.3 (see [20] and [19]). For any $\Gamma \subseteq \mathrm{Sent}_{\sigma}$ and $\Delta \subseteq \mathrm{Form}_{\sigma}$: where $\vdash_{\mathsf{QN4}}$ and $\vdash_{\mathsf{QN3}}$ denote the derivability relations for $\mathsf{QN4}$ and $\mathsf{QN3}$, respectively. Let $\mathcal{M} = \langle \mathcal{W}, \mathscr{A}^+, \mathscr{A}^- \rangle$ be an arbitrary $\mathsf{QBS4}_{\sigma}$-model, that is, a $\mathsf{QBK}_{\sigma}$-model in which the accessibility relation is reflexive and transitive. We associate with it the triple
$$
\begin{equation*}
\mathcal{M}':= \langle \mathcal{W}, (\mathscr{A}^+)', (\mathscr{A}^-)' \rangle
\end{equation*}
\notag
$$
such that for any $w \in W$ and atomic $A_w$-sentence $\Phi$:
$$
\begin{equation*}
\begin{aligned} \, {(\mathfrak{A}_w^+)}' \Vdash \Phi \quad&:\Longleftrightarrow \quad \mathcal{M}, w \Vdash^+ \Box \Phi, \\ (\mathfrak{A}_w^-)' \Vdash \Phi \quad&:\Longleftrightarrow \quad \mathcal{M}, w \Vdash^- \Diamond \Phi. \end{aligned}
\end{equation*}
\notag
$$
Here we set $(A_w)' = A_w$ for all $w \in W$. It is easy to understand that $\mathcal{M}'$ turns out to be a $\mathsf{QN4}_{\sigma}$-model. Moreover, if $\mathcal{M}$ is a $\mathsf{QB3S4}_{\sigma}$-model, then $\mathcal{M}'$ is a $\mathsf{QN3}_{\sigma}$-model. The following statement is similar to Lemma 14 in [11]. Lemma 8.4. Let $\mathcal{M} = \langle \mathcal{W}, \mathscr{A}^+, \mathscr{A}^- \rangle$ be a $\mathsf{QBS4_{\sigma}}$-model. Then for any $w \in W$ and constructive $A_w$-sentence $\Phi$, Proof. By Theorem 8.1 we can assume that $\Phi$ is an n.n.f. Then the proof goes by induction on the complexity of $\Phi$.
The case when $\Phi$ is atomic is trivial. The case when $\Phi = \mathord{\sim} P (t_1, \dots, t_n)$ is slightly more complicated:
$$
\begin{equation*}
\begin{aligned} \, \mathcal{M}', w \Vdash^+ \mathord{\sim} P (t_1, \dots, t_n) \quad&\Longleftrightarrow \quad \mathcal{M}', w \Vdash^- P (t_1, \dots, t_n) \\ \quad&\Longleftrightarrow \quad {(\mathfrak{A}_w^-)}' \Vdash P (t_1, \dots, t_n) \\ \quad&\Longleftrightarrow \quad \mathcal{M}, w \Vdash^- \Diamond P (t_1, \dots, t_n) \\ \quad&\Longleftrightarrow \quad \mathcal{M}, w \Vdash^+ \mathord{\sim} \Diamond P (t_1, \dots, t_n) \\ \quad&\Longleftrightarrow \quad \mathcal{M}, w \Vdash^+ \tau (\mathord{\sim} P (t_1, \dots, t_n)). \end{aligned}
\end{equation*}
\notag
$$
Suppose $\Phi = \forall\,x\ \Psi$. Then
$$
\begin{equation*}
\begin{aligned} \, \mathcal{M}', w \Vdash^+ \forall\,x\ \Psi \quad&\Longleftrightarrow \quad \mathcal{M}', u \Vdash^+ {\Psi (x / \underline{a})} \quad \text{for all} \ u \in R (w) \ \text{and} \ a \in A_u \\ \quad&\Longleftrightarrow \quad \mathcal{M}, u \Vdash^+ {\tau (\Psi (x / \underline{a}))} \quad \text{for all} \ u \in R (w) \ \text{and} \ a \in A_u \\ \quad&\Longleftrightarrow \quad \mathcal{M}, u \Vdash^+ \tau (\Psi) (x / \underline{a}) \quad \text{for all} \ u \in R (w) \ \text{and} \ a \in A_u \\ \quad&\Longleftrightarrow \quad \mathcal{M}, u \Vdash^+ \forall\,x\ \tau(\Psi) \quad \text{for all} \ u \in R (w) \\ \quad&\Longleftrightarrow \quad \mathcal{M}, w \Vdash^+ \Box \forall\,x\ \tau(\Psi) \\ \quad&\Longleftrightarrow \quad \mathcal{M}, w \Vdash^+ \tau (\Phi). \end{aligned}
\end{equation*}
\notag
$$
Suppose $\Phi = \exists\,x\ \Psi$. Then
$$
\begin{equation*}
\begin{aligned} \, \mathcal{M}', w \Vdash^+ \exists\,x\ \Psi \quad&\Longleftrightarrow \quad \mathcal{M}', w \Vdash^+ \Psi (x / \underline{a}) \quad \text{for some} \ a \in A_w \\ \quad&\Longleftrightarrow \quad \mathcal{M}', w \Vdash^+ \tau (\Psi (x / \underline{a})) \quad \text{for some} \ a \in A_w \\ \quad&\Longleftrightarrow \quad \mathcal{M}', w \Vdash^+ \tau (\Psi) (x / \underline{a}) \quad \text{for some} \ a \in A_w \\ \quad&\Longleftrightarrow \quad \mathcal{M}, w \Vdash^+ \exists\,x\ \tau(\Psi) \\ \quad&\Longleftrightarrow \quad \mathcal{M}, w \Vdash^+ {\tau (\Phi)}. \end{aligned}
\end{equation*}
\notag
$$
The remaining cases are handled as in $\mathsf{BK}$; see [11], § 7. The lemma is proved. Remark 8.5. In the formulation of Lemma 8.4 we cannot replace $\Vdash^+$ by $\Vdash^-$. Indeed, suppose $\Phi = \Psi \to \Theta$. Then, as is easily verified, but the converse implication can in general fail. A similar problem arises for ${\Phi =\forall\,x\ \Psi}$. From this one easily obtains the following. Theorem 8.6. For every constructive $\sigma$-sentence $\Phi$, In other words, $\tau$ faithfully embeds $\mathsf{QN4}$ into $\mathsf{QBS4}$. Proof. In view of the completeness theorems for $\mathsf{QN4}$ and $\mathsf{QBS4}$, we need to show that
$$
\begin{equation*}
\vDash_{\mathsf{QN4}} \Phi \quad \Longleftrightarrow \quad \vDash_{\mathsf{QBS4}} {\tau (\Phi)}
\end{equation*}
\notag
$$
(see Theorems 8.3 and 6.3, respectively).
$\Longrightarrow$. Suppose that $\vDash_{\mathsf{QN4}} \Phi$. Consider an arbitrary $\mathsf{QBS4}_{\sigma}$-model $\mathcal{M}$ and some $w \in W$. Since $\mathcal{M}', w \Vdash^+ \Phi$, we have $\mathcal{M}, w \Vdash^+ \tau (\Phi)$ by Lemma 8.4. Hence $\vDash_{\mathsf{QBS4}} \tau(\Phi)$. $\Longleftarrow$. Suppose that $\vDash_{\mathsf{QBS4}} \tau(\Phi)$. Consider an arbitrary $\mathsf{QN4}_{\sigma}$-model $\mathcal{M}$ and some $w \in W$. Obviously, $\mathcal{M}$ can be thought of as a $\mathsf{QBS4}_\sigma$-model; in this case $\mathcal{M}'$ coincides with $\mathcal{M}$. So, since $\mathcal{M}, w \Vdash^+ \tau (\Phi)$, we have $\mathcal{M}, w \Vdash^+ \Phi$ by Lemma 8.4. Hence $\vDash_{\mathsf{QN4}} \Phi$. The theorem is proved. Furthermore, we have the following result. Theorem 8.7. For every constructive $\sigma$-sentence $\Phi$, In other words, $\tau$ faithfully embeds $\mathsf{QN3}$ into $\mathsf{QB3S4}$. The proof follows from Theorem 8.6, taking into account the completeness theorems for $\mathsf{QN4}$, $\mathsf{QBS4}$, $\mathsf{QN3}$ and $\mathsf{QB3S4}$. Remark 8.8. Theorems 8.6 and 8.7 can be reformulated in terms of derivability or semantical consequence relations (with nonempty sets of hypotheses). In fact, such formulations turn out to be equivalent to the original ones in view of the strong completeness theorems for $\mathsf{QN4}$, $\mathsf{QBS4}$, $\mathsf{QN3}$ and $\mathsf{QB3S4}$. A result similar to Theorem 8.7 holds for the logic $\mathsf{QN4}^{\circ}$, which is obtained from $\mathsf{QN4}$ by excluding ‘undefined’, that is, by adding the relativization of the scheme $\mathrm{ExM}$ to the language of $\mathsf{QN4}$. More precisely, set
$$
\begin{equation*}
\mathsf{QBS4}^{\circ}:=\mathsf{QBS4} + \{\mathrm{ExM}\}.
\end{equation*}
\notag
$$
Then $\tau$ embeds $\mathsf{QN4}^{\circ}$ into $\mathsf{QBS4}^{\circ}$. In this case, formally, we need the strong completeness theorem for $\mathsf{QN4}^{\circ}$, which can be proved by analogy with Theorem 6.2, using the canonical model for $\mathsf{QN4}$. Finally, all the results of the present section are easily relativized to the case of constant domains. Here the role of the Barcan scheme for $\mathsf{QN4}$-extensions is played by $\mathrm{CD}$. $\forall\,x\ (\Phi \vee \Psi) \to \Phi \vee \forall\,x\ \Psi$, where $x$ does not occur free in $\Phi$. However, this kind of relativization can be criticized from the constructive point of view, since $\mathrm{CD}$ is refuted in Kleene’s realizability semantics (let alone Nelson’s semantics). § 9. Interpolation propertiesIt is known that some extensions of classical quantified modal logic, $\mathsf{QK}$, have Craig’s interpolation property: see, for example, [21]. In this section, using the technique of § 2 in [13] we are going to show how interpolation results for $\mathsf{QK}$-extensions can be transferred to $\mathsf{QBK}$-extensions. For each $\sigma$-formula $\Phi$ set
$$
\begin{equation*}
\mathrm{O} (\Phi):= \{\varepsilon \in \sigma \mid\varepsilon\ \text{occurs in}\ \Phi\} \cup \mathrm{FV}(\Phi).
\end{equation*}
\notag
$$
Let $L$ be a $\mathsf{QK}$-extension. We say that $L$ has Craig’s interpolation property, or $\mathrm{CIP}$ for short, if for any signature $\sigma$ and $\Phi \to \Psi \in L_{\sigma}$ there exists $\Theta \in \mathrm{Form}_{\sigma}$ such that
$$
\begin{equation*}
\{\Phi \to \Theta, \Theta \to \Psi\}\subseteq L \quad\text{and}\quad \mathrm{O} (\Theta)\subseteq \mathrm{O} (\Phi) \cap \mathrm{O} (\Psi).
\end{equation*}
\notag
$$
Here $\Theta$ is called a Craig interpolant for $\Phi \to \Psi$ in $L$. This terminology will also be used for $\mathsf{QBK}$-extensions. Remark 9.1. In fact, the requirement that $\mathrm{O} (\Phi)$ includes $\mathrm{FV}(\Phi)$ is not crucial since, if necessary, all free variables of $\Phi$ can be replaced by new constant symbols. In addition, a more subtle version of $\mathrm{CIP}$ for $\mathsf{QBK}$-extensions is worth discussing; cf. [16], § 4. By Theorem 3.8 we can restrict ourselves to n.n.f. Given a $\sigma$-n.n.f. $\Phi$ and $P \in \mathrm{Pred}_{\sigma}$, we call an occurrence of $P$ in $\Phi$ positive if it is not inside the scope of $\mathord{\sim}$, and negative otherwise. For each $\sigma$-n.n.f. $\Phi$ we set
$$
\begin{equation*}
\begin{gathered} \, \mathrm{D} (\Phi):= \{c \in \mathrm{Const}_{\sigma} \mid c\ \text{occurs in}\ \Phi\} \cup \mathrm{FV} (\Phi), \\ \mathrm{P}^+ (\Phi):= \{P \in \mathrm{Pred}_{\sigma} \mid P\ \text{occurs positively in}\ \Phi\} \end{gathered}
\end{equation*}
\notag
$$
and
$$
\begin{equation*}
\mathrm{P}^- (\Phi):= \{P \in \mathrm{Pred}_{\sigma} \mid P\ \text{occurs negatively in}\ \Phi\}.
\end{equation*}
\notag
$$
Let $L$ be a $\mathsf{QBK}$-extension. We say that $L$ has the strong interpolation property, or $\mathrm{SIP}$ for short, if for any signature $\sigma$ and any $\sigma$-n.n.f. $\Phi \to \Psi$ in $L$ there exists a $\sigma$-n.n.f. $\Theta$ such that
$$
\begin{equation*}
\begin{gathered} \, \{\Phi \to \Theta, \Theta \to \Psi\}\subseteq L, \qquad \mathrm{D} (\Theta)\subseteq \mathrm{D} (\Phi) \cap \mathrm{D} (\Psi), \\ \mathrm{P}^+ (\Theta)\subseteq \mathrm{P}^+ (\Phi) \cap \mathrm{P}^+ (\Psi)\quad\text{and} \quad \mathrm{P}^- (\Theta)\subseteq \mathrm{P}^- (\Phi) \cap \mathrm{P}^- (\Psi). \end{gathered}
\end{equation*}
\notag
$$
Here $\Theta$ is called a strong interpolant for $\Phi \to \Psi$ in $L$. It is easy to see that $\mathrm{SIP}$ is stronger than $\mathrm{CIP}$: if $L$ has $\mathrm{SIP}$, then it has $\mathrm{CIP}$. Obviously, to each $\mathsf{QBK}$-extension $L$ in $\mathscr{L}$ (from the formulation of Theorem 6.3) there corresponds the $\mathsf{QK}$-extension $\underline{L}$ (without $\mathsf{B}$ in the name). It is known that all such extensions $\underline{L}$ have $\mathrm{CIP}$: see [21]. Our next aim is to obtain $\mathrm{SIP}$ for all logics in $\mathscr{L}$. For any signature $\sigma$ set
$$
\begin{equation*}
\underline{\sigma}:= \sigma \cup \{\underline{P} \mid P \in \mathrm{Pred}_{\sigma}\},
\end{equation*}
\notag
$$
where $\underline{P}$ is a new predicate symbol of the same arity as $P$. Consider an arbitrary $L$ in $\mathscr{L}$ and any signature $\sigma$. With each $L_{\sigma}$-model $\mathcal{M}$ we associate the $\underline{L}_{\underline{\sigma}}$-model
$$
\begin{equation*}
\underline{\mathcal{M}}:=\langle \mathcal{W}, \underline{\mathscr{A}} \,\rangle,
\end{equation*}
\notag
$$
where $\underline{\mathscr{A}}$ denotes the family $\langle \underline{\mathfrak{A}}_w : w \in W \rangle$ such that for every $w \in W$:
Further, we define a translation $\rho$ from the set of all $\sigma$-n.n.f. to the set of all $\underline{\sigma}$-formulae without strong negation as follows (cf. [13], § 2, and [16], § 4):
$$
\begin{equation*}
\begin{aligned} \, \rho (P (t_1, \dots, t_n)) &:= P (t_1, \dots, t_n), \\ \rho (\mathord{\sim} P (t_1, \dots, t_n)) &:= \underline{P} (t_1, \dots, t_n), \\ \rho (\Phi_1 \odot \Phi_2) &:= \rho (\Phi_1) \odot \rho ( \Phi_2), \\ \rho (\bot) &:= \bot, \\ \rho (\mathord{\sim} \bot) &:= \bot \to \bot, \\ \rho (\heartsuit \Phi) &:= \heartsuit \rho (\Phi), \\ \rho ({\mathrm{Q} x}\, \Phi) &:={\mathrm{Q} x}\, \rho (\Phi), \end{aligned}
\end{equation*}
\notag
$$
where $\odot \in \{\wedge, \vee, \to\}$, $\heartsuit \in \{\Box, \Diamond\}$, $\mathrm{Q} \in \{\forall, \exists\}$ and $x \in \mathrm{Var}$. Of course, if necessary, the mapping $\rho$ can be extended to all $\sigma$-formulae by setting Formally, we should write $\rho_{\sigma}$ instead of $\rho$, but it will always be clear from the context which signature we are talking about. Lemma 9.2. For any $L_{\sigma}$-model $\mathcal{M}$, $w \in W$ and $\sigma_{A_w}$-sentence $\Phi$, By Theorem 3.8 we can assume that $\Phi$ is an n.n.f. Then the lemma is proved by an easy induction on the complexity of $\Phi$. Theorem 9.3. For every $\sigma$-formula $\Phi$, In other words, $\rho$ faithfully embeds $L$ into $\underline{L}$. Proof. In view of the completeness theorems for $L$ and $\underline{L}$, we need to show that
$$
\begin{equation*}
\vDash_{L} \Phi \quad \Longleftrightarrow \quad \vDash_{\underline{L}} {\tau (\Phi)}
\end{equation*}
\notag
$$
(see Theorem 6.3 and, for example, [15], § 6). Then we can argue by analogy with the proof of Theorem 8.6, using Lemma 9.2 instead of Lemma 8.4.
The theorem is proved. From this, using some interpolation theorems for $\mathsf{QK}$-extensions, we can obtain the required result. Proof. Consider an arbitrary $L$ in $\mathscr{L}$ and any signature $\sigma$.
Suppose that a $\sigma$-n.n.f. $\Phi \to \Psi$ belongs to $L$. By Theorem 9.3 we have Since $\underline{L}$ has $\mathrm{CIP}$, there exists a Craig interpolant $\Theta$ for $\rho (\Phi) \to \rho (\Psi)$ in $\underline{L}$. Take
$$
\begin{equation*}
\Theta':=\text{the result of replacing each }\underline{P}\text{ in }\Theta\text{ by }\mathord{\sim} P.
\end{equation*}
\notag
$$
Then $\Theta'$ is a $\sigma$-n.n.f. and $\rho (\Theta') = \Theta$. Applying Theorem 9.3 again, we obtain
$$
\begin{equation*}
{\Phi \to \Theta'}\in L \quad\text{and}\quad {\Theta' \to \Psi} \in\ L.
\end{equation*}
\notag
$$
Here, by construction,
$$
\begin{equation*}
\begin{aligned} \, \mathrm{D} (\Theta')&= (\mathrm{O} (\Theta') \cap \mathrm{Const}_{\sigma}) \cup \mathrm{FV} (\Theta') \\ &= (\mathrm{O} (\Theta) \cap \mathrm{Const}_{\sigma}) \cup \mathrm{FV} (\Theta) \\ &\subseteq \mathrm{D} (\rho (\Phi)) \cap \mathrm{D} (\rho (\Psi)) = \mathrm{D} (\Phi) \cap \mathrm{D} (\Psi). \end{aligned}
\end{equation*}
\notag
$$
Moreover, it is easy to check that
$$
\begin{equation*}
\mathrm{P}^+ (\Theta)\subseteq \mathrm{P}^+ (\Phi) \cap \mathrm{P}^+ (\Psi) \quad\text{and}\quad \mathrm{P}^- (\Theta)\subseteq \mathrm{P}^- (\Phi) \cap \mathrm{P}^- (\Psi).
\end{equation*}
\notag
$$
So $\Theta'$ is a strong interpolant for $\Phi \to \Psi$ in $L$.
The theorem is proved. Now let us discuss $\mathsf{QBK}$-extensions of type (i), that is, $\mathsf{QB3K}$ and $\mathsf{QBK}^{\circ}$. We define the translations $\rho^3$ and $\rho^{\circ}$ exactly as $\rho$, but with the following modifications (cf. [13], § 2):
$$
\begin{equation*}
\rho^3 (\mathord{\sim} P (t_1, \dots, t_n)) :=\underline{P} (t_1, \dots, t_n) \wedge \neg P (t_1, \dots, t_n)
\end{equation*}
\notag
$$
and
$$
\begin{equation*}
\rho^{\circ} (\mathord{\sim} P (t_1, \dots, t_n)) :=\underline{P} (t_1, \dots, t_n) \vee \neg P (t_1, \dots, t_n).
\end{equation*}
\notag
$$
Then we have the following result. Lemma 9.5. For any $\mathsf{QB3K}_{\sigma}$-model $\mathcal{M}$, $w \in W$ and $A_w$-sentence $\Phi$, The analogous result holds for $\mathsf{QBK}^{\circ}$ and $\rho^{\circ}$. Proof. Note that for every $\mathsf{QB3K}_{\sigma}$-model $\mathcal{M}$ and every atomic $A_w$-sentence $P (t_1, \dots, t_n)$,
$$
\begin{equation*}
\begin{aligned} \, \mathcal{M}, w \Vdash^+ {\mathord{\sim} P (t_1, \dots, t_n)} \quad &\Longleftrightarrow \quad \underline{\mathcal{M}}, w \Vdash {\underline{P} (t_1, \dots, t_n)} \\ \quad &\Longleftrightarrow \quad \underline{\mathcal{M}}, w \Vdash \underbrace{\underline{P} (t_1, \dots, t_n) \wedge \neg P (t_1, \dots, t_n)}_{\rho^3 (\mathord{\sim} P (t_1, \dots, t_n))}. \end{aligned}
\end{equation*}
\notag
$$
Therefore, we can argue in the same way as in the proof of Lemma 9.2.
For $\mathsf{QBK}^{\circ}$ and $\rho^{\circ}$ the argument is similar. The lemma is proved. On the other hand, for $L \in \{\mathsf{QBK}^{\circ}, \mathsf{QB3K}\}$ it is impossible to find, for each $\mathsf{QK}_{\underline{\sigma}}$-model $\mathcal{N}$, a $L_{\sigma}$-model $\mathcal{M}$ such that $\underline{\mathcal{M}} = \mathcal{N}$. Therefore, we need to work more accurately than with $L \in \mathscr{L}$. With each $\mathsf{QK}_{\underline{\sigma}}$-model $\mathcal{N} = \langle \mathcal{W}, \mathscr{A} \rangle$ we associate the $\mathsf{QB3K}_{\sigma}$-model
$$
\begin{equation*}
\mathcal{N}^3:= \langle \mathcal{W}, \mathscr{A}^{3, +}, \mathscr{A}^{3, -} \rangle,
\end{equation*}
\notag
$$
where $\mathscr{A}^{3, +}$ and $\mathscr{A}^{3, -}$ denote the families $\langle \mathfrak{A}_w^{3, +} \colon w \in W \rangle$ and $\langle \mathfrak{A}_w^{3, +} \colon w \in W \rangle$ such that for every $w \in W$:
$$
\begin{equation*}
\mathcal{N}^{\circ}:= \langle \mathcal{W}, \mathscr{A}^{\circ, +}, \mathscr{A}^{\circ, -} \rangle
\end{equation*}
\notag
$$
is defined, but we need to replace $\cap$ by $\cup$ in the last property: The following statement will play the role of a converse of Lemma 9.5. Lemma 9.6. For any $\mathsf{QK}_{\underline{\sigma}}$-model $\mathcal{N}$, $w \in W$ and $\sigma_{A_w}$-sentence $\Phi$, The analogous result holds for $\rho^{\circ}$ and $\mathcal{N}^{\circ}$. The proof is obtained by easy induction on the complexity of $\Phi$. Theorem 9.7. For every $\sigma$-formula $\Phi$, The analogous result holds for $\mathsf{QBK}^{\circ}$ and $\rho^{\circ}$. In other words, $\rho^3$ and $\rho^{\circ}$ faithfully embed $\mathsf{QB3K}$ and $\mathsf{QBK}^{\circ}$, respectively, into $\mathsf{QK}$. This follows from Lemmas 9.6 (for the direct implication) and 9.5 (for the converse implication), taking into account the completeness theorems for $\mathsf{QB3K}$, $\mathsf{QBK}^{\circ}$ and $\mathsf{QK}$. From this we can already obtain $\mathrm{CIP}$ for extensions of type (i). Proof. Consider an arbitrary signature $\sigma$.
Suppose that $\Phi \to \Psi \in \mathsf{QB3K}_{\sigma}$. By Theorem 9.7 we have Since $\mathsf{QK}$ has $\mathrm{CIP}$, there exists a Craig interpolant $\Theta$ for $\rho^3 (\Phi) \to \rho^3 (\Psi)$ in $\mathsf{QB3K}$. Clearly, $\Theta$ does not necessarily have the form $\rho^3 (\Theta')$ (because there can be ‘free-standing’ formulae $\underline{P} (t_1, \dots, t_n)$ in $\Theta$ which are not connected with $\neg P (t_1, \dots, t_n)$ by means of conjunction). Define
$$
\begin{equation*}
\begin{aligned} \, \widetilde{\Theta}&:= \text{the result of replacing each free-standing }\underline{P} (t_1, \dots, t_n) \text{ in }\Theta \\ &\quad\ \text{ by }\underline{P} (t_1, \dots, t_n) \wedge {\neg P (t_1, \dots, t_n)}. \end{aligned}
\end{equation*}
\notag
$$
It is easy to show that for any $\mathsf{QB3K}_{\sigma}$-model $\mathcal{M}$, $w \in W$ and $A_w$-substitution $\lambda$,
$$
\begin{equation*}
\underline{\mathcal{M}}, w \Vdash \lambda \Theta \quad \Longleftrightarrow \quad \underline{\mathcal{M}}, w \Vdash \lambda \widetilde{\Theta}.
\end{equation*}
\notag
$$
Obviously, $\widetilde{\Theta} = \rho^3 (\Theta')$ for a suitable $\sigma$-formula $\Theta'$. Taking the soundness theorem for $\mathsf{QK}$ into account, this implies that for any $\mathsf{QB3K}_{\sigma}$-model $\mathcal{M}$, $w \in W$ and $A_w$-substitution $\lambda$,
$$
\begin{equation*}
\underline{\mathcal{M}}, w \Vdash {\lambda (\rho^3 (\Phi) \to \rho^3 ( \Theta'))} \quad\text{and}\quad \underline{\mathcal{M}}, w \Vdash {\lambda (\rho^3 (\Theta') \to \rho^3 (\Psi))},
\end{equation*}
\notag
$$
which, in view of Lemma 9.5, is equivalent to
$$
\begin{equation*}
\mathcal{M}, w \Vdash \lambda (\Phi \to \Theta') \quad\text{and}\quad \mathcal{M}, w \Vdash \lambda (\Theta' \to \Psi).
\end{equation*}
\notag
$$
By the completeness theorem for $\mathsf{QB3K}$, the latter means that
$$
\begin{equation*}
\Phi \to \Theta'\in \mathsf{QB3K}_{\sigma} \quad\text{and}\quad \Theta' \to \Psi \in\ \mathsf{QB3K}_{\sigma}.
\end{equation*}
\notag
$$
In addition, it is not hard to check that $\mathrm{O} (\Theta) \subseteq \mathrm{O} (\Phi) \cap \mathrm{O} (\Psi)$. So $\Theta'$ is a Craig interpolant for $\Phi \to \Psi$ in $\mathsf{QB3K}$.
In the case of $\mathsf{QBK}^{\circ}$ we argue similarly. The theorem is proved. Remark 9.9. The logics $\mathsf{QB3K}$ and $\mathsf{QBK}^{\circ}$ do not have $\mathrm{SIP}$. Indeed, in the case of $\mathsf{QB3K}$ we take where $P$ is some $n$-ary predicate symbol. Then $\Phi \to \Psi \in \mathsf{QB3K}$, but there is no strong interpolant for $\Phi \to \Psi$ in $\mathsf{QB3K}$. In the case of $\mathsf{QBK}^{\circ}$ one can take Then $\Phi \to \Psi \in \mathsf{QBK}^{\circ}$, but there is no strong interpolant for $\Phi \to \Psi$ in $\mathsf{QBK}^{\circ}$. Of course, the proof of Theorem 9.8 is easily modified to obtain $\mathrm{CIP}$ for $\mathsf{QB3S4}$, for example. 
Citation in format AMSBIB
\Bibitem{GreSpe24} |
|
||||||||||||||||||||||||||||||||||||||
|
Contact us: |
Terms of Use
|
Registration to the website |
Logotypes |
|