Theory and Applications of Categories, Vol. 18, No. 17, 2007, pp. 473–535.

EXPLORING THE GAP BETWEEN LINEAR AND CLASSICAL LOGIC

FRANÇOIS LAMARCHE

Abstract. The Medial rule was first devised as a deduction rule in the Calculus of Structures. In this paper we explore it from the point of view of category theory, as additional structure on a ∗-autonomous category. This gives us some insights on the denotational semantics of classical propositional logic, and allows us to construct new models for it, based on suitable generalizations of the theory of coherence spaces.

1. Introduction

This paper has two basic goals:

• to explore a recent extension of multiplicative linear logic—the Medial rule—from the point of view of algebra. We will present a categorical axiomatization, as added structure and axioms to the standard definition of ∗-autonomous category, as well as real-life examples of such categories.

• to use this framework as a tool for the construction of “symmetrical” models of classical logic, that is, models that have an underlying ∗-autonomous structure [Bar91, See89, FP05, FP04a, FP04b]. Every object in a “symmetrical” model has a ⊗- comonoid structure, and thus, because of ∗-autonomy, also a ⅋-monoid structure. As is customary, we then say that every object has a bimonoid structure. The use of a ∗-autonomous category with Medial as a waystation is very much a semantical approach: in this paper we try to construct such categories where good classes of bimonoids already exist, which is very different from the syntactic approach of decreeing the existence of rules like contraction and weakening. Until now all the known examples of a denotational semantics—in the sense of a “concrete” category which is not a poset—for “symmetrical” classical logic suffered from degeneracies at the level of the Boolean operations. It was observed that the category of sets and relations is a kind of “Boolean category” (appearing first in Führmann and Pym [FP05]) that identifies conjunction and disjunction, and that this was also true for several other examples like finite-dimensional vector spaces and the category of sets and profunctors, as observed by Hyland [Hyl04]. We will end up with new and interesting classes of such models, some of which are quite natural; they turn out to be very closely related to traditional coherence spaces [GLT89], and to have the same relationship with the category of relations as them.

Received by the editors 2006-06-12 and, in revised form, 2007-10-09.

Transmitted by R. Blute. Published on 2007-10-18.

2000 Mathematics Subject Classification: 03F52, 03G30, 19D23, 18D15, 68Q55.

Key words and phrases: *-autonomous categories, denotational semantics, linear logic, classical logic, deep inference, Medial rule.

\begin{matrix}c \\ ◯ \end{matrix} François Lamarche, 2007. Permission to copy for private use granted.

Until a recent date, any semantics of proofs for classical logic would break some of the inherent symmetry of classical logic. This can be expressed most succinctly by using categorical language, starting with the well-known observation that if any cartesian-closed category (with coproducts) models proofs in intuitionistic linear logic—in other words, is a model of the lambda calculus with sum types—then the presence of a dualizing object forces the collapse of the category to a poset (a Boolean algebra, naturally). This was first observed by André Joyal [LS86, pp.67,116] (see also [Gir91, Appendix]).

It had been observed some while ago [Fil89,Gri90] that control operators in functional programming can be modelled by extending the lambda calculus with constants that correspond to Pierce’s law, which is one simple way to bridge the gap between intuitionistic and classical logic. This was extended to a full natural deduction system for classical logic by Parigot [Par92], that he called the λ-μ-calculus. It has a general categorical axiomatization [Sel01], which is built on the foundations of [SR98]. The “pure λ-calculus” component of this axiomatization is just ordinary cartesian-closed categories, with the expected result that the double-negation of an object X is not isomorphic to X. Furthermore, the operator that models disjunction is not bifunctorial, but only “functorial in each variable separately”, which is another loss of symmetry. From the point of view of operational semantics, this “flaw” of disjunction means that computation in such models is very much sequential.

Girard’s system LC for classical logic [Gir91] is based on a categorical construction in cartesian-closed categories that uses the very same ingredients as [SR98]. The difference is an ingenious system of polarities, that restricts the application of the categorical operators, and forces the identity of an object with its double negation (you can’t apply the categorical negation operator twice, so the formal negation of a negated object is the original object). In this interpretation composition of proofs is not associative, which is not good news. There is an alternative construction in the category of coherence spaces that uses the full model of linear logic available there (multiplicatives, additives and exponentials), and probably more; it corrects that problem of associativity of composition. It is not clear what are the abstract properties that make this construction work, and how it can be exploited by syntax. But anyway both models (and the common sequent calculus which is interpreted in them) suffer from the problem that the connectives as bifunctors are only partially defined, due to the need of some maps to be “in stoup position” in some cases. More work has to be done on this model, but it obviously does not have the necessary symmetries to embody the idea of a “Boolean algebra which is a category”.

Another categorical axiomatization for the λ-μ-calculus has been proposed by Ong [Ong96]. The λ-μ-calculus’ distinction between variables and names (covariables) appears in the semantics itself, which use fibered categories to manage both kinds of variables. Thus the categories involved need not have coproducts, but the symmetries/asymmetries of the semantics are patterned quite closely on those of the syntax: when names appear they act completely symmetrically towards negation, but a variable can also appear at the same place as a name, and variables have the same, “intuitionistic” behavior as in the ordinary lambda calculus.

That was the situation about two years ago. People were aware of one of the main lessons of multiplicative logic, that removing contraction and weakening permits a real involutive negation at the level of the proofs. People also knew that if linear logic is taken as granted, then adding the possibility of weakening and contraction (seen as a left-side rule) to an object is to be seen as giving a comonoid structure to that object. And people knew quite well that if every object of a “linear category” is equipped with a comonoid structure, and if every map in that category respects the comonoid structure in question, then the conjunction/tensor in the linear category is just ordinary categorical product. Thus if we add the involutive negation to this mix, we are back to Joyal’s paradox.

Naturally one way out of this conundrum is to find ∗-autonomous categories such that every object is equipped with a comonoid structure, but where the maps do not preserve that full structure.

A negative requirement like this one doesn’t tell you where to look, and what to expect instead. It took the appearance of two concrete models, both based on proof net syntax [Rob03, LS05b] (differing markedly on the syntactic interpretation of the categorical composition operator), to show that there was indeed such a thing as a “symmetric” model of Boolean logic, one that fulfilled this negative requirement.

And then came the natural question: “What are the essential categorical properties of these models?”. The several solutions that have been proposed [FP05,FP04b,LS05a,Str07] show that we have gone from having no answer at all to having way too many answers.^{1} In [Str07] there is an exhaustive survey of the different possibilities—the present state of the art—that arise when one tries to formalize this notion of “Boolean category”. And there is a possibility that more subtleties will appear when this work is fully extended to first-order logic, a program which has already begun [McK06].

Right now there are not enough concrete semantics to fill all these possibilities, and perhaps there never will be^{2}. This situation is in marked contrast with that of intuitionistic logic, since the axioms for a cartesian-closed category (with coproducts) are maximal in the sense that any non-trivial addition of an equation forces all models to become posets [Sim95,DP04]

The present papers explores a particular class of possibilities among these, the ones that are based on the Medial rule. This rule [BT01,Brü03] was devised to obtain deductive systems for classical logic that are based on deep inference [Gug07]. Rules are much more mobile (there are many more ways of permuting them) in deep inference, and the syntactic motivation of Medial is to allow arbitrary contractions to be be pushed all the way to the atomic formulas. This has an immediate semantical reading: if we have Medial, we know how to define the bimonoid structure on a conjunction A ∧ B from the bimonoid structures on A, B. So as we have said at the beginning of this introduction, our second contribution is the exploitation of that idea in the realm of denotational semantics, i.e., the construction of concrete “symmetrical” models of classical logic. But if the Medial rule is a new syntactic tool for logic—although it has already been observed in the realm of game semantics by Blass [Bla92]—we have to know what it is from the categorical point of view, since we intend first to construct models of linear logic with Medial before attacking classical logic. Thus, most of our axioms and results about Medial also appear in [Str07], but everything there is done in a classical context (weakening and contraction being always assumed a priori), while we do not have that luxury, working in a purely linear context. An outcome of this is that some of our own axioms are propositions in [Str07], and some of our own propositions are harder to prove.

1Two other, related approaches should also be mentioned; we consider they are a little outside the aforementioned “mainstream” we have shamelessly defined by decree. The axiomatization proposed by Došen [DP04] is perfectly symmetrical, but lacks the property of monoidal closure, which is shared by all the above attempts, and that we consider to be essential. The axiomatic suggestions given by Hyland in [Hyl04] are phrased in the language of compact-closed categories, in which tensor and par coincide.

But it is possible to define Frobenius algebras in a ∗-autonomous context, for example by requiring the axiom of graphicality [LS05a, 2.4.4].

2even if we take account of the fact that some of these possibilities are dictated by syntax and would not appear naturally in semantics.

2. Medial and Mix

2.1. preliminaries. We will always be working in a ∗-autonomous category ℂ, although much of what we’re doing can be done in a weakly (aka linearly) distributive category [CS97a] equipped with an involution that exchanges tensor and par. Our notation for the operators of linear logic is almost completely standard: ⊗, ⅋, I, ⊥, (−)^{⊥} ; the tensor unit is nonstandard for typographical reasons. We write the categorical composition of maps f, g either as gf or g ∘ f, depending on whim. We use the traditional (“functional”) order to denote composition.

Here are some notational conventions we will stick to. First we will very seldom write associativity isomorphisms explicitly. In other words we use as few parentheses as we can. We will also never name the unit isos, and just use a standard generic “isomorphism” notation for them, e.g.,

\xymatrix{(A ⅋ ⊥) ⊗ B ⊗ I \ar@{^{(}->}[r] & A ⊗ B .}

For the symmetry we will use the notation T_{A,B} (the T is for Twistmap):

[figure: A ⊗ B; T_{A,B}; B ⊗ A; A ⅋ B; T_{A,B}; B ⅋ A]

without bothering with the distinction between the Tensor-Twist and the Par-Twist, which is always obvious.

In our setting the “right switch” map (which is how we call the linear distributivity)

\xymatrix{S_{A,B,C}^{r}: & (A ⅋ B) ⊗ C \ar[r] & A ⅋ (B ⊗ C)}

is obtained from the ∗-autonomous structure (e.g., [LS06]); it is self-dual (see below for a precise definition of what this means) and commutes with itself in the sense that it can be composed with itself to give a uniquely defined map

S_{A,B;X,Y}^{r} : (A ⅋ X) ⊗ (B ⅋ Y) → A ⅋ B ⅋ (X ⊗ Y),  (1)

natural in all variables. One reason we put the variables in this order in the definition is because this version of switch can be iterated: the different ways to construct

S_{A,B,C;X,Y,Z}^{r} : (A ⅋ X) ⊗ (B ⅋ Y) ⊗ (C ⅋ Z) → A ⅋ B ⅋ C ⅋ (X ⊗ Y ⊗ Z),

by composing Switch all define the same map. So we can use the same notation in a 3-ary, 4-ary, etc. context.

2.2. Proposition. The following two triangles commute,

[figure: (⊥ ⅋ B) ⊗ C; S_{⊥,B,C}^{r}; ⊥ ⅋ (B ⊗ C); B ⊗ C; (A ⅋ B) ⊗ 1; S_{A,B,1}^{r}; A ⅋ (B ⊗ 1); A ⅋ B]

where (as we already said) the diagonal maps are unit isos.

Proof. Look at the rightmost object in the first triangle, and take the transpose of the two maps that have it for target. We get another triangle

[figure: I ⊗ (⊥ ⅋ B) ⊗ C; ev ⊗ C; B ⊗ C; I ⊗ B ⊗ C]

where ev is the evaluation map for I ⊸ B = I^{⊥} ⅋ B. This triangle obviously commutes. The other triangle is obtained by self-duality of Switch.

Because of the presence of a symmetry/Twist the Switch map has several incarnations, which we will have to invoke sometimes. The official “left Switch” map is

\xymatrix{S_{A,B,C}^{l}: & A ⊗ (B ⅋ C) \ar[r] & (A ⊗ B) ⅋ C ,}

its 4-ary version is

S_{A,B;X,Y}^{l} : (A ⅋ X) ⊗ (B ⅋ Y) ⟶ (A ⊗ B) ⅋ X ⅋ Y ,

and the self-duality of Switch is expressed by

[figure: (A^{⊥} ⅋ B^{⊥}) ⊗ C^{⊥}; S_{A^{⊥},B^{⊥},C^{⊥}}^{r}; A^{⊥} ⅋ (B^{⊥} ⊗ C^{⊥}); ((A, ⊗B) ⅋ C))^{⊥}; (S_{A,B,C}^{l})^{⊥}; (A ⊗ (B ⅋ C))^{⊥}]

We will also need other version of Switch, i.e., other combinations with the Twistmap. We will simply use S^{l} as a generic name for things of the form

\xymatrix{A ⊗ (⋯ ⅋ X ⅋ ⋯) \ar[r] & (⋯ ⅋ (A ⊗ X) ⅋ ⋯)}

and also for things of the form

\xymatrix{A ⊗ (⋯ ⅋ I ⅋ ⋯) \ar[r] & (⋯ ⅋ A ⅋ ⋯)}

where a unit iso is involved in addition to a bona fide Switch. Similarly we will use S^{r} as a generic name for things like

\xymatrix{(⋯ ⅋ X ⅋ ⋯) ⊗ B \ar[r] & (⋯ ⅋ (X ⊗ B) ⅋ ⋯)}

and

\xymatrix{(⋯ ⅋ I ⅋ ⋯) ⊗ B \ar[r] & (⋯ ⅋ B ⅋ ⋯) .}

There is another ink-saving convention we will use throughout this paper: we use the symbols 𝕀, ⊥ ⊥ when we mean I, ⊥ but want the symbol to disappear by composition with the unit isos when it is in a context that allows this. This is easier to explain by examples than to formalize: for instance, the map S_{A,⊥ ⊥;X,Y}^{r} goes (A ⅋ X) ⊗ Y → A ⅋ (X ⊗ Y) (and thus S_{A,B,C}^{r} = S_{A,⊥ ⊥;B,C}^{r}) while S_{A,X;𝕀,Y}^{r} goes (A ⅋ I) ⊗ (X ⅋ Y) → A ⅋ X ⅋ Y.

2.3. Mix. When you have a binary operation which is associative, you immediately get its n-ary version for all n ≥ 2 by composition/substitution. We can extend this to the case n = 1 by decreeing that the unary version of the operation is identity; in this case we can say we have access to the n + 1-ary version of the operation. If our operation also has a unit we take it to be us the nullary version of the operation. Thus an associative operation with unit has a version available for all finite arities.

This also works with things like natural transformations. For example the Mix map starts as a “binary” entity

M_{A,B} : A ⊗ B → A ⅋ B  (2)

but we always want the necessary equations [Blu93] that ensure that the two ways of going from A ⊗ B ⊗ C to A ⅋ B ⅋ C (using Switch in addition to Mix) yield the same map, which we write M_{A,B,C} (we also have to show that the binary Mix merges well with the symmetries). Thus, since binary Mix always comes equipped with the necessary monoidal equations, it is actually n + 1-ary Mix. Then nullary Mix is a map I → ⊥, but this is not what we really want in general, since this is not entirely palatable to traditional logicians (although rather common in practice, since I and ⊥ are isomorphic in quite a few denotational semantics). Here is a case where the nullary notion is not desirable. But if we apply Mix to ⊥ ⊗ I we get a map that goes ⊥ → I instead; in [CS97b] a condition (and see right below) is given on that map that allows the general Mix to be deduced from it.

The following already appears in [FP04a]:

2.4. Proposition. In a ∗-autonomous category, a map m: ⊥ ⊗ ⊥ → ⊥ which is associative and commutative determines an n + 1-ary Mix map, by taking

[figure: A ⊗ B; S_{A,B;⊥ ⊥,⊥ ⊥}^{r}; A ⅋ B ⅋ (⊥ ⊗ ⊥); A ⅋ B ⅋ m; A ⅋ B ⅋ ⊥; A ⅋ B .]

Moreover the converse is true, since an n + 1-ary Mix trivially determines an associative, commutative operation on ⊥.

Proof. The only thing to verify is that the binary Mix extends to an n + 1-ary one; and this is very easy to do using the generalized Switch.

The following is probably well-known in some circles.

2.5. Proposition. let e: X → I be any map. Then the map

[figure: m : X ⊗ X; e ⊗ X; I ⊗ X; X]  (3)

defines an associative operation on X.

Proof. An easy diagram chase.

The following gives a concise definition of Mix.

2.6. Proposition. Assume that e: ⊥ → I is such that the associative operation m defined in 3 (with X replaced by ⊥) is also commutative. Then the following (obviously commutative) diagram

[figure: A ⊗ B; (A ⅋ ⊥) ⊗ B; S^{r}; (A ⅋ e) ⊗ B; A ⅋ (⊥ ⊗ B); A ⅋ (e ⊗ B); (A ⅋ I) ⊗ B; S^{r}; A ⅋ (I ⊗ B); A ⅋ B]  (4)

defines the Mix natural transformation associated to m; furthermore if e is self-dual then this Mix is self-dual too.

Proof. The first part is obtained by pasting the following to the right of the above diagram:

[figure: A ⅋ (⊥ ⊗ B); A ⅋ (e ⊗ B); A ⅋ (⊥ ⊗ (⊥ ⅋ B)); A ⅋ S_{⊥,⊥,B}^{l}; A ⅋ (e ⊗ (⊥ ⅋ B)); A ⅋ (⊥ ⊗ ⊥) ⅋ B; A ⅋ (e ⊗ ⊥) ⅋ B; A ⅋ (I ⊗ B); A ⅋ (I ⊗ (⊥ ⅋ B)); A ⅋ S_{I,⊥,B}^{l}; A ⅋ (I ⊗ ⊥) ⅋ B; A ⅋ B]

where the bottom right triangle is Proposition 2.2.

The second statement is just the observation that Diagram (4) is self-dual.

Notice that this has a converse: the map obtained by applying Mix to ⊥ ⊗ I trivially obeys the necessary conditions of this result.

A judicious use of notation would enable us to dispense with squares like Diagram (4), since we are perfectly allowed to write S_{A,e,B}^{r}: (A⅋⊥)⊗B ⟶ A⅋(I⊗B) for its diagonal. We will not make use of this notational trick here, in the hope of making things more readable for beginners.

2.7. Binary Medial. We are interested in a natural map that we call binary Medial, or more-precisely (2, 2)-ary Medial.

[\begin{matrix}A & B \\ C & D \end{matrix}] : (A ⊗ B) ⅋ (C ⊗ D) ⟶ (A ⅋ C) ⊗ (B ⅋ D)  (5)

The general idea behind the two-dimensional (matrix) notation should be clear: entries in a row are separated by tensors, and entries in a column by pars. In the input the rows associate tighter than the columns while it is the reverse in the output. The idea of Medial first appeared in [BT01] as a deduction rule in formalizations of classical logics in the Calculus of Structures, but as we have said its existence had already been noted in semantics [Bla92].

This Medial map is asked to obey four conditions:

• it should be self-dual:

[figure: (A^{⊥} ⊗ B^{⊥}) ⅋ (C^{⊥} ⊗ D^{⊥}); _{[\begin{matrix}A^{⊥} & B^{⊥} \\ C^{⊥} & D^{⊥} \end{matrix} ]}; ((A ⅋ B) ⊗ (C ⅋ D))^{⊥}; _{[\begin{matrix}A & B \\ C & D \end{matrix}]}_{⊥}; (A^{⊥} ⅋ C^{⊥}) ⊗ (B^{⊥} ⅋ D^{⊥}); ((A ⊗ C) ⅋ (B ⊗ D))^{⊥}]

EXPLORING THE GAP BETWEEN LINEAR AND CLASSICAL LOGIC  481

• it should interact well with the symmetry:

[figure: (A ⊗ B) ⅋ (C ⊗ D); T_{A,B} ⅋ T_{C,D}; _{[\begin{matrix}A & B \\ C & D \end{matrix}]}; (B ⊗ A) ⅋ (D ⊗ C); _{[\begin{matrix}B & A \\ D & C \end{matrix}]}; (A ⅋ C) ⊗ (B ⅋ D); T_{A⅋C,B⅋D}; (B ⅋ D) ⊗ (A ⅋ C)]

the dual to this is

[figure: (A ⊗ B) ⅋ (C ⊗ D); T_{A⊗B,C⊗D}; _{[\begin{matrix}A & B \\ C & D \end{matrix}]}; (C ⊗ D) ⅋ (A ⊗ B); _{[\begin{matrix}C & D \\ A & B \end{matrix}]}; (A ⅋ C) ⊗ (B ⅋ D); T_{A,C} ⊗ T_{B,D}; (C ⅋ A) ⊗ (D ⅋ B)]

• it should interact well with itself (with the help of associativity):^{3}

[figure: (A ⊗ B ⊗ C) ⅋ (D ⊗ E ⊗ F); _{[\begin{matrix}A & B ⊗ C \\ D & E ⊗ F \end{matrix} ]}; ^{[\begin{matrix}A ⊗ B & C \\ D ⊗ E & F \end{matrix} ]}; ((A ⊗ B) ⅋ (D ⊗ E)) ⊗ (C ⅋ F); [\begin{matrix}A & B \\ D & E \end{matrix} ] ⊗ (C ⅋ F); (A ⅋ D) ⊗ ((B ⊗ C) ⅋ (E ⊗ F)); (A ⅋ D) ⊗ [\begin{matrix}B & C \\ E & F \end{matrix} ]; (A ⅋ D) ⊗ (B ⅋ E) ⊗ (C ⅋ F)]

(6)

