pith. sign in

arxiv: 1002.3131 · v2 · pith:4JSB3KHInew · submitted 2010-02-16 · 💻 cs.LO

The relational model is injective for Multiplicative Exponential Linear Logic (without weakenings)

classification 💻 cs.LO
keywords exponentialmodellinearlogicmultiplicativeproofsrelationalequivalence
0
0 comments X
read the original abstract

We show that for Multiplicative Exponential Linear Logic (without weakenings) the syntactical equivalence relation on proofs induced by cut-elimination coincides with the semantic equivalence relation on proofs induced by the multiset based relational model: one says that the interpretation in the model (or the semantics) is injective. We actually prove a stronger result: two cut-free proofs of the full multiplicative and exponential fragment of linear logic whose interpretations coincide in the multiset based relational model are the same "up to the connections between the doors of exponential boxes".

This paper has not been read by Pith yet.

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.