Name
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. (A proof of coherence for categories
with binary products and sums simpler than that presented in this paper may be
found in Section 9.4 of {\it Proof-Theoretical Coherence}, revised version of
September 2007, http://www.mi.sanu.ac.yu/~kosta/coh.pdf.) |
Year | DOI | Venue |
|---|---|---|
2002 | 10.1023/A:1020568830946 | Studia Logica |
Keywords | DocType | Volume |
bicartesian categories,coherence,decidability of equality of arrows | Journal | 71 |
Issue | ISSN | Citations |
3 | 0039-3215 | 5 |
PageRank | References | Authors |
0.82 | 0 | 2 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Kosta Dosen | 1 | 143 | 25.45 |
| Zoran Petric | 2 | 40 | 10.82 |