Some thirty years ago, two proposals were made concerning criteria for identity of proofs. Prawitz proposed to analyze identity of proofs in terms of the equivalence relation based on reduction to normal form in natural deduction. Lambek worked on a normalization proposal analogous to Prawitz's, based on reduction to cut-free form in sequent systems, but he also suggested understanding identity of proofs in terms of an equivalence relation based on generality, two derivations having the same generality if after generalizing maximally (...) the rules involved in them they yield the same premises and conclusions up to a renaming of variables. These two proposals proved to be extensionally equivalent only for limited fragments of logic. The normalization proposal stands behind very successful applications of the typed lambda calculus and of category theory in the proof theory of intuitionistic logic. In classical logic, however, it did not fare well. The generality proposal was rather neglected in logic, though related matters were much studied in pure category theory in connection with coherence problems, and there are also links to low-dimensional topology and linear algebra. This proposal seems more promising than the other one for the general proof theory of classical logic. (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)

We study the coherence, that is the equality of canonical natural transformations in non-free symmetric monoidal closed categories . To this aim, we use proof theory for intuitionistic multiplicative linear logic with unit. The study of coherence in non-free smccs is reduced to the study of equivalences on terms in the free category, which include the equivalences induced by the smcc structure. The free category is reformulated as the sequent calculus for imll with unit so that only equivalences on derivations (...) in this system are to be considered. We establish that any equivalence induced by the equality of canonical natural transformations over a model can be axiomatized by some set of “critical” pairs of derivations. From this, we derive certain sufficient conditions for full coherence, and establish that the system of identities defining smccs is not Post-complete: extending this system with an identity that does not hold in the free smcc does not in general cause the free smcc to collapse into a preorder. In order to give a larger context to these results, we study the equality of canonical morphisms in non-free symmetric monoidal categories, and establish that w.r.t. a broad subclass of smccs, the equivalences induced by the equality of canonical natural transformations over a model coincide with the equivalences induced by the equality of canonical morphisms for all interpretations in that model. (shrink)

Split preorders are preordering relations on a domain whose composition is defined in a particular way by splitting the domain into two disjoint subsets. These relations and the associated composition arise in categorial proof theory in connection with coherence theorems. Here split preorders are represented isomorphically in the category whose arrows are binary relations and whose composition is defined in the usual way. This representation is related to a classical result of representation theory due to Richard Brauer.

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 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)