Relational semantics

Relational semantics

This is the simplest denotational semantics of linear logic. It consists in interpreting a formula A as a set A ^* and a proof π of A as a subset π ^* of A ^* .

The category of sets and relations

It is the category $\mathbf{Rel}$ whose objects are sets, and such that $\mathbf{Rel}(X,Y)=\mathcal P(X\times Y)$. Composition is the ordinary composition of relations: given $s\in\mathbf{Rel}(X,Y)$ and $t\in\mathbf{Rel}(Y,Z)$, one sets

$t\circ s=\set{(a,c)\in X\times Z}{\exists b\in Y\ (a,b)\in s\ \text{and}\ (b,c)\in t}$.