zbMATH — the first resource for mathematics

Unification in some substructural logics of BL-algebras and hoops. (English) Zbl 1156.03022
The paper is not sufficiently self-contained and organized to be easily read.
Unification in an equational theory $$E$$ is the process of finding a substitution $$\sigma$$ of individual variables that makes two given terms $$t_1, t_2$$ equal, or unified, modulo the theory $$E$$, i.e. $$\vdash_E \sigma t_1=\sigma t_2.$$ Such a substitution is called a unifier for $$t_1$$ and $$t_2$$.
The unification type of a theory $$E$$ can be unitary, finitary, infinitary or nullary.
The paper studies the unification type of the substructural logics associated to some partially ordered ($$k$$-potent, i.e. $$x^{k+1}=x^k$$, for every $$x$$, with $$k\geq 1$$) algebras containing the residuated pair $$(\cdot, \Rightarrow)$$ (i.e. $$x \cdot y \leq z \Longleftrightarrow x \leq y \Rightarrow z$$, for all $$x,y,z$$) as a reduct: 4mm
hoops, basic hoops, Wajsberg hoops – which do not have a negation, because they do not have $$0$$, the smallest element;
BL-algebras, Gödel algebras, Wajsberg algebras (MV-algebras) – which have a negation $$\neg x=x \Rightarrow 0$$, because they have $$0$$.
The results are: 4mm
the logics of $$k$$-potent hoops and the logics of $$k$$-potent BL-algebras (hence Gödel logic and the finite-valued Łukasiewicz logics) have unitary unification (with transparent unifiers); while
Basic Logic (the logic of BL-algebras) and the $$\infty$$-valued Łukasiewicz logic Ł$$_{\infty}$$ (the logic of Wajsberg algebras (MV-algebras)) do not have unitary unification; consequently,
the logics of $$k$$-potent hoops are hereditarily structurally complete and the $$k$$-potent logics containing Basic Logic are structurally complete in the restricted sense; while
Basic Logic itself and Ł$$_{\infty}$$ are not structurally complete, even in the restricted sense.

MSC:
 03B47 Substructural logics (including relevance, entailment, linear logic, Lambek calculus, BCK and BCI logics) 03G25 Other algebras related to logic 06D35 MV-algebras 06A12 Semilattices 06B99 Lattices 06F05 Ordered semigroups and monoids