It is natural to extend our matrix notation, and call the above map

[\begin{matrix}A & B & C \\ D & E & F \end{matrix} ] : (A ⊗ B ⊗ C) ⅋ (D ⊗ E ⊗ F) ⟶ (A ⅋ D) ⊗ (B ⅋ E) ⊗ (C ⅋ F) ;

while its de Morgan dual is naturally written as the transpose matrix:

[\begin{matrix}A & D \\ B & E \\ C & F \end{matrix}] : (A ⊗ D) ⅋ (B ⊗ E) ⅋ (C ⊗ F) ⟶ (A ⅋ B ⅋ C) ⊗ (D ⅋ E ⅋ F)

3Naturally this could be called Interaction with Associativity.

• it should interact well with Switch:

[figure: ((A ⊗ B) ⅋ (C ⊗ D)) ⊗ X; S_{A⊗B,C⊗D,X}^{r}; [\begin{matrix}A & B \\ C & D \end{matrix}] ⊗ X; (A ⊗ B) ⅋ (C ⊗ D ⊗ X); _{[\begin{matrix}A & C \\ B & D ⊗ X \end{matrix} ]}; (A ⅋ C) ⊗ (B ⅋ D) ⊗ X; (A ⅋ C) ⊗ S_{B,D,X}^{r}; (A ⅋ C) ⊗ (B ⅋ D ⊗ X) .]

Assume that the equation above holds; we can combine it with two applications of interaction with Twist

[figure: ((A ⊗ B) ⅋ (C ⊗ D)) ⊗ X; [\begin{matrix}A & B \\ C & D \end{matrix}] ⊗ X; T_{A⊗B,C⊗D} ⊗ X; (A ⅋ C) ⊗ (B ⅋ D) ⊗ X; T_{A,C} ⊗ T_{B,D} ⊗ X; ((C ⊗ D) ⅋ (A ⊗ B)) ⊗ X; [\begin{matrix}C & D \\ A & B \end{matrix}] ⊗ X; S_{C⊗D,A⊗B,X}^{r}; (C ⅋ A) ⊗ (D ⅋ B) ⊗ X; (C ⅋ A) ⊗ S_{D,B,X}^{r}; (C ⊗ D) ⅋ (A ⊗ B ⊗ X); _{[\begin{matrix}C & D \\ A & B ⊗ X \end{matrix} ]}; T_{C⊗D,A⊗B⊗X}; (C ⅋ A) ⊗ (D ⅋ (B ⊗ X)); T_{C,A} ⊗ T_{D,B⊗X}; (A ⊗ B ⊗ X) ⅋ (C ⊗ D); _{[\begin{matrix}A & B ⊗ X \\ C & D \end{matrix} ]}; (A ⅋ C) ⊗ ((B ⊗ X) ⅋ D)]

and get another version of Interaction with Switch,

[figure: ((A ⊗ B) ⅋ (C ⊗ D)) ⊗ X; S^{r}; [\begin{matrix}A & B \\ C & D \end{matrix}] ⊗ X; (A ⊗ B ⊗ X) ⅋ (C ⊗ D); _{[\begin{matrix}A & B ⊗ X \\ C & D \end{matrix} ]}; ((A ⅋ C) ⊗ (B ⅋ D)) ⊗ X; S^{r}; (A ⅋ C) ⊗ ((B ⊗ X) ⅋ D))]

one where the version of Switch we use doesn’t have its own special symbol. If we allow the order of the object variables to be changed only by applications of Switch, and if X stays at the right as above, there are four versions of Interaction with Switch, and given one of them the other three can be deduced from it by the same kind of trick we have just used. If we put X at the left, there are four more; let us show one of these, and let the reader check that these eight versions of interaction with Switch can be deduced from a single one of them, combined with the other axioms.

[figure: X ⊗ ((A ⊗ B) ⅋ (C ⊗ D)); S_{X,A⊗B,C⊗D}^{l}; X ⊗ [\begin{matrix}A & B \\ C & D \end{matrix}]; (X ⊗ A ⊗ B) ⅋ (C ⊗ D); _{[\begin{matrix}X ⊗ A & B \\ C & D \end{matrix}]}; X ⊗ (A ⅋ C) ⊗ (B ⅋ D); S_{X,A,C}^{l} ⊗ (B ⅋ D); ((X ⊗ A) ⅋ C) ⊗ (B ⅋ D)]

We keep our conventions with “disappearing” units; for example:

\begin{matrix}[\begin{matrix}X & 𝕀 \\ 𝕀 & Y \end{matrix} ] : & X ⅋ Y & ⟶ & (X ⅋ I) ⊗ (I ⅋ Y) \\ [\begin{matrix}X & 𝕀 \\ Y & 𝕀 \end{matrix} ] : & X ⅋ Y & ⟶ & (X ⅋ Y) ⊗ (I ⅋ I) . \end{matrix}

2.8. Remark. Interaction of Medial with the symmetry and itself, along with the Absorption law of the next section, could be expressed in a single phrase by saying that the tensor is a monoidal (bi-)functor over the ⅋-monoidal structure. Or, equivalently, that the par is a co-monoidal (bi-)functor over the ⊗-structure. But we still would have to write down the above equations since we have use them extensively. In a law like Medial, the outer connective (par) gets exchanged with one (tensor) which is stronger. This is the reverse situation from the kind of monoidal bifunctor laws like those presented in [BPS06].

2.9. Remark. For any doubly-indexed family of objects (A_{ij})_{i≤n,j≤m} it is easy to construct a natural map that we write as a matrix

\xymatrix{(A_{11} ⊗ A_{12} ⋯ ⊗ A_{1m}) ⅋ (A_{21} ⊗ A_{22} ⋯ ⊗ A_{2m}) ⋯ ⅋ (A_{n1} ⊗ A_{n2} ⋯ ⊗ A_{nm}) \\  & _{[ \begin{matrix}A_{11} & A_{12} & ⋯ & A_{1m} \\ A_{21} & A_{22} & ⋯ & A_{2m} \\ ⋮ & ⋮ & ... & ⋮ \\ A_{n1} & A_{n2} & ⋯ & A_{nm} \end{matrix} ]} \ar[dl] \\ (A_{11} ⅋ A_{21} ⋯ ⅋ A_{n1}) ⊗ (A_{12} ⅋ A_{22} ⋯ ⅋ A_{n2}) ⋯ ⊗ (A_{1m} ⅋ A_{2m} ⋯ ⅋ A_{nm})}

In an appendix we will show that this map is uniquely defined and say what we mean by this (this result is not needed in the rest of the paper, except for the 2 × 4 case^{4}).

4The proof of the general case was requested by a referee.

2.10. Remark. Our use of matrices is quite different from the one that appears sometimes in the literature on monoidal categories, such as [FY89, Section 4]. In our case the row and column entries “vary multiplicatively”, while in the aforementioned work they “vary additively”. In this paper we could use matrices that way if we decided to present relations (i.e., maps in the categories Rel, Cmp of Section 4) as matrices with coefficients in the two-element locale.

So we’ve started with a (2, 2)-ary operation, and got the general (n + 1, m + 1)-ary version without too much work; moreover there’s no ambiguity about how to define the (1, m)- and (n, 1)-ary versions: an expression like [A_{1}, A_{2}, …, A_{m}] should be the identity map on the object A_{1} ⊗ A_{2} ⊗ ⋯ ⊗ A_{m}, while

[ A_{1} ; A_{2} ; ⋮ ; A_{n} ]

stands for the identity on A_{1} ⅋ A_{2} ⅋ ⋯ ⅋ A_{n}. This can be used to rewrite Equation (6) as follows:

[[\begin{matrix}A & B \\ D & E \end{matrix} ] [ \begin{matrix}C \\ F \end{matrix} ]] ∘ [\begin{matrix}A ⊗ B & C \\ D ⊗ E & F \end{matrix} ] = [[ \begin{matrix}A \\ D \end{matrix} ] [\begin{matrix}B & C \\ E & F \end{matrix} ]] ∘ [\begin{matrix}A & B ⊗ C \\ D & E ⊗ F \end{matrix} ]

We will use bracket nesting of this sort only sporadically, just to emphasize some symmetries that deserve it.

2.11. Proposition. Let B be any object of ℂ. Then the following equations hold:

[\begin{matrix}⊥ ⊥ & B \\ 𝕀 & ⊥ ⊥ \end{matrix}] = [\begin{matrix}𝕀 & ⊥ ⊥ \\ ⊥ ⊥ & B \end{matrix}] ,  [\begin{matrix}⊥ ⊥ & 𝕀 \\ B & ⊥ ⊥ \end{matrix}] = [\begin{matrix}B & ⊥ ⊥ \\ ⊥ ⊥ & 𝕀 \end{matrix}] ,  (7)
[\begin{matrix}𝕀 & B \\ ⊥ ⊥ & 𝕀 \end{matrix} ] = [\begin{matrix}B & 𝕀 \\ 𝕀 & ⊥ ⊥ \end{matrix}] ,  [\begin{matrix}⊥ ⊥ & 𝕀 \\ 𝕀 & B \end{matrix} ] = [\begin{matrix}𝕀 & ⊥ ⊥ \\ B & 𝕀 \end{matrix}] ,  (8)
[\begin{matrix}⊥ ⊥ & 𝕀 \\ B & ⊥ ⊥ \end{matrix}] ∘ T_{⊥,B} = [\begin{matrix}𝕀 & ⊥ ⊥ \\ ⊥ ⊥ & B \end{matrix}] ,  T_{I,B} ∘ [\begin{matrix}⊥ ⊥ & 𝕀 \\ 𝕀 & B \end{matrix} ] = [\begin{matrix}𝕀 & B \\ ⊥ ⊥ & 𝕀 \end{matrix} ] .  (9)

Proof. The very first equation is proved by chasing the following diagram

[figure: (I ⊗ ⊥) ⅋ (⊥ ⊗ B); ^{[\begin{matrix}I & ⊥ \\ ⊥ & B \end{matrix}]}; T_{I⊗⊥,⊥⊗B}; (I ⅋ ⊥) ⊗ (⊥ ⅋ B); T_{I,⊥} ⊗ T_{⊥,B}; ⊥ ⊗ B; B; (⊥ ⊗ B) ⅋ (I ⊗ ⊥); _{[\begin{matrix}⊥ & B \\ I & ⊥ \end{matrix}]}; (⊥ ⅋ I) ⊗ (B ⅋ ⊥)]

where the two triangles commute because of the coherence theorem for monoidal categories, the middle square is just agreement of Medial and Twist, and the outer hexagon is the equation we want to prove. The first equation in (9) is proved by the very similar

[figure: ⊥ ⊗ B; T_{⊥,B}; (I ⊗ ⊥) ⅋ (⊥ ⊗ B); ^{[\begin{matrix}I & ⊥ \\ ⊥ & B \end{matrix}]}; T_{I,⊥} ⅋ T_{⊥,B}; (I ⅋ ⊥) ⊗ (⊥ ⅋ B); T_{I⅋⊥,⊥⅋B}; B; B ⊗ ⊥; (⊥ ⊗ I) ⅋ (B ⊗ ⊥); _{[\begin{matrix}⊥ & I \\ B & ⊥ \end{matrix}]}; (⊥ ⅋ B) ⊗ (I ⅋ ⊥)]

All the other proofs are minor variations on these two.

This can be summarized as follows: the equations of (7) and the first one in (9) say that there is a unique way of going B ⊗ ⊥ → B by using only Medial and Twist, (and obviously ⊥ ⊗ B → B too). By symmetry the equations in (8) the second one in (9) say that there is a unique way of going B → B ⅋ I, etc.

Let us replace B by ⊥ in (7) and call that map

m: ⊥ ⊗ ⊥ ⟶ ⊥

Obviously any way of plugging three instances of ⊥ and one of I in Medial will give m. Given the preceding proposition it is also quite obvious that m is commutative. By duality we also get a map m^{⊥}: I → I⅋I which is co-commutative and obtained by plugging three Is and one ⊥ in Medial.

We can also replace B by ⊥ in (8): let us call the result e

[figure: e = [\begin{matrix}𝕀 & ⊥ ⊥ \\ ⊥ ⊥ & 𝕀 \end{matrix}] = [\begin{matrix}⊥ ⊥ & 𝕀 \\ 𝕀 & ⊥ ⊥ \end{matrix}] : ⊥; I]

It is obviously self dual.

2.12. Proposition. The following

[figure: ⊥ ⊗ ⊥; e ⊗ ⊥; I ⊗ ⊥; ⊥]

is m.

Proof.

[figure: ((I ⊗ ⊥) ⅋ (⊥ ⊗ I)) ⊗ ⊥; [\begin{matrix}I & ⊥ \\ ⊥ & I \end{matrix}] ⊗ ⊥; S_{I⊗⊥,⊥⊗I,⊥}^{r}; (I ⅋ ⊥) ⊗ (⊥ ⅋ I) ⊗ ⊥; (I⅋⊥)⊗S_{⊥,I,⊥}^{r}; ⊥ ⊗ ⊥; (I ⊗ ⊥) ⅋ (⊥ ⊗ I ⊗ ⊥); _{[\begin{matrix}I & ⊥ \\ ⊥ & I ⊗ ⊥ \end{matrix}]}; (I ⅋ ⊥) ⊗ (⊥ ⅋ (I ⊗ ⊥)); ⊥; (I ⊗ ⊥) ⅋ (⊥ ⊗ ⊥); _{[\begin{matrix}I & ⊥ \\ ⊥ & ⊥ \end{matrix}]}; (I ⅋ ⊥) ⊗ (⊥ ⅋ ⊥)]

The left and right triangles commute because of the coherence theorem and Proposition 2.2; the upper middle square commutes because of interaction with Switch; the lower middle square commutes because of naturality.

2.13. Corollary. A ∗-autonomous category with a Medial map also has a self-dual Mix map.

Recall that we denote it by M_{A,B}: A ⊗ B ⟶ A ⅋ B.

2.14. Proposition. The following both give M_{A,B}

[figure: A ⊗ B; A ⊗ [\begin{matrix}⊥ ⊥ & 𝕀 \\ 𝕀 & B \end{matrix} ]; A ⊗ (I ⅋ B); S_{A,I,B}^{l}; (A ⊗ I) ⅋ B; A ⅋ B; A ⊗ B; [\begin{matrix}𝕀 & A \\ ⊥ ⊥ & 𝕀 \end{matrix}] ⊗ B; (A ⅋ I) ⊗ B; S_{A,I,B}^{r}; A ⅋ (I ⊗ B); A ⅋ B]

Proof. If we look at the de Morgan duals of these maps, we get the definition of Mix given in Propositions 2.5 and 2.6, and from the self-duality of e and Switch we get that this is also Mix.

Much to our surprise we have never seen the following result in the literature on Mix, although naturally it follows from the coherence theorem.

2.15. Proposition. The following always commutes:

[figure: A ⊗ B ⊗ C; M_{A,B} ⊗ C; M_{A,B⊗C}; (A ⅋ B) ⊗ C; S_{A,B,C}^{r}; A ⅋ (B ⊗ C)]

Proof.

[figure: A ⊗ B ⊗ C; A ⊗ (⊥ ⅋ B) ⊗ C; A ⊗ S_{⊥,B,C}^{r}; S_{A,⊥,B}^{l} ⊗ C; A ⊗ (⊥ ⅋ (B ⊗ C)); S_{A,⊥,B⊗C}^{l}; ((A ⊗ ⊥) ⅋ B) ⊗ C; S_{A⊗⊥.B,C}^{r}; ((A ⊗ e) ⅋ B) ⊗ C; (A ⊗ ⊥) ⅋ (B ⊗ C); (A ⊗ e) ⅋ (B ⊗ C); ((A ⊗ I) ⅋ B) ⊗ C; S_{A⊗I,B,C}^{r}; (A ⊗ I) ⅋ (B ⊗ C); (A ⅋ B) ⊗ C; S_{A,B,C}^{r}; A ⅋ (B ⊗ C)]

The triangle commutes because of Proposition 2.2. The square just below is just general coherence for Switch (“Switch always commutes with itself”), and the two bottom squares are just naturality.

2.16. Proposition. The following always holds:

[figure: A ⊗ B ⊗ C ⊗ D; A ⊗ T_{B,C} ⊗ D; M_{A⊗B,C⊗D}; A ⊗ C ⊗ B ⊗ D; M_{A,C} ⊗ M_{B,D}; (A ⊗ B) ⅋ (C ⊗ D); _{[\begin{matrix}A & B \\ C & D \end{matrix}]}; (A ⅋ C) ⊗ (B ⅋ D)]

Proof. If we manage to show

[figure: B ⊗ C; T_{B,C}; M_{A,B}; C ⊗ B; _{[\begin{matrix}⊥ ⊥ & 𝕀 \\ 𝕀 & C \end{matrix} ]} ⊗_{[\begin{matrix}𝕀 & B \\ ⊥ ⊥ & 𝕀 \end{matrix} ]}; B ⅋ C; _{[\begin{matrix}𝕀 & B \\ C & 𝕀 \end{matrix} ]}; (I ⅋ C) ⊗ (B ⅋ I)]  (10)

then the claim will follow because of

[figure: A ⊗ B ⊗ C ⊗ D; A ⊗ T_{B,C} ⊗ D; A ⊗ M_{A,B} ⊗ D; A ⊗ C ⊗ B ⊗ D; A ⊗ [\begin{matrix}⊥ ⊥ & 𝕀 \\ 𝕀 & C \end{matrix} ] ⊗ [\begin{matrix}𝕀 & B \\ ⊥ ⊥ & 𝕀 \end{matrix} ] ⊗ D; A ⊗ (B ⅋ C) ⊗ D; A ⊗ [\begin{matrix}𝕀 & B \\ C & 𝕀 \end{matrix} ] ⊗ D; S_{A,B,C}^{l} ⊗ D; A ⊗ (I ⅋ C) ⊗ (B ⅋ I) ⊗ D; S^{l} ⊗ (B ⅋ I) ⊗ D; ((A ⊗ B) ⅋ C) ⊗ D; [\begin{matrix}A & B \\ C & 𝕀 \end{matrix} ] ⊗ D; S_{A⊗B,C,D}^{r}; (A ⅋ C) ⊗ (B ⅋ I) ⊗ D; (A ⅋ C) ⊗ S_{B,I,D}^{r}; (A ⊗ B) ⅋ (C ⊗ D); _{[\begin{matrix}A & B \\ C & D \end{matrix}]}; (A ⅋ C) ⊗ (B ⅋ D)]

where we obtain the identity of the left vertical to M_{A⊗B,C⊗D} by using two applications of Proposition 2.12, and we also get the identity of the right vertical to M_{A,C} ⊗ M_{B,D} by using that result twice, but this time combined with Proposition 2.16. The two bottom squares commute because of interaction with Switch. We now can prove (10). It obviously follows if we get the following,

[figure: B ⊗ C; M_{B,C}; B ⊗ C; T_{B,C}; C ⊗ B; C ⊗ [\begin{matrix}𝕀 & B \\ ⊥ ⊥ & 𝕀 \end{matrix} ]; B ⊗ ((⊥ ⊗ I ⊗ I)⅋(I ⊗ C ⊗ I)); (B); S^{l}; C ⊗ (B⅋I); (⊥ ⊗ I ⊗ B)⅋(I ⊗ C ⊗ I); (C); _{[\begin{matrix}⊥ ⊗ I & B \\ I ⊗ C & I \end{matrix} ]}; _{[\begin{matrix}⊥ & I ⊗ B \\ I & C ⊗ I \end{matrix}]}; ((⊥ ⊗ I)⅋(I ⊗ C)) ⊗ (B⅋I); _{[\begin{matrix}⊥ & I \\ I & C \end{matrix} ]} ⊗_{[ \begin{matrix}B \\ I \end{matrix} ]}; B⅋C; (A); (⊥⅋I) ⊗ ((I ⊗ B)⅋(C ⊗ I)); _{[ \begin{matrix}⊥ \\ I \end{matrix} ]} ⊗_{[\begin{matrix}I & B \\ C & I \end{matrix} ]}; (⊥⅋I) ⊗ (I⅋C) ⊗ (B⅋I)]

where rectangle (C) commutes because of interaction of Medial with itself, and the proof of rectangle (A) is quite easy and will be left to the reader. For proving (B) look at:

[figure: B ⊗ C; ((⊥⊗I)⅋(I⊗B))⊗C; ((⊥⊗I)⅋(I⊗B))⊗C; [\begin{matrix}⊥ & I \\ I & B \end{matrix} ]⊗C; B⊗(⊥⅋I)⊗(I⅋I)⊗C; S^{l}; B⊗(⊥⅋I)⊗T_{1,1}⊗C; (⊥⅋I)⊗(I⅋B)⊗C; (⊥⅋I)⊗T_{1,B}⊗C; B⊗((⊥⊗I)⅋(I⊗I))⊗C; S^{r}; S^{l}; B⊗[\begin{matrix}⊥ & I \\ I & I \end{matrix}]⊗C; B⊗[\begin{matrix}⊥ & I \\ I & I \end{matrix}]⊗C; S^{l}; B⊗((⊥⊗I)⅋(C⊗I)); S^{l}; B⊗(⊥⅋I)⊗(I⅋I)⊗C; S^{l}; ((⊥⊗B)⅋(I⅋I))⊗C; S^{r}; [\begin{matrix}⊥ & B \\ I & I \end{matrix} ]⊗C; (⊥⅋I)⊗(B⅋I)⊗C; S^{r}; (⊥⊗B)⅋(C⊗I); _{[\begin{matrix}⊥ & B \\ C & I \end{matrix} ]}; (⊥⅋C)⊗(B⅋I)]

