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
Abstract: 
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

SCOPUSTM   
Citations

10
checked on Aug 15, 2022

Page view(s)

17
checked on Aug 15, 2022

Google ScholarTM

Check

Altmetric

Altmetric


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