Poset-valued sets or how to build models for linear logics
type: Item
instance of: scholarly article
title: Poset-valued sets or how to build models for linear logics
zbMATH Open document ID: 1055.03040
author: Andrea Schalk
author: Valeria de Paiva
published in: Theoretical Computer Science
publication date: 2004-08-06T00:00:00Z
review text: 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.
reviewed by: Michel Eytan
Mathematics Subject Classification ID: 03G30
Mathematics Subject Classification ID: 03F52
Mathematics Subject Classification ID: 18A99
zbMATH DE Number: 2081674
zbMATH Keywords: poset-valued sets
zbMATH Keywords: linear logic
zbMATH Keywords: categorical models
Wikidata QID: Q56994546
MaRDI profile type: Publication
full work available at URL: j.tcs.2003.11.014
OpenAlex ID: W2073721500
cites work: Games and full completeness for multiplicative linear logic
cites work: Q3024825
cites work: Q3367300
cites work: Localisation and interaction in one dimension
cites work: Linear logic
cites work: Q3994895
cites work: Q4499228
cites work: Glueing and orthogonality for models of linear logic
cites work: Q4222770
cites work: The Carcinogenic Example
cites work: Q3829551
DOI: 10.1016/J.TCS.2003.11.014
DBLP publication ID: journals/tcs/SchalkP04
Recommended article: The linear logic of multisets
Recommended article: Q4250365
Recommended article: Q3975037
Recommended article: A category-theoretic approach to Boolean-valued models of set theory
Recommended article: THE POSET OF ALL LOGICS I: INTERPRETATIONS AND LATTICE STRUCTURE
Recommended article: Q2721201
Recommended article: Symbolic and Quantitative Approaches to Reasoning with Uncertainty
Recommended article: Representation of concrete logics and concrete generalized orthomodular posets
Recommended article: Q3478387
Recommended article: The Hybrid Logic of Linear Set Spaces
description: scientific article; zbMATH DE number 2081674