A. A. Onoprienko, “Bitopological models of intuitionistic epistemic logic”, Russian Math. Surveys, 79:1 (2024), 179

We consider the logic $\mathrm{H4}$, which is an extension of the intuistionistic propositional logic by a modality $\nabla$ satisfying the following schemes of axioms: $(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)$.

Artemov and Protopopescu [1], [2] investigated the intuistionistic epistemic logic with knowledge modality and constructed three formal systems $\mathrm{IEL}^-$, $\mathrm{IEL}$, and $\mathrm{IEL}^+$, the last of which coincides with $\mathrm{H4}$. The logic without axiom $(3^{\nabla})$ was earlier considered by Goldblatt [6], Dragalin [4], and Fairtlough and Mendler [5]. The intiuonistic logic extended by axioms $(1^{\nabla})$, $(2^{\nabla})$, and $(4^{\nabla})$ appeared apparently for the first time in Curry’s book [3]. Macnab [8] considered models of intuitionistic logic with axioms $(1^{\nabla})$, $(2^{\nabla})$, and $(4^{\nabla})$, which were based on fixing a topological space and a distinguished subset of it. The logic $\mathrm{H4}$ is obtained by adding axiom $(3^{\nabla})$, which corresponds precisely to the assumption that the distinguished subset is dense.

Melikhov [10] introduced the joint logic of problems and propositions $\mathrm{QHC}$, which is a conservative extension of the predicate version of $\mathrm{H4}$ [12]. The topological semantics of $\mathrm{QHC}$ gives rise to the following topological semantics of $\mathrm{H4}$ [7], [11]. Let $(X,\tau)$ be some non-empty topological space and $A$ be a dense subset of it. Propositional variables are interpreted as arbitrary open subsets $|\alpha|\subseteq X$. Boolean operators are interpreted in the standard way [13], and $\nabla\varphi$ is understood as $|\nabla\varphi|=X\setminus\operatorname{Cl}(A\setminus|\varphi|)$. It was proved in [7] and [11] that a formula is deducible in $\mathrm{H4}$ if and only if it is true in each topological model.

In this note we generalize the semantics of $\mathrm{H4}$ to the more general class of bitopological models. Massas [9] considered bitopological spaces satisfying $\tau_1\subseteq\tau_2$ as the semantics of the intuitionistics logic.

Let $X$ be a non-empty set endowed with two topologies $\tau_1$ and $\tau_2$ such that $\tau_1\subseteq\tau_2$. Let $\operatorname{Int}_i$ and $\operatorname{Cl}_i$ denote the operators of taking the interior and taking the closure in the topology $\tau_i$. Propositional variables are interpreted as open sets in $\tau_1$. Boolean operators are interpreted in the standard way on the topological space $(X,\tau_1)$, while $\nabla\varphi$ is defined by $|\nabla\varphi|=\operatorname{Int}_1\operatorname{Cl}_2|\varphi|$.

Proof. We start with soundness. It was shown in [9] that $\operatorname{Int}_1\operatorname{Cl}_2$ is a nucleus on the Heyting algebra of sets open in $\tau_1$, that is, it has the following properties (where $U_1,U_2,U\in\tau_1$): $U_1\subseteq U_2\Rightarrow \operatorname{Int}_1\operatorname{Cl}_2U_1\subseteq \operatorname{Int}_1\operatorname{Cl}_2U_2$; $U\subseteq\operatorname{Int}_1\operatorname{Cl}_2U$; $\operatorname{Int}_1\operatorname{Cl}_2U=\operatorname{Int}_1 \operatorname{Cl}_2\operatorname{Int}_1\operatorname{Cl}_2U$; $\operatorname{Int}_1\operatorname{Cl}_2(U_1\cap U_2)= \operatorname{Int}_1\operatorname{Cl}_2U_1\cap \operatorname{Int}_1\operatorname{Cl}_2U_2$. This yields the validity of axioms $(1^{\nabla})$, $(2^{\nabla})$, and $(4^{\nabla})$ of $\mathrm{H4}$ in bitopological models. The validity of axiom $(3^{\nabla})$ can be verified directly since $\operatorname{Int}_1\operatorname{Cl}_2\varnothing=\varnothing$.

Now we prove completeness. Consider a topological model $(X,\tau)$ of $\mathrm{H4}$ with dense subset $A$ which is a counter model for the formula $\varphi$. Set $\tau_1=\tau$, and assume that the topology $\tau_2$ has the basis $\tau\cup\mathcal P(A)$, where $\mathcal P(A)$ is the set of subsets of $A$. Clearly, $\tau_1\subseteq\tau_2$. Note that for each set $M\subseteq X$ we have $\operatorname{Cl}_2(M)=\operatorname{Cl}_1(M)\setminus(A\setminus M)$ because subsets closed in $\tau_2$ can be represented as $C\setminus B$, where $C$ is closed in $\tau_1$ and $B\subseteq A$.

