| Sbornik: Mathematics |
|
|
|
|
|
This article is cited in 7 scientific papers (total in 7 papers) The predicate version of the joint logic of problems and propositions A. A. Onoprienko Steklov Mathematical Institute of Russian Academy of Sciences, Moscow, Russia
Russian version:
Matematicheskii Sbornik, 2022, Volume 213, Number 7, DOI: https://doi.org/10.4213/sm9608 
Bibliographic databases:
    § 1. IntroductionIn this paper we consider the logic $\mathrm{QHC}$, the joint logic of problems and propositions introduced by Melikhov (see [1], [2]). In this logic each variable and each formula is of one of the following two sorts: a proposition or a problem. Formulae of propositional sort are connected with formulae of problem sort via two modal operators, ? and ! . Applying ! to a proposition $p$ we obtain the problem $!p$ denoting ‘to prove the proposition $p$’. Conversely, the application of ? to a problem $\alpha$ yields the proposition $?\alpha$ denoting ‘the problem $\alpha$ has a solution’. The semantics of the propositional fragment of the logic $\mathrm{QHC}$, the logic $\mathrm{HC}$, was studied in detail by this author in [3]. In that work we introduced Lindenbaum HC-algebras, Kripke-style semantics with two sets of worlds and also Kripke-style semantics with audit worlds. The frames of latter type were introduced in [4] as models for the intuitionistic epistemic logic $\mathrm{IEL}^+$. This author proved the completeness of the logic HC with respect to each of these types of model, the finite model property, and also the conservativity of the logic HC over the logic $\mathrm{IEL}^+$ (if the modal operator of $\mathbf K$ is interpreted as $!?$). The system $\mathrm{QHC}$ was inspired by Kolmogorov’s informal calculus of problems, and it is in line with the investigations of the Brouwer-Heyting-Kolmogorov constructive semantics (see [5]–[22]). By combining the modal operators ! and ? of the logic $\mathrm{QHC}$ we can obtain derived modalities. An application of the modality $?!$, denoted by $\Box$, to a proposition $p$ can be understood as the proposition ‘there is a proof of the proposition $p$’ or ‘$p$ is provable’. Likewise, an application of the modality !?, denoted by $\nabla$, to a problem $\alpha$ can be understood as the problem ‘to prove that the problem $\alpha$ has a solution’. Further iterations of the basic modalities ! and ? yield nothing new, since the formulae $!p\leftrightarrow\,!?!p$ and $?\alpha\leftrightarrow\,?!?\alpha$ are provable in $\mathrm{QHC}$ (see [1]). In some sense, the modality $\Box$ corresponds to the classical understanding of the notion of the knowledge about the truth of a proposition, while the modality $\nabla$ corresponds to the intuitionistic understanding. Using the axioms and inference rules of $\mathrm{QHC}$ one can prove (for instance, see [1]) that the modality $\Box$ satisfies the following principles: $(1^{\Box})$ $\Box p\to p$; $(2^{\Box})$ $\Box p\to \Box\Box p$; $(3^{\Box})$ $\cfrac{p}{\Box p}$; $(4^{\Box})$ $\Box(p\to q)\to(\Box p\to \Box q)$. The modality $\nabla$ satisfies the following principles: $(1^{\nabla})$ $\alpha\to\nabla\alpha$; $(2^{\nabla})$ $\nabla\nabla\alpha\to\nabla\alpha$; $(3^{\nabla})$ $\nabla\bot\to\bot$; $(4^{\nabla})$ $\nabla(\alpha\to\beta)\to(\nabla\alpha\to\nabla\beta)$. Axioms and inference rules $(1^{\Box})-(4^{\Box})$ over the classical predicate logic with modal operator $\Box$ define the logic $\mathrm{QS4}$ (the predicate extension of $\mathrm{S4}$). It was proved in [1] that $\mathrm{QHC}$ is a conservative extension of $\mathrm{QS4}$. Axioms $(1^{\nabla})$–$(4^{\nabla})$ over the intuitionistic predicate logic with modal operator $\nabla$ define the logic called $\mathrm{QH4}$ by Melikhov [1]. The intuitionistic modal logic defined by axioms $(1^{\nabla})$, $(2^{\nabla})$ and $(4^{\nabla})$ originated from Goldblatt [23], who studied the logic of the localization operator on a topos. An operator with analogous properties acting on a Heyting algebra also appeared in Dragalin’s work [24], who called it the ‘completion operator’ (the term ‘nucleus’ for such operators is common in the contemporary literature). This logic was subsequently rediscovered by Fairtlough and Mendler, who called it the lax logic. The propositional version of PLL was investigated in [25], and the predicate extension QLL of this logic, in [26]. The logics obtained by adding the axiom $(3^{\nabla})$ are called $\mathrm{PLL}^+$ and $\mathrm{QLL}^+$, respectively. Kripke-style models for the logics $\mathrm{QLL}$ and $\mathrm{QLL}^+$ were constructed in [26]. These models are quite complicated: they contain a nonempty set of possible worlds, two accessibility relations, a function mapping each world to some subset of worlds, and also a set of ‘worlds which are prone to errors’ (only for QLL). The logic QLL was also studied by Aczel [27], another type of semantics for QLL was constructed by Goldblatt (see [28]), and Rogozin [29] studied the lambda-calculus associated with this and several closely related logics. Artemov and Protopopescu conducted a deep analysis of the intuitionistic logic of knowledge and constructed three formal systems, $\mathrm{IEL}^-$, $\mathrm{IEL}$ and $\mathrm{IEL}^+$. The systems $\mathrm{IEL}$ and $\mathrm{IEL}^+$ have turned out to coincide with the logics $\mathrm{PLL}$ and $\mathrm{PLL}^+$, respectively. Kripke models with audit worlds for the logic $\mathrm{IEL}^+$, which form a basis for the semantics of $\mathrm{QHC}$ in this paper, were introduced in [4]. The author proved in [3] that the propositional logic $\mathrm{HC}$ is a conservative extension of $\mathrm{PLL}^+$. Melikhov denoted the logic $\mathrm{PLL}^+$ by $\mathrm{H4}$, and we use this notation in what follows. In this work we prove that $\mathrm{QHC}$ is a conservative extension of the predicate logic $\mathrm{QH4}$ and also construct Kripke models with audit worlds for $\mathrm{QHC}$ and $\mathrm{QH4}$. One possible application of the logic $\mathrm{QHC}$ is as a basis for the construction of various standard theories which is more coherent with the intuitive understanding. Melikhov gives an example of an axiomatization of Tarski’s elementary geometry, formalized on the basis of $\mathrm{QHC}$, arguing that Euclid himself considered postulates and axioms (see [2]). The logic $\mathrm{QHC}$ allows one to make the logical structure of Euclid’s theory clearer and to eliminate the hidden conjectures and paradoxes arising from them. It was shown that this theory contains (in some precise sense) Tarski’s elementary geometry (see [30]) as a classical part and the constructive version of Tarski’s geometry which was introduced by Beeson [31] as an intuitionistic part. In this paper we introduce Kripke semantics for the predicate logic $\mathrm{QHC}$ and show this logic to be sound and complete with respect to this semantics. We also prove the conservativity of $\mathrm{QHC}$ over the intuitionistic modal predicate logic $\mathrm{QH4}$ (the analogous result for the propositional fragments of these logics was established in [3]). We show that the logic $\mathrm{QHC}$ has the disjunction and existence properties, namely, if an intuitionistic formula $\alpha\vee\beta$ is provable in $\mathrm{QHC}$, then either $\alpha$ or $\beta$ is provable in $\mathrm{QHC}$; if an intuitionistic formula $\exists\, x\ \alpha(x)$ is provable in $\mathrm{QHC}$, then $\alpha(c)$ is provable in $\mathrm{QHC}$ for some constant symbol $c$ (provided that the language contains at least one constant symbol). § 2. The logic $\mathrm{QHC}$A signature $\Omega$ of the logic $\mathrm{QHC}$ consists of a set of constant symbols $c_1,c_2,\dots$ and two sets of predicate symbols: the set VarProp of predicate symbols of propositional sort and the set VarProb of predicate symbols of problem sort; the language of the logic $\mathrm{QHC}$, together with the signature $\Omega$, is called the language $\Omega$. With each predicate symbol we associate a natural number representing its arity. We denote predicate symbols of propositional sort by lowercase Latin letters ($p(\mkern-1mu x,\mkern-1mu y,\mkern-1mu z\mkern-1mu),q(\mkern-1mu x\mkern-1mu),\mkern-1mu\dots$ ) and predicate symbols of problem sort by lowercase Greek letters ($\alpha(x),\beta(x,y),\dots$). We also use this notation for formulae of appropriate sorts of the logic $\mathrm{QHC}$. All formulae for which the sort is unknown are denoted by uppercase Greek letters: $A,B,\Phi,\Psi,\dots$ . For simplicity we consider the logic $\mathrm{QHC}$ in a language without functional symbols, but only with predicate and constant symbols. Terms of $\mathrm{QHC}$ are individual variables $x_1, x_2, \dots$ and constant symbols $c_1,c_2,\dots$ (which do not belong to any sort; intuitively, we can assume that these are ‘objects’ which can appear in the formulations of propositions and problems). Each formula of $\mathrm{QHC}$ has one of two sorts: it is either a proposition or a problem. Formulae of $\mathrm{QHC}$ are built from atomic formulae using the standard classical and intuitionistic connectives $\wedge$, $\vee$, $\to$, $\leftrightarrow$ and $\neg$, the classical and intuitionistic quantifiers $\exists$ and $\forall$, and the modal operators $?$ and $!$ with the appropriate restrictions on their arity, while atomic formulae are defined as in the standard predicate logic. As for the propositional fragment of $\mathrm{QHC}$, the logic $\mathrm{HC}$ (see [3]), connectives and quantifiers do not change the sort of a formula, while modal operators do. The classical truth and falsity are denoted by $1$ and $0$, and the intuitionistic truth and falsity are denoted by $\top$ and $\bot$, respectively. The axioms and inference rules of the logic $\mathrm{HC}$ are as follows. I. All axioms and inference rules of the classical propositional logic. One can substitute arbitrary formulae of propositional sort (possibly containing the modal operators $\text{?\ and !}$) for variables in axiom schemata. II. All axioms and inference rules of the intuitionistic propositional logic. One can substitute arbitrary formulae of problem sort (possibly containing the modal operators $\text{?\ and !}$) for variables in the axiom schemata. III. The additional axioms (more precisely, axiom schemata) and inference rules listed below:
