[Prev][Next][Index][Thread]

underivability results of Avron in MLL

Date: Fri, 7 Feb 92 13:03:51 +0100
To: Linear@cs.stanford.edu

%This message is plain TeX file (that should be readable as it is).


\def\LLM{\hbox{\it LLM}}
\def\PAR{+}
\def\TIMES{+}
\def\NIL#1{#1^\perp}
\def\thesis{\vdash}
\def\unprovable{\not\vdash}
\parindent 0pt


In his message to the Linear mbox of Dec 3, 1991 and the related manuscript
``Some properties of Linear Logic proved by Semantic Methods'', Arnon Avron 
showed how to obtain some non-derivability results in (multiplicative) linear
logic by means of a simple arithmetical argument, using a valuation of linear
sequents in the integers. He proved:
\par\smallskip
PROPOSITION 0: (Avron)

    1. For no $n > 1$ a sequent with $n$ copies of a multiplicative formula
       $A$ is derivable, i.e., $\unprovable A,A,\cdots, A$.

    2. If $A_1$, $A_2$, \dots, $A_n$ are provable (for $n>1$), then 
       $\unprovable A_1,A_2,\cdots,A_n$.

    3. If $k-m$ does not divide $k-1$, then $\unprovable m(\NIL{A}), k(A)$. 
       (Here $m(X)$ denotes $m$ copies of $X$).

\par\smallskip
He also asked for an interpretation of these results in terms of proof nets,
and for other (syntactical) proofs. We show here that this proposition follows
>from the ``a-cyclic \& connected'' criterium for proofnets, by presenting an
argument using a ``syntactic'' corrollary of this criterium.

\par\smallskip
For the moment we forget about the units, and look at the proof-structure
representation of pure multiplicative formulas.
Let $A$ be a formula, and take any proof-structure $S$ consisting in the
``tree'' of $A$, say $T(A)$, together with a set of axiom links over its
leaves (the atoms of $A$). $S$ is correct iff under each switching $s$ of
$T(A)$ (roughly said, one disconnects one of the two premises of each
$\PAR$ link in $T(A)$ from its conclusion) it becomes an acyclic and connected
graph. Now, $A$ is provable iff there is such a correct $S$. 

In this case: $C(A) = N(A) + 1$, where $C(A)$ is the number of connected
components of $T(A)$ under any switching $s$, and $N(A)$ is the number of
axiom links in $S$ (this is the usual relation vertices - edges = 1 for
trees). Remarkably, this relation does not depend on $S$, for $C(A)=1+P(A)$
where $P(A)$ is the number of $\PAR$'s in $A$, and $N(A)$ is obviously equal
to the number of negations in $A$ (NB: {\it supposed to be written in the standard form
where only atoms are negated!}). So this relation rewrites to $P(A)=N(A)$.
The same argument on a sequent $\Gamma$ yields:

\par\smallskip
PROPOSITION 1: If $\thesis\Gamma$, then $P(\Gamma)+\#(\Gamma)=N(\Gamma)+1$,
and {\it a fortiori}\/ $P(\Gamma)+N(\Gamma)+\#(\Gamma)\equiv 1$ (mod 2).

\par\smallskip
>From this one easily infers the non-derivability results stated at the
beginning. Even more subtle claims can be formulated: 
\par\smallskip
PROPOSITION 2: If $P(A)+N(A)\equiv
P(B)+N(B)$ (mod 2), then $\unprovable A,B$.

\par\smallskip\smallskip
Our proposition 1 might also be verified by induction on the length of
derivations in the one-sided version of sequent-calculus for multiplicative
linear logic with only {\it atomic} instances of the identity axiom ($\thesis
p, \NIL{p}$) {\it and axiom and rule for the constants}, taking $\NIL{{\bf
1}}$ for $\bot$. We thus obtain an alternative proof of Avron's result in its
full generality, as for any sequent $\Gamma$ provable in (any version of)
multiplicative linear logic with constants there is an equivalent sequent
$\Gamma^{\prime}$ provable in this one-sided calculus.

========================================

Vincent Danos & Harold Schellinx
\end