For a positive number a, each metric space carries the relation D_a consisting of those pairs that are of distance less than a apart. A space X is said to be a-connected, if the graph (X,D_a) is connected (that is, there is a D_a-path between every pair of points in X). We give a complete axiomatization of a-connected metric spaces in the language with a family of distance modalities and the universal modality. Then we give a complete axiomatization of the logic of connected (in the classical topological sense) metric spaces in the language with the topological modality, universal modality, and a single distance modality. We also show that these logics have the finite model property.

In the product $L_1 imes L_2$ of two Kripke complete consistent logics, local tabularity of $L_1$ and $L_2$ is necessary for local tabularity of $L_1 imes L_2$ . However, it is not sufficient: the product of two locally tabular logics may not be locally tabular. We provide extra semantic and axiomatic conditions that give criteria of local tabularity of the product of two locally tabular logics, and apply them to identify new families of locally tabular products. We show that the product of two locally tabular logics may lack the product finite model property. We give an axiomatic criterion of local tabularity for all extensions of . Finally, we describe a new prelocally tabular extension of .

We study the finite model property of subframe logics with expressible transitive reflexive closure modality. For m>0 , let L_m be the logic defined by axiom ◊ ^m+1 p→◊ p∨ p . We construct quotient filtrations for the logics L_m , which implies that these logics and their tense counterparts have the finite model property. Then, we construct selective filtrations of the canonical models of L_m , which implies that all canonical subframe logics containing L_m have the finite model property.

We consider logics derived from Euclidean spaces ℝ^n. Each Euclidean space carries relations consisting of those pairs that are, respectively, distance more than 1 apart, distance less than 1 apart, and distance 1 apart. Each relation gives a uni-modal logic of ℝ^n called the farness, nearness, and constant distance logics, respectively. These modalities are expressive enough to capture various aspects of the geometry of ℝ^n related to bodies of constant width and packing problems. This allows us to show that the farness logics of the spaces ℝ^n are all distinct, as are the nearness logics, and the constant distance logics. The farness and nearness logics of ℝ are shown to strictly contain those of ℚ, while their constant distance logics agree. It is shown that the farness logic of the reals is not finitely axiomatizable and does not have the finite model property.

On relational structures and on polymodal logics, we describe operations which preserve local tabularity. This provides new sufficient semantic and axiomatic conditions for local tabularity of a modal logic. The main results are the following. We show that local tabularity does not depend on reflexivity. Namely, given a class $\mathcal{F}$ of frames, consider the class $\mathcal{F}^\mathrm{r}$ of frames, where the reflexive closure operation was applied to each relation in every frame in $\mathcal{F}$. We show that if the logic of $\mathcal{F}^\mathrm{r}$ is locally tabular, then the logic of $\mathcal{F}$ is locally tabular as well. Then we consider the operation of sum on Kripke frames, where a family of frames-summands is indexed by elements of another frame. We show that if both the logic of indices and the logic of summands are locally tabular, then the logic of corresponding sums is also locally tabular. Finally, using the previous theorem, we describe an operation on logics that preserves local tabularity: we provide a set of formulas such that the extension of the fusion of two canonical locally tabular logics with these formulas is locally tabular.

We study the finite model property of subframe logics with expressible transitive reflexive closure modality. For $m>0$, let $\mathrm{L}_m$ be the logic given by axiom $\lozenge^{m+1} p\to \lozenge p\vee p$. We construct filtrations for the logics $\mathrm{L}_m$. It follows that these logics and their tense counterparts have the finite model property. Then we show that every canonical subframe logic that contains $\mathrm{L}_m$ have the finite model property.

We describe a family of decidable propositional dynamic logics, where atomic modalities satisfy some extra conditions (for example, given by axioms of the logics K5, S5, or K45 for different atomic modalities). It follows from recent results (Kikot, Shapirovsky, Zolin, 2014; 2020) that if a modal logic $L$ admits a special type of filtration (so-called definable filtration), then its enrichments with modalities for the transitive closure and converse relations also admit definable filtration. We use these results to show that if logics $L_1, \ldots , L_n$ admit definable filtration, then the propositional dynamic logic with converse extended by the fusion $L_1*\ldots * L_n$ has the finite model property.

We consider the bimodal language, where the first modality is interpreted by a binary relation in the standard way, and the second is interpreted by the relation of inequality. It follows from Hughes (1990), that in this language, non-k-colorability of a graph is expressible for every finite k. We show that modal logics of classes of non-k-colorable graphs (directed or non-directed), and some of their extensions, are decidable.

We consider the operation of sum on Kripke frames, where a family of frames-summands is indexed by elements of another frame. In many cases, the modal logic of sums inherits the finite model property and decidability from the modal logic of summands [Babenyshev and Rybakov 2010 ; Shapirovsky 2018 ]. In this paper we show that, under a general condition, the satisfiability problem on sums is polynomial space Turing reducible to the satisfiability problem on summands. In particular, for many modal logics decidability in PSpace is an immediate corollary from the semantic characterization of the logic.

Glivenko's theorem states that a formula is derivable in classical propositional logic CL iff under the double negation it is derivable in intuitionistic propositional logic IL: CL proves phi iff IL proves sic sic phi. Its analog for the modal logics S5 and S4 states that S5 proves phi iff S4 proves sic square sic square phi. In Kripke semantics, IL is the logic of partial orders, and CL is the logic of partial orders of height 1. Likewise, S4 is the logic of preorders, and S5 is the logic of equivalence relations, which are preorders of height 1. In this paper we generalize Glivenko's translation for logics of arbitrary finite height.

