USC Talk

<br>
<p>
A <em>residuated lattice</em> 
is an algebra `bfL=<<(L,vv,^^,*,e,\,/)>>` such that `<<(L,vv,^^)>>` is a
lattice, `<<(L,*,e)>>` is a monoid, and for all `x,y,z in L`<p>
<center>`x*y<=z iff x<=z/y iff y<=x\z`</center>
<p>
We usually write `x*y` as `x.y` and use the convention that, 
in the absence of parentheses,
`*` is performed first, followed by `\,/` and then `vv, ^^`.
<p>
The class <b>RL</b> of all residuated lattices is a variety.
An equational basis is given by the monoid and lattice identities together
with, for instance,<p> 
<center>
`x.(y vv z) = x.y vv x.z`     `(x vv y).z = x.z vv y.z`<p>
`x\(y ^^ z) = x\y ^^ x\z`     `(x ^^ y)/z = x/z ^^ y/z`<p>
`x <= x.y/y`     `(x/y).y <= x`    
`y <= x\x.y`     `x.(x\y) <= y`.
</center>
<p>
The subvariety of all integral residuated lattices
is defined by the identity `x^^e=x` and is denoted by <b>IRL</b>. 
<p>
<b>CRL</b> is the variety of commutative residuated lattices.
<p>
Whitman's solution to the word problem is extended to residuated
lattices by adding the following Gentzen rules (with associativity
of `*` assumed in the application):
<p>
<table border=2 align=center>
<tr>
<td>
<table align="center">
<tr><td>
<table align="center">
<tr><td nowrap align=center>
`x<=z`, `y<=w`
<hr NOSHADE>
`x.y <= z.w`<br>
</td><td nowrap align=center>`*`-rule</td>
</table>
</td>
</table>
</td>
<td>
<table align="center">
<tr><td>
<table align="center">
<tr><td nowrap align=center>
`v<=x`, `u.y.w<=z`
<hr NOSHADE>
`(u.v).(x\y).w <= z`<br>
</td><td nowrap align=center>`\`-left</td>
</table>
</td>
</table>
</td>
<td>
<table align="center">
<tr><td>
<table align="center">
<tr><td nowrap align=center>
`x.y<=z`
<hr NOSHADE>
`y <= x\z`<br>
</td><td nowrap align=center>`\`-right</td>
</table>
</td>
</table>
</td>
</tr>
</table>
<table border=2 align=center>
<tr>
<td>
<table align="center">
<tr><td>
<table align="center">
<tr><td nowrap align=center>
`x.y<=z`
<hr NOSHADE>
`x.e.y <= z`<br>
</td><td nowrap align=center>`e`-left</td>
</table>
</td>
</table>
</td>
<td>
<table align="center">
<tr><td>
<table align="center">
<tr><td nowrap align=center>
`v<=x`, `u.y.w<=z`
<hr NOSHADE>
`(u.(y/x)).v.w <= z`<br>
</td><td nowrap align=center>`/`-left</td>
</table>
</td>
</table>
</td>
<td>
<table align="center">
<tr><td>
<table align="center">
<tr><td nowrap align=center>
`x.y<=z`
<hr NOSHADE>
`x <= z/y`<br>
</td><td nowrap align=center>`/`-right</td>
</table>
</td>
</table>
</td>
</tr>
</table>
<p>
Okada and Terui (JSL 1999) proved this result in logical form for
(non)commutative propositional intuitionistic linear logic.
<p>
<b>Theorem:</b> The variety of residuated lattices has a decidable
equational theory.
<br>
<b>Proof:</b> <a href=../reslat/gentzenrl.htm>Click here</a>