An algebraic investigation of Linear Logic

Abstract In this paper we investigate two logics (and their fragments) from an algebraic point of view. The two logics are: $$\textsf{MALL}$$ <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"> <mml:mi>MALL</mml:mi> </mml:math> (multiplicative-additive Linear Logic) and $$\textsf{LL}$$ <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"> <mml:mi>LL</mml:mi> </mml:math> (classical Linear Logic). Both logics turn out to be strongly algebraizable in the sense of Blok and Pigozzi and their equivalent algebraic semantics are, respectively, the variety of Girard algebras and the variety of girales. We show that any variety of girales has a TD-term and hence equationally definable principal congruences. Also we investigate the structure of the algebras in question, thus obtaining a representation theorem for Girard algebras and girales. We also prove that congruence lattices of girales are really congruence lattices of Heyting algebras, thus determining the simple and subdirectly irreducible girales. Finally we introduce a class of examples showing that the variety of girales contains infinitely many nonisomorphic finite simple algebras.