Towards Full Completeness of the Linear Logic of Chu Spaces
Vaughan Pratt · Electronic Notes in Theoretical Computer Science · 1997
We investigate the linear logic of Chu spaces as defined by its dinaturality semantics. For those formulas of multiplicative linear logic limited to at most two occurrences of each variable we prove full completeness of Girard's MIX-free axiomatization, namely that the cut-free proof-nets of such formulas are in a natural bijection with the dinatural elements of the corresponding functors.