We interpret all propositional variables just as in the model $(X,\tau,A)$. We claim that then all formulae have the same interpretation in the models $(X,\tau,A)$ and $(X,\tau_1,\tau_2)$. It is sufficient to consider the case of the induction step using the modality $\nabla$, that is, to prove the equality $X\setminus\operatorname{Cl}_1(A\setminus U)= \operatorname{Int}_1\operatorname{Cl}_2U$ for all $U\in\tau_1$.

We show that $X\setminus\operatorname{Cl}_1(A\setminus U)\subseteq \operatorname{Int}_1\operatorname{Cl}_2U$. We use the equality $X\setminus\operatorname{Cl}_1(A\setminus U)= \bigcup\{V\in\tau_1\mid V\cap A\subseteq U\}$. Consider any $V\in\tau_1$ such that $V\cap A\subseteq U$. Then, as $A$ is dense, we have $V\subseteq\operatorname{Cl}_1(U)$. From $V\cap(A\setminus U)=\varnothing$ we obtain $V\subseteq\operatorname{Cl}_2(U)= \operatorname{Cl}_1(U)\setminus(A\setminus U)$. Hence, since $V\in\tau_1$, it follows that $V\subseteq\operatorname{Int}_1\operatorname{Cl}_2(U)$, which completes the proof of the inclusion.

Now let $V\in\tau_1$ be a set such that $V\subseteq\operatorname{Int}_1\operatorname{Cl}_2M$; then ${V\subseteq\operatorname{Cl}_2U}$. Again, since $A$ is dense, we have $V\cap A\subseteq U$, so that $U\subseteq X\setminus\operatorname{Cl}_1(A\setminus U)$.

Now, as all formulae preserve their interpretation, $(X,\tau_1,\tau_2)$ is a counter model for $\varphi$. The proof is complete.

Axiom $(3^{\nabla})$ corresponds to the density property of the nucleus. By considering Lindenbaum algebras it is easy to see that the logic $\mathrm{H4}$ is complete with respect to the algebraic semantics based on Heyting algebras with dense nuclei. Thus we have shown that $\mathrm{H4}$ is complete with respect to dense nuclei of particular form on the Heyting algebras of open subsets of a topological space.

Remark. The formulae $\alpha\to\nabla\alpha$ and $\nabla\alpha\to\neg\neg\alpha$ are deducible in $\mathrm{H4}$ (the first is axiom $(1^{\nabla})$, while the second was deduced in [1] and [2]). Consider two extreme cases. If $\tau_2$ is a discrete topology, then $\nabla\alpha\leftrightarrow\alpha$ in such a model. On the other hand, if $\tau_2=\tau_1$, then $\nabla\alpha\leftrightarrow\neg\neg\alpha$ in such a model. The logic $\mathrm{H4}$ has a Kripke-type semantics with a set $\mathrm{Aud}$ of audit worlds [1], [12]. The case of discrete topology $\tau_2$ is obtained by taking $A=X$ in the topological model or $\mathrm{Aud}=W$ in the Kripke model (and considering the relevant Alexandroff topology). The case $\tau_2=\tau_1$ is obtained by taking the set of leaves of a finite Kripke model as $\mathrm{Aud}$.

The author is grateful to L. D. Beklemishev and S. A. Melikhov for fruitful discussions and for their interest in this work.

Citation in format AMSBIB

\Bibitem{Ono24}

\by A.~A.~Onoprienko

\paper Bitopological models of intuitionistic epistemic logic

\jour Russian Math. Surveys

\yr 2024

\vol 79

\issue 1

\pages 179--181

\mathnet{http://mi.mathnet.ru//eng/rm10149}

\crossref{https://doi.org/10.4213/rm10149e}

\mathscinet{http://mathscinet.ams.org/mathscinet-getitem?mr=4774058}

\zmath{https://zbmath.org/?q=an:07891396}

\adsnasa{https://adsabs.harvard.edu/cgi-bin/bib_query?2024RuMaS..79..179O}

\isi{https://gateway.webofknowledge.com/gateway/Gateway.cgi?GWVersion=2&SrcApp=Publons&SrcAuth=Publons_CEL&DestLinkType=FullRecord&DestApp=WOS_CPL&KeyUT=001292806100006}

\scopus{https://www.scopus.com/record/display.url?origin=inward&eid=2-s2.0-85205991667}

Bibliography