Authors: Došen, Kosta 
Petrić, Zoran 
Title: Equality of proofs for linear equality
Journal: Archive for Mathematical Logic
Volume: 47
Issue: 6
First page: 549
Last page: 565
Issue Date: 1-Sep-2008
ISSN: 0933-5846
DOI: 10.1007/s00153-008-0096-0
This paper is about equality of proofs in which a binary predicate formalizing properties of equality occurs, besides conjunction and the constant true proposition. The properties of equality in question are those of a preordering relation, those of an equivalence relation, and other properties appropriate for an equality relation in linear logic. The guiding idea is that equality of proofs is induced by coherence, understood as the existence of a faithful functor from a syntactical category into a category whose arrows correspond to diagrams. Edges in these diagrams join occurrences of variables that must remain the same in every generalization of the proof. It is found that assumptions about equality of proofs for equality are parallel to standard assumptions about equality of arrows in categories. They reproduce standard categorial assumptions on a different level. It is also found that assumptions for a preordering relation involve an adjoint situation.
Keywords: Adjunction | Categorial coherence | Congruence relation | Equality | Equality of proofs | Equivalence relation | Generality of proofs | Linear logic | Monoidal categories | Preordering relation
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.