The unification type of Lukasiewicz logic with a bounded number of variables

Abstract

Building on the correspondence between finitely axiomatised theories in Łukasieiwcz logic and rational polyhedra, we prove that the unification type of the fragment of Łukasiewicz logic with $n\ge 2$ variables is nullary. This solves a problem left open in [V. Marra and L. Spada. Ann. Pure Appl. Logic 164 2013, p. 192-210]. Furthermore, we refine the study of unification with bounds on the number of variables. Our proposal distinguishes the number $m$ of variables allowed in the problem and the number $n$ in the solution. We prove that the unification type of Łukasiewicz logic for all $m,n\ge 2$ is nullary.