| Unification type of fusions
Philippe Balbian, Cigdem Gencer and Maryam Rostamigiv
In a modal logic $L$, a unifier of a formula $varphi$ is a substitution $sigma$ such that $sigma(varphi)$ is in $L$.
When unifiable formulas have no minimal complete sets of unifiers, they are nullary. Otherwise, they are either infinitary, or finitary, or unitary depending on the cardinality of their minimal complete sets of unifiers.
The fusion $L_{1}otimesL_{2}$ of modal logics $L_{1}$ and $L_{2}$ respectively based on the modal connectives $Box_{1}$ and $Box_{2}$ is the least modal logic based on these modal connectives and containing both $L_{1}$ and $L_{2}$.
In this paper, we prove that if $L_{1}otimesL_{2}$ is unitary then $L_{1}$ and $L_{2}$ are unitary and if $L_{1}otimesL_{2}$ is finitary then $L_{1}$ and $L_{2}$ are either unitary, or finitary. We also prove that the fusion of arbitrary consistent extensions of $S5$ is nullary when these extensions are different from $Triv$footnote{Dzik conjectured that the fusion $S5otimesS5$ of $S5$ with itself is either nullary, or infinitary~cite[Chapter~$6$]{Dzik:2007}.}.
September 2020
|