JAIST seminar talk

<a href=RLminJAIST1.ps>Minimal Varieties of Residuated Lattices</a>

<a href=../../gap/lambdaRL1.html>Lattice of subvarieties of residuated
lattices</a>

<a href=../../gap/lambdaL.html>Lattice of subvarieties of
lattices</a>

Does the lattice of subvarieties of residuated lattices have
any coatoms? Is RL join-irreducible?

<a href=../../gap/index.html>Lists of finite algebras</a> (36) (58)

Theorem (Dilworth [1939]): Let $X$ be a set of elements
in a residuated lattices that pair-wise join to $e$. Then
$X$ generates a generalized Boolean lattice under $\vee$, $\wedge$.



<h3>Some observations about decidability in $\m{RL}$ and $\m{LG}$</h3>

An important and useful result about $\m{RL}$ is the following.

Theorem (H. Ono and Y. Komori [1985]):
The equational theory of residuated lattices is decidable.

The decision procedure is based on an efficient cut-free Gentzen
system with the subformula property for $\m{FL}$, the full Lambek calculus.

A simple <a href=../../reslat/reslat.htm>implementation</a> in JavaScript
can be found on my webpage (www.math.vanderbilt.edu/~pjipsen).

Compare this with two important results about l-groups:

Theorem (C. Holland and S.H. McCleary [1979]): 
The variety of l-groups has a decidable 
equational theory.

As mentioned before, the algorithm is based on the result that $\m{LG}=\m V(A(\m R))$.
As far as I know, no implementation exists at this point.

With the present algorithm, showing that an identity fails in $A(\m R)$ is easier than
showing that it holds.

Is there a Gentzen system for deciding identities in $\m{LG}$?

Theorem (A.M.W. Glass and Y. Gurevich [1983]): 
The (local) word problem for l-groups is undecidable,
i.e. there exists a finitely presented l-group
(with one relator) for which there is no algorithm that
decides if two words are representatives of the same
element.

Corollary:
The quasi-equational theory of l-groups is undecidable.

This is also refered to as the undecidability of the global 
(or uniform) word problem.

The same theorem holds for semigroups 
(E. Post ~'40) and groups (W. Boone [1959], Novikov [195?])

Residuated lattices are a conservative extension of semigroups,
hence the word problem for residuated lattices is undecidable.

Theorem (N. G. Khisamiew 1966): The universal theory
of abelian l-groups is decidable.

If a class is closed under finite products, then any universal
formula is equivalent to a disjunction of quasi-identities
and negated equations.

Hence such a class has a decidable universal theory iff it has
a decidable quasi-equational theory.

Theorem (V. Weispfenning 1986): The universal theory of
abelian l-groups is co-NP-complete.

Theorem (Y. Gurevich 1967): The first-order theory of
abelian l-groups is hereditarily undecidable. (S. Burris
1985 gives a simple proof).


Is the equational theory of cancellative residuated lattices
decidable? What if we assume commutativity or integrality (or both)?


<a href=../../logic/theoriesPO1.html>Interpretability</a>

<!--center><a href=jaist1p2.htm>Next</a>

</center-->