Unification in some substructural logics of BL-algebras and hoops.

*(English)*Zbl 1156.03022The 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

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 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.

Reviewer: Afrodita Iorgulescu (Bucharest)

##### 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 |