GMV Problem Description
Tomasz Kowalski
2010-Feb-01

The general background is that of residuated lattices (RLs), namely, algebras 
that combine a lattice structure and a residuated monoid structure on the same 
universe. The two are linked by sharing the order: the natural lattice order 
coincides with the residuation order. For more on RLs, see [1], here we only
recall a few things essential to the problem at hand. RLs are equationally
defined by 

(x ^ y) ^ z = x ^ (y ^ z).            
(x V y) V z = x V (y V z). 
x ^ x = x.                            
x V x = x.
x ^ y = y ^ x.                        
x V y = y V x. 
(x ^ y) V x = x.                      
(x V y) ^ x = x.

(x * ((x \ z) ^ y)) V z = z.          
((y ^ (z / x)) * x) V z = z.
(x \ ((x * y) V z)) ^ y = y.
(((y * x) V z) / x) ^ y = y.

(x * y) * z = x * (y * z).            
1 * x = x.                            
x * 1 = x. 

A particularly important subvariety of RLs is the variety of lattice-ordered
groups (l-groups, LGs). These are defined, relative to RL, by

(LG) x * (x \ 1) = 1.  

from which it follows that x \ 1 = 1 / x and so either of these can play the role of
the group inverse. Another important subvariety is that of integral RLs (IRLs), 
defined by  

(I) x \ 1  = 1. 

which is equivalent to the requirement that the monoid unit be the top
element. Three good examples of RLs come from the integers. Firstly, the
integers under addition and the natural ordering form an l-group, where
residuation is given by ordinary subtraction reversed, i.e., 
x \ y = y - x. Secondly, the non-positive integers under addition and truncated 
residuation form an integral RL. Thirdly, an interval [k,0] (k negative, of
course) under truncated addition and truncated subtraction forms an integral RL
which also happens to be an MV-algebra, a member of another important subvariety
of RLs (MV stands for many-valued and goes back to \L{}ukasiewicz's many-valued
logic). 

The three examples above have Generalised MV-algebras (GMVs) as a common
generalisation. GMVs are defined by 

(GMV1) x V y = x / ((x V y) \ x).           
(GMV2) x V y = (x / (x V y)) \ x.

In presence of integrality, GMV1 and GMV2 are respectively equivalent to 

(IGMV1) x V y = x / (y \ x).            
(IGMV2) x V y = (x / y) \ x.

The last thing to observe before we can state the problem is that
LGs and IGMVs are as far apart as they could be, namely, if an algebra
is both an LG and an IGMV, then it is trivial. This suggests that
GMVs should be somehow composed of an LG part and a IGMV part. 
Indeed, we have: 

THEOREM. GMV-algebras decompose as direct products of LGs and IGMVs. 

This is proved in [2] by semantic means. Our goal is to prove the same
syntactically. To this end, we employ the observation that the varieties
LG and IGMV are independent in the sense of [3], namely, there is 
a binary term x @ y, such that

LG   |= x @ y = x
IGMV |= x @ y = y

Indeed, it is easy to see that the term (x * (x \ 1)) * ((y \ 1) \ 1) satisfies the
conditions. We can then axiomatise the varietal join of LG and IGMV by the
following 15 equations:

(1) x @ x = x.                    
(2) (x @ y) @ z = x @ z.          
(3) x @ (y @ z) = x @ z. 

stating that the relations defined by (a,b) \in P1 iff a @ b = b and 
(a,b) \in P2 iff a @ b = a are reflexive and transitive (symmetry also follows) 

(4) (x ^ y) @ (z ^ u) = (x @ z) ^ (y @ u). 
(5) (x V y) @ (z V u) = (x @ z) V (y @ u).
(6) (x \ y) @ (z \ u) = (x @ z) \ (y @ u).
(7) (x / y) @ (z / u) = (x @ z) / (y @ u).

stating that P1 and P2 preserve the operations, so they are congruences, and,
finally  

(8) (x * (x \ 1)) @ 1 = x * (x \ 1).  
(9) 1 @ (x * (x \ 1)) = 1.

(10) (x \ 1) @ 1 = 1.                 
(11) 1 @ (x \ 1) = x \ 1.

(12) (x / (y \ x)) @ (x V y) = x V y.   
(13) ((x / y) \ x) @ (x V y) = x V y. 

(14) (x V y) @ (x / (y \ x)) = x / (y \ x). 
(15) (x V y) @ ((x / y) \ x) = (x / y) \ x. 
 
stating that the P1-image is an LG, and the P2-image an IGMV. Notice
how the LG axiom is "embedded" in (8) and (9), the I axiom in
(10) and (11), and the IGMV axioms in (12)-(15). An equivalent, but slightly
different, set of axioms is given in [4]. Now, to get the desired result, it
suffices to prove that (1)-(15) follow from the GMV axioms. 

References

[1]  Galatos N., Jipsen P., Kowalski T., Ono H.:  Residuated Lattices: An
  Algebraic Glimpse on Substructural Logics.  Studies in Logic and the
  Foundations of Mathematics, vol. 151.  Elsevier, Amsterdam (2007) 

[2] Galatos N., Tsinakis, C.: Generalized MV-algebras.
  Journal of Algebra 
  \textbf{283} 254--291 (2005)

[3]  Gr\"{a}tzer G., Lakser H., P\l onka J.:  
  Joins and direct products of equational classes. 
  Canadian Mathematical Bulletin
  \textbf{12}, 741--744 (1969)

[4]  J\'{o}nsson B., Tsinakis C.:
  Products of classes of residuated structures. 
  Studia Logica 
  \textbf{77}, 267--292 (2004)