Chu spaces and their continuous functions form a *-autonomous category [Bar79], one that is self-dual and symmetric monoidal closed. This places them squarely in the domain of discourse of Girard's linear logic [Bar91,Gir87]. In this section we define the multiplicative fragment of linear logic from the representational viewpoint, in which in particular has a strikingly natural definition.

In ordinary logic the logical connectives denote operations on truth values. Linear logic however makes the most sense when understood as a categorical logic, whose connectives are functors rather than mere operations.

The language of multiplicative linear logic consists of propositional variables and logical connectives , , , and . In the following, denote arbitrary formulas.

In the Chu space interpretation of linear logic, all formulas are interpreted as Chu spaces.

The first operation of linear logic is linear negation, .
This is interpreted simply as the dual
of the Chu space
interpreting *A*.

The operation
is interpreted as the Chu space consisting of
the representations of the continuous functions from the interpretation
of *A* to the interpretation
of *B*.
Recall from section 3 the Chu space
representing
.
Let
denote the set of continuous functions from
to .
Then
is defined as the Chu space
consisting of the representations of those functions viewed as
words of length ,
where
*r*(*f*,(*a*,*y*)) =
= *s*(*f*(*a*),*y*).

This defines the behavior of
on Chu spaces. Its behavior on
morphisms is defined so as to give this operation the characteristics
of an internal homfunctor. Given continuous functions
and
,
we take
to be the continuous function
from
to
defined by
,
sending
the Chu transform
(where
)
to the composite
(where
=
). Since Chu transforms are closed under
composition *hgf* is a Chu transform, whence
is well-defined.

It remains to show that
is continuous. Evidently its adjoint
should map
to
where
is the adjoint of *h*. Instantiating
the adjointness condition calls for the equality of
(namely
*t*(*hgf*,(*a*',*y*'))) and
.
The definition of *t* gives the left hand side as
*S*'(*hgf*(*a*'),*y*') and
the right hand side as
,
but these are equal
because *h* is a Chu transform, and we are done.

Having defined as a functor it is now easy to define , namely as , and , as .

In [Pra97] we make a start on the project of proving full completeness of linear logic interpreted over Chu spaces, by showing that for formulas of multiplicative linear logic having at most two occurrences of each variable, cut-free proof-nets of those formulas are in bijective correspondence with the dinatural elements of the corresponding functors. This shows that, up to this case, dinaturality exactly captures proof on the semantic side of the mathematical ledger.

In more recent work this summer with Gordon Plotkin we have shown that dinaturality is not sufficient for formulas with four occurrences. In particular there are at least four dinaturals from to itself. However by strengthening the naturality condition to logicality, i.e. invariance under logical relations, we believe we can extend full completeness to the whole of MLL.