Abstract Unification problems can be formulated and investigated in an algebraic setting, by identifying substitutions to modal algebra homomorphisms. This opens the door to applications of the notorious duality between Heyting or modal algebras and descriptive frames. Through substantial use of this correspondence, we give a necessary and sufficient condition for formulas to be projective. A close inspection of this characterization will motivate a generalization of standard unification, which we dub relative unification. Applying this result to a number of different logics, we then obtain new proofs of their projective—or non-projective—character. Aside from reproving known results, we show that the projective extensions of $\textbf{K5}$ are exactly the extensions of $\textbf{K45}$. This resolves the open question of whether $\textbf{K5}$ is projective.

Abstract We prove that all extensions of $\textbf{K5}$ have unitary unification, even with parameters. Our proof is constructive in the sense that we can effectively compute, in 4-exponential space, a most general unifier for any unifiable formula. In particular, this proves that unification and admissibility are decidable. We also investigate special unification types: we show that $\textbf{K5}$ and $\textbf{KD5}$ are transparent, and we characterize the projective extensions of $\textbf{K5}$.

Abstract Alongside the traditional Kripke semantics, modal logic also enjoys a topological interpretation, which is becoming increasingly influential. In this paper, we present various developments related to the topological derivational semantics, based on the Cantor derivative operator. We provide several characterizations of the validity of the axioms of bounded depth. We also elucidate the topological interpretation of the axioms of directedness and connectedness—which come in different forms, all of which we examine. We then prove results of soundness and completeness for all of these logics, using a range of old and new techniques.

Abstract Modal logic enjoys topological semantics that may be traced back to McKinsey and Tarski, and the classification of topological spaces via modal axioms is a lively area of research. In the past two decades, there has been interest in extending topological modal logic to the language of the mu-calculus, but previously no class of topological spaces was known to be mu-calculus definable that was not already modally definable. In this paper, we show that the full mu-calculus is indeed more expressive than standard modal logic, in the sense that there are classes of topological spaces (and weakly transitive Kripke frames), which are mu-definable but not modally definable. The classes we exhibit satisfy a modally definable property outside of their perfect core, and thus we dub them imperfect spaces. We show that the mu-calculus is sound and complete for these classes. Our examples are minimal in the sense that they use a single instance of a greatest fixed point, and we show that least fixed points alone do not suffice to define any class of spaces that is not already modally definable.

The µ-calculus can be interpreted over metric spaces and is known to enjoy, among other celebrated properties, variants of the McKinsey-Tarski completeness theorem and of Dawar and Otto’s modal characterization theorem. In its topological form, this theorem states that every topological fixed point may be defined in terms of the tangled derivative, a polyadic generalization of Cantor’s perfect core. However, these results fail when spaces not satisfying basic separation axioms are considered, in which case the base modal logic is not the well-known K4, but the weaker wK4.In this paper we show how these shortcomings may be overcome. First, we consider semantics over the wider class of hemimetric spaces, and obtain metric completeness results for wK4 and related logics. In this setting, the Dawar-Otto theorem still fails, but we argue that this is due to the tangled derivative not being suitably defined for general application in arbitrary topological spaces. We thus introduce the hybrid tangle, which coincides with the tangled derivative over metric spaces but is better behaved in general. We show that only the hybrid tangle suffices to define simulability of finite structures, a key ‘test case’ for an expressively complete fragment of the µ-calculus.