Coherence in linear predicate logic

Abstract

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: http://www.mi.sanu.ac.yu/~kosta/coh.pdf); K. Došen, Z. Petrić, Proof-Net Categories, Polimetrica, Monza, 2007 (preprint available at: http://www.mi.sanu.ac.yu/~kosta/pn.pdf, 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.