Unification in Lukasiewicz logic with a finite number of variables
In this paper, coauthored with Marco Abbadini and Federica Di Stefano, we prove that the unification type of Lukasiewicz logic with a finite number of variables is either infinitary or nullary. To achieve this result we use Ghilardi’s categorical characterisation of unification types in terms of projective objects, the categorical duality between finitely presented MV-algebras and rational polyhedra, and a homotopy-theoretic argument.
Tags: Łukasiewicz logic, MV-algebras, Unification, Universal cover
