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