Duality, projectivity, and unification in Łukasiewicz logic and MV-algebras (Q1935862)

Introduced by Herbrand in 1930, the classical unification problem in logic is the following: given two terms \(s\), \(t\) built from function symbols and variables, find a uniform replacement, called \textit{unifier}, of the variables occuring in \textit{s} and \textit{t} by other terms that make \textit{s} and \textit{t} identical and, more generally, E-unification problem if the identity is replaced by equality modulo a given equational theory E. Most fundamental is the issue of unification type of E, which can be \textit{unitary}, \textit{finitary}, \textit{infinitary} or none of them, then called \textit{nullary}. In this paper the E-unification type of Łukasiewicz infinite-valued propositional logic and the corresponding variety of MV-algebras is proved to be nullary, MV-algebras being the algebraic counterpart of Łukasiewicz logic in the same sense as Boolean algebras are for classical logic. The proof is based on a recent result on projective MV-algebras (by Cabrer and Mundici), the categorical duality between finitely presented MV-algebras and rational polyhedra and, finally, lifts of continuous maps to the universal covering space of the unit circle.