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

Independent sets of constant-only formulas do exist



 By analogy with the well-known notion of
 independent elements in monoids, vector spaces, etc.,
 a set of propositions (formulas)

     $$ E_1,   E_2, ....  E_n $$

 is  strongly independent if there is NO non-trivial correlations
 between them:
 for every (n+m)-ary formula built up of positive literals
 (atomic propositions) and constant 1 by connectives from the set
    { |x|, -o , |+|, &, ! }

  $$ A(p_1,p_2, ..., p_n, r_1,r_2,...,r_m),$$
 
 a sequent of the form
   $$ |- A(E_1,E_2,...,E_n,  r_1,r_2,...,r_m) $$
 is derivable in Linear Logic if and only if the sequent
   $$ |- A(p_1,p_2,...,p_n,  r_1,r_2,...,r_m) $$
 is also derivable in Linear Logic.

 In the case of neutral (constant-only) formulas, it does not work
 for all traditional systems.
 Moreover, it is impossible to construct an independent set of
 neutral formulas even for Linear Logic with Weakening.

 Nevertheless, for Linear Logic we construct

1. strongly independent sets consisting of
   one-literal purely implicational formulas,
2. strongly independent sets consisting of
   1-only multiplicative formulas,
3. strongly independent sets consisting of
   $\bot$-only purely implicational formulas.

 It turned out that full propositional Linear Logic is
 undecidable (Lincoln, Mitchell, Scedrov, and Shankar).
 Here we demonstrate 'positive' aspects of such a 'negative' result.
 Namely, we prove that ALL partial recursive relations are
 strongly definable in Linear Logic

1. by one-literal formulas built up of a single positive literal p
   by connectives from the set
    {  -o ,  &, ! }
   where the storage operator ! is allowed to use only in the
   outside position,
2. by 1-only formulas that are combination of the single constant 1
   by connectives from the set
     { -o , |x|, \Par,  &, ! }
   where the storage operator ! is allowed to use only in the
   outside position,
3. and, hence, by $\bot$-only formulas built up of the single
   constant $\bot$ by connectives from the set
    {  -o ,  &, ! }
   where the storage operator ! is allowed to use only in the
   outside position.
------------------------------------------------------------
The full proof of the existence of independent sets as well as
complexity results on one-literal and constant-only fragments
of LL are contained in the following papers:

1. Kanovich M.,
   Simulating Linear Logic in \mbox{{\large{\bf 1}}-Only} Linear Logic.
   CNRS, Laboratoire de Math\'{e}matiques Discr\`{e}tes,
   Pr\'{e}tirage n$^\circ$ 94-02, January~1994, 81~p.\\
   Available by anonymous ftp from host \mbox{ftp.lmd.univ-mrs.fr}
   and the file \mbox{pub/kanovich/unit-only.dvi.}
2. Kanovich M.,
   The Independent Basis of  Neutral Formulas in Linear Logic.
   CNRS, Laboratoire de Math\'{e}matiques Discr\`{e}tes,
   Pr\'{e}tirage n$^\circ$ 94-08, March~1994, 43~p.\\
   Available by anonymous ftp from host \mbox{ftp.lmd.univ-mrs.fr}
   and the file \mbox{pub/kanovich/neutrals.dvi.}

Best regards,
Max Kanovich.