А. А. Оноприенко, “Битопологические модели интуиционистской эпистемической логики”, УМН, 79:1(475) (2024), 189–190; Russian Math. Surveys, 79:1 (2024), 179

Рассматривается логика $\mathrm{H4}$, являющаяся расширением интуиционистской пропозициональной логики модальностью $\nabla$, для которой выполнены следующие схемы аксиом: $(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)$.

С. Артёмов и Т. Протопопеску [1], [2] исследовали интуиционистскую эпистемическую логику с модальностью знания и построили три формальные системы $\mathrm{IEL}^-$, $\mathrm{IEL}$ и $\mathrm{IEL}^+$, последняя из которых совпадает с логикой $\mathrm{H4}$. Логика без аксиомы $(3^{\nabla})$ возникала ранее в работах Р. Голдблатта [6], А. Г. Драгалина [4], М. Фэтлоу и М. Мендлера [5]. По-видимому, интуиционистская логика, расширенная аксиомами $(1^{\nabla})$, $(2^{\nabla})$ и $(4^{\nabla})$, впервые возникла в книге Х. Карри [3]. Д. Макнаб [8] рассматривал модели интуиционистской логики с аксиомами $(1^{\nabla})$, $(2^{\nabla})$ и $(4^{\nabla})$, основанные на задании топологического пространства с выделенным в нём подмножеством. Логика $\mathrm{H4}$ получается добавлением аксиомы $(3^{\nabla})$, и эта аксиома в точности соответствует требованию плотности подмножества.

С. А. Мелихов [10] ввёл в рассмотрение совместную логику задач и высказываний $\mathrm{QHC}$, которая является консервативным расширением предикатного варианта логики $\mathrm{H4}$ [12]. Топологическая семантика логики $\mathrm{QHC}$ даёт следующую топологическую семантику логики $\mathrm{H4}$ [7], [11]. Пусть $(X,\tau)$ – произвольное непустое топологическое пространство и $A$ – его всюду плотное подмножество. Пропозициональные переменные интерпретируются как произвольные открытые подмножества $|\alpha|\subseteq X$. Булевы связки интерпретируются стандартным образом [13], а $\nabla\varphi$ понимается как $|\nabla\varphi|=X\setminus\operatorname{Cl}(A\setminus|\varphi|)$. В [7], [11] доказано, что формула выводима в логике $\mathrm{H4}$ тогда и только тогда, когда она истинна в любой топологической модели.

В данной работе семантика логики $\mathrm{H4}$ обобщается на более широкий класс битопологических моделей. Битопологические пространства с условием $\tau_1\subseteq\tau_2$ рассматривал Г. Массас [9] в качестве семантики интуиционистской логики.

Пусть $X$ – непустое множество, на котором заданы две топологии $\tau_1$ и $\tau_2$, причём $\tau_1\subseteq\tau_2$. Обозначим через $\operatorname{Int}_i$ и $\operatorname{Cl}_i$ операторы взятия внутренности и замыкания в топологии $\tau_i$. Пропозициональные переменные интерпретируются как открытые в $\tau_1$ множества. Булевы связки интерпретируются стандартным образом на топологическом пространстве $(X,\tau_1)$, а $\nabla\varphi$ понимается как $|\nabla\varphi|=\operatorname{Int}_1\operatorname{Cl}_2|\varphi|$.

