Simplifying Equivalences in Łukasiewicz Logic I am working on an inference system for infinite valued Łukasiewicz logic, using standard MV-algebras.
As a pre-processing step, I would like to perform (non-exhaustive) simplification of formulae.  So I am wondering what simplifying equivalences hold in the algebra of this logic.  I know that the usual lattice axioms hold:
$$a \lor a = a$$
$$a \land a = a$$
$$ \vdots$$
$$ \text{etc.}$$
The absorption laws listed above would are good examples of simplifying formulae.
Anybody know of some other good simplifying algebraic identities for Łukasiewicz logic?
 A: For a convenient set of identities, have you checked the usual axioms of MV-algebras?  For normal forms, have you had a look at McNaughton's theorem?  The answer to these questions may be found in the work by Antonio Di Nola and by Daniele Mundici.  Have you checked the proof-theoretic approach proposed by George Metcalfe?
A: An infinite valued logic on [0, 1] with max(x, y)=(x$\lor$y), min(x, y)=(x$\land$y), (1-x)=$\lnot$x has the same theorems as a three-valued logic on {0, 1/2, 1} with max for $\lor$, min for $\land$, and (1-x) for $\lnot$.  So, we just need to check the three-valued cases for any proposed simplifying equivalence.  See Walker and Nguyen's A First Course in Fuzzy Logic, the section on the logical aspects of fuzzy sets, for an outline of a proof.  Unfortunately, I don't know if we have a similar situation for the richer structure you've referenced. 
A: To give a few that I've come up with, we have the absorption rules I mentioned:
$$ a \land a = a$$
$$ a \lor a = a$$
We also have some other common lattice rules:
$$ 0 \lor a = a$$
$$ 0 \land a = 0$$
$$ 1 \land a = a$$
$$ 1 \lor a = 1 $$
In fact, all of these can be seen as instances of the general absorption pattern (particular to Łukasiewicz logic):
$$ (a \oplus b) \lor a = (a \oplus b) $$
$$ (a \oplus b) \land a = a $$
There's also double negation:
$$ \neg\neg a = a $$
Here are some simplifying implication rules:
$$ a \to a = 1$$
$$ a \to 0 = \neg a $$
$$ \neg a \to \neg b = b \to a $$
