Coherent Obsessional Experiments for Linear Logic Proof-nets

Lorenzo Tortora de Falco

This talk is a contribution to the research field of proof-theory initiated in [Girard 87] with the discovery of linear logic (LL) and 1) its syntax: proof-nets 2) its underlying notion of computation: cutelimination for proof-nets 3) the equivalence relation on proof-nets induced by the coherent semantics.

The cut-elimination procedure for proof-nets induces a (syntactical) equivalence relation on proofnets, which can be roughly defined by: R and R′ are syntactically equivalent iff they have the same normal form.

Denotational semantics gives an “extensional” description of proofs as functions, which is invariant w.r.t. cut-elimination: if π′ is obtained from π by applying some steps of cut-elimination, then π and π′ are interpreted by the same function. Every semantics induces then an equivalence relation on proofs, which can be roughly defined by: π and π′ are semantically equivalent iff they have the same interpretation.

Clearly, two syntactically equivalent proof-nets are also semantically equivalent. In [Tortora 00], we try to “measure” the quality of the representation of proofs as proof-nets by asking whether the converse holds for coherent semantics (which gave birth to LL): in case of positive answer we say that the semantics is injective.

Starting from the definition of experiment of [Girard 87], we introduce the key-notion of “injective obsessional experiment”, which allows to give a positive answer to our question for certain fragments of LL, and to build counter-examples to the injectivity of coherent semantics in the general case.

[Girard 87] Girard J.Y., Linear logic. Theoretical Computer Science, 50:1-101, 1987

[Tortora 00] Tortora de Falco L., Réseaux, cohérence et expériences obsessionnelles, PhD thesis, University Paris 7, January 2000

Address: Équipe Preuves Programmes, Systèmes [EP 2025], Université Paris VII, 2 place Jussieu, 75251 Paris Cedex 05, FRANCE

E-mail: tortora@logique.jussieu.fr