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. (shrink)

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 of categorial proof theory the conjecture that two derivations with the same premises and conclusions stand for the same proof if and only if they have the same generality. For that purpose generality is defined within a category whose arrows are equivalence relations on finite ordinals, where composition is rather complicated. Several examples are given of deductive systems of derivations covering fragments of logic, with the associated map into the category of equivalence relations of generality. This category is isomorphically represented in the category whose arrows are binary relations between finite ordinals, where composition is the usual simple composition of relations. This representation is related to a classical representation result of Richard Brauer. (shrink)

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.

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. (shrink)

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.

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.

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 (...) of categorial proof theory the conjecture that two derivations with the same premises and conclusions stand for the same proof if and only if they have the same generality. For that purpose generality is defined within a category whose arrows are equivalence relations on finite ordinals, where composition is rather complicated. Several examples are given of deductive systems of derivations covering fragments of logic, with the associated map into the category of equivalence relations of generality.This category is isomorphically represented in the category whose arrows are binary relations between finite ordinals, where composition is the usual simple composition of relations. This representation is related to a classical representation result of Richard Brauer. (shrink)

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, (...) Polimetrica, Monza, 2007 ], where coherence was established for categories of the corresponding fragments of propositional classical linear logic, which are related to proof nets, and which could be described as star-autonomous categories without unit objects. (shrink)

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.

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 (...) an isomorphic image within SplPre by a map that preserves composition, but not identity arrows. It was shown previously that SplPre and Gen have an isomorphic representation in Rel in the style of Brauer.The syntactical presentation of Gen and Rel in this paper exhibits the particular Frobenius algebra structure of Gen and the particular bialgebraic structure of Rel, the latter structure being built upon the former structure in SplPre. This points towards algebraic modelling of various categories motivated by logic, and related categories, for which one can establish coherence with respect Rel and Gen. It also sheds light on the relationship between the notions of Frobenius algebra and bialgebra. The completeness of the syntactical presentations is proved via normal forms, with the normal form for SplPre and Gen being in some sense orthogonal to the composition-free, i.e. cut-free, normal form for Rel. The paper ends by showing that the assumptions for the algebraic structures of SplPre, Gen and Rel cannot be extended with new equations without falling into triviality. (shrink)

A formal sequent system dealing with Menelaus' configurations is introduced in this paper. The axiomatic sequents of the system stem from 2-cycles of Δ-complexes. The Euclidean and projective interpretations of the sequents are defined and a soundness result is proved. This system is decidable and its provable sequents deliver incidence results. A cyclic operad structure tied to this system is presented by generators and relations.

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.

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. (shrink)

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 (...) representation of the Yang–Baxter equation of symmetric and braid groups. The assumptions of monoidal categories, and in particular Mac Lane’s pentagonal coherence condition, are explained in the absence of commutativity, and also of the unit object, by a similar preservation of associativity by the biendofunctor . In the final section one finds coherence conditions for medial commutativity in the absence of the unit object. These conditions are obtained by taking the direct product of the symmetric groups for 0≤i≤n. (shrink)

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.

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 (...) is reduced to an inductive definition of a kind of commutativity. (shrink)

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.

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.