Inference rules 3) and 4) are called the necessitation rules. The logic $\mathrm{QHC}$ is an extension of $\mathrm{HC}$. One can instantiate axiom schemata of the logic $\mathrm{QHC}$ with arbitrary formulae of propositional (problem) sort, possibly containing quantifiers. Moreover, the following axioms and inference rules are added to those of $\mathrm{QHC}$: In these schemata it is assumed that the term $t$ is substitutable for $v$. Note that, since $A$ is a formula of propositional or problem sort, we have in fact four axiom schemata.The Bernays rules: In these inference rules it is assumed that $x$ is not a free variable of the formula $A$. As above, since $A$ and $ B$ are formulae of the same (propositional or problem) sort, we have four inference rules.Definition 1. A derivation in the logic $\mathrm{QHC}$ is a finite sequence of formulae $\Phi_1,\dots,\Phi_n$ such that for each $i = 1, \dots, n$ the formula $\Phi_i$ is either an axiom of the logic $\mathrm{QHC}$ or can be obtained from one or two previous formulae in this sequence using one of the inference rules (the modus ponens rule, one of the Bernays rules, or one of the necessitation rules). A formula $\Phi$ is derivable in $\mathrm{QHC}$ (is a theorem of $\mathrm{QHC}$) if there is a derivation such that $\Phi$ is the last formula in it. The notation: $\vdash\Phi$. Definition 2. A quasiderivation of a formula $\Phi$ from hypotheses $\Gamma$ is a finite sequence of formulae $\Phi_1,\dots,\Phi_n$ such that for each $i = 1, \dots, n$ the formula $\Phi_i$ is either an axiom of the logic $\mathrm{QHC}$, a hypothesis, or can be obtained from one or two previous formulae in this sequence using one of the inference rules. Given a quasiderivation $\Phi_1,\dots,\Phi_n$, for each $i=1,\dots,n$ we define the set $\Delta(\Phi_i)\subseteq\Gamma$ recursively:
Informally, $\Delta(\Phi_i)$ is the set of hypotheses on which the formula $\Phi_i$ in the derivation depends. Definition 3. A derivation of a formula $\Phi$ from hypotheses $\Gamma$ is a quasiderivation of $\Phi$ from $\Gamma$ in which each application of the Bernays rules, 10) or 11), to a formula $\Phi_i$ bounds a variable which does not have free occurrences in the formulae in $\Delta(\Phi_i)$. A formula $\Phi$ is derivable from $\Gamma$ if there is a derivation from $\Gamma$ such that $\Phi$ is the last formula in it. The notation: $\Gamma\vdash^*\Phi$. Definition 4. A weak quasiderivation of a formula $\Phi$ from hypotheses $\Gamma$ is a finite sequence of formulae $\Phi_1,\dots,\Phi_n$ such that for each $i = 1, \dots, n$ the formula $\Phi_i$ is either a theorem of the logic $\mathrm{QHC}$, or a hypothesis, or can be obtained from the previous formulae in this sequence using the modus ponens rule or one of the Bernays rules. In a similar way we can define the set $\Delta(\Phi_i)$ for a given weak quasiderivation and the notion of a weak derivation $\Phi$ from a set of hypotheses $\Gamma$. If there is a weak derivation of a formula $\Phi$ from a set of hypotheses $\Gamma$, then we use the notation $\Gamma\vdash\Phi$. If $\Gamma$ and $\Delta$ are two sets of formulae, then we write $\Gamma\vdash\Delta$ ($\Gamma\vdash^*\Delta$) if $\Gamma\vdash\Phi$ ($\Gamma\vdash^*\Phi$) for each $\Phi\in\Delta$. Theorem 1 (deduction theorem). Let $\Gamma$ be a set of formulae and $\Phi$ and $ \Psi$ be formulae of the same sort. If $\Gamma\cup\{\Phi\}\vdash\Psi$, then $\Gamma\vdash\Phi\to\Psi$. This theorem can be proved using induction on the derivation length, the method described in [32]. § 3. Soundness of the logic $\mathrm{QHC}$ with respect to Kripke models with audit worldsLet $\Omega$ be a language of the logic QHC. A Kripke frame with audit worlds for this language is a tuple $\mathcal K=(W,\preccurlyeq,\mathrm{Aud})$, where $(W,\preccurlyeq)$ is a partially ordered set, $\mathrm{Aud}\subseteq W$ and
$$
\begin{equation*}
\forall\, a\in W \ \exists\, b\in W \ (a\preccurlyeq b\wedge b\in\mathrm{Aud}).
\end{equation*}
\notag
$$
A Kripke model of the logic QHC with audit worlds is a Kripke frame with a function $D$ that maps each $a\in W$ to a nonempty set $D_a$ and with a valuation of atoms $\models$. It is assumed that if $a\preccurlyeq b$, then $D_a\subseteq D_b$ (intuitively, $D_a$ is the set of objects constructed by time $a$ and accessible for research; the condition $a\preccurlyeq b\Rightarrow D_a\subseteq D_b$ reflects that objects discovered do not disappear in the future). If the language $\Omega$ contains a constant symbol $c$, then it is assigned an object $\overline c\in D_{a}$ for each $a\in W$. We identify $c$ and $\overline c$ in what follows. The valuation of atoms $\models$ is a binary relation between the set $W$ and the set of atoms of the form $A(x_1,\dots,x_n)$, where $A$ is an $n$-ary predicate symbol of the signature $\Omega$, and $x_1,\dots,x_n\in\bigcup_{a\in W}D_a$. The notation $a\models A(x_1,\dots,x_n)$ can be read in the standard way as follows: “$A(x_1,\dots,x_n)$ is true at $a$”. The following restriction is imposed on the relation $\models$: atoms of problem sort can be true or false in an arbitrary world in the set $W$, while atoms (and other formulae) of propositional sort can be true or false only in worlds in the set $\mathrm{Aud}$. Moreover, $\models$ has the following property: if $a\models A(x_1,\dots,x_n)$, then $\{x_1,\dots,x_n\}\subseteq D_a$, and if $A(x_1,\dots,x_n)$ is an atom of problem sort and $a\preccurlyeq b$, then $b\models A(x_1,\dots,x_n)$ (that is, monotonicity holds for atoms of problem sort). We define the satisfiability relation for all formulae of QHC using recursion on the build-up of a formula. For the classical connectives $\wedge$, $\vee$, $\rightarrow$ and $\neg$ the valuation is defined pointwise at worlds in $\mathrm{Aud}$. For the intuitionistic connectives $\wedge$, $\vee$, $\rightarrow$ and $\neg$ the valuation is defined at worlds in $W$ as in standard Kripke frames. For modal operators the valuation is defined as in Kripke models with audit worlds for the logic HC:
$$
\begin{equation*}
\begin{aligned} \, &a\models\,?\alpha \Leftrightarrow a\models\alpha \quad (\text{for }a\in\mathrm{Aud}), \\ &a\models\,!p \Leftrightarrow \forall\, b\in\mathrm{Aud}\ (a\preccurlyeq b \Rightarrow b\models p)\quad (\text{for }a\in W). \end{aligned}
\end{equation*}
\notag
$$
Now we define the satisfiability relation for the classical quantifiers $\exists$ and $\forall$ (${a\in\mathrm{Aud}}$):
$$
\begin{equation*}
\begin{aligned} \, &a\models\exists\, x \ p(x) \Leftrightarrow (\exists\, v\in D_a)\ a\models p(v), \\ &a\models\forall\, x \ p(x) \Leftrightarrow (\forall\, v\in D_a)\ a\models p(v). \end{aligned}
\end{equation*}
\notag
$$
Finally, we define the satisfiability relation for the intuitionistic quantifiers $\exists$ and $\forall$ ($a\in W$):
$$
\begin{equation*}
\begin{aligned} \, &a\models\exists\, x \ \alpha(x) \Leftrightarrow \exists\, v\in D_a \ a\models \alpha(v), \\ &a\models\forall\, x \ \alpha(x) \Leftrightarrow \forall\, b\succcurlyeq a \ \forall\, v\in D_b \ b\models \alpha(v). \end{aligned}
\end{equation*}
\notag
$$
The proof uses standard induction on the build-up of a formula $\alpha$. A formula of problem (propositional) sort is valid in a model $\mathcal K$ if it is true at every world in the set $W$ ($\mathrm{Aud}$) of this model. Theorem 2 (soundness). If a closed formula of the language $\Omega$ is derivable in the logic $\mathrm{QHC}$, then it is valid in every Kripke model for $\Omega$. Proof. We prove a more general result: if a formula is derivable in QHC, then its universal closure is valid in every Kripke model. Clearly, it is sufficient to check that the universal closure of each axiom is valid in every Kripke frame and the inference rules preserve this property.
For axioms and inference rules of the logic $\mathrm{HC}$ this follows from the soundness of $\mathrm{HC}$ with respect to Kripke models with audit worlds (see [3]), because Kripke models of the logic $\mathrm{QHC}$ with audit worlds are expansions of such models for $\mathrm{HC}$. The fact that modus ponens preserves the property in question of formulae is trivial. It remains to check this for the new axioms and inference rules 8)–11). In the case of their classical versions this follows directly from the definitions, while the proof for the intuitionistic versions can be found in [32], Theorem 53. The theorem is proved. Example (Kripke model with audit worlds). The classical logic is sometimes understood as a logic in which all propositions are divided into true and false ones. In the intuitionistic logic, apart from true and false propositions, there are also unspecified ones, which can become true or false over time. Since there are unprovable and unrefutable propositions in mathematics, the second approach seems to be more reasonable. Let us show that the logic $\mathrm{QHC}$ provides for this possibility. We depict the Kripke frame of the logic $\mathrm{QHC}$ in which the order relation $\preccurlyeq$ is denoted by arrows (if $x\preccurlyeq y$, then an arrow goes from $x$ to $y$) and the set of audit worlds $\mathrm{Aud}$ is $\{b,c\}$:
Let us define a valuation on this frame as follows: $b\models p$, $c\nvDash p$. We obtain $b\models\,!p$ and $c\models\,!\neg p$. Thus, being in the world $a$, there are two worlds above, in one of them there is a proof of $p$, and in the other one there is a proof of $\neg p$. § 4. Derivability from hypotheses in the logic $\mathrm{QHC}$Note several simple properties of the derivability relations $\vdash$ and $\vdash^*$ from hypotheses in the logic $\mathrm{QHC}$. Lemma 2. 1) If $\Gamma$ is a set of formulae of problem sort and $\Gamma\vdash\alpha$, then $?\Gamma\vdash\,?\alpha$. 2) If $\Gamma$ is a set of formulae of propositional sort and $\Gamma\vdash p$, then $!\Gamma\vdash\,!p$. Proof. Let us prove part 1). Since $\Gamma\!\vdash\!\alpha$, there is a finite set of formulae ${\beta_1,\mkern-1mu\dots,\mkern-1mu\beta_n\mkern-1mu\!\in\!\Gamma}$ such that $\{\beta_1,\dots,\beta_n\}\vdash\alpha$. Applying Theorem 1 on deduction several times we obtain Equivalently, Thus, $\beta_1\wedge\dots\wedge\beta_n\to\alpha$ is a theorem of the logic $\mathrm{QHC}$. Therefore, $?(\beta_1\wedge\dots\wedge\beta_n\to\alpha)$ is also a theorem of $\mathrm{QHC}$. Next, since $?\beta_1,\dots,?\beta_n\in\,?\Gamma$, we have Moreover, since $?(\beta_1\wedge\dots\wedge\beta_n\to\alpha)$ is a theorem of $\mathrm{QHC}$, we obtain
$$
\begin{equation*}
?\Gamma\vdash\,?\beta_1\wedge\dots\wedge\,?\beta_n\to\,?\alpha
\end{equation*}
\notag
$$
(here we have used the axiom $?(\beta\to\gamma)\to(?\beta\to\,?\gamma)$ and also the theorem of $\mathrm{QHC}$ $?(\beta\wedge\gamma)\leftrightarrow(?\beta\,\wedge\,?\gamma)$, which was proved in [1]). Finally, applying modus ponens we obtain $?\Gamma\vdash\,?\alpha$.
The proof of 2) is similar: the axiom $!(p\to q)\to(!p\to\,!q)$ holds in the logic $\mathrm{QHC}$, while $!(p\wedge q)\leftrightarrow(!p\,\wedge\,!q)$ is a theorem of $\mathrm{QHC}$. The lemma is proved. Note that we have conservativity in the following sense: in a weak derivation of a formula of problem sort we can keep only the hypotheses of problem sort; in a weak derivation of a formula of propositional sort we can keep only the hypotheses of propositional sort. Definition 5. For a set of formulae $\Gamma$ we denote by $\Gamma^C$ the set of formulae of propositional sort in $\Gamma$ and by $\Gamma^H$ the set of formulae of problem sort in $\Gamma$. In both cases the implication from right to left is trivial, and the implication from left to right is proved using a simple induction on the derivation length. Note also the following connection between the relations $\vdash$ and $\vdash^*$. Proof. The implications from right to left in 1) and 2) are trivial: the hypotheses on the right-hand side are obtained via the necessitation rules from the ones on the left-hand side. The implications from left to right in 1) and 2) are proved using joint induction on the derivation lengths. Clearly, it is sufficient to consider the case when necessitation rules are applied.
1) Assume that $\alpha$ is obtained via the necessitation rule $\cfrac{p}{!p}$; then $\alpha=\,!p$. Thus, $\Gamma\vdash p$. By the induction hypothesis for part 2) of Lemma 3 we have $?\Gamma^H,?!\Gamma^C\vdash p$. Then $!?\Gamma^H,!?!\Gamma^C\vdash \,!p$ follows by Lemma 2. Since the equivalence $!?!q\leftrightarrow \,!q$ is a theorem of the logic $\mathrm{QHC}$, we obtain 2) Assume that $p$ is obtained via the necessitation rule $\cfrac{\alpha}{?\alpha}$, then $p=\,?\alpha$. Thus, $\Gamma\vdash\alpha$. By the induction hypothesis for part 1) of Lemma 3 we have $\Gamma^H,!\Gamma^C\vdash\alpha$. Then $?\Gamma^H,?!\Gamma^C\vdash\,?\alpha$ follows by Lemma 2, as required. The lemma is proved. The lemma follows from the fact that the formulae $\bot\to\alpha$ and $0\to p$ are theorems of $\mathrm{QHC}$: $\bot\to\alpha$ is an intuitionistic tautology for any formula $\alpha$ of problem sort and $0\to p$ is a classical tautology for any formula $p$ of propositional sort. Definition 6. A set of closed formulae $\Gamma$ of some language is called a theory in the logic $\mathrm{QHC}$ if it contains all theorems of $\mathrm{QHC}$, is closed under weak derivability (if $\Gamma\vdash\Phi$, then $\Phi\in\Gamma$) and $?\Gamma^H\subseteq\Gamma^C$. A theory is consistent if it does not contain the constants $0$ and $\bot$. The closure $[\Gamma]$ of a set of closed formulae $\Gamma$ is the smallest theory containing this set with respect to set-theoretic inclusion. Remark 1. Let $\Gamma$ be an arbitrary set of formulae of the logic $\mathrm{QHC}$. Note that to obtain its closure $[\Gamma]$ it is necessary to make the following steps: It is clear that the resulting set is the smallest theory containing $\Gamma$. Lemma 6. Let $\Gamma$ be a theory in the logic $\mathrm{QHC}$. Then $\Gamma\nvdash0$ implies that $\Gamma\nvdash \bot$. Proof. Suppose $\Gamma\vdash\bot$. Then $\bot\in\Gamma$. Since $?\Gamma^H\subseteq\Gamma^C$, we obtain $\Gamma\vdash\,?\bot$. Moreover, $?\bot\to0$ is a theorem of $\mathrm{QHC}$ (for instance, see [1]). Using modus ponens we obtain ${\Gamma\vdash0}$.
The lemma is proved. It follows from Lemma 6 that for the consistency of a theory it is sufficient to require that the constant 0 is not a theorem of this theory. Lemma 7. If $\Gamma$ is an arbitrary set of formulae, $p$ is a formula of propositional sort and $\beta$ is a formula of problem sort, then Proof. Both implications from right to left are trivial. Let us prove the implications from left to right.
1) Assume that $\beta\in[\Gamma]$. It follows from Remark 1 that either $\beta$ is a theorem of the logic $\mathrm{QHC}$, or there is a weak derivation of the formula $\beta$ from $\Gamma$. In either case, we obtain $\Gamma\vdash\beta$ using Lemma 3. 2) Assume that $p\in[\Gamma]$. Consider the set $\Gamma_1$ obtained from $\Gamma$ by adding all the theorems of $\mathrm{QHC}$ and the set $\Gamma_2$ obtained from $\Gamma_1$ by taking the closure under the intuitionistic Bernays rules and modus ponens. It follows from Remark 1 that either $p$ is a theorem of $\mathrm{QHC}$ or there is a weak derivation of $p$ from $?\Gamma_2^H\cup\Gamma_2$. In either case, using Lemma 3 we obtain $?\Gamma_2^H\cup\Gamma_2^C\vdash p$. Since $\Gamma^H\vdash\Gamma_2^H$ and $\Gamma^C\vdash\Gamma_2^C$, we have The lemma is proved. § 5. Completeness of the logic $\mathrm{QHC}$ with respect to Kripke models with audit worldsIn the proof of the completeness theorem we follow the general outline of [32], using also some ideas from [4]. Assume that we have a language $L_M$ containing a countable set of constant symbols $M$. Definition 7. A set of formulae $\Gamma$ of the language $L_M$ is said to be $M$-saturated if Remark 2. 1) If $\Gamma$ is a theory, then $\Gamma\vdash \varphi$ is equivalent to $\varphi\in\Gamma$. 2) If a theory $\Gamma$ is $M$-saturated, then its classical fragment $\Gamma^{C}$ is a complete theory with respect to formulae of propositional sort: for each formula $p$ of propositional sort either $p\in\Gamma$ or $\neg p\in\Gamma$ (but not both, since $0\notin\Gamma$). This follows from the facts that $p\vee\neg p$ is a theorem of $\mathrm{QHC}$ and $\Gamma$ has the disjunction property. Lemma 8. Let $M$ be an at most countable set of constant symbols and $M'$ be its expansion by a countable set of additional constant symbols $\{c_1,c_2,\dots\}$. Let $\Gamma$ be a theory in the logic $\mathrm{QHC}$, $p$ be a formula of the language $L_M$ of the propositional sort, and let $\Gamma\nvdash p$. Then there exists an $M'$-saturated theory $\Gamma'$ of the language $L_{M'}$ such that $\Gamma\subseteq\Gamma'$ and $p\notin\Gamma'$. Proof. We only sketch the proof. A similar assertion for intuitionistic predicate calculus was proved in [32].
We consider the sequence of all existential formulae of the language $L_{M'}$
$$
\begin{equation*}
\exists\, v_0\ \Psi_0(v_0), \quad \exists\, v_1\ \Psi_1(v_1), \quad \exists\, v_2\ \Psi_2(v_2), \quad\dots
\end{equation*}
\notag
$$
and the sequence of all disjunctive formulae of the language $L_{M'}$
$$
\begin{equation*}
\Psi_0\vee\Psi'_0, \ \Psi_1\vee\Psi'_1, \ \Psi_2\vee\Psi'_2, \ \dots\,.
\end{equation*}
\notag
$$
For each $n$ we define the set of formulae $\Gamma_n$ as follows. The set $\Gamma_0$ coincides with $\Gamma$. Next, for each even $n$ find the first formula $\exists\, v\ \Psi(v)$ in the sequence of existential formulae which has not yet been considered and such that $\Gamma_n\vdash\exists\, v\ \Psi(v)$. Let $c$ be a constant symbol not contained in the formulae in $\Gamma_n$ or the formula $\exists\, v\ \Psi(v)$. Let $\widetilde\Gamma_{n+1}=\Gamma_n\cup\{\Psi(c)\}$. For each odd $n$ find the first formula $\Psi\vee\Psi'$ in the sequence of disjunctive formulae which has not yet been considered and such that $\Gamma_n\vdash\Psi\vee\Psi'$. If $\Gamma_n\cup\{\Psi\}\nvdash p$, then let $\widetilde\Gamma_{n+1}=\Gamma_n\cup\{\Psi\}$. Otherwise, let $\widetilde\Gamma_{n+1}=\Gamma_n\cup\{\Psi'\}$. Finally, set $\Gamma_{n+1}=[\widetilde\Gamma_{n+1}]$. We set $\Gamma'=\bigcup_{n=0}^{\infty}\Gamma_n$. Let us show that $\Gamma'\nvdash p$. It is sufficient to prove that $\Gamma_n\nvdash p$ for each $n$. We argue by induction on $n$. Indeed, for $n=0$ this follows from the assumptions of the lemma. Now suppose that we have $\Gamma_n\nvdash p$ for some $n$. We prove that $\Gamma_{n+1}\nvdash p$. Aiming at a contradiction assume that $\Gamma_{n+1}\vdash p$. Since $\Gamma_{n+1}$ is a theory, it follows that $p\in\Gamma_{n+1}$. By Lemma 7 we have
$$
\begin{equation*}
?\widetilde\Gamma^H_{n+1}\cup\widetilde\Gamma^C_{n+1}\vdash p.
\end{equation*}
\notag
$$
We consider two cases. If $n$ is even, then $\widetilde\Gamma_{n+1}=\Gamma_n\cup\{\Psi(c)\}$, where $\Gamma_n\vdash\exists\, v\ \Psi(v)$ and the constant symbol $c$ is not contained in $\exists\, v\ \Psi(v)$ or the formulae in $\Gamma_n$. Assume that $\Psi(c)$ is of propositional sort. Then, since $\widetilde\Gamma^C_{n+1}=\{\Psi(c)\}\cup\Gamma^C_n$ and $\widetilde\Gamma^H_{n+1}=\Gamma^H_{n}$, using Theorem 1 on deduction we obtain Since $\Gamma_n$ is a theory, we have $?\Gamma^H_n\subseteq\Gamma_n$, and we obtain We replace each occurrence of the constant symbol $c$ in this derivation by a variable $u$ not contained in the formulae of this derivation. It is easy to show that $\Gamma_n\vdash\Psi(u)\to p$. Using a Bernays rule we obtain $\Gamma_n\vdash\exists\, v\ \Psi(v)\to p$, and since ${\Gamma_n\vdash\exists\, v\ \Psi(v)}$, we have $\Gamma_n\vdash p$, which contradicts the assumption that $\Gamma_n\nvdash p$.Assume that $\Psi(c)$ is of problem sort. Since $\widetilde\Gamma^C_{n+1}=\Gamma^C_n$ and $?\widetilde\Gamma^H_{n+1}=\,?\Gamma^H_n\cup\{?\Psi(c)\}$, using Theorem 1 on deduction we obtain Since $\Gamma_n$ is a theory, we have $?\Gamma^H_n\subseteq\Gamma_n$, and we obtain We replace each occurrence of the constant symbol $c$ in this derivation by a variable $u$ not contained in the formulae of this derivation. We have ${\Gamma_n\vdash\,?\Psi(u)\to p}$. Using a Bernays rule we obtain $\Gamma_n\vdash\exists\, v\ ?\Psi(v)\to p$. Since $?\exists\, x\ \alpha(x)\leftrightarrow\exists\, x\ ?\alpha(x)$ is a theorem of the logic $\mathrm{QHC}$ (which was proved in [1]), we have Since $\Gamma_n\vdash\exists\, v\ \Psi(v)$ and $\Gamma_n$ is a theory, it follows that and we obtain $\Gamma_n\vdash p$, which contradicts the assumption that $\Gamma_n\nvdash p$.Let $n$ be odd. Then $\Gamma_n\vdash\Psi\vee\Psi'$. We set
$$
\begin{equation*}
\Delta=[\Gamma_n\cup\{\Psi\}]\quad\text{and} \quad \Delta'=[\Gamma_n\cup\{\Psi'\}].
\end{equation*}
\notag
$$
Clearly, it is sufficient to prove that $\Delta\vdash p$ and $\Delta'\vdash p$ imply that $\Gamma_n\cup\{\Psi\vee\Psi'\}\vdash p$, and since $\Gamma_n\vdash\Psi\vee\Psi'$, we obtain a contradiction with $\Gamma_n\nvdash p$. We consider the most difficult case: $\Psi\vee\Psi'$ is of problem sort. Then by Lemma 7
$$
\begin{equation*}
?\Gamma^H_n\cup\Gamma^C_n\cup\{?\Psi\}\vdash p\quad\text{and} \quad ?\Gamma^H_n\cup\Gamma^C_n\cup\{?\Psi'\}\vdash p.
\end{equation*}
\notag
$$
Theorem 1 on deduction yields
$$
\begin{equation*}
?\Gamma^H_n\cup\Gamma^C_n\vdash\,?\Psi\to p\quad\text{and} \quad ?\Gamma^H_n\cup\Gamma^C_n\vdash\,?\Psi'\to p.
\end{equation*}
\notag
$$
Since $\Gamma_n$ is a theory, we have $?\Gamma^H_n\subseteq\Gamma_n$, so $\Gamma_n\vdash\,?\Psi\to p$ and $\Gamma_n\vdash\,?\Psi'\to p$. Since $(q_1\to r)\to((q_2\to r)\to(q_1\vee q_2\to r))$ is an axiom of the logic $\mathrm{QHC}$, we obtain Next, $?(\alpha\vee\beta)\leftrightarrow(?\alpha\,\vee\,?\beta)$ is a theorem of $\mathrm{QHC}$ (proved in [1]), hence Since $\Gamma_n\vdash\Psi\vee\Psi'$ and $\Gamma_n$ is a theory, we have $\Gamma_n\vdash\,?(\Psi\vee\Psi')$, so that $\Gamma_n\vdash p$, which contradicts the assumption $\Gamma_n\nvdash p$.
Thus, we have shown that $\Gamma'\nvdash p$. Clearly, $\Gamma'$ contains all theorems of $\mathrm{QHC}$. The proof of the fact that $\Gamma'$ is closed under weak derivability and has the disjunction and existence properties is analogous to a similar theorem in [32]. Let us show that $?\Gamma'^H\subseteq\Gamma'^C$. In fact, if $\alpha\in\Gamma'^H$, then $\alpha\in\Gamma^H_n$ for some $n$, and since $\Gamma_n$ is a theory, we have $?\alpha\in\Gamma^C_n$, that is, $?\alpha\in\Gamma'$. Thus, $\Gamma'$ is a theory. Finally, it is a consistent theory by Lemma 5 (recall that it is sufficient for consistency to check that $\Gamma'\nvdash0$). Lemma 8 is proved. Definition 8. An $M$-saturated theory $\Gamma$ is reflexive if $\Gamma_{?}\subseteq\Gamma$, where $\Gamma_{?}=\{\alpha\mid\,?\alpha\in\Gamma\}$. Lemma 9. Let $\Gamma$ be a theory, and let $\Gamma\nvdash p$ and $\Delta=[\Gamma_?\cup\Gamma]$. Then $\Delta\nvdash p$. Proof. Aiming at a contradiction, assume that $\Delta\vdash p$. By Lemma 7 we have Since $?\Gamma_?\subseteq\Gamma^C$, we obtain $?\Gamma^H,\Gamma^C,\Gamma_?\vdash p$. Since $\Gamma$ is a theory, we have $?\Gamma^H\subseteq\Gamma^C$ and $\Gamma^C,\Gamma_?\vdash p$. Because $\Gamma_?$ is a set of formulae of problem sort, Lemma 3 yields $\Gamma^C\vdash p$, which contradicts the assumption that $\Gamma\nvdash p$.
The lemma is proved. Lemma 10. Let $M$ be an at most countable set of constant symbols and $M'$ be its expansion by a countable set of additional constant symbols $\{c_1,c_2,\dots\}$. Given an $M$-saturated theory $\Gamma$, if $\Gamma\nvdash p$, then there exists a reflexive $M'$-saturated theory $\Delta$ such that $\Gamma\subseteq\Delta$ and $\Delta\nvdash p$. Proof. Let $M=M_0\subseteq M_1\subseteq M_2\subseteq\dots\subseteq M'$, where $M_{i+1}$ is an expansion of $M_i$ by a countable set of constant symbols, and let $M'=\bigcup_{i=0}^{\infty}M_i$.
We define a sequence of theories $\Gamma^0,\Gamma^1,\Gamma^2,\dots$, where $\Gamma^i$ is an $M_i$-saturated theory, as follows. Let $\Gamma_0=\Gamma$. For $n\geqslant0$ set:
$$
\begin{equation*}
\begin{gathered} \, \Gamma^{n+1}\text{ be an }M_{n+1}\text{-saturated theory} \\ \text{such that }\Gamma'_n=\Gamma^n_{?}\cup\Gamma^n\subseteq\Gamma^{n+1}\text{ and }\Gamma^{n+1}\nvdash p. \end{gathered}
\end{equation*}
\notag
$$
(This is possible since $\Gamma^n\nvdash p$ implies that $\Gamma'_n\nvdash p$ by Lemma 9. Next we extend $\Gamma'_n$ to an $M_{n+1}$-saturated theory $\Gamma_{n+1}$ using Lemma 8.)
We set Clearly, $\Delta$ is a theory. Let us show that $\Delta$ has the disjunction property. Assume that $\psi_1\vee\psi_2\in\Delta$. Then $\psi_1\vee\psi_2\in\Gamma^n$ for some $n\geqslant0$. Since $\Gamma^n$ has the disjunction property, either $\psi_1\in\Gamma^n$ or $\psi_2\in\Gamma^n$. Hence $\psi_1\in\Delta$ or $\psi_2\in\Delta$. Let us show that $\Delta$ has the existence property. Assume that $\exists\, v\ \psi(v)\in\Delta$. Then $\exists\, v\ \psi(v)\in\Gamma^n$ for some $n\geqslant0$. Since $\Gamma^n$ has the existence property, we have $\psi(c)\in\Gamma^n$ for some constant symbol $c\in M_n\subseteq M'$. Hence $\psi(c)\in\Delta$. Let us show that $\Delta$ is reflexive, that is, $\Delta_{?}\subseteq\Delta$. In fact, let $\alpha\,{\in}\,\Delta_{?}$. Then ${?\alpha\,{\in}\,\Delta}$, that is, $?\alpha\in\Gamma^n$ for some $n$. Therefore, $\alpha\in\Gamma^n_{?}$ and $\alpha\in\Gamma^{n+1}$, that is, $\alpha\in\Delta$. It remains to show that $\Delta\nvdash p$. In fact, otherwise $p\in\Gamma^n$ for some $n$, which is a contradiction. It follows that $\Delta\nvdash p$. The lemma is proved. Lemma 11. Let $M$ be an at most countable set of constant symbols and $M'$ be its expansion by a countable set of additional constant symbols $\{c_1,c_2,\dots\}$. Given a theory $\Gamma$ and a formula $p$ in the language $L_M$, if $\Gamma\nvdash\,!p$, then there exists a reflexive $M'$-saturated theory $\Delta$ such that $\Gamma^H\subseteq\Delta$ and $p\notin\Delta$. Proof. Consider the set of formulae $\Gamma'=\Gamma^H\cup\,?\Gamma^H$. Let us show that $\Gamma'\nvdash p$. Indeed, aiming at a contradiction assume that $\Gamma'\vdash p$. Then by Lemma 3 we have $?\Gamma^H\vdash p$. Hence $!?\Gamma^H\vdash\, !p$ by Lemma 2. Since $\alpha\to\,!?\alpha$ is an axiom of the logic $\mathrm{QHC}$, we have $\Gamma^H\vdash\,!?\Gamma^H$, and eventually we obtain $\Gamma^H\vdash\,!p$, which contradicts the assumption that $\Gamma\nvdash\,!p$. Therefore, $\Gamma'\nvdash p$. By Lemma 10 there exists a reflexive $M'$-saturated theory $\Delta$ containing $\Gamma'$ (and hence $\Gamma^H$) such that $p\notin\Delta$, as required.
The lemma is proved. Theorem 3. If an $M$-saturated theory $\Gamma$ in the language $L_M$ is reflexive, then there exist a Kripke model $\mathcal K=(W,\preccurlyeq,\mathrm{Aud},D,\models)$ with audit worlds and its audit world $x$ such that for each formula $\alpha$ of problem sort of the language $L_M$ and for each formula $p$ of propositional sort of the language $L_M$ Proof. We construct a Kripke model with audit worlds $\mathcal K$ as follows. We define a sequence of sets of constant symbols $M_0,M_1,M_2,\dots$ recursively as follows: $M_0=M$, and $M_{i+1}$ is obtained from $M_i$ by adding a countable set of new constant symbols. Let $W$ be the family of all theories $\Delta$ such that:
For $\Delta_1,\Delta_2\in W$ let $\Delta_1\preccurlyeq\Delta_2\rightleftharpoons\Delta_1^H\subseteq\Delta_2^H$; $\Delta\in\mathrm{Aud}$ if and only if $\Delta$ is reflexive. Next, assume that $\Delta\in W$ is an $M_i$-saturated theory. Then let $D_{\Delta}=M_i$, and if $A(c_1,\dots,c_n)$ is an atomic formula with constant symbols $c_1,\dots,c_n\in M_i$, then set
$$
\begin{equation*}
\Delta\models A(c_1,\dots,c_n)\rightleftharpoons A(c_1,\dots,c_n)\in\Delta.
\end{equation*}
\notag
$$
Let us check that we have indeed defined a Kripke model with audit worlds. Clearly, $\preccurlyeq$ is a partial order on $W$ and $\mathrm{Aud}\subseteq W$. Next,
$$
\begin{equation*}
\forall\,\Delta_1\in W\ \exists\,\Delta_2\in W\ (\Delta_1\preccurlyeq\Delta_2\wedge\Delta_2\in\mathrm{Aud})
\end{equation*}
\notag
$$
by Lemma 10 (take $0$ as $p$, for example). Moreover, the monotonicity of the satisfiability relation $\models$ holds for atoms of problem sort (since $\Delta_1\preccurlyeq\Delta_2\Leftrightarrow\Delta_1^H\subseteq\Delta_2^H$). Finally, it follows from the construction that
$$
\begin{equation*}
\Delta_1\preccurlyeq\Delta_2\Rightarrow D_{\Delta_1}\subseteq D_{\Delta_2}.
\end{equation*}
\notag
$$
Thus, we have constructed the Kripke model with audit worlds $\mathcal K=(W,\preccurlyeq , \mathrm{Aud},D,\models)$. Let us prove that for each $\Delta\in W$ the following holds: if $\Delta$ is $M_i$-saturated, then for each closed formula $A$ of the language $L_{M_i}$ (if $A$ is a formula of propositional sort, then we consider this equivalence only for ${\Delta\in\mathrm{Aud}}$). Then we obtain the statement of the theorem immediately by taking ${x=\Gamma}$.The proof goes by induction on the build-up of a formula $A$. For atomic formulae this holds by the definition of $\models$. The proof of the induction step in the cases of intuitionistic connectives and quantifiers is carried out using the method described in [32] for intuitionistic predicate calculus. We give a proof for the most difficult case, the induction step for quantifiers. Fix a formula $\alpha(x)$ with a single free variable $x$. Then since $\alpha(c)$ is a closed formula for each constant symbol $c$, we have the following sequence of equivalences:
$$
\begin{equation*}
\Delta\models\exists\, x\ \alpha(x)\Leftrightarrow\exists\, c\in D_{\Delta} \ (\Delta\models\alpha(c))\Leftrightarrow\exists\, c\in D_{\Delta}\ (\alpha(c)\in\Delta)\Leftrightarrow \exists\, x\ \alpha(x)\in\Delta.
\end{equation*}
\notag
$$
In the last equivalence the implication from left to right holds since $\Delta$ is closed under weak derivability, and the implication from right to left holds since $\Delta$ has the existence property.
Consider the following sequence of equivalences for the universal quantifier:
$$
\begin{equation*}
\begin{aligned} \, &\Delta\models\forall\, x\ \alpha(x)\Leftrightarrow\forall\,\Delta'\succcurlyeq\Delta\ \forall\, c\in D_{\Delta'}\ (\Delta'\models\alpha(c)) \\ &\qquad \Leftrightarrow \forall\,\Delta'\succcurlyeq\Delta\ \forall\, c\in D_{\Delta'} \ (\alpha(c)\in\Delta')\Leftrightarrow\forall\, x\ \alpha(x)\in\Delta. \end{aligned}
\end{equation*}
\notag
$$
Only the last equivalence needs an explanation. In fact, the implication from right to left holds since $\Delta$ is closed under weak derivability. Let us prove the implication from left to right. Assume that
$$
\begin{equation*}
\forall\,\Delta'\succcurlyeq\Delta\ \forall\, c\in D_{\Delta'} \ (\alpha(c)\in\Delta'),
\end{equation*}
\notag
$$
but the condition that $\forall\, x\ \alpha(x)\in\Delta$ does not hold. It follows that $\Delta\nvdash\forall\, x\ \alpha(x)$. Then $\Delta\nvdash\alpha(c)$ for each constant symbol $c\notin D_{\Delta}$. In fact, otherwise, replacing each occurrence of the constant symbol $c$ with a variable $u$ not contained in this derivation, we obtain a derivation from $\Delta$ of the formula $\alpha(u)$, and then we obtain $\Delta\vdash\forall\, u\ \alpha(u)$, which contradicts the assumption that $\Delta\nvdash\forall\, x\ \alpha(x)$. If $\Delta$ is an $M_i$-saturated theory, then for $c\in M_{i+1}\setminus M_i$ we have $\Delta\nvdash\alpha(c)$. By Lemma 8 there exists an $M_{i+2}$-saturated theory $\Delta'$ such that $\Delta\preccurlyeq\Delta'$ and $\alpha(c)\notin\Delta'$, which contradicts the initłassumption.
In the cases of classical connectives and quantifiers the induction step can be proved using even simpler reasoning (or one can define an ‘order’ on the audit worlds by $\Delta^1\preccurlyeq_{\text{class.}}\Delta^2$ if $\Delta^1=\Delta^2$ and then simply repeat the proof for the intuitionistic case). It remains to prove the induction step in the case of modal operators. Assume that $?\alpha\in\Delta$ (we have $\Delta\in\mathrm{Aud}$ since $?\alpha$ is of propositional sort). As $\Delta$ is a reflexive theory, it follows that $\alpha\in\Delta$. By the induction hypothesis $\Delta\models\alpha$. Hence $\Delta\models\,?\alpha$ by the definition of $\models$. Assume that $\Delta\models\,?\alpha$. Then $\Delta\models\alpha$ by the definition of $\models$. By the induction hypothesis $\alpha\in\Delta$. Hence $?\alpha\in\Delta$, since $\Delta$ is a theory. Assume that $!p\in\Delta$. We need to show that $\Delta\models\,!p$, that is,
$$
\begin{equation*}
\forall\,\Delta'\in\mathrm{Aud}\ (\Delta\preccurlyeq\Delta'\Rightarrow\Delta'\models p).
\end{equation*}
\notag
$$
Fix an arbitrary $\Delta'\in\mathrm{Aud}$ such that $\Delta'\succcurlyeq\Delta$. Since $!p\in\Delta$, we have $!p\in\Delta'$ ($!p$ is of problem sort). Because $\Delta'$ is a theory, we have $?!p\in\Delta'$. Since $?!p\,{\to}\, p$ is a theorem of $\mathrm{QHC}$, we obtain $p\in\Delta'$. By the induction hypothesis this means that $\Delta'\models p$. Hence $\Delta\models\,!p$.
Assume that $!p\notin\Delta$. If $\Delta$ is an $M_i$-saturated theory, then by Lemma 11 there exists a reflexive $M_{i+1}$-saturated theory $\Delta'$ such that $\Delta^H\subseteq\Delta'$ and $p\notin\Delta'$. Thus, we have found a reflexive theory $\Delta'\succcurlyeq\Delta$ such that $\Delta'\nvDash p$. This means that $\Delta\nvDash\,!p$. Theorem 3 is proved. Theorem 4. For each consistent theory $\Gamma$ in the logic $\mathrm{QHC}$ there exist a Kripke model $\mathcal K$ and an audit world $x$ of it such that all formulae in $\Gamma$ are true at this world of the model $\mathcal K$. Proof. Let $\Gamma$ be a consistent theory in the logic $\mathrm{QHC}$ in the signature $\Omega$. Then $\Gamma\nvdash0$. By Lemma 8 there exists an $M$-saturated set of formulae $\Gamma'$ of the signature $\Omega'$ that is obtained by adding to $\Omega$ a countable set of additional constant symbols such that $\Gamma\subseteq\Gamma'$. By Lemma 10 there exists a reflexive $M'$-saturated set of formulae $\Gamma''$ of the signature $\Omega''$ that is obtained by adding to $\Omega'$ a countable set of additional constant symbols such that $\Gamma'\subseteq\Gamma''$. By Theorem 3 there exists a Kripke model with audit worlds $\mathcal K$ such that all formulae in $\Gamma''$ are true at some world of this model. Since $\Gamma\subseteq\Gamma''$, $\mathcal K$ is a Kripke model of the set $\Gamma$.
The theorem is proved. This theorem yields the following corollary. Theorem 5 (completeness of $\mathrm{QHC}$ with respect to Kripke models with audit worlds). If a formula $A$ of problem (propositional) sort of a language $\Omega$ is true at every world (audit world, respectively) of every Kripke model with audit worlds for the language $\Omega$, then $A$ is derivable in $\mathrm{QHC}$. § 6. Kripke models of the logic $\mathrm{QH4}$ and conservativityThe logic $\mathrm{QH4}$ is a predicate version of the propositional modal logic $\mathrm{H4}$. The logic $\mathrm{H4}$ was investigated by Artemov and Protopopescu in [4] as an epistemic intuitionistic logic with knowledge modality $\mathbf K$; it was denoted there by $\mathrm{IEL}^+$. In the same work Kripke models with audit worlds of $\mathrm{H4}$ were constructed, and the soundness and completeness theorem was proved. In [3] the finite model property for this class of models of the logic $\mathrm{H4}$ was pointed out, and it was also proved that the logic $\mathrm{HC}$ is a conservative extension of the logic $\mathrm{H4}$. In [4] and also in its journal version [22] the logics $\mathrm{IEL}^-$ and $\mathrm{IEL}$, which are weaker systems close to the logic $\mathrm{IEL}^+$, were investigated. In the work [33] by Su and Sano Kripke-style semantics for the logics $\mathrm{QIEL}^-$ and $\mathrm{QIEL}$, the predicate versions of $\mathrm{IEL}^-$ and $\mathrm{IEL}$, were considered. The completeness theorem for both $\mathrm{QIEL}^-$ and $\mathrm{QIEL}$ with respect to Kripke semantics was proved there. The method in [33] was based on constructing sequent calculus for these logics and considering the set of saturated sequents as a Kripke model. Below we give a different proof of the completeness theorem for the logic $\mathrm{QIEL}^+$ (or $\mathrm{QH4}$), namely, we consider intuitionistic saturated theories. This proof is close to the proof of the completeness theorem for the propositional logic $\mathrm{IEL}^+$ with respect to Kripke semantics (see [4]). Terms of the logic $\mathrm{QH4}$ are individual variables and constant symbols. The language of $\mathrm{QH4}$ contains the intuitionistic connectives $\wedge,\vee,\to,\leftrightarrow$ and $\neg$, the quantifiers $\forall$ and $\exists$ and the modal operator $\nabla$, and also predicate symbols of a single sort (by contrast to the logic $\mathrm{QHC}$). The notion of a formula of $\mathrm{QH4}$ is defined in the standard way. The axioms and inference rules of $\mathrm{QH4}$ are the axioms and inference rules of the intuitionistic predicate calculus and the following axiom schemata: $(1^{\nabla})$ $\alpha\to\nabla\alpha$; $(2^{\nabla})$ $\nabla\nabla\alpha\to\nabla\alpha$; $(3^{\nabla})$ $\nabla\bot\to\bot$; $(4^{\nabla})$ $\nabla(\alpha\to\beta)\to(\nabla\alpha\to\nabla\beta)$. For the logic $\mathrm{QH4}$ one can define the notions of a derivation, a quasiderivation from hypotheses and a derivation from hypotheses similarly to the case of the logic $\mathrm{QHC}$. Let us describe the Kripke models with audit worlds of the logic $\mathrm{QH4}$. Let $\Omega$ be a language of the logic QH4 (without functional symbols). A Kripke frame with audit worlds for this language is a tuple $\mathcal K=(W,\preccurlyeq,\mathrm{Aud})$, where $(W,\preccurlyeq)$ is a partially ordered set, $\mathrm{Aud}\subseteq W$< and the following property holds:
$$
\begin{equation*}
\forall\, a\in W\ \exists\, b\in W\ (a\preccurlyeq b\wedge b\in\mathrm{Aud}).
\end{equation*}
\notag
$$
A Kripke model of the logic $\mathrm{QH4}$ with audit worlds is a Kripke frame with a function $D$ that maps each $a\in W$ to a nonempty set $D_a$ and with a valuation of atoms $\models$. It is assumed that if $a\preccurlyeq b$, then $D_a\subseteq D_b$. If the language $\Omega$ contains a constant symbol $c$, then it is assigned an object $\overline c\in D_{a}$ for each $a\in W$ (we identify $c$ and $\overline c$). The valuation of atoms $\models$ is a binary relation between the set $W$ and the set of all atoms of the form $A(x_1,\dots,x_n)$, where $A$ is an $n$-ary predicate symbol of the signature $\Omega$ and $x_1,\dots,x_n\in\bigcup_{a\in W}D_a$. The notation $a\models A(x_1,\dots,x_n)$ can be read in the standard way as: “$A(x_1,\dots,x_n)$ is true at $a$”. The relation $\models$ satisfies the following property: if $a\models A(x_1,\dots,x_n)$, then $\{x_1,\dots,x_n\}\subseteq D_a$, and if $A(x_1,\dots,x_n)$ is an atomic formula and $a\preccurlyeq b$, then $b\models A(x_1,\dots,x_n)$ (that is, monotonicity holds for atoms). The satisfiability relation for all formulae of $\mathrm{QH4}$ is defined using recursion on the build-up of a formula. For the connectives $\wedge,\vee,\to,\leftrightarrow$ and $\neg$ and the quantifiers $\forall$ and $\exists$ the inductive step in the definition of the satisfiability relation is the same as for Kripke models of intuitionistic predicate calculus. Let us define the satisfiability relation at the inductive step for the modal operator $\nabla$:
$$
\begin{equation*}
a\models\nabla\varphi\Leftrightarrow\forall\, b\in W\ (a\preccurlyeq b\wedge b\in\mathrm{Aud}\Rightarrow b\models\varphi).
\end{equation*}
\notag
$$
Similarly to Lemma 1 we can show that monotonicity holds not only for atoms but for arbitrary formulae. Theorem 6 (soundness). If a closed formula of the language $\Omega$ is derivable in $\mathrm{QH4}$, then it is valid in every Kripke model of the logic $\mathrm{QH4}$ for the language $\Omega$. To prove this theorem, as in Theorem 2 we have to check that if a formula is derivable in $\mathrm{QH4}$, then its universal closure is valid in every Kripke model. Clearly, it is sufficient to check that the universal closure of each axiom is valid in every Kripke model and the inference rules preserve this property. For the axioms and inference rules of intuitionistic predicate calculus this was done in Theorem 2. For the additional axioms of $\mathrm{QH4}$ the proof can be found in [4] (it is clear that models of the logic $\mathrm{QH4}$ are expansions of models of the logic $\mathrm{H4}$). As before, we consider $M$-saturated theories but in the logic $\mathrm{QH4}$, rather than in $\mathrm{QHC}$ (with the following difference: there is no requirement that $?\Gamma^H\subseteq\Gamma^C$ for $M$-saturated theories in $\mathrm{QH4}$). Recall: $\Gamma\vdash\varphi$ means that there is a derivation of $\varphi$ from the hypotheses $\Gamma$; $[\Gamma]$ denotes the smallest theory containing $\Gamma$. Definition 9. An $M$-saturated theory $\Gamma$ in the logic $\mathrm{QH4}$ is reflexive if $\Gamma_{\nabla}\subseteq\Gamma$, where $\Gamma_{\nabla}=\{\varphi\mid\nabla\varphi\in\Gamma\}.$ Lemma 12. Let $M$ be an at most countable set of constant symbols and $M'$ be its expansion by a countable set of additional constant symbols $\{c_1,c_2,\dots\}$. Then for any set of formulae $\Gamma$ and a formula $\beta$ in the language $L_M$, if $\Gamma\nvdash\nabla\beta$, then there exists a reflexive $M'$-saturated theory $\Delta$ such that $\Gamma\subseteq\Delta$ and $\Delta\nvdash\beta$. Proof. The proof of this lemma is very close to the proof of Lemma 10. We set
$$
\begin{equation*}
M=M_0\subseteq M_1\subseteq M_2\subseteq\dots\subseteq M',
\end{equation*}
\notag
$$
where $M_{i+1}$ is an expansion of $M_i$ by a countable set of constant symbols and $M'=\bigcup_{i=0}^{\infty}M_i$. Note that if $\Sigma\nvdash\nabla\varphi$, then $\Sigma_{\nabla}\nvdash\nabla\varphi$ (the proof can be found in Lemma 5 in [4] and Lemma 7 in [3]).
Similarly to Lemma 8, for each set of formulae $\Gamma$ and a formula $\alpha$ of the language $M$, if $\Gamma\nvdash\alpha$, then there exists an $M'$-saturated theory $\Gamma'$ containing $\Gamma$ such that $\Gamma'\nvdash\alpha$ ($M'$ is an expansion of $M$ by a countable set of additional constant symbols). We define the sequence of theories $\Gamma^0,\Gamma^1,\Gamma^2,\dots$ as follows. Let $\Gamma^0=[\Gamma]$ and set:
$$
\begin{equation*}
\Gamma^{n+1}\text{ is an }M_{n+1}\text{-saturated theory such that } \Gamma^n_{\nabla}\subseteq\Gamma^{n+1}\text{ and }\Gamma^{n+1}\nvdash\beta.
\end{equation*}
\notag
$$
Thus, we have the following sequence of inclusions:
$$
\begin{equation*}
\Gamma^0\subseteq \Gamma^0_{\nabla}\subseteq\Gamma^1\subseteq \Gamma^1_{\nabla}\subseteq\Gamma^2\subseteq \Gamma^2_{\nabla}\subseteq\dotsb.
\end{equation*}
\notag
$$
Let Let us prove that $\Delta$ has the required properties. There is a proof of a similar result in Lemma 7 in [3], but for the logic $\mathrm{H4}$, rather than for $\mathrm{QH4}$. Clearly, a similar reasoning can be used to show that $\Delta$ is a theory, $\Delta_{\nabla}\,{\subseteq}\,\Delta$, $\Delta\nvdash\beta$ and $\Delta$ has the disjunction property. It remains to prove that $\Delta$ has the existence property.
Assume that $\exists\, v\ \varphi(v)\in\Delta$. Then $\exists\, v\ \varphi(v)\in\Gamma^n$ for some $n>0$. Since $\Gamma^n$ is an $M_n$-saturated theory, we have $\varphi(c)\in\Gamma^n$ for some constant symbol $c$. Hence $\varphi(c)\in\Delta$. The lemma is proved. Theorem 7. If the set of formulae $\Gamma$ of the language $L_M$ is an $M$-saturated theory, then there exists a Kripke model $\mathcal K=(W,\preccurlyeq,\mathrm{Aud},D,\models)$ with audit worlds of the logic $\mathrm{QH4}$ such that for each formula $A$ of the language $L_M$ Proof. We construct a Kripke model of the logic $\mathrm{QH4}$ as follows (as in Theorem 3). We define a sequence of sets of constant symbols $M_0,M_1,M_2,\dots$ recursively: ${M_0=M}$, and $M_{i+1}$ is obtained from $M_i$ by adding a countable set of new constant symbols. Let $W$ be the family of all theories $\Delta$ such that:
For $\Delta_1,\Delta_2\in W$ let $\Delta_1\preccurlyeq\Delta_2\rightleftharpoons\Delta_1\subseteq\Delta_2$; $\Delta\in\mathrm{Aud}$ if and only if $\Delta$ is reflexive. Next, assume that $\Delta\in W$ is an $M_i$-saturated theory. Then let $D_{\Delta}=M_i$, and if $A(c_1,\dots,c_n)$ is an atomic formula with constant symbols $c_1,\dots,c_n\in M_i$, then set
$$
\begin{equation*}
\Delta\models A(c_1,\dots,c_n)\rightleftharpoons A(c_1,\dots,c_n)\in\Delta.
\end{equation*}
\notag
$$
Let us check that we have indeed defined a Kripke model of the logic $\mathrm{QH4}$. Clearly, $\preccurlyeq$ is a partial order on $W$ and $\mathrm{Aud}\subseteq W$. We show that
$$
\begin{equation*}
\forall\,\Delta_1\in W\ \exists\,\Delta_2\in W\ (\Delta_1\preccurlyeq\Delta_2\wedge\Delta_2\in\mathrm{Aud}).
\end{equation*}
\notag
$$
Fix an arbitrary $\Delta_1\in W$. Assume that $\Delta_1$ is an $M_i$-saturated theory. Since $\Delta$ is consistent, we have $\Delta\nvdash\nabla\bot$, and by Lemma 12 there exists a reflexive $M_{i+1}$-saturated theory $\Delta_2$ such that $\Delta_1\subseteq\Delta_2$ and $\bot\notin\Delta_2$. Thus, we have found the required theory $\Delta_2$. Moreover, the monotonicity of the satisfiability relation $\models$ holds for atoms (since $\Delta_1\preccurlyeq\Delta_2\Leftrightarrow\Delta_1\subseteq\Delta_2$). Finally,
$$
\begin{equation*}
\Delta_1\preccurlyeq\Delta_2\Rightarrow D_{\Delta_1}\subseteq D_{\Delta_2}
\end{equation*}
\notag
$$
by construction.
Thus, we have constructed the Kripke model with audit worlds $\mathcal K=(W,\preccurlyeq,\mathrm{Aud},D,\models)$. Let us prove that for each $\Delta\in W$ the following holds: if $\Delta$ is $M_i$-saturated, then for each formula $A$ of the language $L_{M_i}$ The proof uses induction on the build-up of a formula $A$. For atomic formulae this holds by the definition of $\models$. For connectives and quantifiers the proof is carried out using the method described in [32] (the case of the induction step for quantifiers was considered in Theorem 3). It remains to prove the induction step for the modal operator $\nabla$. Let $\nabla\varphi\in\Delta$. We need to prove that $\Delta\models\nabla\varphi$, that is, $\forall\,\Delta'\supseteq\Delta$ if $\Delta'$ is reflexive, then $\Delta'\models\varphi$. Indeed, fix a reflexive theory $\Delta'\supseteq\Delta$. Since $\nabla\varphi\in\Delta$, we have $\nabla\varphi\in\Delta'$. Because $\Delta'$ is reflexive, we obtain $\varphi\in\Delta'$. The induction hypothesis yields $\Delta'\models\varphi$. Thus, $\Delta\models\nabla\varphi$. Let $\nabla\varphi\notin\Delta$. By Lemma 12 there exists a reflexive theory $\Delta'\supseteq\Delta$ such that ${\varphi\notin\Delta'}$. By the induction hypothesis $\Delta'\nvDash\varphi$. Thus, $\Delta\nvDash\nabla\varphi$. The theorem is proved. Theorem 7 has two important corollaries. Theorem 8 (completeness of $\mathrm{QH4}$). For each consistent set of formulae $\Gamma$ of the logic $\mathrm{QH4}$ there exists a Kripke model $\mathcal K$ of $\mathrm{QH4}$ such that all formulae in $\Gamma$ are true at every world of the model $\mathcal K$. The proof is analogous to the proof of Theorem 4. Theorem 9 (conservativity). The logic $\mathrm{QHC}$ is a conservative extension of the logic $\mathrm{QH4}$. Proof. Consider a formula $\varphi$ not derivable in the logic $\mathrm{QH4}$. Theorem 8 yields a Kripke countermodel $\mathcal K$ of the logic $\mathrm{QH4}$ for $\varphi$. Let $\widetilde\varphi$ be obtained from $\varphi$ by replacing each occurrence of the symbol $\nabla$ with $!?$. The Kripke countermodel of $\mathrm{QHC}$ for the formula $\widetilde\varphi$ coincides with $\mathcal K$, since the truth of formulae in the language of $\mathrm{QH4}$ is coherent in both models (see the proof of Theorem 5 in [3] for propositional versions of these logics; it is clear that the truth definition for quantifiers is also coherent).
The theorem is proved. § 7. Disjunction and existence propertiesThe presentation in this section is close to [32] in many ways. Let $T$ be a consistent theory in the logic $\mathrm{QHC}$. We say that a theory $T$ has the disjunction property if $\alpha\vee\beta\in T$ implies that $\alpha\in T$ or $\beta\in T$ (here $\alpha$ and $\beta$ are arbitrary formulae of problem sort). A theory $T$ has the existence property if $\exists\, x\ \alpha(x)\in T$ implies that there exists a constant symbol $c$ such that ${\alpha(c)\in T}$ (here $\alpha$ is an arbitrary formula of problem sort). Clearly, talking about the existentionality of a theory makes sense only if its language contains at least one constant symbol. Assume that we have two Kripke models with audit worlds
$$
\begin{equation*}
\mathcal K_1=(W_1, \preccurlyeq_1, \mathrm{Aud}_1,D_1,\models_1)\quad\text{and} \quad \mathcal K_2=(W_2,\preccurlyeq_2,\mathrm{Aud}_2,D_2,\models_2)
\end{equation*}
\notag
$$
of the logic $\mathrm{QHC}$ and that $W_1\cap W_2=\varnothing$. The sum of these models is the model $\mathcal K=(W,\preccurlyeq,\mathrm{Aud},D,\models)$ such that:
The sum of the models $\mathcal K_1$ and $\mathcal K_2$ is denoted by $\mathcal K_1+\mathcal K_2$. Clearly, for each formula $A$ we have
$$
\begin{equation*}
(\mathcal K_1+\mathcal K_2)\models A\Leftrightarrow (\mathcal K_1\models_1 A\text{ and }\mathcal K_2\models_2 A).
\end{equation*}
\notag
$$
(Here $\mathcal K\models A$ means that a formula $A$ of problem (propositional) sort is true at every world (audit world, respectively) of the Kripke model $\mathcal K$.) It follows that the sum of two models of a theory is also a model of this theory. The sum $\sum_{i\in I}\mathcal K_i$ of an arbitrary family of Kripke models $\{\mathcal K_i\mid i\in I\}$ is defined similarly. In this case, if each $\mathcal K_i$ ($i\in I$) is a model of a theory $T$, then the sum $\sum_{i\in I}\mathcal K_i$ is also a model of this theory. Given a Kripke model with audit worlds $\mathcal K=(W,\preccurlyeq,\mathrm{Aud}, D,\models)$ of the language $L_M$, where $M\ne\varnothing$, we define a model $\mathcal K'=(W',\preccurlyeq',\mathrm{Aud}',D',\models')$ as follows:
It is clear that the operation $'$ produces a Kripke model with audit worlds. Theorem 10. If the class of models of a theory $T$ is closed under the operation $'$, then the theory $T$ has the disjunctive and existence properties. Proof. The reasoning is the same as in the proof of a similar theorem for the intuitionistic predicate calculus (see [32]). We sketch the proof.
We show that $T$ has the disjunction property. In fact, if $T\nvdash \alpha$ and $T\nvdash\beta$, then there exist Kripke countermodels $\mathcal K_1$ and $\mathcal K_2$ for $\alpha$ and $\beta$, respectively. Then $\mathcal K=(\mathcal K_1+\mathcal K_2)'$, which is a model of the theory $T$ by assumption, is a countermodel for $\alpha\vee\beta$. We show that $T$ has the existence property. In fact, if $T\nvdash\alpha(c)$ for each constant symbol $c\in M$, then for each constant symbol $c\in M$ there exists a Kripke countermodel with audit worlds $\mathcal K_c$ of the theory $T$ such that $\mathcal K_c\nvDash A(c)$. Then $\mathcal K=(\sum_{c\in M}\mathcal K_c)'$, which is a model of the theory $T$ by assumption, is a countermodel for $\exists\, x\ \alpha(x)$. The theorem is proved. Corollary. If the signature $\Omega$ contains at least one constant symbol, then $\mathrm{QHC}$ (in this signature) has the disjunction and existence properties. Since the class of models of $\mathrm{QHC}$ in the signature $\Omega$ is closed under the operation $'$, it remains to use Theorem 10 to finish the proof. We have established the disjunction property for $\mathrm{QHC}$ only in the case when the signature $\Omega$ contains at least one constant symbol. This restriction is not essential as the following theorem shows. The proof is the same as that of a similar theorem in [32]. Remark 3. Since the logic $\mathrm{QHC}$ is a conservative extension of the logic $\mathrm{QH4}$, the logic $\mathrm{QH4}$ also has the disjunction and existence properties. AcknowledgementsThe author is grateful to her scientific advisor L. D. Beklemishev for his invaluable assistance at all stages of work on this paper. The author also thanks the referee for valuable comments and for pointing out to her the paper [33], which is close to the results in § 6. The author is a winner of the stipend competition of the Theoretical Physics and Mathematics Advancement Foundation “BASIS”, and she is grateful to the jury and sponsors of the competition.
Citation in format AMSBIB
\Bibitem{Ono22} |
|
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
|
Contact us: |
Terms of Use
|
Registration to the website |
Logotypes |
|