We give a sufficient condition for Kripke completeness of modal logics enriched with the transitive closure modality. More precisely, we show that if a logic admits what we call definable filtration (ADF), then such an expansion of the logic is complete; in addition, has the finite model property, and again ADF. This argument can be iterated, and as an application we obtain the finite model property for PDL-like expansions of logics that ADF.

Given a class 𝒞 of models, a binary relation ℛ between models, and a model-theoretic language L , we consider the modal logic and the modal algebra of the theory of 𝒞 in L where the modal operator is interpreted via ℛ . We discuss how modal theories of 𝒞 and ℛ depend on the model-theoretic language, their Kripke completeness, and expressibility of the modality inside L . We calculate such theories for the submodel and the quotient relations. We prove a downward Löwenheim–Skolem theorem for first-order language expanded with the modal operator for the extension relation between models.

Let $(\omega^n,\preceq)$ be the direct power of $n$ instances of $(\omega,\leq)$, natural numbers with the standard ordering, $(\omega^n,\prec)$ the direct power of $n$ instances of $(\omega,<)$. We show that for all finite $n$, the modal logics of $(\omega^n,\preceq)$ and of $(\omega^n,\prec)$ have the finite model property and moreover, the modal algebras of the frames $(\omega^n,\preceq)$ and $(\omega^n,\prec)$ are locally finite.

В работе доказана финитная аппроксимируемость и разрешимость одного семейства модальных логик. Бинарное отношение $R$ назовем предтранзитивным, если $R^*=\bigcup_{i\leqslant m} R^i$ для некоторого $m\geqslant 0$, где $R^*$ - транзитивное рефлексивное замыкание $R$. Под высотой шкалы $(W,R)$ будем понимать высоту предпорядка $(W,R^*)$. Построены специальные разбиения (фильтрации) предтранзитивных шкал конечной высоты, из чего следует финитная аппроксимируемость и разрешимость их модальных логик. Библиография: 30 наименований.

The paper proves finite model property and decidability for a family of modal logics. A binary relation $R$ is called pretransitive, if $R^*=\cup_{i\leq m} R^i$ for some $m\geq 0$, where $R^*$ is the transitive reflexive closure of $R$. By the height of $(W,R)$ we mean the height of the preorder $(W,R^*)$. Special partitionings (filtrations) are described for pretransitive frames of finite height, which implies finite model property and decidability of logics of these frames.

In this paper we consider propositional normal modal logics [2]. A modal logic has the finite model property (fmp, for short) if it is complete with respect to a class of finite frames. By Harrop’s theorem, finitely axiomatizable logics with the fmp are decidable. Despite the fact that the fmp of modal logics has been systematically studied for about fifty years, the picture is still incomplete even for the basic language (that is, when we have a single modal operator). Many modal logics are known to have the fmp (cf. [2], [1]). There are logics without the fmp, but in the unimodal case such examples are usually quite artificial. There are also natural examples of unimodal logics for which the fmp is unknown. The most well-known example is perhaps the logic K3 axiomatized by the simple formula p → p. In general, the finite model property and even the decidability of the logics Kn axiomatized by the formulae p → p is an old open problem (cf. [2], problem 11.2 and [8], problem 6), and the answer is unknown for all m, n > 1 with m ̸= n. The modal operator corresponding to the transitive reflexive closure of a binary relation is expressible in the logics Kn for n > m. We call such logics pretransitive. Formally, L is pretransitive if there exists a formula χ(p) such that for any model M with M L, and for any point w in this model we have M, w χ(p) ⇐⇒ ∀u (wR∗u ⇒ M, u p), where R∗ is the transitive reflexive closure of the relation R of the model M . A logic is pretransitive if and only if for some k > 0 it includes the k-transitivity formula p → p, where φ = ∧k i=0 φ (cf. [3]). In particular, for n > m the logic Kn is (n− 1)-transitive. Let K6m be the logic axiomatized by the formula p → p. Thus, K6m is the minimal m-transitive logic. For m > 1, the fmp of K6m is also unknown. For a Kripke complete logic L, the fmp means that if a formula is satisfiable in an L-frame, then it is satisfiable in a finite L-frame. Sahlqvist’s theorem implies that all the logics Kn and K6m are Kripke complete. The frames of these logics have a simple first-order characterization; for example, K3-frames are characterized by the first-order condition R ◦ R ◦ R ⊆ R ◦ R, where ◦ stands for the composition of relations. In general, Kn -frames are characterized by the condition R ⊆ R and K6m-frames by the condition R ⊆ ⋃ i6m R . Hence, there are no known ways to transform an infinite frame into a finite one preserving the satisfiability of a given formula while maintaining the properties mentioned. We were able to construct such transformations in the case when the depth of the frames (that is, the maximal cardinality of chains in the partial order induced by the relation R) is finite.

According to the classical result by Segerberg and Maksimova, a modal logic containing K4 is locally tabular i↵ it is of finite height. The notion of finite height can also be defined for logics, in which the master modality is expressible (‘pretransitive’ logics). We observe that every locally tabular logic is a pretransitive logic of finite height. Then we prove some semantic criteria of local tabularly. By applying them we extend the Segerberg – Maksimova theorem to a certain larger family of pretransitive logics.