\betaegin{document}

\tauitle{An algebraic investigation of Linear Logic}
\alphauthor{Paolo Aglian\`{o}\\
DIISM\\
Universit\`a di Siena\\
Italy\\
agliano@live.com
}
\deltaate{}
\title{An algebraic investigation of Linear Logic}

\betaegin{abstract} In this paper we investigate two logics from an algebraic
point of view. The two logics are: $\mathsf {MALL}$ (multiplicative-additive
Linear Logic) and $\mathsf {LL}$ (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 equationally definable principale congruences and we classify all
varieties of Girard algebras having this property. 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 and we construct examples
in order to show that the variety of girales contains infinitely many
nonisomorphic finite simple algebras.
\varepsilonnd{abstract}

This note is a reworking of a manuscript (which dates back to the late 1990's) that  had a very limited circulation at the time and was never published.
Lately it has been suggested that I made it  available on arxiv so I decided to review it, correcting the usual mistakes and modernizing it a little bit.
I wish to thank Carles Noguera and Wesley Fussner who encouraged me to complete this little project.

\section{Introduction}

When one wishes to investigate a nonclassical logic one has a
choice between two approaches: the syntactical  and the
algebraic.
The first usually gives rise to a {\varepsilonm relational (Kripke-style) semantics},
while the other deals with {\varepsilonm algebraic semantics}.
The great success of Kripke in the sixties with his  relational semantics for
modal and intuitionistic logic was a source of inspiration for many
researches based on his methods, while the algebraic approach
receded into the background. The algebraic approach became fashionable again
starting in the late seventies, mainly because of the work of W. Blok and
D. Pigozzi. W. Blok, in
his Ph.D. thesis \cite{Blok1976},  conducted an
in-depth study of Lewis' modal logic S4, and in \cite{Blok1980} he
investigated the entire {\varepsilonm lattice of modal logics} by purely algebraic
means. Later he and D. Pigozzi investigated thoroughly the matter of
algebraizability of logics \cite{BlokPigozzi1989,BlokPigozzi1992}. This
investigation
set the foundation for a new field, now commonly called {\varepsilonm abstract
algebraic logic}.

One of the first results of their line of investigation was the
identification  of the ``right'' concept of {\varepsilonm algebraizable logic}.
Roughly speaking, a logic $\sf L$ is algebraizable if there is a class $\vv
K$
 of algebras (no
infinitary operations, no relations, no second
order axioms) which is to $\sf L$ what the variety of Boolean algebras is to
classical propositional calculus.  The class $\vv K$ is called the
{\varepsilonm equivalent algebraic semantics}  of {\sf L}. The
knowledge that a given class $\vv K$ of algebras
is the equivalent algebraic semantics of a known logical system
yields a good deal of information on its algebraic structure.
Conversely, one can discover algebraic properties of members of $\vv K$
that can be transformed into logical data.

In this note we will apply this machinery to two logics:
{\varepsilonm multiplicative-additive linear logic} ({\sf MALL}) and
{\varepsilonm classical linear logic} ({\sf LL}).
 Both {\sf MALL} and {\sf LL} will turn out to be
algebraizable. As is  usually the case it is no surprise what
their equivalent classes are: they consist of residuated lattices (possibly with a modal operator) obeying equations reflecting the logical
axioms.

\section{Linear Logic}

Linear Logic
 is a ``resource-conscious'' logic
introduced by J.-Y. Girard in the late 80's \cite{Girard1987}. Since then
Linear Logic has been developed by Girard himself, by his school and by many,
many others  the  full list of whom would be too long to include here.

Linear Logic is resource conscious in that the left side of a sequent
represents a resource that cannot be used freely. In a Gentzen-style
axiomatization this consciousness shows itself by the absence of the
classical weakening and contraction rules. For instance $A,A \vdash B$
means that we use two resources of type $A$ to get a datum of type $B$.
Moreover---and this is the main difference from other substructural
logics---Girard introduced two operators (the {\varepsilonm exponentials}) that serve
to allow
weakening and contraction in a controlled way on individual formulas.

The propositional language of Linear Logic consists of four families
of connectives\varphiootnote{our notation is slightly different from the original formulation, in that $\tauextsf{\betaf 0}$ and $\betaot$ are exchanged; the reason is that the original formulation conflicts with the common usage in residuated lattices.}:
\betaegin{enumerate}
\item[$\betaullet$] the {\varepsilonm multiplicative} connectives: $\cdot$ ,
$\mathrel{\betaindnasrepma}$ (the par, i.e. the parallel ``or''), $\rightarrow$ (the linear implication,
Girard's $\relbar\joinrel\hspace{2.6pt}\smallcirc$), $\tauextsf{\betaf 0}$  and $\tauextsf{\betaf 1}$;
\item[$\betaullet$] the {\varepsilonm additive} connectives: $\vee$, $\wedge$, $\tauop$ and
$\betaot$;
\item[$\betaullet$] the {\varepsilonm linear negation} $\neg$,
which is
a de Morgan
involution with respect to
$\vee$ and $\wedge$;
\item[$\betaullet$] the {\varepsilonm exponentials}: $\varepsilonscl$ and $\tauext{\large$\mathop{?}$\normalsize}$.
\varepsilonnd{enumerate}
A suggestive way of thinking about how these connectives work is to view
formulas as data types. For instance $A \wedge B$ is a datum from which we can
extract, once, either a datum of type $A$ and a datum of type $B$; $A\cdot
B$
is just a pair of data; $A\rightarrow B$ is a method of transforming a single
datum of type $A$ into a datum of type $B$; $\varepsilonscl A$  indicates that
we can extract as many data of type $A$ as we like (weakening and contraction
on the left side of a sequent); and so on.

The original formulation of Linear Logic is in a Gentzen-style
axiomatization. However, in order to take advantage of Blok-Pigozzi's theory
of algebraizability, it is helpful to look at Linear Logic as a 1-deductive
system in the sense of \cite{BlokPigozzi1992}.
When we turn a logical system into a deductive system, we use a
procedure that might not be in accordance with the original motivation for
introducing the logical system. This is patent in the case of substructural
logics, in that any deductive system satisfies all the structural rules
by definition.
In general, if a logical system is presented as the set of theorems
of a Hilbert-style formal system, then it  defines a 1-deductive system
in a standard way.
Here is the Hilbert-style axiomatization of the sistem $\mathsf{LL}$  as presented by A.
Avron \cite{Avron1988},
consisting  of twenty-four axioms and three inference rules.

\betaigskip
\small
\betaegin{tabular}{ll}
$\tauext{(HL1)}\quad p \rightarrow p$
&$\tauext{(HL2)}\quad (p \rightarrow q)\rightarrow((q \rightarrow r)\rightarrow (p \rightarrow r))$\\[.1in]
$\tauext{(HL3)}\quad (p\rightarrow(q\rightarrow r)) \rightarrow (q\rightarrow(p\rightarrow r))$
&$\tauext{(HL4)}\quad \neg\neg p \rightarrow p$\\[.1in]
$\tauext{(HL5)}\quad (p \rightarrow\neg q) \rightarrow (q \rightarrow \neg p)$
&$\tauext{(HL6)}\quad p \rightarrow (q \rightarrow p \cdot q)$\\[.1in]
$\tauext{(HL7)}\quad p\rightarrow(q\rightarrow r) \rightarrow(p\cdot q \rightarrow r)$
&$\tauext{(HL8)} \quad \tauextsf{\betaf 1}$\\[.1in]
$\tauext{(HL9)}\quad \tauextsf{\betaf 1}\rightarrow(p\rightarrow p)$
&$\tauext{(HL10)}\quad p\rightarrow (\neg p\rightarrow \tauextsf{\betaf 0})$\\[.1in]
$\tauext{(HL11)}\quad \neg \tauextsf{\betaf 0}$
&$\tauext{(HL12)}\quad  p \wedge q  \rightarrow p$\\[.1in]
$\tauext{(HL13)}\quad  p \wedge q \rightarrow q$
&$\tauext{(HL14)}\quad (p\rightarrow q) \wedge (p\rightarrow r) \rightarrow (p \rightarrow q \wedge
r)$\\[.1in]
$\tauext{(HL15)}\quad  p \rightarrow p \vee q$
&$\tauext{(HL16)}\quad q \rightarrow p \vee q$\\[.1in]
$\tauext{(HL17)}\quad  (p\rightarrow r) \wedge (q\rightarrow r) \rightarrow (p\vee q \rightarrow r)$
&$\tauext{(HL18)}\quad p \rightarrow \tauop$\\[.1in]
$\tauext{(HL19)}\quad \betaot \rightarrow p $
&$\tauext{(HL20)}\quad  q \rightarrow (\varepsilonscl p \rightarrow q)$\\[.1in]
$\tauext{(HL21)}\quad  (\varepsilonscl p \rightarrow (\varepsilonscl p\rightarrow q))\rightarrow (\varepsilonscl p \rightarrow q)$
&$\tauext{(HL22)}\quad  \varepsilonscl(p\rightarrow q) \rightarrow (\varepsilonscl p \rightarrow \varepsilonscl q)$\\[.1in]
\varepsilonnd{tabular}

\betaegin{tabular}{ll}
$\tauext{(HL23)}\quad \varepsilonscl p \rightarrow p$
&$\tauext{(HL24)}\quad  \varepsilonscl p \rightarrow \varepsilonscl\varepsilonscl p$ \\[.1in]
$\tauext{(MP)} \qquad \deltafrac{p\quad p\rightarrow q}{q}$
&$\tauext{(Adj)}\qquad \deltafrac{p\quad q}{p \wedge q}$\\[.1in]
$\tauext{(Nec)} \qquad \deltafrac{p}{\varepsilonscl p}$&
\varepsilonnd{tabular}

\betaigskip
\normalsize

For the logical reasons why we need to introduce the (Adj) rule, we refer the reader to \cite{Avron1988}, p.171.
We call $\mathsf{MALL}$ the {\varepsilonm multiplicative-additive linear logic}, i.e. the exponential-free fragment; it is of course
axiomatized by (HL1)-(HL19) plus (MP) and (Adj).
Moreover:
\betaegin{enumerate}
\item [-] In {\sf MALL} one can define $p \mathrel{\betaindnasrepma} q$ as $\neg p \rightarrow q$.
\item [-] In {\sf LL} one  can define $\tauext{\large$\mathop{?}$\normalsize} p$ as $\neg \varepsilonscl(\neg p)$.
\item [-] Finally $\vdash_{\sf MALL} p\rightarrow q$ if and only if $\vdash_{\mathsf{MALL}} \Longleftrightarrow
\neg(p\cdot\neg
q)$.
\varepsilonnd{enumerate}

\section{Consequence relations}

In his original paper \cite{Girard1987},
J.-Y. Girard gave absolutely no meaning to the concept
of ``linear logical theory'' or to
any kind of associated consequence relation.
The question was tackled  again  by A. Avron \cite{Avron1988}. He
observed that the classical
methods for associating a consequence relation to the Gentzen-type
presentation of Linear Logic gives rise to two meaningful consequence
relations.

\betaegin{enumerate}
\item [$\betaullet$] (The {\varepsilonm internal} consequence relation)
$$
\vuc {\varphi}n \vdash_{\sf LL}^I \psi
$$
iff the corresponding sequent is derived in the Gentzen-type formalism
iff $\varphi_1 \rightarrow(\varphi_2 \rightarrow(\deltaots(\varphi_n \rightarrow \psi)\deltaots))$ is a theorem of
Linear Logic.
\item[$\betaullet$] (The {\varepsilonm external} consequence relation)
$$
\vuc {\varphi}n \vdash_{\sf LL}^E \psi
$$
iff the sequent $\Rightarrow \psi$ is derivable in the Gentzen-type
formalism
obtained from the linear one by adding $\Rightarrow \varphi_1,\deltaots\Rightarrow
\varphi_n$ as axioms.
\varepsilonnd{enumerate}
These two concepts are well known to coincide in classical and
intuitionistic logic but not for Linear Logic. However,
in Theorem 2.7 of \cite{Avron1988} A. Avron showed that\varphiootnote{He really
proved it for the logic {\sf MALL} but the proof carries through once one
adds the exponentials.}
$\Sigma \vdash_{\sf LL} \varphi$ if and only if $\Sigma \vdash_{\sf LL}^E \varphi$, which
seems to imply that our view of Linear Logic as a deductive system is not
totally disconnected from its motivations.

\section{The algebrization}

While the exponentials $\varepsilonscl$ and $\tauext{\large$\mathop{?}$\normalsize}$ were central in Girard's original
idea, the {\varepsilonm exponential-free fragment} of Linear Logic has also attracted
a lot of interest.  Let us stress that {\sf MALL} is  a
honest-to-God substructural logic close to  the well-studied
system {\sf R} of {\varepsilonm Relevance Logic} \cite{AndersonBelnap}.
This connection can be roughly expressed by the equation
$$
\tauext{ {\sf R} $-$ contraction =  {\sf MALL} $+$ distribution}.
$$
Techniques from {\sf R} have been applied to {\sf MALL} with some success
(see
for instance \cite{AllweinDunn1993}).
Moreover {\sf MALL} is superior to {\sf R} at least in that it has
a {\varepsilonm cut-elimination} theorem. However, everything comes with a price
tag: the lack of distribution in {\sf MALL} makes things harder from
an algebraic point of view.

The relationship between {\sf MALL} and {\sf LL} is complicated.
The axioms (HL22)--(HL24) and (Nec) resemble  the introduction
of an S4 modality.
However (HL20) and (HL21) (weakening and contraction limited to exclamated
formulas) seem to be responsible for a quantum leap: {\sf MALL} is
decidable (really, {\varepsilonm PSPACE-complete})
while {\sf LL} is not \cite{Lincoln1990}.

\betaegin{theorem}\langlebel{MALL} Any fragment of  {\sf LL} contaning $\{\wedge, \rightarrow, \tauextsf{\betaf 1}\}$ is algebraizable with defining
equation
$p \wedge \tauextsf{\betaf 1} = \tauextsf{\betaf 1}$ and congruence formulas $\Delta=\{p\rightarrow q, q \rightarrow p\}$.
\varepsilonnd{theorem}
\betaegin{proof}
The derivations
\betaegin{align*}
&\vdash p \mathrel{\Delta} p\\
&p\mathrel{\Delta} q  \vdash q\mathrel{\Delta}p\\
&p\mathrel{\Delta}q, q \mathrel{\Delta}r\vdash p\mathrel{\Delta} r
\varepsilonnd{align*}
follow readily from axioms (HL1)--(HL3) and
preservation by connectives is  easily checked.

It remains to show that $p\wedge \tauextsf{\betaf 1}\mathrel{\Delta} \tauextsf{\betaf 1} \vdash p$ and that $p\vdash p\wedge \tauextsf{\betaf 1} \mathrel{\Delta} \tauextsf{\betaf 1}$. Thus
for the first
\small
$$
\betaegin{array}{ll}
\tauextsf{\betaf 1} \rightarrow p \wedge \tauextsf{\betaf 1}&\tauext{(Hyp)}\\
\tauextsf{\betaf 1} &\tauext{(HL8)}\\
p\wedge \tauextsf{\betaf 1}&\tauext{(MP)}\\
p &\tauext{(HL12)}
\varepsilonnd{array}
$$
\normalsize
and for the second
\small
\setlength{\alpharraycolsep}{.2 in}
$$
\betaegin{array}{ll}
\tauextsf{\betaf 1} \rightarrow (p \rightarrow p) &\tauext{(HL9)}\\
p\rightarrow(\tauextsf{\betaf 1} \rightarrow p) &\tauext{(HL3) + (MP)}\\
p &\tauext{(Hyp)}\\
\tauextsf{\betaf 1} \rightarrow p &\tauext{(MP)}\\
\tauextsf{\betaf 1} \rightarrow \tauextsf{\betaf 1} &\tauext{(HL1)}\\
(\tauextsf{\betaf 1} \rightarrow p) \wedge (\tauextsf{\betaf 1} \rightarrow \tauextsf{\betaf 1}) \rightarrow (\tauextsf{\betaf 1} \rightarrow p\wedge
\tauextsf{\betaf 1})&\tauext{(HL14)}\\
\tauextsf{\betaf 1} \rightarrow (p\wedge \tauextsf{\betaf 1}) &\tauext{(MP)}\\
p\wedge \tauextsf{\betaf 1} \rightarrow \tauextsf{\betaf 1} &\tauext{(HL13)}\\
p\wedge \tauextsf{\betaf 1}\mathrel{\Delta} \tauextsf{\betaf 1}
\varepsilonnd{array}
$$
\varepsilonnd{proof}

Let $\mathsf{T}$ be any fragment of $\mathsf{MALL}$ containing $\{\rightarrow,\wedge, \tauextsf{\betaf 1}\}$. The type of its EAS $\vv K_{\mathsf {T}}$ is determined by the connectives in $\sf T$ and we will follow the common usage of
denoting them by the same symbols. Moreover
$$
\Gamma \vdash_{\sf T} p \qquad \tauext{iff}
\qquad \{q \wedge \tauextsf{\betaf 1} = \tauextsf{\betaf 1} : q \in \Gamma\} \vDash_{\mathsf{ K_T}} p \wedge\tauextsf{\betaf 1} =
\tauextsf{\betaf 1}.
$$

A (pointed) {\betaf Girard semilattice} is an algebra $\langle A, \rightarrow ,\wedge, 1\rangle$ where, $\langle A, \wedge, 1\rangle$ is a pointed semilattice and moreover for all $a,b,c \in A$
\betaegin{align*}
&1 \rightarrow a = a \tauag{L1}\\
&a \rightarrow a \gammae 1 \tauag{L2}\\
&(a \rightarrow b) \wedge (a \rightarrow c) = a \rightarrow (b \wedge c) \tauag{L3}\\
&a \rightarrow b \le (c \rightarrow a) \rightarrow (c\rightarrow b) \tauag{L4}\\
&a \rightarrow (b \rightarrow c) \le  b \rightarrow (a \rightarrow c) \tauag{L5}\\
& a \rightarrow b, b \rightarrow a \gammae 1 \quad\tauext{implies}\quad a =b \tauag{L6}
\varepsilonnd{align*}
Girard semilattices form a quasivariety $\mathsf{GS}$ that is not a variety (this can be shown by an easy reworking of known  examples).
Let us also observe that $\rightarrow$ is  a BCI implication that is not a residuation (so a Girard semilattice is not in general a residuated semilattice in the sense of
\cite{NemWha1971}).

The following can be proved by standard techniques:

\betaegin{theorem} If $T=\{\rightarrow, \wedge, \tauextsf{\betaf 1}\}$ then $\mathsf{K_T}$ is the quasivariety  of Girard semilattices.
\varepsilonnd{theorem}

\betaegin{proof} Let $\alphalg A \in \mathsf{K_T}$. We define a relation on $A$ by setting
$$
a \le b \qquad  \tauext{iff}\qquad  (a \rightarrow b) \wedge 1 = 1.
$$
The relation is reflexive by (H1), transitive by (H2)  and
the congruence formulas imply antisymmetricity. Hence $\le $ is a partial order on $A$ and
(H12)--(H14) imply that
$a \wedge b$ is the greatest lower bound  of $a$ and $b$, making $\alphalg A$  a pointed semilattice in which (L6) holds.

The rest consists of standard calculations; first observe that (L2) is a direct consequence of (HL9), (L3) comes in the same fashion from
(HL14), (L4) from (HL2) and (HL3) and (L5) from (HL3).   For (L1) we observe that the following derivations hold in $\sf T$:
\small

\setlength{\alpharraycolsep}{.2 in}
$$
\betaegin{array}{ll}
\tauextsf{\betaf 1} \rightarrow (p \rightarrow p) &\tauext{(HL9)}\\
p\rightarrow(\tauextsf{\betaf 1} \rightarrow p) &\tauext{(HL3) + (MP)}\\
\varepsilonnd{array}
$$
\small
\setlength{\alpharraycolsep}{.2 in}
$$
\betaegin{array}{ll}
(\tauextsf{\betaf 1} \rightarrow p) \rightarrow (\tauextsf{\betaf 1} \rightarrow p) &\tauext{(HL1)}\\
\tauextsf{\betaf 1} \rightarrow ((\tauextsf{\betaf 1} \rightarrow p) \rightarrow p )&\tauext{(HL3) + (MP)}\\
(\tauextsf{\betaf 1} \rightarrow p) \rightarrow p &\tauext{(HL8) + (MP))}\\
\varepsilonnd{array}
$$
\normalsize
Via the usual translation this implies (L1).
\varepsilonnd{proof}

Introducing the join causes no problems; an algebra $\langle A,\rightarrow,\vee,\wedge,1\rangle$ is a {\betaf Girard lattice} if
\betaegin{enumerate}
\item[$\betaullet$] $\langle A, \vee, \wedge\rangle$ is a lattice;
\item[$\betaullet$] $\langle A,\rightarrow, \wedge,1\rangle$ is a Girard semilattice;
\item[$\betaullet$] for all $a,b,c \in A$
\betaegin{equation}
(a \rightarrow c) \wedge (b \rightarrow c) = (a \vee b) \rightarrow c. \tauag{L6}
\varepsilonnd{equation}
\varepsilonnd{enumerate}
Clearly the equivalent algebraic semantics of the $\{\rightarrow,\vee\,\wedge,\tauextsf{\betaf 1}\}$-fragment is the quasivariety $\mathsf{GL}$ of Girard lattices.

If we consider the equivalent algebraic semantics of the positive (i.e. without negation) fragment
of linear logic, then we have a BCI-implication that, thanks to (L6) and (L7), forms a residuated pair with $\cdot$. This implies that the equivalent algebraic semantics is is just the variety $\mathsf{CRL}$ of {\betaf commutative residuated lattices}, with or without bounds.

\section{An embedding}\langlebel{firstembedding}

In this section we would like to show that the positive fragment of $\sf MALL$ is not a conservative extension of the $\{\rightarrow,\wedge,\tauextsf{\betaf 1}\}$-fragment. The translation into algebraic terms consist in proving that
the $\{\rightarrow,\wedge,1\}$-subreducts of algebras in $\sf CRL$ form a proper subclass (as a matter of fact a subvariety) of $\sf{GS}$.
This is a consequence of the following well-known fact proved first in \cite{Agliano1996b} and rediscovered many times in the literature.

\betaegin{theorem} \cite{Agliano1996b} For every variety $\vv V$ of commutative residuated lattices, the class of $\{\wedge,\rightarrow,1\}$-subreducts of $\vv V$ is a variety.
\varepsilonnd{theorem}

It is very easy to find a quasiequation holding in the varieties of $\{\rightarrow,\wedge,1\}$-subreducts but not in $\sf GS$; in fact in $\sf CRL$, $\rightarrow $ is a residuation and this somehow carries over
 in the sense that  for all $\{\rightarrow,\wedge,1\}$-subreduct $\alphalg A$ and for all $a,b \in A$
$$
a \rightarrow b\gammae 1 \quad\tauext{implies}\quad   a \le b.
$$
Now it is easily checked that this quasiequation does not hold in $\sf GS$ (since a Girard semilattice in not in general a residuated semilattice).

Let $\vv V$ be the variety of Girard semilattices satisfying the further equation
\betaegin{equation}
x \le ((x \rightarrow y) \wedge 1) \rightarrow y\tauag{L7}
\varepsilonnd{equation}
We claim that $\vv V$ is the variety of $\{\rightarrow,\wedge,1\}$-subreducts of $\sf CRL$.
Now it is easy to show that (L7) holds in any $\{\rightarrow,\wedge,1\}$-subreduct and implies (L6). Hence we only need to show that any member of $\vv V$ is embeddable in a commutative residuated lattice.
First let's prove that the algebras in $\vv V$ have {\varepsilonm residuals without residuations}:

\betaegin{lemma}\langlebel{reslemma} Let $\alphalg A \in \vv V$ and let $a,b,c \in A$; then
\betaegin{enumerate}
\item $a \le b$ if and only if $a \rightarrow b \gammae 1$;
\item $a \le (a \rightarrow b) \rightarrow b$;
\item $a \le b$ implies  $b \rightarrow c \le  a \rightarrow c$ and $c \rightarrow a \le c \rightarrow b$.
\varepsilonnd{enumerate}
\varepsilonnd{lemma}
\betaegin{proof} Suppose $a \le b$; then $a \wedge b = a$. Then by (L3)
$$
(a \rightarrow a) \wedge (a \rightarrow b) = a \rightarrow (a \wedge b) = a \rightarrow a;
$$
so $a \rightarrow b \gammae a \rightarrow a \gammae 1$ by (L2).

Conversely, assume $a \rightarrow b \gammae 1$; then by (L7) and (L1)
$$
a \le ((a \rightarrow b) \wedge 1) \rightarrow b = 1 \rightarrow b = b.
$$

For (2), by (L5) and (L2) we get
$$
a \rightarrow ((a \rightarrow b) \rightarrow b) = (a \rightarrow b) \rightarrow (a \rightarrow b) \gammae 1
$$
and by (1) $a \le (a \rightarrow b ) \rightarrow b$.

The proof of (3) is routine using (1), (L3) and (L5).
\varepsilonnd{proof}

The embedding we are going use is based on the theory of frames developed in \cite{Dunn1993}.  Let $\alphalg A \in \vv V$ and let $\Gamma_\alphalg A$ be the set of semilattice filters of $\alphalg A$; we say that a subset $X \subseteq \Gamma_\alphalg A$ is {\betaf hereditary} if for all $F,G \in \Gamma_\alphalg A$,  $F \in X$ and $F \subseteq G$ implies $G \in X$. We also define for $a \in A$,  $\mathbf a = \{F \in \Gamma_\alphalg A: a \in F\}$ and we note that $\mathbf a$ is hereditary. Note that the the intersection of any family of hereditary subsets is hereditary; so we can define a closure operator in which the closed subsets are precisely the hereditary subsets of $\Gamma_\alphalg A$. It follows that the hereditary subsets of $\Gamma_\alphalg A$ form an algebraic lattice $D(\alphalg A)$ ordered by inclusion.

 Next we define a ternary relation on $\Gamma_\alphalg A$; for $F,G,H \in \Gamma_\alphalg A$
$$
R(F,G,H)\qquad\tauext{if and only if}\qquad \tauext{for all $a,b \in A$, $a \in F$ and $a \rightarrow b \in G$ implies $b \in H$}.
$$
This relation allows us to introduce additional operations: if $X,Y \in D(\alphalg A)$
\betaegin{align*}
&X \circ Y = \{H: \varepsilonxists F \in Y, \varepsilonxists G \in X \ \tauext{with}\ R(F,G,H) \}\\
&X \rightarrow Y = \{H: \varphiorall F,G \ \tauext{if $R(F,H,G)$ and $F \in X$, then $G \in Y$}\}.\\
\varepsilonnd{align*}
Of course the relationships between equations satisfied in $D(\alphalg A)$ and the properties of $R$ are relevant. In \cite{Dunn1986} there is a long list of these correspondences  with no proofs, simply quoting the work of R. Routley and R. Meyer on the semantics of entailment \cite{RoutleyMeyer1973}; some proofs are indeed there, but they are so embedded in the general abstract theory of entailment that their connection to this algebraic setting is not immediately  clear. That's why here we prefer to present direct proofs.

\betaegin{lemma} For any $\alphalg A \in \vv V$, $\langle D(\alphalg A),\circ,\tauextsf{\betaf 1}\rangle$ is a commutative monoid.
\varepsilonnd{lemma}
\betaegin{proof} Proving that $D(\alphalg A)$ is closed under $\circ$ is straightforward.
 Let then $X,Y \in D(\alphalg A)$ and suppose that $H \in X \circ Y$; then there is an $F \in Y$ and a $G \in F$ with $R(F,G,H)$. Let $a \in G$ and $a \rightarrow b \in F$; then (by Lemma \ref{reslemma} $a \le (a \rightarrow b) \rightarrow b \in G$. So since $a \rightarrow b \in F$ and $R(F,G,H)$ we get $b \in H$; so $R(G,F,H)$ holds and hence $H \in Y \circ X$. This shows that $\circ$ is commutative.

Let $\nabla_A$ be the {\varepsilonm positive cone} of $\alphalg A$, i.e. the principal filter generated by $1$. Note that
for any $F \in \Gamma_\alphalg A$, $R(F,\nabla_A,F)$ holds and, since
$\nabla_A \in \tauextsf{\betaf 1}$, we get at once that $ X \subseteq \tauextsf{\betaf 1} \circ  X$. Conversely, let
$H \in \tauextsf{\betaf 1} \circ X$; then there is an $F \in X$ and a $G \in \tauextsf{\betaf 1}$ with
$R(F,G,H)$. If $a \in F$, then $a \rightarrow a \gammae 1 \in G$ and hence
$a \in H$, so that $F\subseteq H$. But $X$ is hereditary and $F \in X$, so
$H \in X$ and eventually $\tauextsf{\betaf 1}\circ X = X$.

Associativity requires more work.  Let $X,Y,Z \in D(\alphalg A)$ with with $H \in (X\circ Y)\circ Z$; then there is an $F \in Z$ and a $U \in X\circ Y$ with $R(F,U,H)$ and  a $K \in X$ and a $G \in Y$ with $R(G,K,U)$.
Let $L=\{ d \in A: b \le a \rightarrow d\ \tauext{for some}\ a \in F, b \in G\}$; then using Lemma \ref{reslemma} we can show that $L \in \Gamma_\alphalg A$ and  clearly $R(F,G,L)$.   Assume now $d \in L$ and $d \rightarrow c \in K$; again by
Lemma \ref{reslemma}, (L4) and (L5) we get
$$
d \rightarrow c \le (a \rightarrow d) \rightarrow (a \rightarrow c)
$$
 so $(a \rightarrow d) \rightarrow (a \rightarrow c) \in K$. Since $d \in L$ there are $a \in F$ and $b \in G$ with $b \le a \rightarrow d$, so $a \rightarrow d  \in G$ and, since $R(G,K,U)$, we get $a \rightarrow c \in U$. But $a \in F$, $a \rightarrow c \in U$ and $R(F,U,H)$ implies $c \in H$. Hence we conclude that $R(L,K,H)$.

Now by definition $L \in Y \circ Z$ and hence, since $R(F,G,L)$,  $H \in X \circ (Y \circ Z)$; we have thus proved that $(X \circ Y) \circ Z \subseteq X \circ (Y \circ Z)$. The opposite inclusion follows from a similar argument, hence
$\circ$ is associative.
\varepsilonnd{proof}

\betaegin{lemma} For each $\alphalg A \in \vv V$, $(\rightarrow,\circ)$ form a residuated pair w.r.t. the lattice ordering of $D(\alphalg A)$.
\varepsilonnd{lemma}
\betaegin{proof} Since we already know that $D(\alphalg A)$ is closed under $\circ$ we have only to check that it is closed under $\rightarrow$ as well. Let then $H \in X \rightarrow Y$; then if $H \subseteq H'$ and $a \rightarrow b \in H'$, then
$a \rightarrow b \in H$. It follows that if $R(F,H',G)$, then $R(F,H,G)$ for all $F,G \in \Gamma_\alphalg A$ and so $H' \in X\rightarrow Y$ which is then hereditary.

Next we have to show that
$$
X \circ Y \subseteq Z \qquad\tauext{if and only if}\qquad X \subseteq Y \rightarrow Z.
$$
Assume then that $X \circ Y \subseteq Z$ and let $H \in X$. Let $F \in Y$ such that $R(F,H,G)$; then by definition $G \in X\circ Y$ and hence $G \in Z$. But this implies $H \in Y \rightarrow Z$, as wished.  Conversely suppose $X \le Y \rightarrow Z$ and let $H \in X \circ Y$; then there are $F \in Y$ and $G \in X$ with $R(F,G,H)$. But then $G \subseteq Y \rightarrow Z$, so if $F \in Y$ and $R(F,G,H)$, then $H \in  Z$ as wished.
\varepsilonnd{proof}

Hence we have shown that:

\betaegin{theorem} For any $\alphalg A \in \vv V$, $\alphalg D(\alphalg A) =\langle D(\alphalg A), \rightarrow,\vee, \wedge,\circ, \tauextsf{\betaf 1}\rangle$ is commutative residuated lattice.
\varepsilonnd{theorem}

Finally we prove the embedding.

\betaegin{theorem} Any algebra $\alphalg A \in \vv V$ is embeddable in $\alphalg D(\alphalg A)$.
\varepsilonnd{theorem}

\betaegin{proof}
Define a mapping $h:\alphalg A \longmapsto H(\alphalg A)$ by
$$
h(a) = \mathbf a.
$$
We start showing that for any $a,b \in A$, $H \in h(a\rightarrow b)$ if and only if $H \in \mathbf a \rightarrow \mathbf b$. This is equivalent to showing that, for $a,b \in A$
$$
a \rightarrow b \in H\qquad\tauext{if and only if}\qquad\tauext{$\varphiorall F,G$ if $R(F,H,G)$ and $a \in F$, then $b \in G$}.
$$
The left-to-right implication is a straightforward consequence of the definitions. Assume now that $a \rightarrow b  \notin H$; we will show that there exists $F,G$ with $a \in F$, $R(F,H,G)$ but $b \notin G$.
Let's denote by $[a)$ the principal filter generated by $a$. Let $F=[a)$ and $G= \{d: \ \tauext{there is a}\ c \in H\ c\le a \rightarrow d\}$; note that $b \notin G$ otherwise $c \le a\rightarrow b$ for some $c \in H$ and since $H$ is a filter we would have $a\rightarrow b \in H$, contrary to the hypothesis. Again we can show that $G$ is a filter using Lemma \ref{reslemma}; so $G \in \Gamma_\alphalg A$, $a \in F$ and $b \notin G$. Now we show that $R(F,H,G)$;  if $u \in F$ and
$u \rightarrow v  \in H$, then $a \le u$ and hence $u \rightarrow v\le a \rightarrow v$,  which by definition implies $v \in G$ and thus  $R(F,H,G)$.

Now $a\le b$ implies  that $\mathbf a \subseteq \mathbf b$, so $h$ is order preserving; hence to conclude the proof it is enough to show that  $h$ is injective. But if $\mathbf a = \mathbf b$, since
$[a) \in \mathbf a$, we get $[a) \in \mathbf b$ so $b \in [a)$; by the same fashion $a \in [b)$ and hence $a =b$.
\varepsilonnd{proof}

\section{Algebraizing $\sf MALL$ and $\sf LL$}

For the complete $\sf MALL$ we have to work a little bit more.  An element $a$ of a commutative residuated lattice is {\betaf involutive} if for all $b \in A$, $(b \rightarrow a) \rightarrow a = b$; it is well known
 \cite{BusanicheCignoli2009}  that if in case we define  $\mathop{\sim} b := (b \rightarrow a) \rightarrow a$, then $\mathop{\sim}$ is a  negation with the following properties
\betaegin{enumerate}
\item[$\betaullet$] $\mathop{\sim}\mathop{\sim} a = a$   (involutive);
\item[$\betaullet$]  $\mathop{\sim} (a \vee b) = \mathop{\sim} a \wedge \mathop{\sim} b$ and $\mathop{\sim}(a\wedge b) = \mathop{\sim} a \vee \mathop{\sim} b$  (De Morgan);
\item[$\betaullet$]  $a \le b$ implies $\mathop{\sim} b \le \mathop{\sim} a$  (antitonic);
\item[$\betaullet$]  $\mathop{\sim}(a\cdot \mathop{\sim} b) = a \rightarrow b$  (contraposition).
\varepsilonnd{enumerate}
It is easily seen that these properties are not independent; for instance any negation that is involutive and satisfies one of the other three properties must satisfy them all.

A structure $\langle A,\vee,\wedge, \rightarrow,\cdot,0,1\rangle$ is a {\betaf Girard algebra} if
\betaegin{enumerate}
\item[$\betaullet$] $\langle A, \vee,\wedge, \rightarrow,\cdot,1\rangle$ is a commutative residuated lattice;
\item[$\betaullet$] $0$ is an involutive element.
\varepsilonnd{enumerate}
In this case $\mathop{\sim} x = x \rightarrow 0$ is an involutive and antitonic so it also De Morgan and satisfie contraposition; so $\rightarrow$ and $\cdot$ are definable in terms of each other.
Conversely any commutative residuated lattice with a negation $\mathop{\sim}$ that is involutive and De Morgan can be seen as a Girard algebra upon defining
$0 = \mathop{\sim} 1$. A {\betaf bounded Girard algebra} is a Girard algebra with an additional constant $\tauop$ satisfying $x \rightarrow \tauop \gammae 1$; we define $\betaot := \mathop{\sim} \tauop$.  By the usual standard arguments we get:

\betaegin{theorem} The equivalent algebraic semantics of $\sf MALL$ is the variety of bounded Girard algebras.
\varepsilonnd{theorem}

Note that there $0$ and $1$ can be in any ordering relation; in particular it may happen that $1 \le 0$, which implies that $\sf MALL$ is not an explosive logic or, alternatively, it is a paraconsistent logic. It is worth noting that explosivity in our case means that
$$
0 = 0 \cdot 1 = 0 \cdot \mathop{\sim} 0 \le a
$$
for all $a$. This implies $0=\betaot$ and hence $1= \tauop$; hence the minimal explosive extension of $\sf MALL$ has as equivalent algebraic semantics the variety of integral Girard algebras. Since in this case the negation is a orthocomplementation  it can be also seen as the variety of residuated ortholattices.

If we look at $\sf LL$ it is clear that adjoining the exponentials corresponds to considering Girard algebras superimposed with a certain S4 modality. A {\betaf girale} is an algebra $\langle A,\vee,\wedge,\rightarrow,\cdot,\mathop{\sim},1, \varepsilonscl\rangle$
where
\betaegin{enumerate}
\item[$\betaullet$] $\langle A,\vee,\wedge,\rightarrow,\cdot,\mathop{\sim},1\rangle$ is a Girard algebra;
\item[$\betaullet$] $\varepsilonscl$ is unary and for all $a,b \in A$
\betaegin{align*}
&\varepsilonscl 1 = 1 \tauag{G1}\\
&\varepsilonscl a \le a \wedge 1 \tauag{G2}\\
&\varepsilonscl a  \varepsilonscl b = \varepsilonscl(a \wedge b) \tauag{G3}\\
&\varepsilonscl\varepsilonscl a = \varepsilonscl a. \tauag{G4}
\varepsilonnd{align*}
\varepsilonnd{enumerate}

Let's prove some algebraic properties of girales.

\betaegin{lemma}\langlebel{girlemma} Let $\alphalg A$ be a girale; then for any $a,b,c \in A$
\betaegin{enumerate}
\item $a \le b$ implies $\varepsilonscl a \le \varepsilonscl b$;
\item $b \le \varepsilonscl a \rightarrow b$;
\item $\varepsilonscl a = \varepsilonscl a \varepsilonscl a$;
\item $ab \le c$ implies $\varepsilonscl a \varepsilonscl b \le \varepsilonscl c$;
\item $a \gammae 1$ implies $\varepsilonscl a =1$;
\item $\varepsilonscl(\varepsilonscl a \varepsilonscl b) = \varepsilonscl a \varepsilonscl b \le \varepsilonscl(ab)$;
\item $\varepsilonscl(a \rightarrow b) \le \varepsilonscl a \rightarrow \varepsilonscl b$;
\item $\varepsilonscl a \rightarrow (\varepsilonscl a \rightarrow b) \le \varepsilonscl a \rightarrow b$.
\varepsilonnd{enumerate}
\varepsilonnd{lemma}
\betaegin{proof} (1) is immediate from (G2) and (G3); next note that in any commutative residuated lattice $b \le (a \wedge 1) \rightarrow b$, thus (2) follows from (G2), while (3) is again a straightforward consequence
of (G3).

If $ab \le c$, then $\varepsilonscl (a \wedge b) = \varepsilonscl a \varepsilonscl b \le c$; hence (4) follows from (1) and (G4) while (5) follows from (1), (G1) and (G2).  For (6) we compute
$$
\varepsilonscl (\varepsilonscl a \varepsilonscl b) = \varepsilonscl \varepsilonscl (a \wedge b) = \varepsilonscl(a \wedge b) = \varepsilonscl a \varepsilonscl b.
$$
Moreover $\varepsilonscl a\varepsilonscl b \le ab$ so
by (1) $\varepsilonscl(\varepsilonscl a \varepsilonscl b) \le \varepsilonscl(ab)$ and hence $\varepsilonscl a \varepsilonscl b \le \varepsilonscl(ab)$.
Next since $\varepsilonscl a \le a$, we get $a \rightarrow b \le \varepsilonscl a \rightarrow b$;
so $(a\rightarrow b) \varepsilonscl a \le b$, so $\varepsilonscl (a \rightarrow b) \varepsilonscl a \le b$ and by (6) $\varepsilonscl (a \rightarrow b) \varepsilonscl a \le \varepsilonscl b$.  So (7) holds.

For (8) we observe that in any  residuated lattice, if $a$ is an idempotent element in a residuated lattice then for all $b$
$$
a(a \rightarrow (a \rightarrow b)) =a^2(a \rightarrow (a \rightarrow b)) \le b
$$
and by residuation
$$
a \rightarrow (a \rightarrow b) \le a \rightarrow b.
$$
Since $\varepsilonscl a$ is idempotent by (3) we conclude that
$$
\varepsilonscl a \rightarrow (\varepsilonscl a \rightarrow b) \le  (\varepsilonscl a \rightarrow b)
$$
so (8) follows.
\varepsilonnd{proof}

Now using Lemma \ref{girlemma} and the usual techniques of algebrization of logical systems it is straightforward to show that:

\betaegin{theorem} $\sf LL$ is strongly algebraizable and its equivalent algebraic semantics is the variety $\vv G$ of bounded girales.
\varepsilonnd{theorem}

So in a way girales have the same relationship to $\sf MALL$  that interior algebras have to classical logic.
More generally they belong to the very general class of (residuated) lattices with a superimposed modality.

\section{Another embedding theorem}

We will show that $\sf LL$ is a conservative extension of $\sf MALL$. Of course we will do it from the algebraic side, i.e. we will prove that the class of subreducts of girales to the type of Girard algebras is the variety of Girard algebras.  This is equivalent to showing that any Girard algebra is embeddable in a girale; in order to do so we will collect several information, that will be useful for other investigations as well, on the algebraic structures of girales.

Let $\alphalg P$ be any poset; we say that $Q$ is a {\betaf relatively complete} subset of $P$ if for all $p \in P$
$$
\sup\{q \in Q: q \le p\}\qquad \inf\{q \in Q: q \le p\}
$$
both exist.

Let $\alphalg A$ be a Girard algebra and let as usual $A^- = \{ a : a \le 1\}$;  a {\betaf relatively complete Heyting} subset of $A$ is a subset $H \subseteq A^-$ with the following properties:
\betaegin{enumerate}
\item  $1 \in H$;
\item $H$ is a relatively complete subset of $A$;
\item $H$ is closed under multiplication;
\item for all $a \in H$, $a^2 = a$.
\varepsilonnd{enumerate}

\betaegin{lemma}\langlebel{relheyting} Let $\alphalg A$ be a Girard algebra and let $H$ be a relatively complete Heyting subset of $A$. If we define $\varepsilonscl_{\small H} a = \sup\{b \in H: b \le a\}$, then
$\langle \alphalg A, \varepsilonscl_{\small H}\rangle$ is a girale. Conversely if $\alphalg A$ is a girale then  $H = \varepsilonscl A = \{\varepsilonscl a: a \in A\}$ is a relatively complete Heyting subset of
$\alphalg A$ and $\varepsilonscl_{\small H} a = \varepsilonscl a$.
\varepsilonnd{lemma}
\betaegin{proof} We have to check that $\varepsilonscl_H$ satisfies (G1)-(G4);  (G1) is obvious since $H \subseteq A^-$ and $1 \in H$ and (G2) follows from the definition of $\varepsilonscl_H$.
Since clearly $a \le b$ implies $\varepsilonscl_H a \le \varepsilonscl_H b$ and $\varepsilonscl_H a \varepsilonscl_H a = \varepsilonscl_H a$, from $\varepsilonscl_H(a \wedge b) \le \varepsilonscl_H a, \varepsilonscl_H b$ we get $\varepsilonscl_H(a\wedge b) \le \varepsilonscl_H a \varepsilonscl_H b$.
For the converse, note that $\varepsilonscl_H a \le a \wedge 1$ and $\varepsilonscl_H b \le b \wedge 1$; since $H$ is closed under multiplication we get
$$
\varepsilonscl_H a \varepsilonscl_H b = (\varepsilonscl_H a \varepsilonscl_H b)(\varepsilonscl_H a \varepsilonscl_H b) \le (a \wedge 1)(b \wedge 1) \le a \wedge b \wedge 1.
$$
This proves that $\varepsilonscl_H a \varepsilonscl_H b \le \varepsilonscl_H (a \wedge b)$ and hence (G3). Finally (G4) is obvious from the definition of $\varepsilonscl_H$.

Since $1 \in \varepsilonscl A$ by (G1), $\varepsilonscl A\subseteq A^-$ by (G2),  it is closed under products by (G3) and consists of idempotents by Lemma \ref{girlemma}(3),  we need only to show that
$$
\varepsilonscl a =\sup\{\varepsilonscl b: \varepsilonscl b \le a\}.
$$
Now if $b \le \varepsilonscl a$, then $\varepsilonscl b \le \varepsilonscl a$ by Lemma \ref{girlemma}(1); so $\varepsilonscl a$ is an upper bound.  Let $\varepsilonscl b \le c$ for all $\varepsilonscl b \in \varepsilonscl A$ such that $\varepsilonscl b \le a$; since $\varepsilonscl a \le a$ we get that
$\varepsilonscl a \le c$, so $\varepsilonscl a$ is the least upper bound.
\varepsilonnd{proof}

\betaegin{corollary} Every complete Girard algebra is embeddable in (as a matter of fact, it is a reduct of) a girale.
\varepsilonnd{corollary}
\betaegin{proof} In this case the set $H= \{a: a\le 1\ \tauext{and}\  a^2=a\}$ is a nonempty relatively complete Heyting subset of $A$ and Lemma \ref{relheyting} applies.
\varepsilonnd{proof}

So to prove that Girard algebras are exactly subreducts of girales it is enough to show that any Girard algebra can be embedded in a complete Girard algebra. Now we could be tempted to use the same embedding
we used for Girard lattices; as a matter of fact it is not hard to show that if $\alphalg A$ is a commutative residuated lattice then $\alphalg A$ is embeddable in the complete and commutative residuated lattice $D(\alphalg A)$
(see \cite{Agliano1996b} for details). However introducing an involutive De Morgan negation causes problems; these problems can of course be solved by constructing a different embedding using for instance the circle
of ideas in \cite{AllweinDunn1993}, but we have a different and more direct embedding that does the job and we proceed to illustrate it.

Let $\alphalg A$ be a Girard algebra; we define a binary relation $R$ on $A$ by $(a,b) \in R$ if and only if $\mathop{\sim} b \not\gammae a$; this relation is symmetric since $\mathop{\sim}$ is De Morgan. As for all binary relations
there is a closure operator $Q$ naturally associated to it; if $U \subseteq A$ we can define $Q(U) = \{a: (u,a) \in R\ \tauext{for some}\ u \in U\}$. It is a standard exercise to prove that $Q$ is a closure
operator on $A$ and hence the closed sets form a complete lattice with universe $C(\alphalg A)$.

\betaegin{lemma} Let $\alphalg A$ be a girard algebra; then $\alphalg C(\alphalg A) = \langle C(\alphalg A),\vee,\wedge, \rightarrow, \cdot, \mathop{\sim}, \mathbf 1\rangle$ is a complete Girard algebra upon defining for $X,Y \in C(\alphalg A)$
\betaegin{align*}
&X \cdot Y = Q(\{ab: a \in X, b \in Y\}) \\
&\mathop{\sim} X = \{b: \mathop{\sim} c \not\gammae b\ \tauext{implies}\ c \gammae a\ \tauext{for all}\  a \in X\}\\
&X \rightarrow Y = \mathop{\sim}(X \cdot \mathop{\sim} Y)\\
&\tauextsf{\betaf 1} = Q(1).
\varepsilonnd{align*}
\varepsilonnd{lemma}

By our previous discussion to prove the lemma it is enough to show that the negation defined above is involutive and satisfies contraposition; this is a simple exercise, using the analogous properties of the negation in Girard algebras, and we leave it to the reader.
The next lemma is more important.

\betaegin{lemma} Let $\alphalg A$ be a Girard algebra and for $a \in A$ let's denote by $(a]$ the principal ideal generated by $a$. Then
\betaegin{enumerate}
\item for any $a \in A$, $(a]= Q(a) \in C(\alphalg A)$;
\item the mapping $a \longmapsto (a]$ is an embedding of $\alphalg A$ in $\alphalg C(\alphalg A)$.
\varepsilonnd{enumerate}
\varepsilonnd{lemma}
\betaegin{proof} Observe that
$$
 Q(a) = \{b: c \not\gammae b  \ \tauext{implies}\ c\not\gammae a\}.
$$
Suppose that $b \notin (a]$; then  $b \not \le a$ and then $b \notin Q(a)$. Conversely if $b \notin Q(a)$,
then there exists a $c$ with $\mathop{\sim} c \not\gammae b$,
and $\mathop{\sim} c \gammae a$; hence $b \not\le a$ and  so
$b \notin (a]$. This proves (1).

For (2) it is obvious that the mapping is a meet homomorphism.
Let's  show that
$$
(a] \vee (b] = (a \vee b]
$$
 Observe that $(a] \vee (b] = Q((a] \cup (b])$. Since
$(a] \cup (b] \subseteq (a \vee b]$ and the latter is closed, one inclusion is
clear. Next observe that
$$
(a]\vee (b] = \{c: \mathop{\sim} d \not\gammae c \ \tauext{implies}\ (\mathop{\sim} d\not\gammae e\ \tauext{for
some}\ e \le a\ \ \tauext{or}\ \ \mathop{\sim} d\not\gammae f\ \tauext{for some}\ f \le b)\}.
$$
Let  $c \notin (a] \vee (b]$. Then there exists a $d$
with $\mathop{\sim} d \not\gammae c$ but $\mathop{\sim} d \gammae a$ and $\mathop{\sim} d \gammae b$. Hence
$\mathop{\sim} d \gammae a \vee b$ and so, since $\mathop{\sim} d \not\gammae c$,  $c \notin (a \vee b]$.

A similar argument shows that
$$
(a]\cdot (b] = Q(\{uv:  u\le a, \ v \le b\}) = (ab].
$$
Next we check that
$$
(\mathop{\sim} a] =\mathop{\sim}(a] = \{ b: c \not \gammae b \ \tauext{implies}\ c \not\le a\}.
$$
Suppose that $b \notin \mathop{\sim}(a]$. Then there
exists a $c$ with $\mathop{\sim} c \not\gammae b$ and $c \le a$. Thus $b \not\le \mathop{\sim} a$,
otherwise
$b \le \mathop{\sim} a \le \mathop{\sim} c$.
Conversely if  $b\not\le \mathop{\sim} a$, then $\mathop{\sim} a \not\gammae b$ and thus
 $b \notin \mathop{\sim}(a]$.

Since $\rightarrow$ is definable in both cases by the negation the mapping is a homomorphism and it is obviously injective.
\varepsilonnd{proof}

\betaegin{corollary} Every (bounded) Girard algebra is embeddable in a (bounded) girale; hence the variety of (bounded) Girard algebras is exactly the class of subreducts
of (bounded) girales. Therefore $\sf LL$ is a conservative extension of $\sf MALL$.
\varepsilonnd{corollary}

\section{Congruences}

Congruences in commutative residuated lattices are well known; since the variety $\sf CRL$ of commutative residuated lattices is ideal-determined in the sense of \cite{AglianoUrsini1992} the congruences ar completely determined by certain subsets of the universe that we call {\betaf U-ideals} (Ursini ideals). In case of $\sf CRL$ these subsets have a particularly transparent description; if $\alphalg A \in \vv{CRL}$ a {\betaf filter} of $\alphalg A$ is a subset $F \subseteq A$ such that
\betaegin{enumerate}
\item[$\betaullet$] $F$ is a lattice filter;
\item[$\betaullet$] $1 \in F$;
\item[$\betaullet$] if $a, a \rightarrow b \in F$ , then $b \in F$.
\varepsilonnd{enumerate}
Since the intersection of any family of filters is clearly a filter, there is a closure operator on $A$ in which the closed sets are exactly the filters; the operator is easily shown to be algebraic,  so the filters of $\alphalg A$ form an algebraic lattice $\omegap{Fil}(\alphalg A)$. The following fact was observed first in \cite{Agliano1996b} and has been rediscovered many times since.

\betaegin{theorem}\langlebel{confil} If $\alphalg A \in \vv{CRL}$ then $\Con A$ and $\omegap{Fil}(\alphalg A)$ are isomorphic through the mappings $\tauheta \longmapsto 1/\tauheta$ and
$F \longmapsto \tauheta_F = \{(a,b): a \rightarrow b, b \rightarrow a \in F\}$.
\varepsilonnd{theorem}

Now it is evident that a congruence of a Girard algebra is a congruence of its underlying commutative residuated lattice structure, so Theorem \ref{confil} specializes easily to Girard algebras.  What about girales? They are still  ideal-determined, so the congruences are totally determined by the U-ideals. However the operation
$\varepsilonscl$ is a {\varepsilonm compatible operation} in the sense of \cite{Agliano1996b}; this in turn implies that the U-ideals of a girale $\alphalg A$ are just the filters of its underlying Girard algebra, that are closed under $\varepsilonscl$.
We will name these subsets  {\varepsilonm filters} as well and let the context clear the meaning. In any case Theorem \ref{confil} holds; if $\alphalg A$ is a girale its congruence lattice is isomorphic with the lattice of filters.
Moreover we get the following useful description:

\betaegin{lemma}\langlebel{filgen} Let $\alphalg A$ be a girale, let $X \subseteq A$ and let $\omegap{Fil}_\alphalg A(X)$ the filter generated by $X$; then
$$
\omegap{Fil}_\alphalg A(X) = \{a: \varepsilonscl b_1 \deltaots \varepsilonscl b_n \le a\ \tauext{for some}\ \vuc bn \in X\}.
$$
\varepsilonnd{lemma}
\betaegin{proof}  Let $F$ be the set described by the right hand side of the equality. Then  $F$ is a lattice filter, since it is the union of a directed family of lattice filters; moreover if
$a \in F$, then there are $\vuc bn \in X$ such that
$$
\varepsilonscl (b_1 \wedge \deltaots \wedge b_n) = \varepsilonscl b_1\deltaots \varepsilonscl b_n \le a.
$$
This implies immediately that $\varepsilonscl a \in F$, so $F$ is a filter which contains $X$. If $G$ is another filter containing $X$ then $F \subseteq G$, so $= \omegap{Fil}_\alphalg A(X)$.
\varepsilonnd{proof}

Lemma \ref{filgen} has obvious consequences; let $[a)$ denote the principal filter generated by $a$.

\betaegin{corollary}\langlebel{cor1} Let $\alphalg A$ be a girale; then for any $a \in A$, $\omegap{Fil}_\alphalg A(a) = [\varepsilonscl a)$. In other words  every principal filter of $\alphalg A$ is principal as a lattice filter.
\varepsilonnd{corollary}

\betaegin{corollary} The variety $\sf Gi$ of girales has equationally definable principal congruences.
\varepsilonnd{corollary}
\betaegin{proof} For any girale $\alphalg A$ and for $a,b \in A$ let $a \leftrightarrow b:= (a \rightarrow b) \wedge (b \rightarrow a)$ and by $[a)$ the principal lattice filter generated by $a$. Then by $\omegap{Fil}_\alphalg A(a \leftrightarrow b) = [\varepsilonscl(a \leftrightarrow b)$; hence $ c \leftrightarrow d \in \omegap{Fil}_\alphalg A(a \leftrightarrow b)$ if and only if $\varepsilonscl(a \leftrightarrow b) \le c \leftrightarrow b$. But using the isomorphism between the congurence lattice and the filter lattice it is easily seen that $\omegap{Cg}_\alphalg A(a,b) = \omegap{Cg}_\alphalg A(1,\varepsilonscl(a \leftrightarrow b))$. So we get that
$$
(c,d) \in \omegap{Cg}_\alphalg A(a,b)\qquad\tauext{if and only if}\qquad \varepsilonscl(a \leftrightarrow b) \le c \leftrightarrow d
$$
i.e.  $\vv{Gi}$ has equationally definable principal congruences.
\varepsilonnd{proof}

Through the general theory of algebraizable logics we get that $\sf LL$ has the deduction theorem: $\Gamma, p \vdash_{\sf LL} q$ if and only if $\Gamma \vdash_{\sf LL} \varepsilonscl p \rightarrow q$. But this is of course
well known \cite{Avron1988}.

From Lemma \ref{relheyting} we know that $\varepsilonscl A$ is a relatively complete Heyting subset of $\alphalg A$; with some adjustment it can be made into a Heyting algebra
$\varepsilonscl \alphalg A$ which is deeply connected with $\alphalg A$.

\betaegin{theorem} For any girale $\alphalg A$, $\varepsilonscl \alphalg A = \langle \varepsilonscl A, \vee, \wedge_{!},\rightarrow_{!},\betaot,1\rangle$ is a Heyting algebra, where for $u,v \in \varepsilonscl A$
$$
u \wedge_{!} v = u \wedge v\qquad  u \rightarrow_{!}v = \varepsilonscl (u \rightarrow v).
$$
Moreover $\Con A \cong \omegap{Con}(\varepsilonscl \alphalg A)$.
\varepsilonnd{theorem}
\betaegin{proof} We observe first that $\varepsilonscl$ is a {\varepsilonm conucleus} in the sense of \cite{MontagnaTsinakis2010}; then we apply Lemma 3.1 in \cite{MontagnaTsinakis2010} to conclude that
 $\varepsilonscl \alphalg A$ is a commutative residuated lattice. Since $\varepsilonscl 1  = 1$, it is also integral and by Lemma \ref{girlemma}(3) every element
of $\varepsilonscl \alphalg A$ is idempotent. This is enough to deduce that $\varepsilonscl \alphalg A$ is a Heyting algebra.

Next  we  show that the  the mappings
$$
H \longmapsto H \cap \varepsilonscl A \qquad\qquad
G \longmapsto \omegap{Fil}_{\alphalg A} (G)
$$
induce a lattice isomorphism between the filter lattice of $\alphalg A$ and the filter lattice of $\varepsilonscl \alphalg A$.  Since they both clearly preserve the ordering we need only check that they are well defined and their
composition is the identity on the respective domains.

That for any filter $H$ of $\alphalg A$,  $H \cap \varepsilonscl A$ is a filter of $\varepsilonscl \alphalg A$, it is a consequence of
Lemma \ref{girlemma}(4). Now let $G$ be a filter of $\varepsilonscl \alphalg A$ and let
$H = \omegap{Fil}_{\alphalg A}(G)$. We will show that $ H \cap \varepsilonscl A = G$.
Clearly $G \subseteq H \cap \varepsilonscl A$.
If $\varepsilonscl a \in H$, then  by Lemma \ref{filgen} there are $\vuc {\varepsilonscl b}n \in G$
such that
$$
\varepsilonscl b_1\deltaots \varepsilonscl b_n \le \varepsilonscl a.
$$
But since
$$
\varepsilonscl b_1\deltaots \varepsilonscl b_n= \varepsilonscl(b_1 \wedge\deltaots\wedge b_n) = \varepsilonscl b_1 \wedge_! \deltaots \wedge_! \varepsilonscl b_n
$$
by the usual description of filters in a Heyting algebras
we get that $\varepsilonscl_F a \in G$.

On the other hand if $H$ is a filter of $\alphalg A$, it is obvious that $\omegap{Fil}_{\alphalg A}(H \cap \varepsilonscl A) =H$ is obvious,
since $\varepsilonscl a \le a$.
\varepsilonnd{proof}

Let us define an operator $\omegap{Heyt}$ on a class $\vv K$ of girales by
$$
\omegap{Heyt}(\vv K)= \{ \varepsilonscl \alphalg A: \alphalg A \in \vv K\}.
$$

\betaegin{theorem} For any variety $\vv V$ of girales, $\omegap{Heyt}(\vv V)$ is a variety of (pointed) Heyting algebras.
\varepsilonnd{theorem}
\betaegin{proof} We need only to show that $\omegap{Heyt}(\vv V)$ is closed under ${\mathbf H},{\mathbf S}$ and ${\mathbf P}$. Let $\varepsilonscl \alphalg A \in \omegap{Heyt}(\vv V)$ and
let $G \in \omegap{Fil}(\varepsilonscl \alphalg A)$. Let $F= \{ b \in A: \varepsilonscl a \le b \ \tauext{for some}\ \varepsilonscl a \in G\}$; then $F$ is  a filter of $\alphalg A$
and $F \cap\varepsilonscl A = G$.  So $\varepsilonscl (\alphalg A/F) \cong \varepsilonscl \alphalg A/G$ and $\varepsilonscl \alphalg A/G \in \omegap{Heyt}(\vv V)$. That $\omegap{Heyt}(\vv V)$ is closed under direct products
is obvious so let $\varepsilonscl \alphalg A \in \omegap{Heyt}(\vv V)$ and let $\alphalg C$ be a subalgebra of $\varepsilonscl \alphalg A$ and let $\alphalg B = \omegap{Sub}_\alphalg A(C)$. Clearly $\alphalg C \subseteq \varepsilonscl \alphalg B$;
conversely, as $\alphalg C$ generates $\alphalg B$ in $\alphalg A$, every element of $\varepsilonscl \alphalg B$ is $\varepsilonscl t(\vuc cn)$ for some $n$-ary term of $\alphalg A$ and $\vuc cn\in C$.
Now an induction on the complexity of $t(\vuc xn)$ shows that if $\vuc cn \in C$ then $\varepsilonscl t(\vuc cn) \in \varepsilonscl C$ .  The only nontrivial part is to show that
if $c \in C$, then $\varepsilonscl \mathop{\sim} \varepsilonscl c \in C$.

  Observe that  from
$\mathop{\sim} \varepsilonscl c \varepsilonscl c \le \mathop{\sim} 1$ and $\varepsilonscl \mathop{\sim} \varepsilonscl c \le \mathop{\sim}
\varepsilonscl c$ we get $\varepsilonscl \mathop{\sim} \varepsilonscl c  \varepsilonscl c \le \mathop{\sim} 1$ and
hence $\varepsilonscl \mathop{\sim} \varepsilonscl c \varepsilonscl c \le \varepsilonscl \mathop{\sim} 1$.

By residuation $\varepsilonscl \mathop{\sim} \varepsilonscl c \le \varepsilonscl c \rightarrow \varepsilonscl \mathop{\sim} 1$
and hence $\varepsilonscl\mathop{\sim} \varepsilonscl c \le \varepsilonscl(\varepsilonscl c \rightarrow \varepsilonscl \mathop{\sim} 1)=
\varepsilonscl c \rightarrow_{!} \varepsilonscl \mathop{\sim} 1$. On the other hand
$$
\mathop{\sim} \varepsilonscl c = \varepsilonscl c \rightarrow \mathop{\sim} 1 \gammae \varepsilonscl c \rightarrow \varepsilonscl \mathop{\sim} 1,
$$
implying
$$
\varepsilonscl\mathop{\sim} \varepsilonscl c \gammae \varepsilonscl(\varepsilonscl c \rightarrow \varepsilonscl \mathop{\sim} 1)= \varepsilonscl c \rightarrow_{!}\varepsilonscl \mathop{\sim} 1.
$$
In conclusion $\varepsilonscl\mathop{\sim}\varepsilonscl c =\varepsilonscl c \rightarrow_{!} \varepsilonscl\mathop{\sim} 1 \in C$.
\varepsilonnd{proof}

The mapping $\vv V \longmapsto \omegap{Heyt}(\vv V)$
is a join homomorphism from the lattice of subvarieties of  girales to the lattice of subvarieties of Heyting
algebras:
\betaegin{align*}
\omegap{Heyt}(\vv V \vee \vv V') &= \omegap{Heyt}({\mathbf V}(\vv V \cup \vv V'))
= {\mathbf V}(\omegap{Heyt}(\vv V \cup \vv V'))\\
&={\mathbf V}(\omegap{Heyt}(\vv V) \cup \omegap{Heyt}(\vv V')) = \omegap{Heyt}(\vv V) \vee \omegap{Heyt}(\vv
V').
\varepsilonnd{align*}
However it is not a meet homomorphism, as we shall see later.

Thus the lattice of varieties of girales can be
partitioned into equivalence classes that are also join semilattices;
information on these classes can be recovered from the varieties of Heyting
algebras that are their ``natural'' representatives. Such pieces of
information can be
glued together to get a clearer picture of the whole lattice of varieties
of girales.

Let's call a girale $\alphalg A$ a {\betaf Boolean girale} if $\omegap{Heyt}(\alphalg A)$ is a Boolean algebra; a variety $\vv V$ of girales
is {\betaf Boolean} if every algebra in $\vv V$ is Boolean.
We will give a recipe to construct a family
of simple Boolean
girales of unbounded cardinality.
By J\'onnson Lemma \cite{Jonsson1967}, any two of them
generate  distinct  Boolean varieties of girales.

Let $\alphalg G_n$ be the height three lattice
with $n$ atoms. Let $\betaot$ and $\tauop$ be the bottom and the top of the
lattice and let $1$, $0$ be two distinct atoms. Define
$\mathop{\sim}$ on $G_n$ by setting $\mathop{\sim} \betaot = \tauop$, $\mathop{\sim}\tauop =  \betaot$,
$\mathop{\sim} 1 = \betaot$, $\mathop{\sim} 0 = 1$ and $\mathop{\sim} a =a$ for any other
$a \in G_n$. Define  $\cdot$ on $G_n$
by
\betaegin{align*}
&\betaot \cdot a = a \cdot \betaot =\betaot  \\
&1 \cdot a = a \cdot 1 = a \\
&a \cdot a = \betaot \qquad  a \notin\{0,1,\betaot,\tauop\}\\
& a \cdot b = \tauop \qquad\tauext{otherwise}
\varepsilonnd{align*}
Finally define $\varepsilonscl 1 = \varepsilonscl \tauop = 1 $ and $\varepsilonscl a = \betaot$
otherwise. Some calculations show that each $\alphalg G_n$ is a Boolean girale;
the subdirectly irreducible algebras in ${\mathbf V}(\alphalg G_n)$ are exactly
the $\alphalg G_m$, $1\le m\le n$.

\betaegin{figure}[htbp]
\betaegin{center}
\betaegin{tikzpicture}[scale=1]
\deltaraw (0,0) -- (0,1);
\deltaraw (2,0) -- (1,1) -- (2,2) -- (3,1) -- (2,0) ;
\deltaraw (5,0) -- (4,1) -- (5,2) -- (5,0) -- (6,1) -- (5,2);
\deltaraw  (8,0) -- (7,1) -- (8,2) -- (7.6,1) -- (8,0) -- (8.4,1) -- (8,2) -- (9,1) -- (8,0) ;
\deltaraw[fill] (0,0) circle [radius=0.05];
\deltaraw[fill] (0,1) circle [radius=0.05];
\node[left] at (0,0) {\varphiootnotesize$0=\betaot$};
\node[left] at (0,1) {\varphiootnotesize $1=\tauop$};

\deltaraw[fill] (2,0) circle [radius=0.05];
\deltaraw[fill] (1,1) circle [radius=0.05];
\deltaraw[fill] (2,2) circle [radius=0.05];
\deltaraw[fill] (3,1) circle [radius=0.05];
\node[left] at (2,0) {\varphiootnotesize$\betaot$};
\node[left] at (1,1) {\varphiootnotesize $1$};
\node[right] at (2,2) {\varphiootnotesize $\tauop$};
\node[right] at (3,1) {\varphiootnotesize $0$};

\deltaraw[fill] (5,0) circle [radius=0.05];
\deltaraw[fill] (4,1) circle [radius=0.05];
\deltaraw[fill] (5,2) circle [radius=0.05];
\deltaraw[fill] (6,1) circle [radius=0.05];
\deltaraw[fill] (5,1) circle [radius=0.05];
\node[left] at (5,0) {\varphiootnotesize$\betaot$};
\node[left] at (4,1) {\varphiootnotesize $1$};
\node[right] at (5,2) {\varphiootnotesize $\tauop$};
\node[right] at (6,1) {\varphiootnotesize $0$};

\deltaraw[fill] (8,0) circle [radius=0.05];
\deltaraw[fill] (7,1) circle [radius=0.05];
\deltaraw[fill] (8,2) circle [radius=0.05];
\deltaraw[fill] (7.6,1) circle [radius=0.05];
\deltaraw[fill] (8.4,1) circle [radius=0.05];
\deltaraw[fill] (9,1) circle [radius=0.05];
\node[left] at (8,0) {\varphiootnotesize$\betaot$};
\node[left] at (7,1) {\varphiootnotesize $1$};
\node[right] at (8,2) {\varphiootnotesize $\tauop$};
\node[right] at (9,1) {\varphiootnotesize $0$};

\node[below] at (0,-.2) {\varphiootnotesize  $\alphalg G_1$};
\node[below] at (2,-.2) {\varphiootnotesize  $\alphalg G_2$};
\node[below] at (5,-.2) {\varphiootnotesize  $\alphalg G_3$};
\node[below] at (8,-.2) {\varphiootnotesize  $\alphalg G_4$};
\varepsilonnd{tikzpicture}
\caption{Boolean girales}\langlebel{girales}
\varepsilonnd{center}
\varepsilonnd{figure}

The algebra $\alphalg G_1$ in Figure \ref{girales} is the two element Boolean
algebra and hence $\omegap{Heyt}({\mathbf V}(\alphalg G_1)) = \vv B$, the variety of Boolean algebras. On the other hand,
since both $\alphalg G_1$ and $\alphalg G_2$  are finite simple algebras with no proper
subalgebras  both ${\mathbf V}(\alphalg B)$ and ${\mathbf V}(\alphalg G_2)$ are atoms in the lattice of
varieties of girales and  their intersection is the trivial variety.
However $\omegap{Heyt}({\mathbf V}(\alphalg G_2)) = \vv B$ as well,  so
$\omegap{Heyt}({\mathbf V}(\alphalg G_1)) \cap \omegap{Heyt}({\mathbf V}(\alphalg G_2)) = \vv B$.
This shows that the map $\vv V \longmapsto \omegap{Heyt}(\vv V)$ is not a meet homomorphism.

\section{Fragments and expansions of $\mathsf{LL}$}

\subsection{Fragments}
Any fragment of $\mathsf{LL}$ whose language contains the connectives
$\rightarrow,\wedge$ is algebraizable. This is obvious if $1$ is contained
in the language as well, since in this case, by Corollary 2.12 of
\cite{BlokPigozzi1989}, the defining equation and congruence formulas are the
same as for $\mathsf {LL}$. It is easily checked that these fragments are in
fact strongly algebraizable.

If $1$ is not contained in the language, then we get something very
similar to what happens in  Relevance Logic.
We will describe one case in detail and leave all the others to the
interested reader. Let $\mathsf {LR}$ be the system axiomatized by axioms
(HL1)--(HL7), (HL12)--(HL19), (MP) and (Adj). The system is algebraizable
with defining equation $p \wedge (p \rightarrow p)= p \rightarrow p$ and equivalence
formulas $\Delta= \{p \rightarrow q,q\rightarrow p\}$. The Lindenbaum algebra of
$\mathsf {LR}$ is easily seen to be a bounded lattice with involution and
with an implication satisfying (2.2)--(2.5). Unfortunately the variety $\vv
V$
of such algebras is not the equivalent algebraic semantics of $\mathsf {LR}$,
since the natural
ordering of the underlying lattice does not model adequately the residuation
in $\mathsf {LR}$. It turns out that the variety  of
$\mathsf {LR}$-algebras, i.e.  the subvariety of $\vv V$ axiomatized by the equation
$$
((x \rightarrow x)\wedge (y\rightarrow y))\rightarrow z \le z,
$$
is the  equivalent algebraic semantics for $\mathsf{LR}$.

In this context the variety $\vv R$ of relevant algebras is a subvariety
of the variety $\vv H$ of $\mathsf {LR}$-algebras. Since $\vv R$ does not have
equationally definable principal congruences, the variety of $\mathsf{LR}$-algebras  does not have it as
well.
However, if we add to $\mathsf {LR}$ the {\varepsilonm mingle axiom}
$$
p\rightarrow (p\rightarrow p),
$$
then the resulting equivalent algebraic semantics has equationally definable
principal congruences and thus the system has the deduction theorem. This
displays once
more the strong connections between Linear Logic and Relevance Logic.

The  implicational fragment of $\mathsf CLL$ gives rise to a well known
deductive system, BCI-logic, which is not algebraizable
\cite{BlokPigozzi1989}. In \cite{BlokPigozzi1992}, Blok and Pigozzi noted
also that the $\{\rightarrow,\cdot\}$-fragment of $\mathsf {LL}$ is not algebraizable.
We describe briefly its logical matrices: let $\langle A,\rightarrow,\cdot,\le\rangle$
be a commutative
partially ordered residuated semigroup. A {\varepsilonm filter} of $\alphalg A$ is
an order filter of $A$ closed under multiplication. One sees easily
that a reduced matrix
for the $\{\rightarrow,\cdot\}$-fragment of $\mathsf {LL}$ is $\langle A,\nabla_A\rangle$
where $\alphalg A$ is a commutative p.o. residuated semigroup and
$\nabla_A$ is the filter generated by the set $\{a\rightarrow a: a \in A\}$.
Hence the reduced matrix semantics is the class of {\varepsilonm reduced filtered
commutative residuated partially ordered semigroups}. The reason why this
class cannot be replaced by a class of proper algebras lies in
the fact that the partial order cannot be recovered from the operations.
By the same argument one sees that the multiplicative fragment of $\mathsf {LL}$
is not algebraizable.

Finally any algebraizable fragment whose language contains $\varepsilonscl$ has the
deduction theorem and  gives rise to an equivalent algebraic semantics
having equationally definable principal congruences.

\subsection{Intuitionistic Linear Logic}
There are at least two  versions of intuitionistic linear logic.
The first one is $\mathsf {ILL}$ (see \cite{Girard1987}) which is obtained from
classical linear logic in the
same way Gentzen's system $\mathsf {LJ}$ (intuitionistic logic) is obtained from
$\mathsf {LK}$: a left side of a sequent can contain at most one formula.
So we are forced to drop all connectives and constants whose rules do not
obey to this restriction, i.e. $\tauext{\large$\mathop{?}$\normalsize}, \neg, \betaot, \mathrel{\betaindnasrepma}$. $\mathsf {ILL}$ can be seen
as a deductive system axiomatized Hilbert-style by (HL1)--(HL3),
(HL6)--(HL9),
(HL12)--(HL24) with (MP), (Adj) and (Nec).

It is sometimes convenient, to get a more suitable comparison with classical
linear logic, to
consider $\mathsf {ILN}$ \cite{Abrusci1990}, i.e. {\varepsilonm intuitionistic Linear
Logic with negation}. This is done by adding two ``ad hoc'' rules for $\mathop{\sim}$
in the sequent calculus. On the Hilbert-style side we just add (HL5),
(HL10), (HL11) (one of course has to define $\betaot$ as $\mathop{\sim} \tauextsf{\betaf 1}$). Finally,
if we drop (HL20)--(HL24) and (Nec) from $\mathsf {ILL}$ or $\mathsf {ILN}$ we get the
exponential-free fragments.

It is clear that all these systems are fragments of $\mathsf {LL}$ with respect
to
suitable languages. Since the connectives appearing
in the congruence formulas and defining equation for $\mathsf {LL}$ belong to
all these languages, we can conclude at once (by Corollary 2.12 in
\cite{BlokPigozzi1989}) that all the systems are algebraizable (and they in fact  strongly
algebraizable).

\subsection{Noncommutative Linear Logics}
If in the sequent formulation of Linear Logic we delete the
{\varepsilonm exchange rule}, we get {\varepsilonm noncommutative Linear Logic}.
It is not hard (only boring) to work out a Hilbert-style axiomatization
of non commutative Linear Logic. In this framework one has to deal with two
implications and two negations and the product $\cdot$ is no
longer commutative. Of course also in this case we have interesting fragments
and in particular one can get {\varepsilonm noncommutative intuitionistic linear
logic} \cite{Abrusci1991}. Noncommutative Linear Logics are algebraizable
(the proof is similar to the one for Linear Logic, only more work
has to be done to take care of the doubling of implication and
negation)
and the equivalent algebraic semantics are varieties of $\mathsf{FL}$-algebras
with further operations.

\providecommand{\betaysame}{\leavevmode\hbox to3em{\hrulefill}\tauhetainspace}
\providecommand{\MR}{\relax\ifhmode\unskip\space\varphii MR }

\providecommand{\MRhref}[2]{
  \href{http://www.ams.org/mathscinet-getitem?mr=#1}{#2}
}
\providecommand{\href}[2]{#2}
\betaegin{thebibliography}{10}

\betaibitem{Abrusci1990}
V.M. Abrusci, \varepsilonmph{Sequent {C}alculus for {I}ntuitionistic {L}inear
  {P}ropositional {L}ogic}, pp.~223--242, Springer US, Boston, MA, 1990.

\betaibitem{Abrusci1991}
\betaysame, \varepsilonmph{Phase semantics and sequent calculus for pure noncommutative
  classical linear logic}, J. Symb. Log. \tauextbf{56} (1991), 1403--1451.

\betaibitem{Agliano1996b}
P.~Aglian\`o, \varepsilonmph{Ternary deduction terms in residuated structures}, Acta
  Sci. Math. (Szeged) \tauextbf{64} (1998), 397--429.

\betaibitem{AglianoUrsini1992}
P.~Aglian\`o and A.~Ursini, \varepsilonmph{Ideals and other generalizations of
  congruence classes}, J. Aust. Math. Soc. \tauextbf{53} (1992), 103--115.

\betaibitem{AllweinDunn1993}
G.~Allwein and J.M. Dunn, \varepsilonmph{Kripke models for linear logic}, J. Symb. Log.
  \tauextbf{58} (1993), 514--545.

\betaibitem{AndersonBelnap}
A.R. Anderson and N.D. Belnap, \varepsilonmph{Entailment. {T}he {L}ogic of {R}elevance
  and {N}ecessity, {I}}, Princeton University Press, Princeton, 1975.

\betaibitem{Avron1988}
A.~Avron, \varepsilonmph{The semantics and proof theory of {L}inear {L}ogic}, Theoret.
  Comput. Sci. \tauextbf{57} (1988), 161--184.

\betaibitem{Blok1976}
W.J. Blok, \varepsilonmph{Varieties of interior algebras}, Ph.D. thesis, University of
  Amsterdam, 1976.

\betaibitem{Blok1980}
\betaysame, \varepsilonmph{The lattice of modal logics: an algebraic investigation}, J.
  Symb. Logic \tauextbf{45} (1980), 221--236.

\betaibitem{BlokPigozzi1989}
W.J. Blok and D.~Pigozzi, \varepsilonmph{{A}lgebraizable {L}ogics}, Mem. Amer. Math.
  Soc., no. 396, American Mathematical Society, Providence, Rhode Island, 1989.

\betaibitem{BlokPigozzi1992}
\betaysame, \varepsilonmph{Algebraic {S}emantics for {U}niversal {H}orn {L}ogic without
  equality}, Universal {A}lgebra and {Q}uasi-{G}roup {T}heory (A.~Romanowska
  and J.H.D. Smith, eds.), Heldermann Verlag, Berlin, 1992, pp.~1--56.

\betaibitem{EDPC3}
\betaysame, \varepsilonmph{On the structure of varieties with equationally definable
  principal congruences {III}}, Algebra Universalis \tauextbf{32} (1994),
  545--608.

\betaibitem{BusanicheCignoli2009}
M.~Busaniche and R.~Cignoli, \varepsilonmph{Residuated lattices as an algebraic
  semantics for paraconsistent nelson logic}, J. Logic Comput. \tauextbf{19}
  (2009), 1019--1029.

\betaibitem{Dunn1986}
J.M. Dunn, \varepsilonmph{Relevane logic and entailment}, Handbook of {P}hilosophical
  {L}ogic {III} (D.~Gabbay and F.~G\"unther, eds.), D. {R}eidel {P}ubl.
  {C}omp., {D}ordrecht, 1986, pp.~117--224.

\betaibitem{Dunn1993}
\betaysame, \varepsilonmph{Partial {G}aggles applied to {L}ogics with {R}estricted
  {S}tructural {R}ules}, Substructural {L}ogics (P.~Schroeder-Heister and
  K.~Do\v sen, eds.), Clarendon {P}ress, {O}xford, 1993, pp.~63--108.

\betaibitem{Girard1987}
J.-Y. Girard, \varepsilonmph{{L}inear {L}ogic}, Theoret. Comput. Sci. \tauextbf{50}
  (1987), 1--102.

\betaibitem{Jonsson1967}
B.~J\'onsson, \varepsilonmph{Algebras whose congruence lattices are distributive}, Math.
  Scand. \tauextbf{21} (1967), 110--121.

\betaibitem{Lincoln1990}
P.D. Lincoln, J.~Mitchell, A.~Scedrov, and N.~Shankar, \varepsilonmph{Decision problems
  for propositional linear logic}, Report sri-csl-90-08, SRI International
  Computer Science Laboratory, Menlo Park, CA, USA, 1990.

\betaibitem{MontagnaTsinakis2010}
F.~Montagna and C.~Tsinakis, \varepsilonmph{Ordered groups with a conucleus}, J. Pure
  Appl. Alg. \tauextbf{214} (2010), 71--88.

\betaibitem{NemWha1971}
W.~Nemitz and T.~Whaley, \varepsilonmph{Varieties of implicative semilattices}, Pacific
  J. Math. \tauextbf{37} (1971), 759--769.

\betaibitem{RoutleyMeyer1973}
R.~Routley and R.K. Meyer, \varepsilonmph{The semantics of entailment, {I}}, Truth
  {S}yntax and {S}emantics (H.~Leblanc, ed.), North {H}olland, {A}msterdam,
  1973, pp.~194--243.

\varepsilonnd{thebibliography}

\varepsilonnd{document}