Authors: Došen, Kosta 
Petrić, Zoran 
Affiliations: Mathematical Institute of the Serbian Academy of Sciences and Arts 
Title: Coherence in linear predicate logic
Journal: Annals of Pure and Applied Logic
Volume: 158
Issue: 1-2
First page: 125
Last page: 153
Issue Date: 1-Mar-2009
Rank: M22
ISSN: 0168-0072
DOI: 10.1016/j.apal.2008.10.003
Coherence with respect to Kelly-Mac Lane graphs is proved for categories that correspond to the multiplicative fragment without constant propositions of classical linear first-order predicate logic without or with mix. To obtain this result, coherence is first established for categories that correspond to the multiplicative conjunction-disjunction fragment with first-order quantifiers of classical linear logic, a fragment lacking negation. These results extend results of [K. Došen, Z. Petrić, Proof-Theoretical Coherence, KCL Publications (College Publications), London, 2004 (revised version available at:; K. Došen, Z. Petrić, Proof-Net Categories, Polimetrica, Monza, 2007 (preprint available at:, 2005)], where coherence was established for categories of the corresponding fragments of propositional classical linear logic, which are related to proof nets, and which could be described as star-autonomous categories without unit objects.
Keywords: Classical linear logic | Coherence | Criteria of identity for proofs | Cut elimination | First-order predicate logic | Proof-net category
Publisher: Elsevier
Project: Ministry of Science of Serbia (Grants 144013 and 144029)

Show full item record


checked on Jul 14, 2024

Page view(s)

checked on May 9, 2024

Google ScholarTM




Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.