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.
Duality, projectivity, and unification in Łukasiewicz logic and MV-algebras
We prove that the unification type of Lukasiewicz infinite-valued propositional logic and of its equivalent algebraic semantics, the variety of MV-algebras,is nullary. The proof rests upon Ghilardi’s algebraic characterisation of unification types in terms of projective objects, recent progress by Cabrer and Mundici in the investigation of projective MV-algebras, the categorical duality between finitely presented MV-algebras and rational polyhedra, and, finally, a homotopy-theoretic argument that exploits lifts of continuous maps to the universal covering space of the circle. We discuss the background to such diverse tools. In particular, we offer a detailed proof of the duality theorem for finitely presented MV-algebras and rational polyhedra – a fundamental result that, albeit known to specialists, seems to appear in print here for the first time.
Duality, projectivity, and unification in Łukasiewicz logic and MV-algebras
The unification type of Łukasiewicz logic is nullary
This is the most updated version of a talk presenting the result contained here. The talk was given in plenary session at Topology, Algebra, and Category in Logic -TACL- V, Marseille, 28$^{th}$ July. 2011
The unification type of Łukasiewicz logic is nullary
