Simplifying Equivalences in Łukasiewicz Logic

Question

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?

Answer 1

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?

Answer 2

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

Answer 3

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.