Unification and projectivity in Fregean varieties (Q2903751)

Equational unification for a variety of algebras is the problem of solving equations of terms by finding substitutions into their variables, called unifiers, that make terms equivalent with respect to the variety. In particular, the problem of existence of a most general unifier (an MGU), i.e., such that any other unifier is an instance of it, is one of the central issues of unification theory. NEWLINENEWLINENEWLINE NEWLINEEquational unification has been studied for many varieties related to logic. In the present paper, the author analyses the problem of unification, and, in particular, the question of existence of projective unifiers for a wide class of such structures -- the congruence-permutable (CP) Fregean varieties. NEWLINENEWLINENEWLINE NEWLINEFor a CP Fregean variety, the author proves a sufficient condition for a unifiable term to be projective. Using this result she gives a twofold characterization of CP Fregean varieties with projective unifiers. Firstly, she shows that this class can be described by a set of identities. Secondly, she characterizes varieties with projective unifiers by properties of their subdirectly irreducible algebras. As a consequence, she deduces that for each CP Fregean variety there exists a unique largest subvariety that has projective unifiers (e.g., for the variety of Heyting algebras, it is the subvariety of Gödel-Dummett algebras). Moreover, under the additional assumption of finite signature, it is possible to characterize all unifiable terms as well as describe a unification algorithm in a variety with projective unifiers. The method presented here gives new proofs of unitarity for several known cases and leads to some new results.