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 |

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

#### SCOPUS^{TM}

Citations

2
checked on Jul 13, 2024

#### Page view(s)

38
checked on May 9, 2024

#### Google Scholar^{TM}

Check
#### Altmetric

#### Altmetric

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