ABSTRACT. Dynamic topological logic and its variant, intuitionistic temporal logic, combine topological semantics with linear temporal logic in order to reason about topological dynamics. I will provide a historical overview of the field, from its inception to recent results and open questions.

ABSTRACT. The Goldblatt-Thomason theorem is a classic result of modal definability of Kripke frames. Its topological analogue for the closure semantics has been proved by Gabelaia et al. (2009). In this paper we prove a version of the Goldblatt-Thomason theorem for the topological semantics via the Cantor derivative. We work with derivative spaces which provide a natural generalisation of topological spaces on the one hand and of weakly transitive frames on the other.

ABSTRACT. Polymodal provability logic GLP is known to be Kripke incomplete. However, it was shown by Ignatiev that the closed (i.e. variable free) fragment of GLP is Kripke complete w.r.t. a certain Kripke frame, which is now known as Ignatiev frame, moreover he has shown that it is complete w.r.t. a specific set of its points, which are called the main axis. We show that the closed fragment of GLP is strongly complete w.r.t. an extended variant of Ignatiev frame, whereas it is not strongly complete w.r.t. the main axis and moreover w.r.t. neither Icard nor Beklemishev-Gabelaia topological spaces, which are known to provide topological completeness for the closed fragment of GLP and GLP itself correspondingly.

ABSTRACT. The Reflection Calculus (RC) is the fragment of the polymodal logic GLP whose formulas are built using only conjunction and diamond modalities. RC is complete with respect to the arithmetical interpretation associating modalities with reflection principles and is useful in several interesting applications of provability logic, such as ordinal analysis.

We present TRC, a tree rewriting system adequate and complete with respect to RC and designed to simulate RC derivations. TRC is based on a correspondence between positive formulas and modal trees, finite labeled trees with nodes labeled with lists of propositional variables and edges labeled with natural numbers. Modal trees are presented as an inductive type, allowing for precise positioning and transformations which give rise to the formal definition of rewriting rules and facilitates its formalization in proof assistants. Furthermore, we provide a rewrite normalization theorem for systematic rule application. The normalization of the rewriting process enhances proof search efficiency and facilitates implementation. By providing TRC as an efficient provability tool for RC, we aim to aid in the study of various aspects of the logic such as the subformula property and rule admissibility.

ABSTRACT. Polyhedral semantics is a recently introduced branch of spatial modal logic, in which modal formulas are interpreted as piecewise linear subsets of an Euclidean space. Polyhedral semantics for the basic modal language has already been well investigated. However, for many practical applications of polyhedral semantics, it is advantageous to enrich the basic modal language with a reachability modality. Recently, a language with an Until-like spatial modality has been introduced, with demonstrated applicability to the analysis of 3D meshes via model checking. In this paper, we exhibit an axiom system for this logic, and show that it is complete with respect to polyhedral semantics. The proof consists of two major steps: First, we show that this logic, which is built over Grzegorczyk's system Grz, has the finite model property. Subsequently, we show that every formula satisfied in a finite poset is also satisfied in a polyhedral model, thereby establishing polyhedral completeness.

ABSTRACT. Bisimulations are standard in modal logic and, more generally, in the theory of state-transition systems. The quotient structure of a Kripke model with respect to the bisimulation relation is called a bisimulation contraction. The bisimulation contraction is a minimal model bisimilar to the original model, and hence, for (image-)finite models, a minimal model modally equivalent to the original. Similar definitions exist for bounded bisimulations (k-bisimulations) and bounded bisimulation contractions. Two finite models are k-bisimilar if and only if they are modally equivalent up to modal depth k. However, the quotient structure with respect to the k-bisimulation relation does not guarantee a minimal model preserving modal equivalence to depth k. In this paper, we remedy this asymmetry to standard bisimulations and provide a novel definition of bounded contractions called rooted k-contractions. We prove that rooted k-contractions preserve k-bisimilarity and are minimal with this property. Finally, we show that rooted k-contractions can be exponentially more succinct than standard k-contractions.

ABSTRACT. In this paper, we introduce the simulations and bisimulations on polarity-based semantics for non-distributive modal logic, which are natural generalizations of those notions on Kripke semantics for modal logic. We also generalize other important model-theoretic notions about Kripke semantics such as image-finite models, modally-saturated models, ultrafilter extension and ultrapower extension to the nondistributive setting. By using these generalizations, we prove the Hennessy-Milner theorem and the van Benthem characterization theorem for non-distributive modal logic based on polarity-based semantics.

ABSTRACT. In studies of first-order modal logic (FOML), in order to give a semantics on varying-domain models, we usually use free logic. However, we can also keep the classical first-order logic, but revise the semantics of the modal operator instead, as shown in works on the so-called "common sense predicate modal logic". In this paper, following the latter approach, we introduce a binary strict implication operator ϕ⇛ψ, which is more expressive than the common sense □-operator, and is able to characterize a lot of our reasoning about necessity (or time, knowledge, etc.) in natural language that involves existence and non-existence of objects. We offer complete axiomatizations of the FOML of ⇛ on the class of all varying-domain models, the class of symmetric models, as well as the class of transitive models with a special property we call the "continual existence property".

ABSTRACT. We study the completeness problem for propositionally quantified modal logics on quantifiable general frames, where the admissible sets are the propositions the quantifiers can range over and expressible sets of worlds are admissible, and Kripke frames, where the quantifiers range over all sets of worlds. We show that any normal propositionally quantified modal logic containing all instances of the Barcan scheme is strongly complete with respect to the class of quantifiable general frames validating it. We also provide a sufficient condition for the truth of all formulas, possibly with quantifiers, to be preserved under passing from a quantifiable general frame to its underlying Kripke frame. This is reminiscent of both the idea of elementary submodel in model theory and the persistence concepts in propositional modal logic. The key to this condition is the concept of finite generated diversity (Fritz 2023), and with it, we show that if $\Theta$ is a set of Sahlqvist formulas whose class of Kripke frames has finite generated diversity, then the smallest normal propositionally quantified modal logic containing $\Theta$, Barcan, a formula stating the existence of world propositions, and a formula stating the definability of successor sets, is Kripke complete. As a special case, we have a simple finite axiomatization of the logic of Euclidean Kripke frames.

ABSTRACT. We examine the interplay between projectivity (in the sense that was introduced by S.~Ghilardi) and uniform post-interpolant for the classical and intuitionistic propositional logic. More precisely, we explore whether a projective substitution of a formula is equivalent to its uniform post-interpolant, assuming the substitution leaves the variables of the interpolant unchanged. We show that in classical logic, this holds for all formulas. Although such a nice property is missing in intuitionistic logic, we provide Kripke semantical characterisation for propositions with this property.

As a main application of this, we show that the unification type of some extensions of intuitionistic logic are finitary. In the end, we study admissibility for intuitionistic logic, relative to some sets of formulae.

The first author of this paper recently considered a particular case of this relativised admissibility and found it useful in characterising the provability logic of Heyting Arithmetic.

ABSTRACT. As well known, weak K4 and the difference logic DL do not enjoy the Craig interpolation property. Our concern here is the problem of deciding whether any given implication does have an interpolant in these logics. We show that the nonexistence of an interpolant can always be witnessed by a pair of bisimilar models of polynomial size for DL and of triple-exponential size for weak K4, and so the interpolant existence problems for these logics are decidable in coNP and coN3ExpTime, respectively. We also establish coNExpTime-hardness of this problem for weak K4, which is higher than the PSpace-completeness of its decision problem.