19 found
Order:
  1.  38
    Generality of Proofs and Its Brauerian Representation.Kosta Došen & Zoran Petrić - 2003 - Journal of Symbolic Logic 68 (3):740 - 750.
    The generality of a derivation is an equivalence relation on the set of occurrences of variables in its premises and conclusion such that two occurrences of the same variable are in this relation if and only if they must remain occurrences of the same variable in every generalization of the derivation. The variables in question are propositional or of another type. A generalization of the derivation consists in diversifying variables without changing the rules of inference. This paper examines in the (...)
    Direct download (10 more)  
     
    Export citation  
     
    Bookmark   7 citations  
  2.  15
    Bicartesian Coherence.Kosta Došen & Zoran Petrić - 2002 - Studia Logica 71 (3):331-353.
    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 (...)
    Direct download  
     
    Export citation  
     
    Bookmark   6 citations  
  3.  13
    Generality of Proofs and its Brauerian Representation.Kosta Došen & Zoran Petrić - 2003 - Journal of Symbolic Logic 68 (3):740-750.
    The generality of a derivation is an equivalence relation on the set of occurrences of variables in its premises and conclusion such that two occurrences of the same variable are in this relation if and only if they must remain occurrences of the same variable in every generalization of the derivation. The variables in question are propositional or of another type. A generalization of the derivation consists in diversifying variables without changing the rules of inference.This paper examines in the setting (...)
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark   4 citations  
  4.  27
    Syntax for Split Preorders.Kosta Došen & Zoran Petrić - 2013 - Annals of Pure and Applied Logic 164 (4):443-481.
    A split preorder is a preordering relation on the disjoint union of two sets, which function as source and target when one composes split preorders. The paper presents by generators and equations the category SplPre, whose arrows are the split preorders on the disjoint union of two finite ordinals. The same is done for the subcategory Gen of SplPre, whose arrows are equivalence relations, and for the category Rel, whose arrows are the binary relations between finite ordinals, and which has (...)
    Direct download (5 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  5.  48
    Coherence in Substructural Categories.Zoran Petrić - 2002 - Studia Logica 70 (2):271 - 296.
    It is proved that MacLane''s coherence results for monoidal and symmetric monoidal categories can be extended to some other categories with multiplication; namely, to relevant, affine and cartesian categories. All results are formulated in terms of natural transformations equipped with graphs (g-natural transformations) and corresponding morphism theorems are given as consequences. Using these results, some basic relations between the free categories of these classes are obtained.
    Direct download (6 more)  
     
    Export citation  
     
    Bookmark   3 citations  
  6.  33
    Bicartesian Coherence.Kosta Došen & Zoran Petrić - 2002 - Studia Logica 71 (3):331 - 353.
    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 (...)
    Direct download (6 more)  
     
    Export citation  
     
    Bookmark   3 citations  
  7.  20
    Coherence for Star-Autonomous Categories.Kosta Došen & Zoran Petrić - 2006 - Annals of Pure and Applied Logic 141 (1):225-242.
    This paper presents a coherence theorem for star-autonomous categories exactly analogous to Kelly and Mac Lane’s coherence theorem for symmetric monoidal closed categories. The proof of this theorem is based on a categorial cut-elimination result, which is presented in some detail.
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   2 citations  
  8. Proof-Net Categories.Kosta Dosen, Zoran Petric & Lutz Strassburger - 2008 - Bulletin of Symbolic Logic 14 (2):268-271.
     
    Export citation  
     
    Bookmark   2 citations  
  9.  22
    Coherence in Linear Predicate Logic.Kosta Došen & Zoran Petrić - 2009 - Annals of Pure and Applied Logic 158 (1-2):125-153.
    Coherence with respect to Kelly–Mac Lane graphs is proved for categories that correspond to the multiplicative fragment without constant propositions of classical linear first-order predicate logic without or with mix. To obtain this result, coherence is first established for categories that correspond to the multiplicative conjunction–disjunction fragment with first-order quantifiers of classical linear logic, a fragment lacking negation. These results extend results of [K. Došen, Z. Petrić, Proof-Theoretical Coherence, KCL Publications , London, 2004 ; K. Došen, Z. Petrić, Proof-Net Categories, (...)
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  10.  30
    Associativity as Commutativity.Kosta Dǒsen & Zoran Petrić - 2006 - Journal of Symbolic Logic 71 (1):217 - 226.
    It is shown that coherence conditions for monoidal categories concerning associativity are analogous to coherence conditions for symmetric strictly monoidal categories, where associativity arrows are identities. Mac Lane's pentagonal coherence condition for associativity is decomposed into conditions concerning commutativity, among which we have a condition analogous to naturality and a degenerate case of Mac Lane's hexagonal condition for commutativity. This decomposition is analogous to the derivation of the Yang-Baxter equation from Mac Lane's hexagon and the naturality of commutativity. The pentagon (...)
    Direct download (6 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  11.  49
    Equality of Proofs for Linear Equality.Kosta Došen & Zoran Petrić - 2008 - Archive for Mathematical Logic 47 (6):549-565.
    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 (...)
    Direct download (8 more)  
     
    Export citation  
     
    Bookmark  
  12.  31
    Cartesian Isomorphisms Are Symmetric Monoidal: A Justification of Linear Logic.Kosta Došen & Zoran Petrić - 1999 - Journal of Symbolic Logic 64 (1):227-242.
    It is proved that all the isomorphisms in the cartesian category freely generated by a set of objects (i.e., a graph without arrows) can be written in terms of arrows from the symmetric monoidal category freely generated by the same set of objects. This proof yields an algorithm for deciding whether an arrow in this free cartesian category is an isomorphism.
    Direct download (8 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  13.  12
    Representing Conjunctive Deductions by Disjunctive Deductions.Kosta Došen & Zoran Petrić - 2017 - Review of Symbolic Logic 10 (1):145-157.
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark  
  14.  5
    Modal Functional Completeness.Kosta Dosen & Zoran Petric - 1996 - In H. Wansing (ed.), Proof Theory of Modal Logic. Kluwer Academic Publishers.
  15.  18
    Isomorphic Formulae in Classical Propositional Logic.Kosta Došen & Zoran Petrić - 2012 - Mathematical Logic Quarterly 58 (1):5-17.
    Isomorphism between formulae is defined with respect to categories formalizing equality of deductions in classical propositional logic and in the multiplicative fragment of classical linear propositional logic caught by proof nets. This equality is motivated by generality of deductions. Characterizations are given for pairs of isomorphic formulae, which lead to decision procedures for this isomorphism.
    Direct download (5 more)  
     
    Export citation  
     
    Bookmark  
  16.  6
    Cartesian Isomorphisms Are Symmetric Monoidal: A Justification of Linear Logic.Kosta Dosen & Zoran Petric - 1999 - Journal of Symbolic Logic 64 (1):227-242.
    It is proved that all the isomorphisms in the cartesian category freely generated by a set of objects can be written in terms of arrows from the symmetric monoidal category freely generated by the same set of objects. This proof yields an algorithm for deciding whether an arrow in this free cartesian category is an isomorphism.
    Direct download  
     
    Export citation  
     
    Bookmark  
  17.  9
    Medial Commutativity.Kosta Došen & Zoran Petrić - 2007 - Annals of Pure and Applied Logic 146 (2):237-255.
    It is shown that all the assumptions for symmetric monoidal categories follow from a unifying principle involving natural isomorphisms of the type →, called medial commutativity. Medial commutativity in the presence of the unit object enables us to define associativity and commutativity natural isomorphisms. In particular, Mac Lane’s pentagonal and hexagonal coherence conditions for associativity and commutativity are derived from the preservation up to a natural isomorphism of medial commutativity by the biendofunctor . This preservation boils down to an isomorphic (...)
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark  
  18.  9
    G-Dinaturality.Zoran Petrić - 2003 - Annals of Pure and Applied Logic 122 (1-3):131-173.
    An extension of the notion of dinatural transformation is introduced in order to give a criterion for preservation of dinaturality under composition. An example of an application is given by proving that all bicartesian closed canonical transformations are dinatural. An alternative sequent system for intuitionistic propositional logic is introduced as a device, and a cut-elimination procedure is established for this system.
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark  
  19.  4
    Coherence and Confluence.Kosta Doˇsen & Zoran Petric - 2007 - In Jean-Yves Béziau & Alexandre Costa-Leite (eds.), Perspectives on Universal Logic. pp. 205.
    Direct download  
     
    Export citation  
     
    Bookmark