The first-down-then-right path is quite trivially equal to the equivalent path in (B), that is, modulo unit isos. The first-right-then-down path is also equal to its equivalent in (B), for only slightly less trivial reasons (one has to use naturality of Twist and Switch, along with Proposition 2.11(9), in addition to the unit isos). The crux of the proof that the above diagram commutes is the middle triangle, which (once again) commutes because of Proposition 2.11(9). The remaining quadrangles are mostly instance of interaction of Medial with Switch, along with Proposition 2.2 triangles in the upper left corner.

This completes the proof.

The previous proof should give food for thought to people who believe that a proof by diagram chasing is necessarily a trivial affair. We do not claim we have the simplest possible proof of the result we wanted, but there is something intrinsically nontrivial about the whole thing: we have to expand B ⊗ C into an object which is trivially isomorphic to it, but this object is the result of an absolutely nontrivial choice of a combination of units.

2.17. Nullary Medial. We now know how to get (n, m)-ary Medial whenever n, m > 0. But does it make sense when n = 0 or m = 0? It does not take long to realize that the (0, 2)-ary Medial should be a map ⊥ → ⊥ ⊗ ⊥ (that we will denote [ ∅ ∅ ]) and that the (2, 0)-ary Medial is a map

[ \begin{matrix}∅ \\ ∅ \end{matrix} ] : I ⅋ I → I ;

it is natural to ask that one be the dual to the other. Some of the original conditions in the definition of (2, 2)-ary Medial are easy to translate: good interaction between Medial and Twist is just requiring that the maps above be co-commutative and commutative, respectively; good interaction between Medial and itself is requiring that they be coassociative and associative.^{5} Thus

2.18. Definition. We say that ℂ is has nullary Medial if I is equipped with a commutative semigroup structure, or equivalently, if ⊥ is equipped with a co-commutative co-semigroup structure, which are notated as above.

It is also natural to have a condition that says that this new nullary version interacts well with the original 2-ary one, in the same way that the latter interacted well with itself. It does not take long to see that this translates (in bracket-nesting notation) as the requirement that

[[ \begin{matrix}A \\ B \end{matrix} ] [ \begin{matrix}∅ \\ ∅ \end{matrix} ]] ∘ [\begin{matrix}A & 𝕀 \\ B & 𝕀 \end{matrix}] = [ \begin{matrix}A \\ B \end{matrix} ] ,  (11)

the dual of this being

[\begin{matrix}A & B \\ ⊥ ⊥ & ⊥ ⊥ \end{matrix}] ∘ [\begin{matrix}[A & B] \\ [ ∅ & ∅] \end{matrix}] = [A B ]  (12)

(these equations need additional coherence isos involving units for them to type correctly). We will call this rule Absorbtion. In a more conventional notation, version (12) of Absorption is the requirement that

