[TYPES] connectedness and acyclicity in IMLL proof nets

[soloviev@irit.fr]

Dear all,

in fact, the acyclicity and
connectedness follows very easily from the fact
that a) every IMLL derivation can be obtained by
substitution of I, elimination of "redundant" I's
(like in A x I and I-o A) and identification of variables
from some derivation of a balanced sequent without I (balanced = every
variable occurs exactly twice with opposite signs)
b) in case of a derivable balanced sequent there is
no cycles, for example, because IMLL derivations
may be seen also as a subclass of derivations
in classical logics, and for balanced sequents
there are trivial valuations that show the absence of cycles.

I had a lemma A. Babaev, S. Soloviev "A coherence theorem for
canonical morphisms in cartesian closed categories", Journal of Soviet
Math., v.20 , pp.2263-2282 (1982)  (lemma 3) which describes
this valuation, and in my ph.d. thesis (1985) similar results
and their consequences for a logical system for
Symmetric Monoidal Closed Categories (equivalent to IMLL)
were obtained. I discussed this also in my lectures in
Munich in 1995 (it may be still on the site of LMU).

I would like to stress here that these
results may be obtained quite easily.

Best

Sergei Soloviev


> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list
> ]
>
> Dear Aurelien,
>
> In MLL, your observation holds if a proof structure satisfies
> the equation #(ID) = #( x ) + 1, where #(ID) is the number of
> the ID-links and #( x ) is the number of the tensor-links in
> the proof structure.
>
> The equation is an invariant of MLL proof nets, which you can find
> in "Le Point Aveugle I" by Girard.
>
> Best regards,
> --
> Satoshi Matsuoka
> National Institute of
> Advanced Industrial Science and Technology
> 1-1-1 Umezono,Tsukuba,Ibaraki
> 305-8563, Japan
> E-mail : matsuoka at ni.aist.go.jp
> TEL : +81-29-861-4106
>
>
>