[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}