[Prev][Next][Index][Thread]
translations of classical into LL
Date: Mon, 8 Jun 92 10:32:46 +0200
To: linear@cs.stanford.edu
In their important paper in LICS'91, Lincoln, Scedrov and Shankar give
a translation of a contraction- and cut-free system for implicational
intuitionistic logic into a fragment of propositional linear logic.
In the short LaTeX abstract below, we present how, somewhat in a similar
spirit, we can give a translation of the full propositional classical
logic into the full propositional linear logic without exponentials.
Comments and remarks are welcome.
Simone Martini e Andrea Masini
Dipartimento di Informatica,
Universita' di Pisa, Italy.
===========================================================
\documentstyle{article}
\newtheorem{pro}{Proposition}
\newtheorem{de}{Definition}
\newtheorem{teo}{Theorem}
\newcommand{\n}{\mbox{$\neg$}}
\newcommand{\sse}{\mbox{$\equiv$}}
\newcommand{\vel}{\mbox{$\vee$}}
\newcommand{\et}{\mbox{$\wedge$}}
\newcommand{\imp}{\mbox{$\supset$}}
\newcommand{\ms}[2]{
\begin{array}{c}
#1
\end{array}
\!
\begin{array}{c}
\!\!\!\vdash\!\!\!
\end{array}
\!
\begin{array}{c}
#2
\end{array}
}
\newcommand{\due}[1]{
\begin{array}{c}
#1
\end{array}
}
\newcommand{\bms}[4]{
\begin{array}{c}
#1
\end{array}
\begin{array}{c}
;
\end{array}
\begin{array}{c}
#2
\end{array}
\!
\begin{array}{c}
\!\!\!\vdash\!\!\!
\end{array}
\!
\begin{array}{c}
#3
\end{array}
\begin{array}{c}
;
\end{array}
\begin{array}{c}
#4
\end{array}
}
\newcommand
{\lr}[5]{ \displaystyle{
\frac{\ms{#1}{#2}}{\ms{#3}{#4}} \; #5\vdash }}
\newcommand
{\rr}[5]{ \displaystyle
\frac{\ms{#1}{#2}}{\ms{#3}{#4}} \vdash#5 }
\newcommand{\mlr}[7]
{\displaystyle
\frac{\ms{#1}{#2} \hspace{.5in} \ms{#3}{#4} }{\ms{#5}{#6}} \;
#7\vdash }
\newcommand{\mrr}[7]
{ \displaystyle
\frac{\ms{#1}{#2} \hspace{.5in} \ms{#3}{#4} }{\ms{#5}{#6}}
\vdash#7 }
\newcommand{\cut}[7]
{ \displaystyle
\frac{\ms{#1}{#2} \hspace{.5in} \ms{#3}{#4} }{\ms{#5}{#6}}
\; #7 }
\title{An exponential-free interpretation of classical logic into linear
logic\\
{\normalsize Preliminary abstract}}
\author{Simone Martini\ \ \ \ \ Andrea Masini\\
Dipartimento di Informatica\\
Universit\`a di Pisa\\
Italy\\
e-mail: {\tt \{martini,masini\}@di.unipi.it}}
\begin{document}
\maketitle
Several translations of classical and intuitionistic logic into
linear logic have been proposed. Almost all of them agree on a
heavy use of {\em modalities} ($!$ and $?$) in order to
mimick weakening and contraction rules, the notable exception being \cite{LSS},
where a translation of the intuitionistic implicational logic into
the intuitionistic fragment of multiplicative-additive linear logic
(IMALL) is given that does not use modalities.
In the spirit of \cite{LSS}, we present here how the full propositional classical logic can
be translated into propositional linear logic {\em without modalities},
and without factorizing the interpretation through a translation
of classical logic into intuitionistic logic.
The translation can be extended to first-order classical logic,
but for this, at least at the current stage of research, modalities
are needed.
The translation is an ``asymmetrical interpretation'' and, as such, it
does not validate the cut-rule (that is, it translates cut-free proofs
in a suitable formal system for classical logic into
cut-free proofs in {\bf LL}).
The main ideas for the translation are:
\begin{itemize}
\item It is well known that there are systems for classical logic
where contraction is eliminable (e.g. \cite{Gallier}).
\item The contraction-free sequent calculus has, for a given
connective, a multiplicative left rule and an additive
right rule (or vice-versa).
\item Weakenings can be ``simulated'' in linear logic by use of
constants (${\bf 0}$, for instance, but other choices
are possibile), in the spirit of \cite{LSS}, but in a
simpler context.
\item The use of {\em full} linear logic as a target makes almost
immediate the completeness of the translation.
\end{itemize}
Once these facts are realized, the translation and the
proof of its correctness and completeness are very simple.
\section{The translation}
\begin{de}
The sequent calculus {\bf G} for propositional classical logic is
given by the following axioms and rules.
$\Gamma$ and $\Delta$ are multisets of formulas; $A$, $B$ and $C$ are generic
formulas; $p$ is a generic atom.
\begin{description}
\item[axioms]
\[ \ms{A,\Gamma}{A,\Delta}\]
\item[cut rule]
\[
\due{
\underline{
\ms{\Gamma}{A,\Delta} \hspace{5ex}
\ms{\Gamma,A}{\Delta}
}
\\
\ms{\Gamma}{\Delta}
}
\]
\item[contraction]
\[
\lr{\Gamma,A,A}{\Delta}{\Gamma,A}{\Delta}{c}
\hspace{10ex}
\rr{\Gamma}{\Delta,A,A}{\Gamma}{\Delta,A}{c}
\]
\item[conjunction]
\[
\lr{\Gamma,A, B}{\Delta}
{\Gamma,A\et B}{\Delta}{\et}
\]
\[
\mrr{\Gamma}{\Delta, A }
{\Gamma}{\Delta, B }
{\Gamma}{\Delta, A\et B}{\et}
\]
\item[disjunction]
\[
\mlr{\Gamma, A }{\Delta}
{\Gamma, B }{\Delta}
{\Gamma, A\vel B }
{\Delta } {\vel}
\]
\[
\rr{\Gamma}{ \Delta, A, B }
{\Gamma}{ \Delta, A\vel B}{\vel}
\]
\item[implication]
\[
\mlr{\Gamma, B}{\Delta}
{\Gamma}{\Delta, A }
{\Gamma,A\imp B}
{\Delta}{\imp}
\]
\[
\rr{\Gamma, A}{\Delta, B }
{\Gamma}{\Delta, A \imp B}{\imp}
\]
\item[negation]
\[
\lr{\Gamma}{\Delta, A }
{\Gamma,\n A }{\Delta}{\n}
\hspace{5ex}
\rr{\Gamma, A }{\Delta}
{\Gamma}{\Delta, \n A }{\n}
\]
\end{description}
%************
\end{de}
\begin{pro}
The cut-rule and the contraction rules are eliminable from {\bf G}.
\end{pro}
\begin{de}
(i) Formulas of the language of classical logic are
translated into linear formula as follows ($p$ stands for an atom):
\[
\begin{array}{ll}
(p)^+ = p & (p)^- = p\wp {\bf 0 }\\
(A \imp B)^+ = (A^-)^\bot \wp B^+ & (A \imp B)^- = (A^+)^\bot\oplus B^- \\
(A \et B)^+ = A^+ \& B^+ & (A \et B)^- = A^- \otimes B^- \\
(A \vel B)^+ = A^+ \wp B^+ & (A \vel B)^- = A^- \oplus B^- \\
(\n A)^+ = (A^-)^\bot & (\n A)^- = (A^+)^\bot
\end{array}
\]
\end{de}
The previous definition extends trivially to multisets of formulas.
\begin{teo}
$\Gamma\vdash_{\bf G} \Delta\ \ \ \Longleftrightarrow\ \ \
\Gamma^-\vdash_{\bf LL} \Delta^+$
\end{teo}
{\bf proof idea}\\
($\Rightarrow$) By induction on a cut- and contraction-free
derivation. The main case is the axiom, where the implicit weakening
is simulated as follows
\[
\due{
\underline{
\ms{p}{p} \hspace{5ex} \ms{{\bf 0}, \Gamma^-}{\Delta^+}
}
\\
\ms{p\wp {\bf 0} , \Gamma^-}{\Delta^+, p}
}.
\]
All other cases follow easily from the definition of the translation.\\
($\Leftarrow$) Any derivation of a sequent $\Gamma^-\vdash_{\bf LL} \Delta^+$
can be interpreted as a derivation in {\bf LK}, replacing
$\oplus,\wp$ with $\vel$; $\otimes,\&$ with $\et$; $A^\bot$ with $\n A$
for any formula $A$; ${\bf 0},\bot$
with any contradictory formula; ${\bf 1},\top$ with a tautology.
The equivalence of {\bf LK} with {\bf G} is routine.
\begin{thebibliography}{99}
\bibitem{LSS}
Lincoln, P., A. Scedrov and N. Shankar. Linearizing Intuitionistic
Implication. In {\em Logic in Computer Science 1991} (LICS 91), Amsterdam,
51--61.
\bibitem{Gallier}
Gallier, J. Constructive Logics. Part I. Res. Rep. no. 8, Digital Paris
Research Lab. May 1991.
\end{thebibliography}
\end{document}