\xymatrix{ &  & (A ⊗ B) ⅋ [∅ ∅] \ar[dr] &  & ^{[\begin{matrix}A & B \\ ⊥ ⊥ & ⊥ ⊥ \end{matrix}]} \ar[dr] \\ A ⊗ B \ar@{^{(}->}[r] & (A ⊗ B) ⅋ ⊥ &  & (A ⊗ B) ⅋ (⊥ ⊗ ⊥) &  & A ⊗ B}  (13)

be the identity.

2.19. Proposition. Let ℂ be equipped with both a binary and nullary Medial. Then TFAE:

1. e is the co-unit of [∅ ∅].

2. m ∘ [∅ ∅] is the identity on ⊥.

5It does not seem that a rule that would correspond to Interaction with Switch can be formulated.

3. the following is the identity

[figure: I; I ⅋ ⊥; I ⅋ [∅ ∅]; I ⅋ (⊥ ⊗ ⊥); ^{[\begin{matrix}𝕀 & 𝕀 \\ ⊥ ⊥ & ⊥ ⊥ \end{matrix}]}; I]

4. e is the unit of [ \begin{matrix}∅ \\ ∅ \end{matrix} ].

5. [ \begin{matrix}∅ \\ ∅ \end{matrix} ] ∘ m^{⊥} is the identity on I.

6. the following is the identity

\xymatrix{ & ^{[\begin{matrix}𝕀 & ⊥ ⊥ \\ 𝕀 & ⊥ ⊥ \end{matrix}]} \ar[dr] &  & [ \begin{matrix}∅ \\ ∅ \end{matrix} ] ⊗ ⊥ \ar[dr] \\ ⊥ &  & (I ⅋ I) ⊗ ⊥ &  & I ⊗ ⊥ \ar@{^{(}->}[r] & ⊥}

7. The Absorption law holds.

Proof. The equivalences 1⇔4, 2⇔5 and 3⇔6 are obvious because of duality (and selfduality of e in the first case). Statements 1 and 2 are equivalent because of Proposition 2.12. The implication 7⇒3 is obtained by replacing both A, B by I in Equation (13). Let us assume 1, which also gives us 2, 4 and 5. Then 3 is obtained as follows

[figure: (I ⊗ I) ⅋ ⊥; (I ⊗ I) ⅋ [∅ ∅]; (I ⊗ I) ⅋ (⊥ ⊗ ⊥); ^{[\begin{matrix}I & I \\ ⊥ & ⊥ \end{matrix}]}; (I ⊗ I) ⅋ (e ⊗ ⊥); (I ⅋ ⊥) ⊗ (I ⅋ ⊥); (I ⅋ e) ⊗ (I ⅋ ⊥); I; (I ⊗ I) ⅋ (I ⊗ ⊥); _{[\begin{matrix}I & I \\ I & ⊥ \end{matrix}]}; (I ⅋ I) ⊗ (I ⅋ ⊥); [ \begin{matrix}∅ \\ ∅ \end{matrix} ] ⊗ (I ⅋ ⊥); I; I ⊗ (I ⅋ ⊥); I]

where the left quadrangle commutes because of 1, the bottom quadrangle because of 5, the right rectangle because of 4, and the middle rectangle because of naturality of Medial.

We are left to show 3⇒7, and this is obtained by chasing

[figure: A ⊗ B ⊗ ((I ⊗ I) ⅋ ⊥); A ⊗ B⊗((I ⊗ I) ⅋ [∅ ∅]); A ⊗ B; (A ⊗ B) ⅋ ⊥; (A ⊗ B) ⅋ [∅ ∅]; A ⊗ B⊗((I ⊗ I) ⅋ (⊥ ⊗ ⊥)); A ⊗ B ⊗ [\begin{matrix}I & I \\ ⊥ & ⊥ \end{matrix}]; S^{l}S^{l}; A ⊗ B ⊗ (I ⅋ ⊥) ⊗ (I ⅋ ⊥); S^{l}S^{l}; (A ⊗ B) ⅋ (⊥ ⊗ ⊥); _{[\begin{matrix}A & B \\ ⊥ & ⊥ \end{matrix}]}; (A ⅋ ⊥) ⊗ (B ⅋ ⊥); A ⊗ B]

The rectangle at the bottom is actually a combination of two Interaction with Switch squares; the top quadrangle is 3 and the remaining “triangle” and quadrangle are combinations of applications of Proposition 2.2.

2.20. Remark. The Absorption Law has important consequences when we start modelling classical logic. Not only does it entail that the Boolean (i.e., bimonoid) structure for units is entirely imposed by the linear axioms (what we mean by “linear” here includes (n, m)-ary Medial and Absorption, of course), but also that this bimonoid structure is quite trivial. From the point of view of logic, it means that proofs of t can have exactly one possible denotation. Attempts at weaker versions of this axiomatic system—for instance, decreeing that [∅ ∅] has a co-unit, but that it is not necessarily e—result in very messy computations and not much else.

In this section we have concentrated more on the algebra than on the logic. There are some open problems from the logical point of view, the main one being whether the formulation of Medial absolutely depends on deep inference. In a deductive system based on the concept of deep inference [Gug07], the functoriality of connectives and the naturality of rules like Switch or Medial is inherent and explicit, which allows one to apply these rules on arbitrary subformulas of a given formula. This is quite different from traditional approaches to deduction like the sequent calculus or natural deduction, where one can work only on an outer layer of connectives (“shallow inference”). It could be that deep inference cannot be dispensed with to formalize linear logic with Medial, as is the case for BV [Tiu06]. But we still cannot exclude the possibility of a sequent calculus formulation, perhaps with a rather complex system of structural connectives. Some very recent work [McK05b] leads us to put our bets on the second possibility.

Another standard open problem is that of coherence, in the usual category-theoretic sense of “coherence theorem”. The least ambitious possible version of a coherence result turns out to be false:

Given two formulas that contain no constants and that have the same proof graph (set of axiom links), are they equal in the theory of CLL + Medial, or CLL + Medial + Absorption?

There are several counterexamples to this in [Str07, 7.21]. The first of these is due to McKinley [McK05a], and a unitless version of it is [Str07, mix-m-t̂]. One reason why this problem is difficult is the complexity of the interaction of arbitrary objects with constants: for instance (e.g., Proposition 2.16) there are some equations that are true in these theories, where constants do not appear, but that very much seem to need the use of constants in their proofs. Thus we need more equations to get a good algebraic theory—a finite number of them or not?—and adding equations can perturb provability.

Unsurprisingly, formulating—let alone proving—a correctness criterion is a completely open problem.

3. Bimonoids

3.1. A series of definitions. In what follows, except when we say otherwise ℂ will always be a ∗-autonomous category with finitary (binary and nullary) Medial, and with the Absorption law.

A bimonoid is a quintuple X = (X, Δ, Π, ∇, ⨿)^{6} where

• X is an object of ℂ.

• (Δ, Π) is a co-commutative ⊗-comonoid structure on X.

• (∇, ⨿) is a commutative ⅋-monoid structure on X.

The reader who hasn’t seen the diagrams associated with monoids and comonoids yet should consult [FP05,FP04b,Str07].

We call Δ the diagonal, ∇ the codiagonal, Π the co-unit or the projection, ⨿ the unit or the coprojection.. Notice that we always assume commutativity and co-commutativity in our bimonoids, and from now on we will simply say bimonoid, without adding these qualifiers.

A bimonoid is said to be proper if the following law (the bimonoid equation) also holds:

[figure: X ⅋ X; Δ ⅋ Δ; ∇; (X ⊗ X) ⅋ (X ⊗ X); ^{[\begin{matrix}X & X \\ X & X \end{matrix} ]}; (X ⅋ X) ⊗ (X ⅋ X); ∇ ⊗ ∇; X; Δ; X ⊗ X .]  (14)

6For simplicity of notation we will sometimes identify the underlying object and the whole objectwith-a-bimonoid-structure. We use the indices (e.g., Δ_{X}) only where really necessary

3.2. Remark. Notice that the “bimonoid equation” does not hold for every object we call a bimonoid, only for the ones we call proper. This slight terminological inaccuracy has its roots in history: the bimonoid equation always holds when algebraists define a bimonoid, or bialgebra [Kas95]. They work in a context where the par and the tensor are identified, and thus the equation above can be simplified, with Medial becoming a trivial coherent iso. A way to keep in line with the algebraic tradition would be to use the slightly pedantic term sesquimonoid for what we call a bimonoid. We will see (Remark 3.14) that our richer setting leads to more subtleties with respect to the algebraists’ definition.

Given two bimonoids X, Y and two maps f, g: X → Y between the underlying objects, we define their superposition f + g: X → Y (often called convolution) as

[figure: X; Δ; X ⊗ X; f ⊗ g; M_{X,X}; Y ⊗ Y; M_{Y,Y}; X ⅋ X; f ⅋ g; Y ⅋ Y; ∇; Y]

Given a bimonoid (X, Δ, Π, ∇, ⨿) we define its negation \overline{X} as

\overline{X} = (X^{⊥}, ∇^{⊥}, ⨿^{⊥}, Δ^{⊥}, Π^{⊥}) .

Because of duality it is not hard to see that this is also a bimonoid, and that it is proper if X is.

We define the bimonoid f to have, for underlying object ⊥, its ⅋-monoid structure being the trivial one, where everything is a coherent isomorphism, and its ⊗-comonoid structure being ([∅ ∅] , e) (remember that nullary Medial says that [∅ ∅] is associative and Absorption that e is its counit). We define t as t = \overline{f}; thus its ⊗-comonoid structure is all-iso. It is easy to show, using the Absorption rule, that these two bimonoids are proper.

Given a bimonoid X we define its doubling map 𝒟_{X}: X → X as the superposition of the identity with itself, i.e., 𝒟_{X} = ∇_{X} ∘ M_{X,X} ∘ Δ_{X}.

Thus 𝒟_{I}, 𝒟_{⊥} are both the identity, once again because of the Absorption law.

Given bimonoids X, Y, a morphism of bimonoids is a map f: X → Y in ℂ between the underlying objects that respects both the monoid and comonoid structures, in the obvious sense.

We do not need a very fine taxonomy of the different possible kinds of maps that can exist between bimodules, as is presented in [Str07], where morphisms of bimonoids are called strong maps.

Given two bimonoids X, Y we define their conjunction X ∧ Y as having X ⊗ Y as underlying object, and where Δ_{X∧Y} and ∇_{X∧Y} are

[figure: X ⊗ Y; Δ ⊗ Δ; X ⊗ X ⊗ Y ⊗ Y; X ⊗ T ⊗ Y; X ⊗ Y ⊗ X ⊗ Y; (X ⊗ Y) ⅋ (X ⊗ Y); _{[\begin{matrix}X & Y \\ X & Y \end{matrix} ]}; (X ⅋ X) ⊗ (Y ⅋ Y); ∇ ⅋ ∇; X ⅋ Y]

respectively, and Π_{X∧Y} and ⨿_{X∧Y} are

[figure: X ⊗ Y; Π_{X} ⊗ Π_{Y}; I ⊗ I; I; ⊥; _{[_{∅ ∅}]}; ⊥ ⊗ ⊥; ⨿_{X} ⊗ ⨿_{Y}; X ⊗ Y .]

The disjunction X ∨ Y is defined as X ∨ Y = \overline{\overline{X} ∧ \overline{Y}}; the reader should work out the equivalent of the four definitions above.

3.3. Remark. As we have said in the introduction, the definition above is the raison d’être of Medial from the point of view of semantics.

3.4. Proposition. The conjunction of two bimonoids is a bimonoid. It follows by duality that their disjunction is a bimonoid too.

Before we begin the proof proper, let us mention a well-known fact [Fox76]^{7} that we will cannibalize for parts in what follows.

3.5. Proposition. Given a symmetric monoidal category ℂ, the category of cocommutative comonoids and morphisms of comonoids is a symmetric monoidal category itself, where the tensor product is defined just as above (i.e. by forgetting the monoids in the definition of X ∧ Y). Moreover in this category the tensor is actually the categorical product.

Conversely, if every object in a monoidal category is equipped with a natural cocommutative comonoid structure (i.e., every map in the category is a morphism of comonoids) then that monoidal structure is the ordinary categorical product and the comultiplication is the ordinary diagonal.

Proof. (of Proposition 3.4) We have to show that on X ∧ Y the defined (Δ_{X∧Y} , Π_{X∧Y}) is coassociative, cocommutative and obeys the counit law, and also that (∇_{X∧Y} , ⨿_{X∧Y}) is commutative, associative and obeys the unit law. The first result (comonoid structure) is a recycled component of Proposition 3.5. As for the monoid structure: the associativity of multiplication on X ∧ Y is obtained by chasing a 2 × 2 square, one corner of which is the dual of Equation 6, its opposite corner the associativity law for X tensored with the associativity law for Y, and the two remaining squares naturality of Medial. The proof of commutativity and unit are left to the reader.

7A more general and difficult version of this can be found in [Bur93].

3.6. Corollary. The category of bimonoids in ℂ and morphisms of bimonoids has products and coproducts.

Proof. Just apply Proposition 3.5 twice, dualizing.

3.7. What we are looking for. Given ℂ as above, our goal is to construct a new category 𝔼 from it which will be a model of classical logic. We can be imprecise for the time being on what that means exactly, and not choose immediately between the several proposals [FP05, FP04b, LS05a, Str07] for a categorical axiomatization of classical logic. But we know that

Requirement 1. We want 𝔼 to be ∗-autonomous.

Requirement 2. We want every object of 𝔼 to be equipped with a bimonoid structure, where every operation is a map in 𝔼.

Every one of the several proposals mentioned above obeys these requirements.

Problem. But how do we define the maps in 𝔼?

At least, because of Corollary 3.6 and “Joyal’s paradox”, we know that we can’t use morphisms of bimonoids for the maps of 𝔼. We want a ∗-autonomous category, but because of that result its tensor structure cannot be the categorical product. Every one of the several proposals above mentions this restriction.

So we have to relax the notion of map between bimonoids to something less strong than an all-structure preserving map in ℂ. The simplest (laziest?) approach would be to decree, given bimonoids X, Y, that a “classical” map X → Y is any map in ℂ. Then 𝔼 would obviously be equivalent to a full subcategory of ℂ, determined by its objects. that have a (possibly more than one) bimonoid structure.

For anybody who has a background in algebra, this is a surprising answer: if we add structure to some objects in a category, clearly we have to change the notion of map.

But if we overcome our ideological prejudices, there are other, serious technical obstacles that lie ahead. Suppose there is an object X of ℂ for which there are indeed two distinct bimonoid structures, say X_{1} = (X, Δ_{1}, Π_{1}, ∇_{1}, ⨿_{1}) and X_{2} = (X, Δ_{2}, Π_{2}, ∇_{2}, ⨿_{2}). Then any iso X → X (for instance, the identity) in ℂ becomes an iso X_{1} → X_{2} in 𝔼 because it has an inverse. But this contradicts the intuitive definition of an iso: if two objects are isomorphic they have to have the very same structure, and this is obviously not the case here. And this is more than hair-splitting for philosophy majors: if we are given an object X of 𝔼 we want to look at its (say) diagonal, since we need it for interpreting contraction, so it has to be intrinsic to the object. But here we have two objects of 𝔼 that cannot be distinguished by the available categorical structure in 𝔼, but nevertheless give two different answers to the question “what is your diagonal?”. Clearly we can’t claim success in our enterprise without addressing this question. We see four Options for dealing with this conundrum.

Option 1. Relinquish the autonomy of semantics. Given a language for propositional classical logic like LK or CL [LS05b], all we need to interpret it in ℂ is to choose a ℂ-bimonoid for every atomic type in the language. Then we will be able to interpret all formulas as ℂ-bimonoids and all objects as maps in ℂ. If we are careful it should be possible to avoid a syntactic proof construct from being interpreted by one of these unwanted isos. This would imply that the target category is not really a semantics by itself, since the semantics cannot have any existence without the language that one wants to interpret in it. We think such an approach should be called an interpretation instead of a semantics. Interpretations that are not semantics happen in real life, for example with the Geometry of Interaction [Gir89], where the base category—which actually is a monoid whose single hom-set is equipped with an additive structure and other things—that is used to interpret the proofs is much too degenerate to make distinctions at the level of the types. Thus the GOI does not really have an independent existence from the syntax of the logic.

Closer to our immediate concerns, the use of Frobenius algebras presented in [Hyl04] should more be thought of as an interpretation than as a semantics (and the title of the paper hints that its author shares our need to distinguish semantics and interpretation), although it is possible that a full working out of the category which is sketched therein conceivably could lead to a semantics in our sense.

The techniques that will be presented in Section 4 can be used to get interesting interpretations that are not semantics, but the present paper’s focus is on semantics.

Option 2. Introduce non-determinism. In other words, given an object X of ℂ we can retain all possible bimonoid structures on it as useable interpretations of contraction, which forces us to make an arbitrary choice every time a contraction is effected. Although non-determinism is an interesting avenue for classical logic, this particular approach would introduce an enormous, uncontrollable amount of it in the interpretation. The reason is that if accept several interpretations for binary contraction, then going up to 3-ary, 4-ary, n-ary contraction produces a combinatorial explosion in the possibilities. And remember that, given a single contraction, a consequence of its associativity and commutativity (better: its raison d’être) is to have a uniquely defined n-ary contraction whatever the value of n.

We think that following this approach is counterproductive.

The above discussion leads us to adding

Requirement 3. Maps in 𝔼 that are isos in ℂ should be isomorphisms of bimonoids.

In order to achieve this goal, some conceptual apparatus will be necessary.

3.8. Definition. Let ℂ be a monoidal category and X = (|X|, ∇, ⨿) a monoid in ℂ, and α: |X| → |Y | an iso. We define the transport of the monoid X along α to be the monoid

(|Y |, α ∘ ∇ ∘ (α^{−1} ⊗ α^{−1}), α ∘ ⨿) .

The reader should check that this is indeed a monoid. The transported monoid structure is the only possible one that makes α an isomorphism of monoids.

Since we will need it later, let us see what happens when ℂ is the category of sets. Thus if (X, ·, e) is an ordinary monoid, the transport of that structure along α: X → Y is

x ·^{α} y = α(α^{−1}(x) · α^{−1}y)
e^{α} = α(e)

Naturally the definition of transport applies to any mathematical structure, defined in any category. For the record, let us write down the definition of transport for comonoids: given a comonoid (|X|, Δ, Π) and α: |X| → |Y | as before, then the result of transporting along α is the comonoid

(|Y |, (α ⊗ α) ∘ Δ ∘ α^{−1}, Π ∘ α^{−1}) .

Those who look at [Joy81] can see that the concept of transport is the cornerstone of a general, abstract definition of mathematical structure.

A way to obtain this is to find classes of bimonoids that are intrinsic, in the following sense:

3.9. Definition. Let ℰ be a class of bimonoids in ℂ. We say ℰ is intrinsic if,

• given an object X in ℂ there is at most one bimonoid in ℰ with X as underlying object,

• given two objects X_{1}, X_{2} in ℂ, each one having a bimonoid structure in ℰ, and an iso α: X_{1} → X_{2}, then transporting the first structure along α always yields the second structure.

It should be clear that an intrinsic class of bimonoids obeys Requirement 3, when maps of ℂ are taken as maps of bimonoids.

3.10. Proposition. The second part of the definition above is equivalent to

• Given an object X in ℂ that has an ℰ -structure, then this bimonoid structure is stable under transport along all automorphisms of X.

Proof. Exercise.

So, if we accept Requirement 3, there are two Options left that we will explore in more details:

Option 3. Find a notion of map for 𝔼 which is weaker than the concept of morphism of bimonoids, and obeys all three Requirements.

Option 4. Find classes ℰ of monoids that are intrinsic in ℂ. Then the maps in the category obtained from ℰ will coincide with those of ℂ.

At first glance Option 4 seems to be rather difficult to achieve. We will first present an attempt at Option 3, which will show that Option 4 is the best approach we have right now.

But before we do this we need a few more technical results.

3.11. Proposition. Given bimonoids X, Y, Z then the associativity iso (X ⊗ Y) ⊗ Z → X ⊗ (Y ⊗ Z), twistmap X ⊗ Y → Y ⊗ X and unit X ⊗ I → X are actually morphisms of bimonoids (X ∧ Y) ∧ Z → X ∧ (Y ∧ Z), X ∧ Y → Y ∧ X and X ∧ t → X. This automatically dualizes to the case where ⊗ is replaced by ⅋ and ∧ by ∨.

Proof. A complete case analysis gives us twelve cases to check:

{counit, comult, unit, mult} × {assoc, twist, unit} .

Everything related to the comonoid structure is well-known, being ingredients for Proposition 3.5. So we are left with checking the remaining six cases of preservation of the monoid components by coherent isos.

That the associativity iso commutes with multiplication is proved by

[figure: ((X ⊗ Y) ⊗ Z) ⅋ ((X ⊗ Y) ⊗ Z); _{[\begin{matrix}X ⊗ Y & Z \\ X ⊗ Y & Z \end{matrix} ]}; (X ⊗ (Y ⊗ Z)) ⅋ (X ⊗ (Y ⊗ Z)); _{[\begin{matrix}X & Y ⊗ Z \\ X & Y ⊗ Z \end{matrix} ]}; ((X ⊗ Y) ⅋ (X ⊗ Y)) ⊗ (Z ⅋ Z); [\begin{matrix}X & Y \\ X & Y \end{matrix} ] ⊗ (Z ⅋ Z); (X ⅋ X) ⊗ ((Y ⊗ Z) ⅋ (Y ⊗ Z))); (X ⅋ X) ⊗ [\begin{matrix}Y & Z \\ Y & Z \end{matrix} ]; ((X ⅋ X) ⊗ (Y ⅋ Y)) ⊗ (Z ⅋ Z); (∇_{X} ⊗ ∇_{Y}) ⊗ ∇_{Z}; (X ⅋ X) ⊗ ((Y ⅋ Y) ⊗ (Z ⅋ Z)); ∇_{X} ⊗ (∇_{Y} ⊗ ∇_{Z}); (X ⊗ Y) ⊗ Z; X ⊗ (Y ⊗ Z)]

where the top square is Interaction of Medial with itself, but with the associativity isos made explicit (without naming them). The bottom square is just associativity. That the associativity iso commutes with the unit is due to the coassociativity of [∅ ∅]. That the twist iso commutes with multiplication is due to Interaction of Medial with Twist, and the commutativity of the monoids. That the twist iso commutes with the unit is just the cocommutativity of [∅ ∅].

That the unit isos commute with multiplication is proved as follows, where the Absorption law is needed:

[figure: (A ⊗ I) ⅋ (A ⊗ I); _{[\begin{matrix}A & I \\ A & I \end{matrix}]}; A ⅋ A; (A ⅋ A) ⊗ (I ⅋ I); (A ⅋ A) ⊗ [ \begin{matrix}∅ \\ ∅ \end{matrix} ]; ∇ ⊗ [ \begin{matrix}∅ \\ ∅ \end{matrix} ]; (A ⅋ A) ⊗ I; ∇ ⊗ I; A ⊗ I; A ⊗ I]

The bottom square/triangle being just bifunctoriality.

3.12. Proposition. If X, Y are proper bimonoids, then X ∧ Y is proper Proof. Look at

[figure: (X⊗Y)⅋(X⊗Y); ^{[ \begin{matrix}X & Y \\ X & Y \end{matrix} ]}; (Δ⊗Δ)⅋(Δ⊗Δ); (X⅋Y)⊗(Y ⅋Y); ∇_{X}⊗∇_{Y}; (Δ⅋Δ)⊗(Δ⅋Δ); X⊗Y; Δ⊗Δ; (X⊗X⊗Y ⊗Y)⅋(X⊗X⊗Y ⊗Y); _{[ \begin{matrix}X⊗X & Y ⊗Y \\ X⊗X & Y ⊗Y \end{matrix} ]}; (X⊗T⊗Y)⅋(X⊗T⊗Y); ((X⊗X)⅋(X⊗X))⊗((Y ⊗Y)⅋(Y ⊗Y)); _{[ \begin{matrix}X & X \\ X & X \end{matrix} ]} ⊗_{[ \begin{matrix}Y & Y \\ Y & Y \end{matrix} ]}; (X⊗Y ⊗X⊗Y)⅋(X⊗Y ⊗X⊗Y); _{[ \begin{matrix}X⊗Y & X⊗Y \\ X⊗Y & X⊗Y \end{matrix} ]}; (X⅋X)⊗(X⅋X)⊗(Y ⅋Y)⊗(Y ⅋Y); ∇⊗∇⊗∇⊗∇; (X⅋X)⊗T⊗(Y ⅋Y); X⊗X⊗X⊗X; X⊗T⊗Y; ((X⊗Y)⅋(X⊗Y))⊗((X⊗Y)⅋(X⊗Y)); _{[ \begin{matrix}X & Y \\ X & Y \end{matrix} ]} ⊗_{[ \begin{matrix}X & Y \\ X & Y \end{matrix} ]}; (X⅋X)⊗(Y ⅋Y)⊗(X⅋X)⊗(Y ⅋Y); ∇⊗∇⊗∇⊗∇; X⊗Y ⊗X⊗Y]

The top left square is naturality, the top right one is the equation that says X is proper, tensored with the one for Y, and the bottom right square is naturality of Twist. For the bottom left square, the trick is to write the two dotted diagonals, using Interaction of Medial with itself, in such a way that the naturality of Medial can be used to make the quadrangle with dotted arrows commute. This is also a consequence of the coherence theorem we give in the appendix.

3.13. Proposition. Given a bimonoid X then TFAE:

1. X is proper.

2. The diagonal X → X ∧ X commutes with the respective codiagonals of X, X ∧ X.

3. The codiagonal X ∨ X → X commutes with the respective diagonals of X ∨ X, X.

Just observe that the bimonoid equation is equivalent to 2. and 3. above. Also notice that the diagonal always commutes with itself.

3.14. Remark. We see that there is a slightly stronger possible definition of proper bimonoid, one where we require in addition that Π, ⨿ be morphisms of bimonoids. The reader can write down these additional equations, and verify that they are vacuous for classical algebraists (⊗ = ⅋), but not here. We will not say more, since they are not needed here, and they are all explicitly treated in [Str07].

We remind the reader that 𝒟_{X} is the doubling map (superposition of the identity with itself) associated to a bimonoid X.

3.15. Proposition. Given two arbitrary bimonoids X, Y, we have

𝒟_{X∧Y} = 𝒟_{X} ⊗ 𝒟_{Y} , 𝒟_{X∨Y} = 𝒟_{X} ⅋ 𝒟_{Y} and 𝒟_{X}^{⊥} = 𝒟_{X^{⊥}}

Proof.

[figure: X ⊗ Y; Δ_{X} ⊗ ΔY; X ⊗ X ⊗ Y ⊗ Y; X ⊗ T ⊗ Y; M_{X,X} ⊗ M_{Y,Y}; X ⊗ Y ⊗ X ⊗ Y; M_{X⊗Y,X⊗Y}; X ⊗ Y; (X ⅋ X) ⊗ (Y ⅋ Y); ∇_{X} ⅋ ∇_{Y}; (X ⊗ Y) ⅋ (X ⊗ Y); _{[\begin{matrix}X & Y \\ X & Y \end{matrix} ]}]

The long path is the definition of 𝒟_{X∧Y}, the short path is just 𝒟_{X} ⊗ 𝒟_{Y} and the square commutes because of Proposition 2.16 (the twistmap is an iso). The second result is obtained by dualizing this diagram, and the third is trivial.

3.16. An attempt at a definition of map of bimonoids. We can now propose our definition for a map of bimonoids which is weaker than that of a full morphism:

3.17. Definition. Given bimonoids X, Y a balanced map is a f: X → Y in ℂ that commutes with 𝒟, i.e, such that f ∘ 𝒟_{X} = 𝒟_{Y} ∘ f

3.18. Proposition. Morphisms of bimonoids are balanced maps.

Proof. Let f: X → Y be a morphism of bimonoids. Just look at

[figure: X; Δ; f; X ⊗ X; M_{X,X}; f ⊗ f; X ⅋ X; ∇; f ⅋ f; X; f; Y; Δ; Y ⊗ Y; M_{Y,Y}; Y ⅋ Y; ∇; Y]

The two outer squares commutes because f is a morphism of bimonoids, the inner square is naturality, and the composite rectangle shows f is balanced.

3.19. Definition. A bimonoid X = (X, Δ, Π, ∇, ⨿) is said to be germane if it is proper and Π, ⨿ are balanced.

3.20. Corollary. Germane bimonoids are closed under conjunction and disjunction.

Proof. All that’s left to show is that, given germane X, Y the unit and co-unit of X ∧ Y are balanced too and that amounts to two trivial diagram chases.

Notice also that the bimonoids t, f are trivially germane.

3.21. Theorem. The category of germane bimonoids and balanced maps is ∗-autonomous.

Proof. We have to verify that the operations ∧, ∨, (\overline{−}) are functorial. For ∧, ∨ this is an immediate consequence of Proposition 3.15; the contravariant functoriality of (\overline{−}) is rather trivial. The bimonoid t is the unit to ∧ and this is because the iso X ⊗ I ≅ X is a balanced map X ∧ t ≅ X, which is also due to Proposition 3.15 (along with the remark that 𝒟_{I} is the identity, a consequence of Absorption); we immediately also get that f is the unit to ∨. The associativity, twistmap and unit isos are balanced because they are morphisms of bimonoids.

All that’s left to show is that, given a balanced map X ∧ Y → Z the transpose X → \overline{Y} ∨ Z is balanced too (and vice-versa). This is an immediate consequence of Proposition 3.15, and the following pair of diagrams:

[figure: X ⊗ Y; 𝒟_{X} ⊗ 𝒟_{Y}; Z; 𝒟_{Z}; X ⊗ Y; Z; X; 𝒟_{X}; Y^{⊥} ⅋ Z; 𝒟_{Y}^{⊥} ⅋ 𝒟_{Z}; X; Y^{⊥} ⅋ Z]

since one square is the “transpose” of the other (in an obvious sense), one commutes iff the other does.^{8}

Thus we have constructed a category 𝔼 that satisfies Requirements 1 and 2, and where the morphisms are potentially different from those of ℂ. We still have to see if this simplifies life with respect to Requirement 3, though.

The reader might wonder why we have not chosen to define a germane bimonoid as one where all the operations (i.e. diagonal and codiagonal as well as unit and counit) are asked to be balanced, since balanced maps are what really matters for the category. The reason is that stability under (−) ∧ (−) of this weaker condition seems impossible to prove, while it is quite simple (Proposition 3.12) when the bimonoid equation holds.

One interesting observation is the following:

8Note for beginners: showing the equivalence of these two squares is an essential exercise, and should be proved in the context of any Symmetric Monoidal Closed Category

3.22. Proposition. Let 𝔼 be a ∗-autonomous category of bimonoids in ℂ where all the maps are balanced. Then for every object X in 𝔼 the doubling map is an involution, i.e., 𝒟_{X} ∘ 𝒟_{X} is the identity on X. In particular, 𝒟_{X} is an isomorphism.

Proof. In the first diagram below the map ˆ1 is the transpose of the identity X → X (the name of the identity) and it commutes because 𝒟_{I} is the identity and because of Proposition 3.15 and the fact that 𝒟_{X^{⊥}} = (𝒟_{X})^{⊥}.

[figure: I; ˆ1; 1_{I}; X^{⊥} ⅋ X; 𝒟_{X}^{⊥} ⅋ 𝒟_{X}; I; ˆ1; X^{⊥} ⅋ X; X; 1_{X}; X; 𝒟_{X}; X; 𝒟_{X}; 1_{X}; X]

The second diagram is the “transpose” of the first (also in an obvious sense) and proves our claim.

3.23. Definition. A bimonoid X is said to be weakly idempotent if 𝒟_{X} is the identity. It is said to be idempotent if f +f = f for any f: X → X. A class/category of bimonoids is (weakly) idempotent if every one of its bimonoids is (weakly) idempotent.

Notice that the distinction between idempotent and weakly idempotent is purely semantical, because one can show by induction that in a weakly idempotent model we will have f + f for the denotation of any proof f.

We immediately get

3.24. Proposition. Let ℬ be a subclass of bimonoids in ℂ that are all germane and weakly idempotent. Then every map in ℂ between objects of ℬ is balanced.

3.25. Remark. If we look at the “canonical” idempotent model presented in [LS05b, LS05a] we see that in general idempotent models cannot count how often an axiom (seen as an axiom link, i.e., a pair of occurrences of an atom and a negated atom in a formula/sequent) is used, only whether it is used or not. Thus we think that the construction of interesting non-idempotent semantics is an important goal. In [Str07] it is shown that the bimonoid equation is dangerous, in the sense that it can easily interact with other equations (in particular contractibility [LS05a, 2.4.3] and [Str07, 8.5]) to force idempotency. On the other hand, the bimonoid equation is useful from the syntactic point of view, because it gives a natural resolution to the contraction-against-contraction case in the cut-elimination procedure. One way to avoid idempotency is simply not to resolve a cut when a contraction is applied against a contraction, as is done in [Str05]. This is not as crazy as it seems, because we have the technology of deep inference, along with Medial, and the only contractions that have to be dealt with are on atomics. But it is still a rather radical approach, that seems to be burdened by bureaucracy. In subsequent work we will show how denotational semantics can suggest new ways of getting a good theory of cut-elimination.

When 𝒟 is an involution, it is very close to being the identity, as will be the case for the germane bimonoids we will construct, which will turn out to be idempotent. Thus, we have to conclude that we have not advanced much in trying to obey Requirement 3. We still have to use something like Option 4 to construct a viable category, with or without germane bimonoids.

4. The Models

4.1. Coherences. The model we present is based on the general techniques presented in [Lam95] (for a completely different point of view, see [dPA04]).

All models based on general notions of “coherence”, like the original coherence spaces [GLT89] and hypercoherences [Ehr93], are built by adding structure to the objects of the category Rel of sets and relations, which is itself a ∗-autonomous category, but (as we said in the introduction) a very degenerate one, where the two multiplicatives coincide, the two additives coincide too, and the (−)^{⊥} involution is identity.

It is well known [Lam94, NW04] that Rel can be embedded in a larger category Cmp that we will call, following Lambek [Lam94], the category of posets and comparisons. An object of Cmp is just a poset (M, ⊑) and a comparison f: M → N is a “relation” f ⊆ M ×N which is down-closed in the source and up-closed in the target (we will always write m f n for (m, n) ∈ f), i.e.,

m f n , m′ ⊑ m  implies m′ f n
m f n , n ⊑ n′  implies m f n′ .

Composition of maps is ordinary relational composition: given f: M → N, g: N → P

m gf p iff (∃_{n∈N}) m f n, n g p .

The reader who is new to this should check that this does indeed give a category, and that it is ∗-autonomous. It is slightly less degenerate than Rel, since M^{⊥} = M^{op} (the poset with the reverse order), but the tensor/par and with/plus pairs are still identified, the former still being the Cartesian product and the latter the disjoint sum.

When posets are replaced by more general categories, the maps we have just defined are very well-known, and either called profunctors [Wra75], or distributors [Bén73], or bimodules. The latter terminology comes from a very general construction [Law73] that goes way beyond categories or posets.

It should be obvious that maps {∗} → N in Cmp are in bijective correspondence with up-closed subsets of N.

Thus the set Hom_{Cmp}({∗}, N) is naturally ordered by subset inclusion. It is also easy to see that given f: N → M in Cmp then the induced

Hom_{Cmp}({∗}, N) → Hom_{Cmp}({∗}, M)

is a monotone function for the inclusion order.

There is a standard (anti-)monotone function N^{op} → Hom({∗}, N), (the Yoneda embedding for posets), given by n ↦ n↑, where n↑ = { m | n ⊑ m }.

4.2. Proposition. [Yoneda’s Lemma, Lite Version] This map is a (contravariant) embedding, i.e. n ⊑ m iff m↑ ⊆ n↑.

Moreover, the elements in the image of the Yoneda embedding have an important poset-theoretic characteristic: sets of the form n↑ are exactly the {∗} → N that are the complete primes,^{9} where an up-closed U ⊆ N is completely prime [NPW81] when, given a family (V_{i})_{i∈I} of up-closed subsets, such that U ⊆ ⋃_{i} V_{i} there is at least one i ∈ I with U ⊆ V_{i}. This is important because it allows the recovery of the poset N^{op} inside the much bigger Hom_{Cmp}({∗}, N), through purely poset-theoretic considerations.

A property of Cmp which can be surprising for newcomers is that given a poset M, the identity function M → M is not the identity graph as in Rel, but the relation { (m, n) | m ⊑ n } instead.

Given an arbitrary R ⊆ M × N it can be turned into a map in Cmp via the following closure operator:

R↕ = { (m, n) ∈ M × N | (∃_{m′,n′}) m ⊑ m′, m′ R n′, n′ ⊑ n }

This operator does not respect the composition of relations, as can easily be seen. This property is at least true if one of the maps is an iso, as is shown in the following two useful propositions:

4.3. Proposition. Let M, N be two posets, and α ⊆ M × N a relation which is an isomorphism of posets N → M. Then α↕ is an iso M → N in Cmp. Conversely, given an iso f: M → N in Cmp, there is a uniquely defined bijective relation α such that f = α↕.

Proof. So assume α is bijective. Notice that

m α↕ n iff α(m) ⊑ n  (15)
iff m ⊑ α^{−1}(n)  (16)

(we’ll leave this as an exercise). Let h = (α^{−1}↕) ∘ (α↕) in Cmp. We have

m h m′ iff (∃_{n∈N}) m α↕ n, n ^{α^{−1}↕} m′
iff (∃_{n∈N}) α(m) ⊑ n, n ⊑ α(m′)  (17)

The first inequality in (17) is just (15), while the second one is (16) with α replaced by α^{−1}. If we apply the isomorphism of posets α^{−1} to both inequalities, we get

m h m′ iff (∃_{n∈N}) m ⊑ α^{−1}(n), α^{−1}(n) ⊑ m′

9the more correct term “complete coprime” is also used, as well as just “prime” and “coprime”, when the context is clear enough.

And this is obviously equivalent to m h m′ iff m ⊑ m′—α being bijective—which shows h is the identity in Cmp.

For the converse, let f: M → N be a map which is an iso in Cmp, and thus has an inverse. Functors preserves isos, so in particular the functor Hom_{Cmp}({∗}, −) induces a bijection between the sets Hom_{Cmp}({∗}, M) → Hom_{Cmp}({∗}, N). In addition we know that both this map and its inverse are monotone for the inclusion order, and thus that this bijection is actually an isomorphism of posets. But the images of N, M via Yoneda in these big posets are characterized by the purely poset-theoretic property of being the complete primes, and thus the isomorphism of big posets restricts to an ordinary isomorphism of posets α: N ≅ M between the much smaller Yoneda images. It is trivial to check that α↕ is indeed f.

4.4. Proposition. Let α: M → N be an isomorphism of posets, seen as a graph α ⊆ M × N, and let g: N → N′, f: M′ → M be maps in Cmp. Then

g ∘ α = g ∘ α↕  (18)
α ∘ f = α↕ ∘ f  (19)

(in order for this to type correctly, the compositions have to be effected in Rel, naturally).

Proof. It should be obvious that g ∘α ⊆ g ∘α↕, so let m g ∘ α↕ n. By definition we know that there is p ∈ N with m α↕ p and p g n; because of (15) we know that α(m) ⊑ p and because g is left-down-closed by definition we have α(m) g n and this shows m g ∘ α n, so g ∘ α ⊇ g ∘ α↕ and we get (18). The proof of (19) is the same.

Let Q be a ∗-autonomous poset. In other words, Q = (Q, ≤, ⊗, I, ⅋, ⊥) is a poset which, seen as a category, is a ∗-autonomous category. A ∗-autonomous poset has Medial if (m ⊗ n) ⅋ (p ⊗ q) ≤ (m ⅋ p) ⊗ (n ⅋ q) always.

We will develop the theory for a general ∗-autonomous poset Q, even if Q will turn out to be a very special case in this paper. The reason for this is that the proofs are conceptually simpler and more perspicuous in the general, more algebraic setting, and can be reused in subsequent work.

4.5. Definition. A Q-coherence A is a pair A = (|A|, ρ_{A}) where |A| is a poset—i.e., (|A|, ⊑), and ρ_{A}: |A| × |A| → Q a monotone function which is symmetric: ρ_{A}(a, b) = ρ_{A}(b, a). Given Q-coherences A, B a map A → B is an f: |A| → |B| in Cmp such that ∀a, a′ ∈ |A|, b, b′ ∈ |B|

a f b, a′ f b′ implies ρ_{A}(a, a′) ≤ ρ_{B}(b, b′)

Thus, unlike [Lam95] we do not require Q to be a quantale (i.e., to be complete) since we do not need to construct exponentials here.

It should be obvious that this defines a category Q-Coh. Given two Q-coherences, we define A ⊗ B, A ⅋ B by |A ⊗ B| = |A ⅋ B| = |A| × |B| with

ρ_{A⊗B}((a, b), (a′, b′)) = ρ_{A}(a, b) ⊗ ρ_{B}(a′, b′) and
ρ_{A⅋B}((a, b), (a′, b′)) = ρ_{A}(a, b) ⅋ ρ_{B}(a′, b′) .

We take |I| = |⊥| = {∗}, but ρ_{I}(∗, ∗) = I_{Q} and ρ_{⊥}(∗, ∗) = ⊥_{Q}. The orthogonal A^{⊥} has |A^{⊥}| = |A|^{op} and ρ_{A^{⊥}}(a, b) = ρ_{A}(a, b)^{⊥}. It is easy to check the bifunctoriality of (−) ⊗ (−) and (−) ⅋ (−), and the contravariant functoriality of (−)^{⊥} as we have defined them.

Notice also that a map I → A can be identified with a kind of clique: a I → A is a ⊑-up-closed subset U ⊆ |A| such that (∀_{a,b∈U})ρ_{A}(a, b) ≥ I. In the same way, maps A → ⊥ (equivalently I → A^{⊥} can be thought of as ⊑-down-closed anticliques: subsets U ⊆ |A| with (∀_{a,b∈U})ρ(a, b) ≤ ⊥.

There is an obvious forgetful functor Q-Coh → Cmp.

The first half of what follows is a minor variation on [Lam95].

4.6. Theorem. The category Q-Coh is ∗-autonomous. If Q has Medial, then Q-Coh is a category with Medial as we defined previously. The proof of the first statement is an absolutely straightforward generalization of the one in [Lam95]. Basically the main observation is that both the set of maps A ⊗ B → C and the set of maps A → B^{⊥} ⅋ C are in bijective correspondence with up-closed subsets of A^{op} ×B^{op} ×C that are cliques in the sense above. As for the second statement, let us first say a map f: A → B in Q-Coh is an entropy if f is an iso in Cmp. We will show there are a lot of entropies, and natural transformations all whose components are entropies.

In the two results that follow 𝒯 is the first-order theory of of ∗-autonomous posets with Medial. In more details it has two binary function symbols ⊗, ⅋, two constants I, ⊥, one unary function symbol (−)^{⊥} and one binary predicate ≤, along with the obvious axioms that make every model of 𝒯 a ∗-autonomous poset with Medial.

4.7. Proposition. Let w(x_{1}, x_{2}, …, x_{n}) be a term in 𝒯 which is linear (the x_{i} each appear only once in w) and which uses only the symbols ⊗, ⅋.^{10} Given Q a chosen model of 𝒯 and X_{1}, X_{2}, …, X_{n} a family of Q-coherences, then there is an obvious Qcoherence w^{♯}(X_{1}, …, X_{n}) obtained by plugging the X_{i} in the x_{i}, whose underlying poset is |w^{♯}(X_{1}, …, X_{n})| = |X_{1}| × ⋯ × |X_{n}|. Then we have

ρ_{w^{♯}(X_{1},...,X_{n})}((a_{1}, …, a_{n}), (b_{1}, …, b_{n})) = w^{∗}((ρ_{X_{1}}(a_{1}, b_{1}), …, ρ_{X_{n}}(a_{n}, b_{n})) .

where w^{∗}: Q^{n} → Q is the standard first-order interpretation of w.

Proof. The proof is a completely straightforward induction.

It is easy to show, using Proposition 4.4, that the operation

(X_{1}, …, X_{n}) ↦ w^{♯}(X_{1}, …, X_{n})

defines a functor w^{♯}: Q-Coh^{n} → Q-Coh, covariant in all variables.

4.8. Proposition. Let w(x_{1}, …, x_{n}), v(x_{1}, …, x_{n}) be two linear terms built using only ⊗, ⅋ and that share the same variables, and such that w ≤ v is a theorem in 𝒯 . Let Q be chosen. Then the identity relation in Cmp is a natural transformation w^{♯} → v^{♯} between the covariant functors w^{♯}, v^{♯}: Q-Coh^{n} → Q-Coh.

Proof. This is also completely straightforward, via Proposition 4.3.

10This restriction is only there to simplify our life.

Out of this we get that Q-Coh has Medial and this completes the proof of the Theorem.

Naturally the result above can be generalized in several directions. The fact that 𝒯 is the theory of ∗-autonomous posets with Medial is absolutely inessential, as is the fact that the natural transformations obtained from “linear” inequalities (as w ≤ v above) that are theorems in 𝒯 need to involve term/functors that are covariant in all variables.

We now fix Q to be the two-element Boolean algebra 𝔹 = {0, 1}: obviously any Boolean algebra is a poset with Medial. So, given a 𝔹-coherence A, if we define a ⌣ ⌢ b iff ρ_{A}(a, b) = 1, we get that a map A → B in 𝔹-Coh is a f: |A| → |B| in Cmp that obeys

a ⌣ ⌢ a′, a f b, a′ f b′ implies b ⌣ ⌢ b′ .

Thus 𝔹-coherences look very much like ordinary coherence spaces [GLT89], except for one single, very important detail: we permit an element of |A| not to be coherent with itself, which allows us to distinguish between the two multiplicative units.

This one “little” difference makes some things actually quite different. In particular, standard notation like a ⌢ b becomes next to meaningless here. But we can safely use a ⌢ ⌣ b, which is prettier than a ⌣̸ ⌢ b (both obviously meaning ρ_{A}(a, b) = 0).

Maps I → A in 𝔹-Coh are now “real” cliques: they are ⊑-up-closed subsets U ⊆ |A| such that a ⌣ ⌢ a′ for every a, a′ ∈ U. And maps A → ⊥ are ⊑-down-closed anticliques, with a ⌢ ⌣ a′ for every pair of elements in the subset that represents the map.

4.9. Remark. But notice that any down-closed subset of |A| defines a map A → I, and any up-closed subset of A defines a map ⊥ → A.

It should be obvious that given 𝔹-coherences A, B and (a, b), (a′, b′) ∈ |A| × |B| we have

(a, b) ⌣ ⌢ (a′, b′) iff  a ⌣ ⌢ a′ and b ⌣ ⌢ b′  in A ⊗ B  (20)
(a, b) ⌣ ⌢ (a′, b′) iff  a ⌣ ⌢ a′ or b ⌣ ⌢ b′  in A ⅋ B  (21)

and that the (−)^{⊥} operator simply exchanges ⌣ ⌢ and ⌢ ⌣.

4.10. Definition. A 𝔹-coherence (A, ρ) is said to be discrete if ρ(a, b) = 0 always holds, ie., we always have a ⌢ ⌣ b. It is said to be codiscrete if ρ(a, b) = 1 always (i.e., a ⌣ ⌢ b).

The interested reader can check that there is a “discrete” functor which is the left adjoint to the forgetful 𝔹-Coh → Cmp and a “codiscrete” one which is the right adjoint.

4.11. Remark. Here is an open problem: are there other, non-degenerate ∗-autonomous posets with Medial than just Boolean algebras? By non-degenerate, we mean where the tensor is different from the par: a ∗-autonomous poset where they coincide will always have Medial, trivially. A standard way to construct ∗-autonomous posets is the following: given an ordered Abelian group (G, +, 0, ≤), taking the tensor to be +, we can decree that any element d ∈ G is the dualizing element, defining g^{⊥} = d − g. The reader can check that this will always give us a ∗-autonomous poset. The problem for us is that the only value of d that will give us Medial is d = 0. Also, Medial will always hold if the tensor is the inf and the par is the sup; but if assume this, given that we need our posets to be ∗-autonomous, only Boolean algebras are left.

One important aspect of categories like Q-Coh, is that the notion of clique—and thus map—is “downward closed” for the inclusion order: if U is an up-closed clique in an arbitrary A (which can be of the form B^{⊥} ⅋ C, thus defining a map), and V ⊆ U is another ⊑-up-closed set, then V also immediately represents a map I → A. In particular the empty set is always a clique, and there is always guaranteed to be a zero map B → C. It is hard to get rid of the zero map in semantics like the one we present; the only exception we know is presented in [Loa94], and the technique used there obviously cannot be used here.

4.12. Bimonoids. We haven’t done the real work yet. The challenge is to find good classes of bimonoids in Q-Coh, and then ensure that these classes are intrinsic. First we observe

4.13. Proposition. Let (M, ⊑, ·, e) be a poset which is equipped with a commutative monoid structure ( ·, e) such that the binary · is ⊑-monotone.^{11} Then if we define ∇: M × M → M and ⨿: {∗} → M in the category Cmp as

(m, n) ∇ p iff m · n ⊑ p , ∗ ⨿ m iff e ⊑ m

we get a (commutative) monoid in the symmetric monoidal category (Cmp, ×, {∗}). Similarly if we define Δ: M → M × M and Π: M → {∗} as

m Δ (n, p) iff m ⊑ n · p , m Π ∗ iff m ⊑ e

we get a (cocommutative) comonoid in the same category.

Proof. The commutativity and cocommutativity are trivial to check. The associativity and coassociativity are almost as trivial—but notice that monotonicity of · is essential— the two ways of chasing the associativity square giving us the same map a: M ×M ×M → M, which is described by

(m, n, p) a q iff m · n · p ⊑ q ,

and the two ways of chasing coassociativity yield the map c: M → M × M × M given by

m c (n, p, q) iff m ⊑ n · p · q .

As for the unit, looking at the diagram

[figure: M; 1_{M} × ⨿; M × M; ∇; M]

11some people would feel the need to add “in both variables” but this is not necessary.

The first map f: M → M × M is given by

m f (n, p) iff m ⊑ n, e ⊑ p

and if we post-compose this with ∇ we get a map g defined by

m g q iff (∃_{n,p}) m ⊑ n, e ⊑ p, n · p ⊑ q

and this is obviously equivalent to m g q iff m ⊑ q (because m ⊑ n, e ⊑ p implies m · e ⊑ n · p by monotonicity of (−) · (−)), which is the identity. The same goes for the proof of the counit law.

4.14. Proposition. Let (M, ⊑, ·, e) be as above, and let (M, ∇, Π) and (M, Δ, ⨿) be the monoid and comonoid structures in Cmp obtained by applying the above result. let α: M → N be an isomorphism of posets; we know (Proposition 4.3) that α↕ is an iso in Cmp. Then the bimonoid in Cmp obtained by transporting (M, ∇, Π) and (M, Δ, ⨿) along α↕ coincides with the bimonoid obtained by applying Proposition 4.13 to the monoid (N, ⊑, ·^{α}, e^{α}), obtained by transporting (M, ⊑, ·, e) along α.

Proof. If we make use of Proposition 4.3 the proof is just an easy calculation.

If we want to lift this construction to 𝔹-Coh we need to find 𝔹-coherence structures on our monoids such that the operations we defined in Cmp will still be valid in 𝔹-Coh. There is an easy, surefire trick: given a monoid M, put either the discrete or the codiscrete structure on it. The monoid structure in Cmp will (trivially) lift correctly to 𝔹-Coh. This certainly does not make full use of the power of 𝔹-coherences, but at least it is rather natural from an intuitive point of view: in the first case we think that the object approximates a provable formula, while in the second case it approximates an object whose negation is provable—a discrete object will actually have one proof, namely the empty clique, which is unavoidable as we have said, and which intuitively has no contents whatsoever. We will see other, more subtle 𝔹-coherence structures that can be given to some particular intrinsic classes, but we know we can always depend on these two “simplistic” ones (the presence of negation in the logic forces us to have both as soon as we have one of them).

But now we have to find intrinsic classes of bimonoids. There is a good, useful criterion that ensures that a bimonoid or comonoid in 𝔹-Coh constructed by the means above is intrinsic: if the ordinary monoid operations (·, e) can be deduced entirely from the poset structure, then we are guaranteed to have an intrinsic class. Thus, we can use binary sup or inf for the monoid structure, which are as intrinsic as operations can be: it is well-known that they are properties of a poset instead of extra structure, and these binary operations are uniquely defined if the poset has that desired property. And they are well-known to be associative and commutative. In what follows, given a poset (M, ⊑), the sup is written ⊔ (if it is defined), the inf written ⊓, the top (unit to ⊓) is t and the bottom (unit to ⊔) is b.

Immediately there are two different categories that impose themselves on our attention:

• We can decide that the inf describes Δ, in other words m Δ (n, p) iff m ⊑ n ⊓ p. So a poset M that belongs to the model is an inf-semilattice, with a top element. Since we want M^{op} also to be in there to model negation, we get that M is also a sup-semilattice, and this forces ∇ to be modelled by that operation: (m, n) ∇ p iff m⊔n ⊑ p. Let us call this the diagonal-is-inf model. Naturally Π is determined by the top element of that poset, and ⨿ by the bottom.

• We can decide that the sup describes Δ, in other words m Δ (n, p) iff m ⊑ n⊔p. So a poset M that belongs to the model is a sup-semilattice, with a bottom element. Since we want M^{op} also to be in there to model negation, we get that M is also an inf-semilattice, and this forces ∇ to be modelled by that operation: (m, n) ∇ p iff m⊓n ⊑ p. Let us call this the diagonal-is-sup model. Naturally Π is determined by the bottom element of that poset, and ⨿ by the top.

Notice that a diagonal-is-inf or a diagonal-is-sup structure on a 𝔹-coherence M are obtained purely from the poset structure of the underlying object M; the map ρ_{M} itself has nothing to do in the definition of the bimonoid operations; it is only required to be compatible with them.

Let us now do some computations, starting with the diagonal-is-inf model. First we can rewrite the diagonal-is-inf operations, using the universal property of sup and inf:

m Δ (n, p) iff m ⊑ n and m ⊑ p  (22)
m Π ∗ always  (23)
(m, n) ∇ p iff m ⊑ p and n ⊑ p  (24)
∗ ⨿ m always.  (25)

But notice that the monoid operations and constants ⊔, ⊓, t, b have actually disappeared from these definitions; this strongly suggests that the lattice structure on the poset is not necessary for the diagonal-is-inf model. The reader can check that this is indeed the case: for any poset, not necessarily a lattice, these definitions will give us bimonoid structures in Cmp.

We claim that the bimonoid equation (14) holds in the diagonal-is-inf model. First, given a lattice M, if we define f = ∇ ∘ Δ we see that

(m, m′) f (n, n′) iff (∃_{p}) m, m′ ⊑ p, p ⊑ n, n′
iff m, m′ ⊑ n, n′ ,

the second line being due to the fact that we have binary sups and infs. If g is the other half of the bimonoid equation, i.e.,

g = (∇ ⊗ ∇) ∘ [\begin{matrix}M & M \\ M & M \end{matrix} ] ∘ (Δ ⅋ Δ) ,

we see that

(m, m′) g (n, n′) iff (∃_{p,p′,q,q′}) m ⊑ p, p′, m′ ⊑ q, q′ and p, q ⊑ n, p′, q′ ⊑ n′ ,

where we make use here of Proposition 4.4 and the fact that the Medial map is an entropy (cf. Theorem 4.6). It is then easy to see that the above is equivalent to (m, m′) f (n, n′).

Another interesting property of this model is the following.

4.15. Proposition. Let M, N be diagonal-is-inf bimonoids in 𝔹-Coh, and f, f′: M → N be two maps in there. Then f + f′ = f ∩ f′, i.e., the intersection of their graphs.

Proof. By definition we have

m f + f′ n iff (∃_{p,p′,q,q′}) m ⊑ p, p′ and p f q and p′ f′ p′ and p, p′ ⊑ n

and given that both f, f′ are down-closed to the left and up-closed to the right, this immediately translates to

m f + f′ n iff m f n and m′ f′ n′

and this completes the proof.

A consequence of this is that the inclusion order on maps/cliques is definable through the basic abstract categorical structure we want the model to have: f ⊆ f′ iff f + f′ = f′. The axiomatic properties that are needed to allow this are explored in [FP04a, Str07]. Notice that this kind of semantics explains why the order on hom-sets was chosen as it is in [FP05]. It turns out to be the reverse of the one presented in [Str07], which was obtained by looking at the proof net semantics of [LS05b], which favors the opposite direction.

4.16. Corollary. Diagonal-is-inf bimonoids are idempotent.

It is not hard to get interesting 𝔹-coherence structures in the diagonal-is-inf model. Actually, any coherence structure will work:

4.17. Proposition. Let (M, ⊑) be a lattice^{12} and ρ any 𝔹-coherence structure on M. Then the diagonal-is-inf structure on the poset M is a map in 𝔹-Coh.

Proof. Let us verify for the diagonal: with the help of Equation (20) we want to show that

m ⌣ ⌢ m′, m Δ (p, q), m′ Δ (p′, q′) implies p ⌣ ⌢ p′ and q ⌣ ⌢ q′

and this is quite trivial, given that m Δ (p, q) is equivalent to m ⊑ p, q, m′ Δ (p′, q′) is equivalent to m′ ⊑ p′, q′ and that the ⌣ ⌢ relation is up-closed. This will also work for the codiagonal, since it is the diagonal in the ρ^{⊥} coherence.

12As we’ve said, any poset will do actually, but the general proof that we get bimonoids has to be supplied by the reader.

Before we go on to other models we should add that the diagonal-is-inf model is contractible, in the sense of [LS05a, 2.4.3].

Let us now turn our attention to the diagonal-is-sup model, first looking at the bimonoid equation again. If as before f = ∇∘Δ is the “small” half of the bimonoid equation and g the “large” half, it is easy to see that

(m, m′) f (n, n′) iff m ⊓ m′ ⊑ n ⊔ n′ ,

while a mechanical computation gives us

(m, m′) g (n, n′) iff (∃_{p,p′,q,q′}) m ⊑ p ⊔ p′, m′ ⊑ q ⊔ q′ and p ⊓ q ⊑ n, p′ ⊓ q′ ⊑ n′ .

We claim that this is equivalent to

(m, m′) g (n, n′) always,

in other words that the graph of g is the full product M × M × M × M. In order to prove this, just put p = m, p′ = b, q = b, q′ = m′ in the above, and check that the other inequalities will hold, whatever the values of n, n′.

There are situations where f ≠ g, i.e., f ⊂ g; for an easily computed case, just take ⊑ to be a total ordering. Thus we have shown that diagonal-is-sup bimonoids are not proper in general. Another similar calculation proves that the doubling map 𝒟 is always the full graph. Just write down the definition:

m 𝒟 n iff (∃_{p,p′}) m ⊑ p ⊔ p′ and p ⊓ p′ ⊑ n

and put p = t, p′ = b; this will always hold, whatever m, n.

We conclude from this that the diagonal-is-sup model is not very subtle: it is not idempotent, but the doubling operation has a “black hole” effect, which is not very interesting from the point of view of the semantics of proofs.

4.18. Another class of bimonoids. It would be interesting to have an intrinsic class 4.17 of bimonoids in 𝔹-Coh where the operation of superposition/convolution is not idempotent, and in a more subtle way than in the preceding example. There is a simple “benchmark” for testing a model: ideally we would like to have objects X such that 𝒟_{X}, 𝒟_{X} ∘ 𝒟_{X}, 𝒟_{X} ∘ 𝒟_{X} ∘ 𝒟_{X} … never stabilizes, and seeing how high we can iterate 𝒟 before the sequence stabilizes is a measure of how well the model can distinguish the number of times an axiom—seen as a pair of occurrences of an atom and its negation in a formula—is used in a proof. Another “benchmark” would be to see how many distinct Church numerals we can get. But these two benchmarks are closely related and if a model does well for one it will do well for the other, and the 𝒟-test is easier to compute.

4.19. Remark. In what follows we will be working in Cmp, and not bother with 𝔹coherence structures, since they have no influence on the equations, and we know we can always use the discrete and codiscrete structures.

We are interested in nonempty, finite, totally ordered posets. Given a positive integer N, we define the canonical N + 1-element total ordering as

⟨N⟩ = [ 0, N] = { 0, 1, 2, …, N }

Total finite orders have the great advantage that they have no nontrivial automorphisms (in other words, given any two such posets of the same cardinality, there is a unique iso between them), thus greatly easing the quest for intrinsic families.

Naturally, we will have to take Cartesian products of canonical posets, and in the end the posets in our models will be of the form

⟨N_{1}⟩ × ⟨N_{2}⟩ × ⋯ × ⟨N_{n}⟩  (26)

for finite families N_{1}, N_{2}, …, N_{n} of positive integers. We allow n = 0 and define the product of the empty family as ⟨0⟩ = {0}.

We will first concentrate on posets of the form ⟨N⟩ for a given N ∈ ℕ.

There is a bewildering number of monoid structures that can be put on finite intervals. After much fumbling around we settled for the following:

4.20. Proposition. Let ℤ be the ring of integers and [M_{0}, M_{1}] ⊂ ℤ a finite interval that contains 0. Then the operation (−) · (−) defined below is commutative, associative and monotone on [M_{0}, M_{1}], with e = 0 as unit.

i · j = \begin{cases}inf(i + j, M_{1}) & if i, j ≥ 0 \\ sup(i + j, M_{0}) & if i, j < 0 \\ inf(i, j) & if one is ≥ 0 and one is < 0 \end{cases}

Proof. This operation is obviously commutative. For associativity, we have to show (x + y) + z = x + (y + z) by cases. If all three elements are ≥ 0 then obviously both sides are equal to inf(x + y + z, M_{1}). If all three elements are < 0 both sides are equal to sup(x + y + z, M_{0}). If exactly one of the three elements is negative, then it is the value of both sides of the equation. If two elements are negative, then the least of them is the value of both sides of the equation. The fact that 0 is the unit is trivial to check.

For monotonicity of (−) · (−), all we have to show is that for any x the function x · (−) is monotone. But if x ≥ 0 this function is

y ↦ \begin{cases}y & if y < 0 \\ inf(x + y, M_{1}) & if y ≥ 0 \end{cases}

which is obviously monotone, and if x < 0 the function is

y ↦ \begin{cases}sup(x + y, M_{0}) & if y < 0 \\ x & if y ≥ 0 \end{cases}

which is also obviously monotone.

Given an N + 1-element canonical poset ⟨N⟩, we want to transport the monoid structure defined above to it. Actually this is more a family of monoid structures, since there are parameters we can instantiate to our taste. We do this by choosing e ∈ ⟨N⟩, and decreeing that it will be the unit in the transported structure. Then this canonical poset is obviously poset-isomorphic to [−e, N − e ] ⊂ ℤ, with the bijection α(x) = x + e, x ∈ [−e, N − e ]. Thus if we transport our monoid structure along that bijection, we get the following (where we drop the α indices we had in the definition of transport)

i · j = \begin{cases}inf(i + j − e, N) & if i, j ≥ e \\ sup(i + j − e, 0) & if i, j < e \\ inf(i, j) & if one is ≥ e and one is < e \end{cases}  (27)

Notice that the three components of the definition overlap correctly around e. Thus the following definition is not really a definition by cases, but it is still correct… and much more symmetrical.

i · j = \begin{cases}inf(i + j − e, N) & if i, j ≥ e \\ sup(i + j − e, 0) & if i, j ≤ e \\ inf(i, j) & if one is ≥ e and one is ≤ e \end{cases}  (28)

Now, there is a contravariant involution (antiisomorphism) ⟨N⟩ → ⟨N⟩ given by i ↦ N −i, and we can transport our monoid (contravariance will ensure that the resulting operation will still be monotone). If we define e^{∗} = N − e, which will obviously be the unit in the transported structure, we get, choosing Equation (28) as the standard of presentation

i ∗ j = \begin{cases}inf(i + j − e^{∗}, N) & if i, j ≥ e^{∗} \\ sup(i + j − e^{∗}, 0) & if i, j ≤ e^{∗} \\ sup(i, j) & if one is ≥ e^{∗} and one is ≤ e^{∗} \end{cases}  (29)

So the third clause is the real difference between (−) · (−) and (−) ∗ (−), the one thing that shows that transport along an antiiso gives a different result from transport along an iso.

We still have quite a lot of choice on how to construct bimonoids in Cmp. We know that choosing (−)·(−) for diagonal will force (−)∗(−) for codiagonal; it is a better choice than the reverse, because in the latter case we will find ourselves in a situation a lot like the diagonal-is-sup model.

So let us choose N and e ∈ ⟨N⟩ and try to calculate Δ for this bimonoid (as we have said before, this is all happening in Cmp but we know the coherence structure is not relevant here). If we choose a ∈ ⟨N⟩ it is easy to see that the set { b | a 𝒟 b } will be

{ x ∗ y | a ≤ x · y }↑ .  (30)

(The operation ↑ here is taken in ⟨N⟩, not in ℕ of ℤ.)

It is also easy to see that this set will always be nonempty. Trivially, determining its least element will determine the whole set. So let

L(a) = the least element of (30).

4.21. Proposition. Let N and a, e ∈ ⟨N⟩ be chosen. Then the sets

{ (x, y) ∈ ⟨N⟩ × ⟨N⟩ | a ≤ sup(x + y − e, 0) }

and

{ (x, y) ∈ ⟨N⟩ × ⟨N⟩ | a ≤ inf(x + y − e, N) }

are both equal to

{ (x, y) ∈ ⟨N⟩ × ⟨N⟩ | a + e ≤ x + y } .

Proof. The constraint a ≤ sup(x + y − e, 0) is equivalent to a ≤ x + y − e because 0 ≤ a and the constraint a ≤ inf(x + y − e, N) is equivalent to a ≤ x + y − e because a ≤ N.

We will determine L(a) by a case analysis on ⟨N⟩×⟨N⟩. Since (−)∗(−) is commutative we can simplify by assuming that x ≤ y always. The respective position of e, e^{∗} is very important in the analysis, so we assume, through an educated guess, that e ≤ e^{∗}. Now look at

1  0 ≤ x ≤ y < e  a + e ≤ x + y  sup(x + y − e^{∗}, 0)
2  0 ≤ x < e ≤ y < e^{∗}  a ≤ x  sup(x + y − e^{∗}, 0)
3 0 ≤ x < e, e^{∗} ≤ y ≤ N  a ≤ x  x
4  e ≤ x ≤ y ≤ e^{∗}  a + e ≤ x + y  sup(x + y − e^{∗}, 0)
5  e ≤ x ≤ e^{∗} ≤ y ≤ N  a + e ≤ x + y  x
6  e^{∗} ≤ x ≤ y ≤ N  a + e ≤ x + y  inf(x + y − e^{∗}, N)

In the above, the third column is the constraint a ≤ x·y (simplified using Proposition 4.21 when it applies) in the region of { (x, y) ∈ ⟨N⟩ × ⟨N⟩ | x ≤ y } determined by the second column, and the fourth column is the value of x ∗ y in the same region.

Thus, we have decomposed (30) into the union of six subsets (some of which may be empty, depending on the value of a). If we take the minimum element of each of these sets, the least of them will be L(a). Notice that the decomposition above does not exactly amount to a partition of { (x, y) | x ≤ y } because sets 4 and 5 overlap when x = y = e^{∗}. But the (dual of the) equivalence between (27) and (28) allows us to have a little overlap in the computation of x ∗ y.

Claim: We have L(a) = sup(a + e − e^{∗}).

We will first create an approximation L′ of L and then will show that it is actually equal to L. We calculate L′ by cases by looking only at sets 1, 4, 6, which are chosen depending on the value of a.

• 0 ≤ a < e. Clearly the only one of 1, 4, 6 that can be nonempty is 1, and it is nonempty iff 0 ≤ a < e can hold. So we want to find the least element of

{ sup(x + y − e^{∗}, 0) | a + e ≤ x + y, 0 ≤ x, y < e }

Since the constraint x, y < e^{∗} is an upper limit we can drop it and rewrite the set as

{ sup(z − e^{∗}, 0) | a + e ≤ z }

and its least element is obviously

L′(a) = sup(a + e − e^{∗}, 0) .

• e ≤ a ≤ e^{∗}. Looking at case 4

{ sup(x + y − e^{∗}, 0) | a + e ≤ x + y, e ≤ x ≤ y ≤ e^{∗} }

The largest possible value of x + y is 2e^{∗}, and since e ≤ a ≤ e^{∗} we always have a + e ≤ 2e^{∗} and the set is guaranteed to be nonempty for the given range of a. The least possible value of x + y is 2e, and since a ≥ e we always have that a + e is above that minimum. Thus we can do as before and remove the second constraint, so L′(a) is the least element of

{ sup(z − e^{∗}, 0) | a + e ≤ z }

getting

L′(a) = sup(a + e − e^{∗}, 0) .

• e^{∗} ≤ a ≤ N. Looking at case 6

{ inf(x + y − e^{∗}, N) | a + e ≤ x + y, e^{∗} ≤ x, y ≤ N }

It is guaranteed to be nonempty; since the least element satisfying the second constraint is 2e^{∗} which is always ≥ a + e, so we can remove the second constraint, getting (by the same argument as before)

L′(a) = inf(a + e − e^{∗}, N)

but since e ≤ e^{∗} and a ≤ N we have L′(a) = a + e − e^{∗}, and since a ≥ e^{∗} ≥ e the value of L(a) is always guaranteed to be ≥ 0, and once again we get

L′(a) = sup(a + e − e^{∗}, 0) .

In order to show that L′ = L all we have do to is check that the sets defined in cases 2, 3, 5, when nonempty, do not have minima that go below L′.

• Case 2 is the set

{ sup(x + y − e^{∗}, 0) | a ≤ x, 0 ≤ x < e ≤ y < e^{∗} } ,

but x ≥ a and y ≥ e, so x + y − e^{∗} ≥ a + e − e^{∗}.

• Case 3 is

{ x | a ≤ x, 0 ≤ x < e, e^{∗} ≤ y ≤ N } ,

but a ≤ x and a + e − e^{∗} ≤ a.

• Case 5 is

{x | a + e ≤ x + y, e ≤ x ≤ e^{∗} ≤ y ≤ N }

So a + e ≤ e + e^{∗} ≤ x + y and x ≥ a + e − e^{∗} follows immediately.

So we conclude that when e ≤ e^{∗}, we have

a 𝒟 b iff b ≥ sup(a + e − e^{∗}, 0) .

Thus when e = e^{∗}, or equivalently N = 2e (i.e., the interval has an odd (N + 1) number of elements and e = e^{∗} is smack in the middle), the doubling map is the identity in Cmp, which is one thing we are trying to avoid. We also see that nonzero values of e^{∗} − e are interesting, and especially those that have a small absolute value, because we will be able to do more iterations to the map 𝒟 before the bounds of the interval force the sequence to stabilize.

So the best case is

• N is odd and e = (N − 1)/2, forcing e^{∗} = (N + 1)/2 and e^{∗} − e = 1

And the doubling map is then given by

a 𝒟 b iff b ≥ sup(a − 1, 0)

and it is easy to see that its kth iteration is

a 𝒟^{k} b iff b ≥ sup(a − k, 0) .

Thus we get 𝒟 ≠ 𝒟^{2} ≠ ⋯ ≠ 𝒟^{N−1} ≠ 𝒟^{N} and 𝒟^{N} = 𝒟^{N+1} is given by (N, 0)↕. So we get a model which is as nice as can be, given that because the structures are finite, we have to have the (𝒟^{k})_{k} sequence eventually stabilize for some k. But we can make that upper bound k as big as we want.

When e^{∗} < e the resulting 𝒟 is a more complicated function, which we will let the interested reader compute.

It is now time to take products of canonical posets. In order to do things like proving intrinsicness we have to define some things carefully.

4.22. Definition. A rank is a number n ≥ 0. A ranking r is a pair r = (n, (N_{i})_{i}) where n is a rank and (N_{i})_{i∈[1,n]} a family of positive numbers. When the rank n = 0 that family is the empty family.

A ranking r = (n, (N_{i})_{i}) defines a poset

P(r) = ∏_{i∈[1,n]} ⟨N_{i}⟩ ;

thus an element of P(r) is a vector a = (a_{i})_{i∈[1,n]} of natural numbers a_{i} ∈ ⟨N_{i}⟩, and P(r) is naturally ordered by the product ordering. The poset defined by the ranking (0, ∅) of rank zero is ⟨0⟩.

Suppose that for every i ∈ [1, n] the poset ⟨N_{i}⟩ is given a commutative monoid structure ( ·_{i}, e_{i}). Then the poset P(r) has the standard product monoid structure:

(a_{1}, a_{2}, …, a_{n}) · (b_{1}, b_{2}, …, b_{n}) = (a_{1} ·_{1} b_{1}, a_{2} ·_{2} b_{2}, …, a_{n} ·_{n} b_{n})

with unit (e_{1}, e_{2}, …, e_{n}).

Thus, suppose that we are given a set 𝒜 ⊆ ℕ of positive natural numbers, and for every N ∈ 𝒜 two uniquely defined monoid structures (·, e) and (∗, e^{∗}) on ⟨N⟩. We obviously get an intrinsic class of bimonoids in Cmp (we don’t have to worry about transport…), but it’s not closed under the logical operators. For example we can take 𝒜 to be the set of all odd numbers, and take as bimonoid structures the ones we just identified as most desirable. We can also choose 𝒜 to be a singleton {N}, with N odd again.

But we have to ensure that the class of all finite products of structures in 𝒜 is an intrinsic class.

4.23. Definition. Given two rankings r^{1} = (n^{1}, (N_{i}^{1})_{i}) and r^{2} = (n^{2}, (N_{i}^{2})_{i}) an isomorphism α: r^{1} → r^{2} or rankings is defined only when n_{1} = n_{2} (so we write n_{1} = n_{2} = n), and it is given by a permutation α: [1, n] → [1, n] such that N_{i}^{1} = N_{α(i)}^{2} for all i ∈ [1, n]. Obviously an isomorphism of rankings defines an isomorphism of posets P(α): P(r^{1}) → P(r^{2}), by

P(α)((a_{i})_{i∈[1,n]}) = (a_{α(i)})_{i∈[1,n]} .

whose inverse is P(α^{−1}).

4.24. Proposition. Let r = (n, (N_{i})_{i}) be a ranking and for every i let there be a monoid structure on ⟨N_{i}⟩ such that whenever N_{i} = N_{j} then the monoid structures coincide on ⟨N_{i}⟩, ⟨N_{j}⟩. Then given an autormorphism α: r → r, transporting the product monoid structure on P(r) along P(α) gives the very same monoid structure.

Proof. Since any permutation is generated by composing only transpositions, we can restrict to the case when α simply exchanges two numbers in [1, n] and leaves the rest unchanged. It is easy to see that without loss of generality we can suppose in addition that these two numbers are 1, 2. Thus given two vector a, b ∈ P(r) we can write them as a = (a_{1}, a_{2}, a′) and b = (b_{1}, b_{2}, b′) where a′, b′ are shorthand for a_{3}, …, a_{n} and b_{3}, …, b_{n} respectively. We get (dropping the indices on these monoid structures)

[figure: ((a_{1}, a_{2}, a′), (b_{1}, b_{2}, b′)); P(α)^{−1} × P(α)^{−1}; (−) · (−); ((a_{2}, a_{1}, a′), (b_{2}, b_{1}, b′)); (−) · (−); (a_{1} · b_{1}, a_{2} · b_{2}, a′ · b′); P(α); (a_{2} · b_{2}, a_{1} · b_{1}, a′ · b′)]

The first-right-then-down-then-left path computes the value for the transported monoid, and the just-down path computes it for the standard product monoid; they obviously coincide. The argument for units is pretty trivial.

If, for any ranking r = (n, (N_{i})_{i}) with N_{i} ∈ 𝒜, we can prove that any posetautomorphism of P(r) is of the form P(α) for some automorphism α of r, combining the previous result with Propositions 3.10 and 4.14 will allow us to conclude that the class of all bimonoids obtained from products in 𝒜 is an intrinsic class of bimonoids.

So let (A, ≤) be a poset which is of the form A = P(r). We will give a self-contained proof that its only automorphisms are induced by automorphisms of r; the reader who is familiar with “Birkhoff Duality” (the contravariant equivalence between the category of finite posets and the category of finite lattices) can find an even shorter proof.^{13}

We recall the standard definition of predecessor/successor

a ≺ b if a < b and for any x, a ≤ x ≤ b implies x = a or x = b .

Clearly in our case we have a ≺ b iff there exists i (uniquely defined) such that a_{i} ≠ b_{i}, with a_{i} = b_{i} − 1.

4.25. Proposition. Let a, b, c ∈ A, with a ≠ b. If a ≺ c ≻ b then there exists a unique d with a ≻ d ≺ b and if a ≻ c ≺ b there exists a unique d with a ≺ d ≻ b.

Proof. Obvious.

Let us denote by 𝒮 (a) the set 𝒮 (a) = { x | a ≺ x }.

4.26. Proposition. Let a ≺ b. Then the map χ_{a}^{b}: 𝒮 (a) − {b} → 𝒮 (b) defined by

χ_{a}^{b}(c) = the unique d with c ≺ d ≻ b

is always injective, and either it is surjective, or there is a unique b′ ∈ 𝒮 (b) which is not in its image.

Proof. We know there is i with b = (a_{1}, a_{2}, …, a_{i} + 1, …, a_{n}). For j ∈ [1, n] let j be the vector whose jth component is 1 and which is is zero everywhere else. Then χ_{a}^{b} is defined by a + j ↦ b + j, where j ranges over [1, n] − {i}, and it is obviously injective. Its image is the set { b + j | j ≠ i }. If a_{i} + 1 = N_{i} the map χ_{b}^{a} is surjective. If a_{i} + 1 ≠ N_{i} then the only element not in the image of χ_{a}^{b} is b′ = b + i.

13We would like to thank Luigi Santocanale for pointing this out.

Let us denote the bottom element of A as 0 = (0, 0, …, 0).

Let now a ∈ 𝒮 (0). We can define the sequence a^{0} ≺ a^{1} ≺ ⋯ ≺ a^{m} to be the longest sequence satisfying

a^{0} = 0, a^{1} = a
a^{k+1} = the unique d ∈ 𝒮 (a^{k}) not in the image of χ_{a^{k−1}}^{a^{k}}

Since 𝒮 (0) is in bijective correspondence with [1, n], there is i ∈ [1, n] such that for every k the ith component of the vector a^{k} is a_{i}^{k} = k and all the other components are 0. Thus the length of the sequence is m = N_{i} and there is an order-isomorphism between set { a^{k} | k ∈ ⟨N_{i}⟩ } and ⟨N_{i}⟩. Let us denote that set by A_{i}; it is defined for every i ∈ [1, n] (equivalently for every a ∈ 𝒮 (0)).

So now let β be an order-automorphism of A. Clearly the set 𝒮 (0) is stable under β. Thus because of the bijective correspondence between 𝒮 (0) and [1, n], β induces a permutation on [1, n], that we will call β̄. Moreover, given i ∈ [1, n], since A_{i} is entirely defined by order-theoretic considerations, β has to map A_{i} to A_{β̄(i)}. And since every element of a ∈ A is the sup of { b ∈ ⋃_{i} A_{i} | b ≤ a}, and the sup is also a purely order-theoretic concept, we have proved that β = P(β̄).

It is easy to prove a little bit more, namely that we can define the operations (−) · (−) and (−) ∗ (−) just by looking at the order on A.

The class of bimonoids we have just constructed is rather satisfying, although calculations in it tend sometimes to be much less trivial than they should be. It would be nice to be able to extend it to products of (ℤ, ⊑) instead of finite subsets of ℤ, but a technique has to be devised to get rid of the unwanted isomorphisms, that kill intrinsicness.

4.27. Additives. Since this paper is already rather long, this final section will be a bit sketchy.

It is interesting that some denotational models of classical logic have additive equivalents &, +^{14} to the “multiplicative” conjunction and disjunction ∧, ∨ we have defined above. Naturally the pairs & ↔ ∧ and + ↔ ∨ are equivalent from the point of view of provability, but not from that of proof identification.

14We reserve the use of the symbol ⊕ for operations that are biproducts in the category-theoretic sense.

4.28. Definition. Let X, Y be objects of 𝔹-Coh. We define X & Y and X + Y as

|X & Y | = |X + Y | = |X| + |Y |, i.e., the disjoint sum

ρ_{X&Y} (z, z′) = \begin{cases}ρ_{X}(z, z′) & if z, z′ ∈ |X| \\ ρ_{Y} (z, z′) & if z, z′ ∈ |Y | \\ 1 & if z ∈ |X|, z′ ∈ |Y | or vice-versa \end{cases}

ρ_{X+Y} (z, z′) = \begin{cases}ρ_{X}(z, z′) & if z, z′ ∈ |X| \\ ρ_{Y} (z, z′) & if z, z′ ∈ |Y | \\ 0 & if z ∈ |X|, z′ ∈ |Y | or vice-versa . \end{cases}

Obviously (X & Y)^{⊥} = X^{⊥} + Y^{⊥}.

4.29. Proposition. Let X, Y be bimonoids in Cmp. The following defines a bimonoid X ⊕ Y in Cmp.

− |X ⊕ Y | = |X| + |Y |,
− (x, y) Δ^{X⊕Y} (x_{1}, y_{1}, x_{2}, y_{2}) iff x Δ^{X} (x_{1}, x_{2}) and y Δ^{Y} (y_{1}, y_{2}),
− (x_{1}, y_{1}, x_{2}, y_{2}) ∇^{X⊕Y} (x, y) iff (x_{1}, x_{2}) ∇^{X} x and (y_{1}, y_{2}) ∇^{Y} y,
− (x, y) Π^{X⊕Y} ∗  iff x Π^{X} ∗ and y Π^{Y} ∗,
− ∗ ⨿^{X⊕Y} (x, y)  iff ∗ ⨿^{X} x and ∗ ⨿^{Y} y .

Proof. The proof is an easy computation.

One important point about this construction is that the original bimonoid structures on X, Y can be recovered by looking at X ⊕ Y. The natural injections X → X + Y and Y → X +Y in the category of sets translate easily into morphisms X → X ⊕Y, Y → X ⊕ Y, X ⊕Y → X, X ⊕Y → Y in Cmp. Given that product is functorial in Cmp, we also get natural X×X → (X⊕Y)×(X⊕Y), etc. Thus, given, say Δ: (X⊕Y) → (X⊕Y)×(X⊕Y) we can pre- and postcompose with the right maps

\xymatrix{X \ar[r] & X ⊕ Y \ar[r] & (X ⊕ Y) × (X ⊕ Y) \ar[r] & X × X}

to recover Δ_{X}: X → X × X, and the same goes for Δ_{Y} : Y → Y × Y and the rest of the original structure.

The operation ⊕ defines a symmetric monoidal structure on Cmp; this is easy to see, and even more so if we notice that it obeys the property of being a biproduct [Mac71, VII,2]. It is also easy to see that ⊕ is not just a binary operation, and is defined for infinite families. Its unit is the empty set.

Thus, we can combine the two results above, and for any pair of bimonoids X, Y in 𝔹-Coh we can construct bimonoids X & Y and X + Y: it is easy to see that the bimonoid operations in Cmp are also maps in 𝔹-Coh.

4.30. Theorem. Let ℰ be an intrinsic class of bimonoids in 𝔹-Coh, such that every object X ∈ ℰ has a connected underlying poset, and which closed under ∧, ∨ and negation. let ℰ′ be obtained from ℰ as follows: an object X ∈ ℰ′ is a 𝔹-coherence such that

• its underlying poset is a finite disjoint sum ∑_{i} X_{i} of underlying posets from ℰ,

• the coherence ρ_{X} restricted to any X_{i} defines an object of ℰ,

• every operation of the bimonoid structure ⨁_{i} X_{i} in Cmp respects the coherence structure on X.

Then the class ℰ′ is closed under ∧, ∨, &, + and negation and is an intrinsic class of bimonoids.

Proof. Closure under the connectives is easy to show and will be left to the reader. Let us show that ℰ′ is an intrinsic family. Let X ∈ ℰ′, and α be an automorphism of X in 𝔹-Coh. We want to show that α is an automorphism for the bimonoid structure on X. We know we can forget the 𝔹-structure and look only at the poset structure on X.

Let Y ⊆ X be a connected sub-poset. By definition we know Y is an underlying poset for an object in ℰ. Since α is a poset iso, its image α(Y) ⊆ X also comes from something in ℰ, and since it is an intrinsic class we know that the restriction α|_{Y} : Y → α(Y) of α to Y is an isomorphism of bimonoids, when the bimonoid structure on X is restricted to Y and α(Y). Thus, choosing Δ as a component of the bimonoid structure, the outer square in the diagram below commutes in Cmp, where the diagonal arrows are just inclusion maps.

[figure: Y; α|_{Y}; Δ|_{Y}; α(Y); Δ|_{α(Y)}; X; α; Δ; X; Δ; X × X; α × α; X × X; Y × Y; α|_{Y} × α|_{Y}; α(Y) × α(Y)]

Since it commutes for an arbitrary connected subposet Y ⊆ X, it commutes for all connected subposets of X, and this implies that the inner square commutes, because the maps in that square are all completely determined by their values on the connected subposets.

The proof that α respects the other operations of the bimonoid structure is done the same way.

As an example of this procedure, we can choose for ℰ the set { t, f }. Then ℰ′ is a category which is very much like ordinary coherence spaces, where the objects always have the discrete (trivial) order structure. The Δ, ∇ operations are obtained from the ordinary set-diagonal. This ties up nicely with the original model presented in [FP05].

4.30.1. Conclusion. The general framework we have given for constructing bimonoid structures in Cmp can be specialized in a great number of ways. We have chosen two basic examples, one where the bimonoid structures are determined by the orders on the objects of Cmp, and one where some real work is involved in constructing them. Both these examples actually double up in pairs of models, according to whether a structure or its de Morgan is assigned to the diagonal (the codiagonal being forced to be the de Morgan dual of the assignment). In each case, one these assignment is much more interesting than its dual, giving

• for the first example a class of models that obey both idempotency and the bimonoid equation,

• for the second example a class of models where neither equation is obeyed, showing that such models actually exist, and giving the real possibility of counting how often an axiom is used in a proof.

The first example is very natural. The second example is much more contrived, but its complementary aspect illustrates the power of our approach.

5. Appendix: The Unicity of (n, m)-ary Medial

We present here a proof that the axioms we gave for (2,2)-ary Medial allow the construction of an (n, m)-ary Medial which is uniquely defined, in a sense that we will make clear. In the time elapsed between the submission of this paper and the present final version, a proof of a version of this result has been proposed [DP07]. Our own approach is weaker and less general, but it fits the constraints of the present paper well. The proof we present strives to exhibit the maximal amount of algebraic structure and could be made shorter, for instance by the use of duality. There are several closely related “coherence ” theorems in the literature on iterated loop spaces, for instance [BFSV03], but they make essential use of a unit which is common to the multiple tensor structures under study, even for statements where that unit does not explicitly appear.

For the purpose of this section we define a bimonoidal category (ℂ, ⊗, ⅋, I, ⊥) to be a category ℂ equipped with two symmetric monoidal structures (⊗, I), (⅋, ⊥) (as a matter of fact we will not use the units). We are interested in triples (F, ψ^{F} , ϕ^{F}), that we will call bimonoidal functors^{15} where

• F is a functor 𝔻 → ℂ, between bimonoidal categories, • ψ^{F} (X, Y): F X ⅋ F Y ⟶ F (X ⅋ Y) is a map, natural in X, Y,

15No claim of relation to any definition of “bimonoidal functor” given elsewhere. Notice that we do not involve the units, which is rather nonstandard.

• ϕ^{F} (X, Y): F (X ⊗ Y) ⟶ F X ⊗ F Y is a map, natural in X, Y,

subject to the following standard compatibility with associativity equations [EK66]

\xymatrix{(F X⅋F Y)⅋F Z \ar[d]_{ψ^{F} (X,Y) ⅋ F Z} \ar@{^{(}->}[r] & F X⅋(F Y ⅋F Z) \ar[d]^{F X⅋ψ^{F} (Y,Z)} & F ((X⊗Y)⊗Z) \ar[d]_{ϕ^{F} (X⊗Y,Z)} \ar@{^{(}->}[r] & F (X⊗(Y ⊗Z)) \ar[d]^{ϕ^{F} (X,Y ⊗Z)} \\ F (X⅋Y)⅋F Z \ar[d]_{ψ^{F} (X⅋Y,Z)} & F X⅋F (Y ⅋Z) \ar[d]^{ψ^{F} (X,Y ⅋ Z)} & F (X⊗Y)⊗F Z \ar[d]_{ϕ^{F} (X,Y) ⊗ F Z} & F X⊗F (Y ⊗Z) \ar[d]^{F X ⊗ ϕ^{F} (Y,Z)} \\ F ((X⅋Y)⅋Z) \ar@{^{(}->}[r] & F (X⅋(Y ⅋Z)) & (F X⊗F Y)⊗F Z \ar@{^{(}->}[r] & F X⊗(F Y ⊗F Z)}

and compatibility with Twist

\xymatrix{F X ⅋ F Y \ar@{^{(}->}[r] \ar[d]_{ψ^{F} (X,Y)} & F Y ⅋ F X \ar[d]_{ψ^{F} (Y,X)} & F (X ⊗ Y) \ar@{^{(}->}[r] \ar[d]_{ϕ^{F} (X,Y)} & F (Y ⊗ X) \ar[d]^{ϕ^{F} (Y,X)} \\ F (X ⅋ Y) \ar@{^{(}->}[r] & F (Y ⅋ X) & F X ⊗ F Y \ar@{^{(}->}[r] & F Y ⊗ F X}

The following is well-known

5.1. Proposition. For n ≥ 2 the data F, ψ, ϕ above defines a unique natural

ψ_{n}^{F} (X_{1}, …, X_{n}): F X_{1} ⅋ ⋯ ⅋ F X_{n} ⟶ F (X_{1} ⅋ ⋯ ⅋ X_{n})

(with ψ_{2}^{F} = ψ^{F}) and a unique natural

ϕ_{n}^{F} (X_{1}, …, X_{n}): F (X_{1} ⊗ ⋯ ⊗ X_{n}) ⟶ F X_{1} ⊗ ⋯ ⊗ F X_{n}

(with ϕ_{2}^{F} = ϕ^{F}), modulo the different bracketings of these multiple pars and tensors. Moreover, given n ≥ 2, a family (X_{i})_{i=1,...,n} of objects of ℂ and a permutation α of the set { 1, …, n}, then ϕ_{n}^{F} commutes with the isomorphisms F (⨂_{i}^{n} X_{i}) → F (⨂_{i}^{n} X_{αi}) and ⨂_{i}^{n} F_{X_{i}} → ⨂_{i}^{n} F_{X_{αi}} induced by α, and the same goes for ψ_{n}^{F} and the isomorphisms induced on the corresponding pars.

More precisely if we choose one of the bifunctors, say ⊗, n ≥ 2 and a family X_{1}, …, X_{n} of objects of 𝔻, the bifunctoriality of ⊗ ensures that two isomorphic bracketings of F (⨂_{i}^{n} X_{i}) and ⨂_{i}^{n} F X_{i} uniquely determine a map from the former to the latter, and the equation(s) above, along with the coherence theorem, ensure that this map will “track” any possible rebracketing, making the exact choice of bracketing at either end irrelevant. This result will still hold if we add permutations to rebracketings.

We can take ψ_{1}^{F} and ϕ_{1}^{F} to be the identity natural transformation on F.

An immediate consequence of this is that

\xymatrix{(F X_{1} ⅋ ⋯ ⅋ F X_{m}) ⅋ (F X_{m+1} ⅋ ⋯ ⅋ F X_{m+n}) \ar[d]^{ψ_{m}^{F}(X_{1},...,X_{m}) ⅋ ψ_{n}^{F} (X_{m+1},...,X_{m+n})} \\ F (X_{1} ⅋ ⋯ ⅋ X_{m}) ⅋ F (X_{m+1} ⅋ ⋯ ⅋ X_{m+n}) \ar[d]^{ψ^{F} (X_{1}⅋···⅋X_{m}, X_{m+1}⅋···⅋X_{m+n})} \\ F ((X_{1} ⅋ ⋯ ⅋ X_{n}) ⅋ (X_{m+1} ⅋ ⋯ ⅋ X_{m+n}))}  (31)

is ψ_{m+n}^{F} and the following

\xymatrix{F ((X_{1} ⊗ ⋯ ⊗ X_{m}) ⊗ (X_{m+1} ⊗ ⋯ ⊗ X_{m+n})) \ar[d]^{ϕ^{F} (X_{1}⊗···⊗X_{m}, X_{m+1}⊗···⊗X_{m+n})} \\ F (X_{1} ⊗ ⋯ ⊗ X_{m}) ⊗ F (X_{m+1} ⊗ ⋯ ⊗ X_{m+n}) \ar[d]^{ϕ_{m}^{F}(X_{1},...,X_{m}) ⊗ ϕ_{n}^{F} (X_{m+1},...,X_{m+n})} \\ (F X_{1} ⊗ ⋯ ⊗ F X_{m}) ⊗ (F X_{m+1} ⊗ ⋯ ⊗ F X_{m+n})}  (32)

is ϕ_{m+n}^{F}.

Given two bimonoidal functors F, G: 𝔻 → ℂ a bimonoidal natural transformation α: F → G is an ordinary natural transformation that obeys in addition

ψ^{G}(X, Y) ∘ (α_{X} ⅋ α_{Y}) = α_{X⅋Y} ∘ ψ^{F} (X, Y)  and
ϕ^{G}(X, Y) ∘ α_{X⊗Y} = (α_{X} ⊗ α_{Y}) ∘ ϕ^{F} (X, Y)

for all X, Y.

Given a monoidal categories ℂ, 𝔻, their ordinary product is also a bimonoidal category, defining (X, Y) ⊗ (X′, Y′) = (X ⊗ X′, Y ⊗ Y′), etc.

Now fix a bimonoidal ℂ and let it be equipped in addition with a natural (2,2)-ary Medial

[\begin{matrix}A & B \\ C & D \end{matrix}] : (A ⊗ B) ⅋ (C ⊗ D) ⟶ (A ⅋ C) ⊗ (B ⅋ D)

which obeys Interaction with Twist, Interaction with Itself, allowing us to define (2,3)-ary Medial

[\begin{matrix}A & B & C \\ D & E & F \end{matrix} ] : (A ⊗ B ⊗ C) ⅋ (D ⊗ E ⊗ F) ⟶ (A ⅋ D) ⊗ (B ⅋ E) ⊗ (C ⅋ F)

and the de Morgan dual of that condition (which does not need an involution to be written down), which allows us to define (3,2)-ary Medial

[\begin{matrix}A & D \\ B & E \\ C & F \end{matrix}] : (A ⊗ D) ⅋ (B ⊗ E) ⅋ (C ⊗ F) ⟶ (A ⅋ B ⅋ C) ⊗ (D ⅋ E ⅋ F) .

If we are given (F, ψ^{F} , ϕ^{F}): 𝔻 → ℂ and (G, ψ^{G}, ϕ^{G}): 𝔻′ → ℂ we can define

(F ˆ⊗ G, ψ^{F ˆ⊗G}, ϕ^{F ˆ⊗G}): 𝔻 × 𝔻′ → C and (F ˆ⅋ G, ψ^{F ˆ⅋G}, ϕ^{F ˆ⅋G}): 𝔻 × 𝔻′ → ℂ

in the following manner. First, take F ˆ⊗ G (X, Y) = F X ⊗ GY and F ˆ⅋ G (X, Y) = F X ⅋ GY. Then the following^{16}

[figure: F ˆ⊗G (X, Y) ⅋ F ˆ⊗G (X′, Y′); (F X ⊗ GY) ⅋ (F X′ ⊗ GY′); _{[\begin{matrix}F X & GY \\ F X′ & GY′ \end{matrix}]}; (F X ⅋ F X′) ⊗ (GY ⅋ GY′); ψ^{F} (X, X′) ⊗ ψ^{G}(Y, Y′); F (X ⅋ X′) ⊗ G(Y ⅋ Y′); F ˆ⊗G ((X, Y) ⊗ (X′, Y′)); F ˆ⊗G ((X, Y) ⊗ (X′, Y′)); F (X ⊗ X′) ⊗ G(Y ⊗ Y′); ϕ^{F} (X, X′) ⊗ ϕ^{G}(Y, Y′); F X ⊗ F X′ ⊗ GY ⊗ GY′; F X ⊗ T ⊗ GY′; F X ⊗ GY ⊗ F X′ ⊗ GY′; F ˆ⊗G (X, Y) ⊗ F ˆ⊗G (X′, Y′)]

(33)

define ψ^{F ˆ⊗G}, ϕ^{F ˆ⊗G} respectively, and the following

[figure: F ˆ⅋G (X, Y) ⅋ F ˆ⅋G (X′, Y′); F X ⅋ GY ⅋ F X′ ⅋ GY′; F X ⅋ T ⅋ GY′; F X ⅋ F X′ ⅋ GY ⅋ GY′; ψ^{F} (X, X′) ⅋ ψ^{G}(Y, Y′); F (X ⅋ X′) ⅋ G(Y ⅋ Y′); F ˆ⅋ G ((X, Y) ⅋ (X′, Y′)); F ˆ⅋G ((X, Y) ⊗ (X′, Y′)); F (X ⊗ X′) ⅋ G(Y ⊗ Y′); ϕ^{F} (X, X′) ⅋ ϕ^{G}(Y, Y′); (F X ⊗ F X′) ⅋ (GY ⊗ GY′); _{[\begin{matrix}F X & F X′ \\ GY & GY′ \end{matrix}]}; (F X ⅋ GY) ⊗ (F X′ ⅋ GY′); F ˆ⅋G (X, Y) ⊗ F ˆ⅋G (X′, Y′)]

(34)

give ψ^{F ˆ⅋G}, ϕ^{F ˆ⅋G} respectively. We claim that:

16this is the only place where the symmetry is present. But it is not really necessary, and at the price of making the distinction between monoidal and comonoidal functor we could get a result like the one in [DP07], for non-symmetric monoidal categories.

[figure: ((F X⊗GY)⅋(F X′⊗GY′))⅋(F X′′⊗GY′′)); [ \begin{matrix}F X & GY \\ F X′ & GY′ \end{matrix} ] ⅋ (F X′′⊗GY′′); (F X⊗GY)⅋((F X′⊗GY′)⅋(F X′′⊗GY′′); (F X⊗GY) ⅋ [ \begin{matrix}F X′ & GY′ \\ F X′′ & GY′′ \end{matrix} ]; ((F X⅋F X′)⊗(GY ⅋GY′))⅋(F X′′⊗GY′′); (ψ^{F} (X,X′)⊗ψ^{G}(Y,Y′))⅋(F X′′⊗GY′′); _{[ \begin{matrix}F X⅋F X′ & GY ⅋GY′ \\ F X′′ & GY′′ \end{matrix} ]}; (F X⊗GY)⅋((F X′⅋F X′′)⊗(GY′⅋GY′′)); (F X⊗GY)⅋(ψ^{F} (X′,X′′)⊗ψ^{G}(Y′,Y′′)); _{[ \begin{matrix}F X & GY \\ F X′⅋F X′′ & GY′⅋GY′′ \end{matrix} ]}; (F X⅋F X′⅋F X′′)⊗(GY ⅋GY′⅋GY′′); (F (X⅋X′)⊗G(Y ⅋Y′))⅋(F X′′⊗GY′′); _{[ \begin{matrix}F (X⅋X′) & G(Y ⅋Y′) \\ F X′′ & GY′′ \end{matrix} ]}; (F X⊗GY)⅋(F (X′⅋X′′)⊗G(Y′⅋Y′′)); _{[ \begin{matrix}F X & GY \\ F (X′⅋X′′) & G(Y′⅋Y′′) \end{matrix} ]}; (F (X⅋X′)⅋F X′′)⊗(G(Y ⅋Y′)⅋GY′′); ψ^{F} (X⅋X′, X′′)⊗ψ^{G}(Y ⅋Y′, Y′′); (F X⅋F (X′⅋X′′))⊗(GY ⅋G(Y′⅋Y′′)); ψ^{F} (X, X′⅋X′′)⊗ψ^{G}(Y, Y′⅋Y′′); F ((X⅋X′)⅋X′′)⊗G((Y ⅋Y′)⅋Y′′); F (X⅋(X′⅋X′′))⊗G(Y ⅋(Y′⅋Y′′)); (ψ^{F} (X,X′)⅋F X′′)⊗(ψ^{G}(Y,Y′)⅋F Y′′); (F X⅋ψ^{F} (X′,X′′))⊗(F Y ⅋ψ^{G}(Y′,Y′′))]

Figure 1: proof of compatibility of ψ^{F ˆ⊗G} with associativity.

• F ˆ⊗ G, F ˆ⅋ G are bimonoidal functors 𝔻 × 𝔻′ → ℂ.

• Given three bimonoidal functors (F_{i}: 𝔻_{i} → ℂ)_{i=1,2,3} then the associativity and symmetry isos on ℂ induce monoidal natural transformations (F_{1} ˆ⊗ F_{2}) ˆ⊗ F_{3} → F_{1} ˆ⊗ (F_{2} ˆ⊗ F_{3}), F_{1} ˆ⊗ F_{2} → F_{2} ˆ⊗ F_{1} and (F_{1} ˆ⅋ F_{2}) ˆ⅋ F_{3} → F_{1} ˆ⅋ (F_{2} ˆ⅋ F_{3}), F_{1} ˆ⅋ F_{2} → F_{2} ˆ⅋ F_{1}.

• The standard pentagon and hexagon laws hold for these.

All these assertions are easy but tedious to verify; one example of the computations involved is given in Figure 1, which shows the compatibility of ψ^{F ˆ⊗G} with associativity. In this diagram, the formula in the middle should be two formulas, related by an associativity isomorphism. Then the top pentagon/hexagon is the dual version of Interaction of Medial with itself/associativity. The bottom pentagon/hexagon is the interaction of ψ^{F} and ψ^{G} with associativity, tensored together. The two side squares are naturality of (2,2)-ary Medial.

Several other components of the proof are very similar to this one.

The identity functor (I, 1_{I}, 1_{I}): ℂ → ℂ is obviously bimonoidal. This allows us to construct the bimonoidal functors I ˆ⊗ I, I ˆ⅋ I, that will abbreviated to ⊗^{2}, ⅋^{2}. Obviously these are just the ordinary tensor and par bifunctors on ℂ. Notice that the definition of these immediately imply that

ψ^{⊗^{2}}((X, Y), (X′, Y′)) = ϕ^{⅋^{2}}((X, X′), (Y, Y′)) = [\begin{matrix}X & Y \\ X′ & Y′ \end{matrix}] .  (35)

Let ⊗^{n}: ℂ^{n} → ℂ be I ˆ⊗ ⋯ ˆ⊗ I and ⅋^{n}: ℂ^{n} → ℂ be I ˆ⅋ ⋯ ˆ⅋ I (since this is ambiguous the reader can choose a favorite normalized bracketing). Our aim is to prove that ψ_{n}^{⊗^{m}} = ϕ_{m}^{⅋^{n}} for all n, m. But we have to make a slight adjustment for things to type correctly, as is already apparent just above. Given an n × m matrix (X_{ij})_{i≤n,j≤m} of objects of ℂ, the transformation ψ_{n}^{⊗^{m}}((X_{11}, … X_{1m}), (X_{21}, …, X_{2m}), …, (X_{n1}, …, X_{nm})) has the type

[figure: (X_{11} ⊗ ⋯ ⊗ X_{1m}) ⅋ (X_{21} ⊗ ⋯ ⊗ X_{2m}) ⅋ ⋯ ⅋ (X_{n1} ⊗ ⋯ ⊗ X_{nm}); (X_{11} ⅋ ⋯ ⅋ X_{n1}) ⊗ (X_{12} ⅋ ⋯ ⅋ X_{n2}) ⊗ ⋯ ⊗ (X_{1m} ⅋ ⋯ ⅋ X_{nm})]

but the corresponding version of ϕ_{m}^{⅋^{n}} with the same type is a “transposed” version ϕ_{m}^{⅋^{n}}((X_{11}, …, X_{n1}), (X_{12}, …, X_{n2}), …, (X_{1m}, …, X_{nm})). So we use angle brackets to express this reparametrization: the above will also be written

ϕ_{m}^{⅋^{n}}⟨⟨X_{11}, … X_{1m}⟩, ⟨X_{21}, …, X_{2m}⟩, …, ⟨X_{n1}, …, X_{nm}⟩⟩

and what we want to prove is ψ_{n}^{⊗^{m}}() = ϕ_{m}^{⅋^{n}}⟨⟩ for all n, m.

Take Equation (32) and substitute ⅋^{2} for F. Since the source of that functor is ℂ^{2} the family X_{1}, …, X_{m+n} of objects is now a family of pairs (X_{1}, Y_{1}), …, (X_{m+n}, Y_{m+n}) and the equation translates immediately (assuming equation (35)) as

[figure: ((X_{1} ⊗ ⋯ ⊗ X_{m}) ⊗ (X_{m+1} ⊗ ⋯ ⊗ X_{n+m})) ⅋ ((Y_{1} ⊗ ⋯ ⊗ Y_{m}) ⊗ (Y_{m+1} ⊗ ⋯ ⊗ Y_{n+m})); ((X_{1} ⊗ ⋯ ⊗ X_{m}) ⅋ (Y_{1} ⊗ ⋯ ⊗ Y_{m})) ⊗ ((X_{m+1} ⊗ ⋯ ⊗ X_{m+n}) ⅋ (Y_{m+1} ⊗ ⋯ ⊗ Y_{m+n})); ((X_{1} ⅋ Y_{1}) ⊗ ⋯ ⊗ (X_{m} ⅋ Y_{m})) ⊗ ((X_{m+1} ⅋ Y_{m+1}) ⊗ ⋯ ⊗ (X_{m+n} ⅋ Y_{m+n})); ϕ_{m}^{⅋^{2}}⟨⟨X_{1},...,X_{m}⟩,⟨Y_{1},...,Y_{m}⟩⟩ ⊗ ϕ_{n}^{⅋^{2}}⟨⟨X_{m+1},...⟩,⟨...,Y_{m+n}⟩⟩; _{[\begin{matrix}X_{1} ⊗ ⋯ ⊗ X_{n} & X_{m+1} ⊗ ⋯ ⊗ X_{m+n} \\ Y_{1} ⊗ ⋯ ⊗ Y_{m} & Y_{m+1} ⊗ ⋯ ⊗ Y_{m+n} \end{matrix}]}]

being equal to ϕ_{m+n}^{⅋^{2}}. But now look at the left part of Equation (33), and put F = ⊗^{m}, G = ⊗^{n}, along with X = (X_{1}, …, X_{m}), Y = (X_{m+1}, …, X_{m+n}), X′ = (Y_{1}, …, Y_{m}), Y′ = (Y_{m+1}, …, Y_{m+n}), thus showing that

[figure: ((X_{1} ⊗ ⋯ ⊗ X_{m}) ⊗ (X_{m+1} ⊗ ⋯ ⊗ X_{m+n})) ⅋ ((Y_{1} ⊗ ⋯ ⊗ Y_{m}) ⊗ (Y_{m+1} ⊗ ⋯ ⊗ Y_{m+n})); ((X_{1} ⊗ ⋯ ⊗ X_{m}) ⅋ (Y_{1} ⊗ ⋯ ⊗ Y_{m})) ⊗ ((X_{m+1} ⊗ ⋯ ⊗ X_{m+n}) ⅋ (Y_{m+1} ⊗ ⋯ ⊗ Y_{m+n})); ((X_{1} ⅋ Y_{1}) ⊗ ⋯ ⊗ (X_{m} ⅋ Y_{m})) ⊗ ((X_{m+1} ⅋ Y_{m+1}) ⊗ ⋯ ⊗ (X_{m+n} ⅋ Y_{m+n})); ψ_{m}^{⅋^{2}}((X_{1},...,X_{m}),(Y_{1},...,Y_{m})) ⊗ ϕ_{n}^{⅋^{2}}((X_{m+1},...),(...,Y_{m+n})); _{[\begin{matrix}X_{1} ⊗ ⋯ ⊗ X_{n} & X_{m+1} ⊗ ⋯ ⊗ X_{m+n} \\ Y_{1} ⊗ ⋯ ⊗ Y_{m} & Y_{m+1} ⊗ ⋯ ⊗ Y_{m+n} \end{matrix}]}]

is equal to ψ^{⊗^{m+n}}. Thus, we have a proof by induction that ϕ_{n}^{⅋^{2}}⟨⟩ = ψ^{⊗^{n}}(). The dual argument can be applied, using Equation (31) and the right part of Equation (34) to give ψ_{n}^{⊗^{2}} = ϕ^{⅋^{n}}.

Now Figure 1 says that

\xymatrix{ &  & (F X ⊗ GY) ⅋ (F X′ ⊗ GY′) ⅋ (F X′′ ⅋ GY′′) \\  & _{[\begin{matrix}F X & GY \\ F X′ & GY′ \\ F X′′ & GY′′ \end{matrix} ]} \ar[dr] \\  &  & (F X ⅋ F X′ ⅋ F X′′) ⊗ (GY ⅋ GY′ ⅋ GY′′) \\ ψ_{3}^{F} (X, X′, X′′) ⊗ ψ_{3}^{G}(Y, Y′, Y′′) \ar[drr] \\  &  & F (X ⅋ X′ ⅋ X′′) ⊗ G(Y ⅋ Y′ ⅋ Y′′)}

is ψ_{3}^{F ˆ⊗G}((X, Y), (X′Y′), (X′′, Y′′)), which is the process that gives us ψ_{3}^{F ˆ⊗G} from ψ^{F ˆ⊗G}. This process can be iterated to give (dropping the exact typing)

ψ_{n}^{F ⊗G} = (ψ_{n}^{F} ⊗ ψ_{n}^{G}) ∘ ψ_{n}^{⊗^{2}} .

If we put F = ⊗^{m}, G = ⊗^{p} we get

ψ_{n}^{⊗^{m+p}} = (ψ_{n}^{⊗^{m}} ⊗ ψ_{n}^{⊗^{p}}) ∘ ψ_{n}^{⊗^{2}} ,  (36)

and from Equation (32) we also get (dropping the same kind of details, which also dispenses us from distinguishing between ψ() and ψ⟨⟩)

ϕ_{m+p}^{⅋^{n}} = (ϕ_{m}^{⅋^{n}} ⊗ ϕ_{p}^{⅋^{n}}) ∘ ϕ_{m+p}^{⅋^{n}} ,

and since we have already established ψ_{n}^{⊗^{2}} = ϕ^{⅋^{n}} we get a proof by induction of the desired ψ_{n}^{⊗^{m}}() = ϕ_{m}^{⅋^{n}}⟨⟩; let us write θ_{n,m} for that natural transformation—i.e., (n, m)-ary Medial. Equation (31) is an associative “vertical composition” of Medials, write it (−) ∗ (−), that allows us to construct and show θ_{n+n′,m} = θ_{n,m} ∗ θ_{n′,m}, while Equations (32) and (36) give us an associative “horizontal composition”, write it (−) · (−) that allow us to get θ_{n,m+m′} = θ_{n,m} · θ_{n,m′}. Thus the exchange law holds trivially:

(θ_{n,m} ∗ θ_{n′,m}) · (θ_{n,m′} ∗ θ_{n′,m′}) = (θ_{n,m} · θ_{n,m′}) ∗ (θ_{n′,m} · θ_{n′,m′}) = θ_{n+n′,m+m′} ,

and there are an enormous lot of ways to decompose a large n×m matrix as a combination of horizontal/vertical composites of smaller ones, and we know they all yield the same (n, m)-ary Medial; this is illustrated in more detail in [DP07], which shows moreover that any combination of Medials that has the type of an (n, m)-ary Medial will be that (n, m)-ary Medial.

Acknowledgements I want to thank the following people, who contributed in several ways in making this paper what it is: Rick Blute, Eugenia Cheng, Alessio Guglielmi, Richard McKinley, Luigi Santocanale, and Lutz Straßburger.

References

[Bar91] Michael Barr. ∗-Autonomous categories and linear logic. Mathematical Structures in Computer Science, 1(2):159–178, 1991.

[Bén73] Jean Bénabou. Les distributeurs. Technical Report 33, Inst. de Math. Pure et Appliquée, Université Catholique de Louvain, 1973.

[BFSV03] C. Balteanu, Z. Fiedorowicz, R. Schwänzl, and R. Vogt. Iterated monoidal categories. Advances in Mathematics, 176:277–349, 2003.

[Bla92] A. Blass. A games semantics of linear logic. Annals of Pure and Applied Logic, 56:183–220, 1992.

[Blu93] R. Blute. Linear logic, coherence and dinaturality. Theoretical Computer Science, 115(1):3–41, 1993.

[BPS06] R. Blute, P. Panangaden, and S. Slavnov. Deep inference and probabilistic coherence spaces. Unpublished, 2006.

[Brü03] Kai Brünnler. Deep Inference and Symmetry in Classical Proofs. PhD thesis, Technische Universität Dresden, 2003.

[BT01] Kai Brünnler and Alwen Fernanto Tiu. A local system for classical logic. In R. Nieuwenhuis and A. Voronkov, editors, LPAR 2001, volume 2250 of Lecture Notes in Artificial Intelligence, pages 347–361. Springer-Verlag, 2001.

[Bur93] Albert Burroni. Higher-dimensional word problems with applications to equational logic. Theoretical Computer Science, 115(1):46–62, 1993.

[CS97a] R. Cockett and R. Seely. Weakly distributive categories. J. Pure and Appl. Algebra, 173:133–173, 1997.

[CS97b] R. Cockett and R. A. G Seely. Proof theory for full intuitionistic linear logic, bilinear logic and mix categories. Theory and Appl. of Categories, 3, 1997.

[DP04] K. Došen and Z. Petrić. Proof-Theoretical Coherence. KCL Publications, London, 2004.

[DP07] Kosta Došen and Zoran Petrić. Intermutation. Preprint, arXiv:math.CT/0701325v1, 2007.

[dPA04] V. de Paiva and Schalk A. Poset-valued sets or how to build models for linear logics. Theoretical Computer Science, 315(1):83–107, 2004.

[Ehr93] Th. Ehrhard. Hypercoherences, a strongly stable model of linear logic. Mathematical Structures in Computer Science, 3:365–385, 1993.

[EK66] S. Eilenberg and G. M. Kelly. Closed categories. In S. Eilenberg, D.K. Harrison, S. MacLane, and H. Roehrl, editors, Proceedings of the La Jolla Conference in Categorical Algebra, pages 421–562. Springer, 1966.

[Fil89] Andrzej Filinski. Declarative continuations and categorical duality. Master’s thesis, University of Copenhagen, August 1989. DIKU Report 89/11.

[Fox76] T. Fox. Coalgebras and cartesian categories. Communications in Algebra, 4(7):665–667, 1976.

[FP04a] Carsten Führmann and David Pym. On the geometry of interaction for classical logic. preprint, 2004.

[FP04b] Carsten Führmann and David Pym. On the geometry of interaction for classical logic (extended abstract). In 19th Annual IEEE Symposium on Logic in Computer Science (LICS), pages 211–220, 2004.

[FP05] Carsten Führmann and David Pym. Order-enriched categorical models of the classical sequent calculus. J. Pure App. Algebra, 204(1):21–68, 2005.

[FY89] P. J. Freyd and D. Yetter. Braided compact closed categories with applications to low dimensional topology. Advances in Math., 77:156–182, 1989.

[Gir89] Jean-Yves Girard. Geometry of interaction 1: Interpretation of System F. In R. Ferro et al., editor, Logic Colloquium 88, pages 221–260. North-Holland, 1989.

[Gir91] J.-Y. Girard. A new constructive logic: Classical logic. Math. Stuct. in Comp. Sci, 1:255–296, 1991.

[GLT89] Jean-Yves Girard, Yves Lafont, and Paul Taylor. Proofs and Types. Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 1989.

[Gri90] Th. Griffin. A formulae-as-types notion of control. In Principles of Programming Languages, pages 47–58. ACM Press, 1990.

[Gug07] Alessio Guglielmi. A system of interaction and structure. ACM Transac. on Comp. Logic, 8(1), 2007.

[Hyl04] J. Martin E. Hyland. Abstract interpretation of proofs: Classical propositional calculus. In Jerzy Marcinkowski and Andrzej Tarlecki, editors, Computer Science Logic, CSL 2004, volume 3210 of LNCS, pages 6–21. Springer-Verlag, 2004.

[Joy81] A. Joyal. Une théorie combinatoire des séries formelles. Advances in Mathematics, 42:1–82, 1981.

[Kas95] Ch. Kassel. Quantum Groups. Graduate Texts in Mathematics. Springer, 1995.

[Lam94] J. Lambek. Bilinear logic in algebra and linguistics. In J.Y. Girard, Y. Lafont, and L. Regnier, editors, Advances in Linear Logic, volume 222 of London Math. Soc. Lec. Notes, pages 43–59. Cambridge University Press, 1994.

[Lam95] François Lamarche. Generalizing coherence spaces and hypercoherences. In Michael Mislove, editor, Proceedings of MFPS 1995, first issue of Electronic Notes in Theoretical Computer Science. North-Holland, 1995.

[Law73] W. Lawvere. Metric spaces, generalized logic and closed categories. Rendiconti del Seminario Matematico e Fisico di Milano, XLIII:135–166, 1973. Available as a TAC reprint: http://www.tac.mta.ca/tac/reprints/articles/1/tr1.pdf.

[Loa94] R. Loader. Totality and full completeness. In S. Abramsky, editor, Ninth Annual IEEE Symposium on Logic In Computer Science (LICS), pages 292–298. IEEE Computer Society Press, 1994.

[LS86] J. Lambek and P. J. Scott. Introduction to Higher Order Categorical Logic, volume 7 of Cambridge studies in advances mathematics. Cambridge University Press, 1986.

[LS05a] F. Lamarche and L. Straßburger. Constructing free boolean categories. In LICS Proceedings. IEEE Press, 2005.

[LS05b] F. Lamarche and L. Straßburger. Naming proofs in classical logic. In P. Urzyczyn, editor, TLCA Proceedings, volume 3461 of LNCS, pages 246–261. Springer, 2005.

[LS06] F. Lamarche and L. Straßsburger. From proof nets to the free ∗-automonous category. Logical Methods in Computer Science, 2(4:3), 2006.

[Mac71] Saunders Mac Lane. Categories for the Working Mathematician. Springer-Verlag, Berlin, 1971.

[McK05a] Richard McKinley. New bureaucracy/coherence. Email to the Frogs mail-

ing list on 2005-06-03, archived at http://news.gmane.org/gmane.science.
mathematics.frogs, 2005.

[McK05b] Richard McKinley. Virtual propositions: A sequent calculus for medial logic. Talk Given in Dresden, Dec 2005.

[McK06] Richard McKinley. Categorical Models of First-order Classical Proofs. PhD thesis, University of Bath, 2006.

[NPW81] M. Nielsen, G. Plotkin, and G. Winskel. Petri nets, event structures and domains, part I. Theoretical Computer Science, 13(1):85–108, 1981.

[NW04] M. Nygaard and G. Winskel. Domain theory for concurrency. Theoretical Computer Science, 316:153–190, 2004.

[Ong96] C.-H. L. Ong. A semantical view of classical proofs: Type-theoretic, categorical and denotational characterizations. In Eleventh Annual IEEE Symposium on Logic in Computer Science (LICS), pages 230–241. IEEE Press, 1996.

[Par92] Michel Parigot. λμ-calculus: An algorithmic interpretation of classical natural deduction. In Logic Programming and Automated Reasoning, LPAR 1992, volume 624 of LNAI, pages 190–201. Springer-Verlag, 1992.

[Rob03] Edmund P. Robinson. Proof nets for classical logic. Journal of Logic and Computation, 13:777–797, 2003.

[See89] R. Seely. Linear logic, ∗-autonomous categories and cofree coalgebras. In J. Gray and A. Scedrov, editors, Categories in Computer Science and Logic, volume 92 of Contemporary Mathematics. Am. Math. Soc, 1989.

[Sel01] Peter Selinger. Control categories and duality: on the categorical semantics of the lambda-mu calculus. Mathematical Structures in Computer Science, 11:207– 260, 2001.

[Sim95] Alex Simpson. Categorical completeness results for the simply typed lambda calculus. In M. Dezani and G. Plotkin, editors, Proceedings of TLCA95, volume 902 of Lect. Notes in Comp. Sci., pages 414–427. Springer, 1995.

[SR98] Thomas Streicher and Bernhard Reus. Classical logic, continuation semantics and abstract machines. Journal of Functional Programming, 8(6):543–572, 1998.

[Str05] Lutz Straßburger. From deep inference to proof nets. In Structures and Deduction — The Quest for the Essence of Proofs (Satellite Workshop of ICALP 2005), 2005. On the web at http://www.ps.uni-sb.de/˜ lutz/papers/deepnet.pdf.

[Str07] Lutz Straßburger. On the axiomatization of Boolean categories, with or without Medial. Theory and Applications of Categories, 18:471–533, 2007.

[Tiu06] A. F. Tiu. A system of interaction and structure II: The need for deep inference. Logical Methods in Comp. Science, 2(4):1–24, 2006.

[Wra75] G. C. Wraith. Lectures on elementary topoi. In F. W. Lawvere, C. Maurer, and G. C. Wraith, editors, Model Theory and Topoi, volume 445 of Lect. Notes in Math., pages 114–205. Springer, 1975.

Loria & INRIA-Lorraine, Projet Calligramme 615, rue du Jardin Botanique 54602 Villers-lès-Nancy, France

Email: Francois.Lamarche@loria.fr

This article may be accessed at http://www.tac.mta.ca/tac/ or by anonymous ftp at

ftp://ftp.tac.mta.ca/pub/tac/html/volumes/18/17/18-17.{dvi,ps,pdf}

THEORY AND APPLICATIONS OF CATEGORIES (ISSN 1201-561X) will disseminate articles that significantly advance the study of categorical algebra or methods, or that make significant new contributions to mathematical science using categorical methods. The scope of the journal includes: all areas of pure category theory, including higher dimensional categories; applications of category theory to algebra, geometry and topology and other areas of mathematics; applications of category theory to computer science, physics and other mathematical sciences; contributions to scientific knowledge that make use of categorical methods. Articles appearing in the journal have been carefully and critically refereed under the responsibility of members of the Editorial Board. Only papers judged to be both significant and excellent are accepted for publication. Full text of the journal is freely available in .dvi, Postscript and PDF from the journal’s server at http://www.tac.mta.ca/tac/ and by ftp. It is archived electronically and in printed paper format.

Subscription information. Individual subscribers receive abstracts of articles by e-mail as they are published. To subscribe, send e-mail to tac@mta.ca including a full name and postal address. For institutional subscription, send enquiries to the Managing Editor, Robert Rosebrugh, rrosebrugh@mta.ca.

Information for authors. The typesetting language of the journal is TEX, and L^{A}TEX2e strongly encouraged. Articles should be submitted by e-mail directly to a Transmitting Editor. Please obtain detailed information on submission format and style files at http://www.tac.mta.ca/tac/.

Managing editor. Robert Rosebrugh, Mount Allison University: rrosebrugh@mta.ca

TEXnical editor. Michael Barr, McGill University: mbarr@barrs.org

Transmitting editors.

Richard Blute, Université d’ Ottawa: rblute@uottawa.ca Lawrence Breen, Université de Paris 13: breen@math.univ-paris13.fr Ronald Brown, University of North Wales: ronnie.profbrown (at) btinternet.com Aurelio Carboni, Università dell Insubria: aurelio.carboni@uninsubria.it Valeria de Paiva, Xerox Palo Alto Research Center: paiva@parc.xerox.com Ezra Getzler, Northwestern University: getzler(at)northwestern(dot)edu Martin Hyland, University of Cambridge: M.Hyland@dpmms.cam.ac.uk P. T. Johnstone, University of Cambridge: ptj@dpmms.cam.ac.uk G. Max Kelly, University of Sydney: maxk@maths.usyd.edu.au Anders Kock, University of Aarhus: kock@imf.au.dk Stephen Lack, University of Western Sydney: s.lack@uws.edu.au F. William Lawvere, State University of New York at Buffalo: wlawvere@acsu.buffalo.edu Jean-Louis Loday, Université de Strasbourg: loday@math.u-strasbg.fr Ieke Moerdijk, University of Utrecht: moerdijk@math.uu.nl Susan Niefield, Union College: niefiels@union.edu Robert Paré, Dalhousie University: pare@mathstat.dal.ca Jiri Rosicky, Masaryk University: rosicky@math.muni.cz Brooke Shipley, University of Illinois at Chicago: bshipley@math.uic.edu James Stasheff, University of North Carolina: jds@math.unc.edu Ross Street, Macquarie University: street@math.mq.edu.au Walter Tholen, York University: tholen@mathstat.yorku.ca Myles Tierney, Rutgers University: tierney@math.rutgers.edu Robert F. C. Walters, University of Insubria: robert.walters@uninsubria.it R. J. Wood, Dalhousie University: rjwood@mathstat.dal.ca