Broadening the denotational semantics of linear logic (Preliminary Report)

AbstractThe proof-theoretic origins and specialized models of linear logic make it primarily operational in orientation. In contrast first-order logic treats the operational and denotational aspects of general mathematics quite evenhandedly. Here we show that linear logic has models of even broader denotational scope than those of first order logic, namely Chu spaces, the category of which Barr has observed to form a model of linear logic. We have previously argued that every category of n-ary relational structures embeds fully and concretely in the category of Chu spaces over 2n. The main contributions of this paper are improvements to that argument, and an embedding of every small category in the category of Chu spaces via a symmetric variant of the Yoneda embedding