Authors: Došen, Kosta 
Petrić, Zoran 
Affiliations: Mathematical Institute of the Serbian Academy of Sciences and Arts 
Title: Bicartesian coherence
Journal: Studia Logica
Volume: 71
Issue: 3
First page: 331
Last page: 353
Issue Date: 1-Jan-2002
ISSN: 0039-3215
DOI: 10.1023/A:1020568830946
Coherence is demonstrated for categories with binary products and sums, but without the terminal and the initial object, and without distribution. This coherence amounts to the existence of a faithful functor from a free category with binary products and sums to the category of relations on finite ordinals. This result is obtained with the help of proof-theoretic normalizing techniques. When the terminal object is present, coherence may still be proved if of binary sums we keep just their bifunctorial properties. It is found that with the simplest understanding of coherence this is the best one can hope for in bicartesian categories. The coherence for categories with binary products and sums provides an easy decision procedure for equality of arrows. It is also used to demonstrate that the categories in question are maximal, in the sense that in any such category that is not a preorder all the equations between arrows involving only binary products and sums are the same. This shows that the usual notion of equivalence of proofs in nondistributive conjunctive-disjunctive logic is optimally defined: further assumptions would make this notion collapse into triviality.
Keywords: Bicartesian categories | Coherence | Decidability of equality of arrows
Publisher: Springer Link

Show full item record


checked on Jul 13, 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.