6533b852fe1ef96bd12aa424

RESEARCH PRODUCT

Unification in first-order transitive modal logic

subject

description

We introduce unification in first-order transitive modal logics, i.e. logics extending Q–K4, and apply it to solve some problems such as admissibility of rules. Unifiable formulas in some extensions of Q–K4 are characterized and an explicit basis for the passive rules (those with non-unifiable premises) is provided. Both unifiability and passive rules depend on the number of logical constants in the logic; we focus on extensions of Q–K4 with at most four constants ⊤,⊥,□⊥,◊⊤⁠. Projective formulas, defined in a way similar to propositional logic, are used to solve some questions concerning the disjunction and existence properties. A partial characterization of first-order modal logics with projective unification is given. Then logics with filtering unification are characterized and the unification type of certain logics extending Q–K4.2 and Q–K4.3 is settled. To this aim the weak existence property is adapted for first-order modal logics.