Poset-valued sets or how to build models for linear logics (Q1826627)

The authors construct yet another model for linear logic that gives precise control over items like: classical vs intuitionistic (properties of negation can be specified); products and coproducts coincide on objects or not, id for their units; tensor and par coincide on objects or not, id for their units. After giving two examples, they define the category \(P_F\)-\textbf{Set} (of \(P_F\) sets), where \(P\) is a poset and \(F\) is an endofunctor on \textbf{Rel} as follows: an object is a map \(FA \rightarrow P\); an arrow \((\alpha: FA \rightarrow P) \rightarrow (\beta: FB \rightarrow P)\) is a relation \(R: A \mapsto B\) such that \(x(FR)y\) implies \(\alpha(x) \leq \beta(y).\) The set \(A\) ``takes values'' (via \(F\)) in \(P\), whence the name. Identities in \(P_F\)-\textbf{Sets} are identity relations and composition is that of relations. Define now a categorical model of intuitionistic linear logic to be a category which: is symmetric monoidal closed; has finite products; is equipped with a linear exponential comonad [\textit{G. M. Berman}, ``What is a categorical model of intuitionistic linear logic?'', Lect. Notes Comput. Sci. 902, 73--93 (1995; Zbl 0813.68040)]. A model for classical linear logic is a category which: is *-autonomous; has finite products and (so) coproducts; is equipped with a linear exponential comonad and (so) a linear exponential monad. Theorem: If \(P\) is *-autonomous and a complete lattice and \(F\) satisfies the conditions of Proposition 3.3, then \(P_F\)-\textbf{Set} is a model for classical linear logic. In addition it has arbitrary products and coproducts. If P is symmetric monoidal closed and a complete lattice and \(F\) satisfies the conditions of Proposition 3.3, then \(P_F\)-\textbf{Set} is a model for intuitionistic linear logic. In addition, it has arbitrary products and coproducts.