# About the unification type of simple symmetric modal logics

## TL;DR

This paper investigates the unification problem in simple symmetric modal logics, demonstrating that certain logics like KB, KDB, and KTB contain formulas with no minimal complete set of unifiers, called nullary formulas.

## Contribution

It establishes the existence of nullary formulas in specific simple symmetric modal logics, advancing understanding of unification properties in these systems.

## Key findings

- KB, KDB, and KTB have nullary formulas
- Nullary formulas lack minimal complete unifier sets
- Results deepen the understanding of unification in modal logics

## Abstract

The unification problem in a normal modal logic is to determine, given a formula F, whether there exists a substitution s such that s(F) is in that logic. In that case, s is a unifier of F. We shall say that a set of unifiers of a unifiable formula F is complete if for all unifiers s of F, there exists a unifier t of F in that set such that t is more general than s. When a unifiable formula has no minimal complete set of unifiers, the formula is nullary. In this paper, we prove that KB, KDB and KTB possess nullary formulas.