Доказательство. Начнем с утверждения о корректности. В работе [9] было показано, что $\operatorname{Int}_1\operatorname{Cl}_2$ является оператором пополнения (англ.: nucleus) на гейтинговой алгебре множеств, открытых в топологии $\tau_1$, т. е. для него выполнены следующие свойства (где $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$. Это даёт нам истинность аксиом $(1^{\nabla})$, $(2^{\nabla})$, $(4^{\nabla})$ логики $\mathrm{H4}$ в битопологических моделях. Истинность оставшейся аксиомы $(3^{\nabla})$ проверяется непосредственно, так как $\operatorname{Int}_1\operatorname{Cl}_2\varnothing=\varnothing$.

Докажем утверждение о полноте. Рассмотрим топологическую модель $(X,\tau)$ логики $\mathrm{H4}$ со всюду плотным множеством $A$, являющуюся контрмоделью формулы $\varphi$. Возьмём $\tau_1=\tau$, и пусть топология $\tau_2$ порождена базой $\tau\cup\mathcal P(A)$, где $\mathcal P(A)$ – множество всех подмножеств $A$. Ясно, что $\tau_1\subseteq\tau_2$. Заметим, что для любого множества $M\subseteq X$ выполнено равенство $\operatorname{Cl}_2(M)=\operatorname{Cl}_1(M)\setminus(A\setminus M)$ в силу того, что замкнутые множества в топологии $\tau_2$ представимы как $C\setminus B$, где $C$ замкнуто в $\tau_1$, а $B\subseteq A$.

Проинтерпретируем все пропозициональные переменные так же, как это было в модели $(X,\tau,A)$. Проверим, что тогда интерпретации любых формул в моделях $(X,\tau,A)$ и $(X,\tau_1,\tau_2)$ совпадают. Достаточно проверить случай индуктивного перехода с использованием модальности $\nabla$, т. е. доказать, что $X\setminus\operatorname{Cl}_1(A\setminus U)= \operatorname{Int}_1\operatorname{Cl}_2U$ для всех $U\in\tau_1$.

Докажем, что $X\setminus\operatorname{Cl}_1(A\setminus U)\subseteq \operatorname{Int}_1\operatorname{Cl}_2U$. Воспользуемся тем, что $X\setminus\operatorname{Cl}_1(A\setminus U)= \bigcup\{V\in\tau_1\mid V\cap A\subseteq U\}$. Возьмём произвольное $V\in\tau_1$ такое, что $V\cap A\subseteq U$. Тогда в силу всюду плотности $A$ имеем $V\subseteq\operatorname{Cl}_1(U)$. Так как $V\cap(A\setminus U)=\varnothing$, получаем $V\subseteq\operatorname{Cl}_2(U)= \operatorname{Cl}_1(U)\setminus(A\setminus U)$. Отсюда в силу $V\in\tau_1$ получаем $V\subseteq\operatorname{Int}_1\operatorname{Cl}_2(U)$, что окончательно доказывает требуемое включение.

Теперь пусть $V\in\tau_1$ таково, что $V\subseteq\operatorname{Int}_1\operatorname{Cl}_2M$, тогда ${V\subseteq\operatorname{Cl}_2U}$. Снова в силу всюду плотности $A$ имеем $V\cap A\subseteq U$, следовательно, $U\subseteq X\setminus\operatorname{Cl}_1(A\setminus U)$.

Таким образом, поскольку интерпретация всех формул сохранилась, $(X,\tau_1,\tau_2)$ – контрмодель формулы $\varphi$. Теорема доказана.

Аксиома $(3^{\nabla})$ соответствует свойству плотности оператора пополнения. Нетрудно убедиться путём рассмотрения алгебр Линденбаума, что логика $\mathrm{H4}$ полна относительно алгебраической семантики, основанной на алгебрах Гейтинга с плотным оператором пополнения. Таким образом, нами показана полнота логики $\mathrm{H4}$ относительно плотных операторов пополнения конкретного вида на гейтинговых алгебрах открытых подмножеств топологического пространства.

Замечание. В логике $\mathrm{H4}$ выводимы формулы $\alpha\to\nabla\alpha$ и $\nabla\alpha\to\neg\neg\alpha$ (первая является аксиомой $(1^{\nabla})$, вторая выведена в [1], [2]). Рассмотрим два крайних случая. Если $\tau_2$ – дискретная топология, то в таких моделях $\nabla\alpha\leftrightarrow\alpha$. Если же $\tau_2=\tau_1$, то в таких моделях $\nabla\alpha\leftrightarrow\neg\neg\alpha$. Для логики $\mathrm{H4}$ имеется семантика типа Крипке с множеством $\mathrm{Aud}$ отмеченных миров [1], [12]. Случай дискретной $\tau_2$ получается, если взять $A=X$ в топологической модели или $\mathrm{Aud}=W$ в модели Крипке (и рассмотреть соответствующую александровскую топологию). Случай $\tau_2=\tau_1$ получается, если в качестве $\mathrm{Aud}$ взять множество всех листьев в конечной модели Крипке.

Автор выражает благодарность Л. Д. Беклемишеву и С. А. Мелихову за плодотворные дискуссии и интерес к этой работе.

Цитирование в формате AMSBIB

\RBibitem{Ono24}

\by А.~А.~Оноприенко

\paper Битопологические модели интуиционистской эпистемической логики

\jour УМН

\yr 2024

\vol 79

\issue 1(475)

\pages 189--190

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

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

\mathscinet{https://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}

\transl

\jour Russian Math. Surveys

\yr 2024

\vol 79

\issue 1

\pages 179--181

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

\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}

Список литературы