# Coherence spaces and full completeness for the implicative fragment of linear logic

Linear logic isn't complete for coherence space semantics since $1$ and $\top$ get identified. But it is, I believe, complete for the fragment of linear logic whose only connective is $\multimap$.

I was wondering if there's a full completeness result for theories in the fragment of linear logic whose only connective is $\multimap$? I think this is equivalent to asking: is the term model of $\lambda$ terms whose variables only get bound exactly once (over some signature, modulo $=_{\eta\beta}$) a coherence space?

Since the system I'm interested in is very limited, I was also wondering if there are any simpler structures for which full completeness holds?

• Could you define more precisely what you mean by completeness, please? For what concerns full completeness, I assume you mean the standard property: every morphism in the model is the interpretation of a proof/term. This does not hold for coherence spaces (for instance, the empty clique is not not the interpretation of anything). – Damiano Mazza Jun 13 '17 at 4:51