Theory and Applications of Categories, Vol. 18, No. 18, 2007, pp. 536–601.

ON THE AXIOMATISATION OF BOOLEAN CATEGORIES WITH AND WITHOUT MEDIAL

LUTZ STRASSBURGER

Abstract. The term “Boolean category” should be used for describing an object that is to categories what a Boolean algebra is to posets. More specifically, a Boolean category should provide the abstract algebraic structure underlying the proofs in Boolean Logic, in the same sense as a Cartesian closed category captures the proofs in intuitionistic logic and a ∗-autonomous category captures the proofs in linear logic. However, recent work has shown that there is no canonical axiomatisation of a Boolean category. In this work, we will see a series (with increasing strength) of possible such axiomatisations, all based on the notion of ∗-autonomous category. We will particularly focus on the medial map, which has its origin in an inference rule in KS, a cut-free deductive system for Boolean logic in the calculus of structures. Finally, we will present a category of proof nets as a particularly well-behaved example of a Boolean category.

1. Introduction

The questions “What is a proof?” and “When are two proofs the same?” are fundamental for proof theory. But for the most prominent logic, Boolean (or classical) propositional logic, we still have no satisfactory answers.

This is not only embarrassing for proof theory itself, but also for computer science, where Boolean propositional logic plays a major role in automated reasoning and logic programming. Also the design and verification of hardware is based on Boolean logic. Every area in which proof search is employed can benefit from a better understanding of the concept of proof in Boolean logic, and the famous NP-versus-coNP problem can be reduced to the question whether there is a short (i.e., polynomial size) proof for every Boolean tautology [CR79].

Usually proofs are studied as syntactic objects within some deductive system (e.g., tableaux, sequent calculus, resolution, …). This paper takes the point of view that these syntactic objects (also known as proof trees) should be considered as concrete representations of certain abstract proof objects, and that such an abstract proof object can be represented by a resolution proof tree and a sequent calculus proof tree, or even by several different sequent calculus proof trees.

From this point of view the motivation for this work is to provide an abstract algebraic

Received by the editors 2006-06-12 and, in revised form, 2007-10-05. Transmitted by R. Blute. Published on 2007-10-18. Reference corrected 2007-12-13. 2000 Mathematics Subject Classification: 03B05, 03G05, 03F03, 18D15, 18D35. Key words and phrases: Boolean category, *-autonomous category, proof theory, classical logic, proof

nets.

\begin{matrix}c \\ ◯ \end{matrix} Lutz Straßburger, 2007. Permission to copy for private use granted.

theory of proofs. Already Lambek [Lam68, Lam69] observed that such an algebraic treatment can be provided by category theory. For this, it is necessary to accept the following postulates about proofs:

• for every proof f of conclusion B from hypothesis A (denoted by f: A → B) and every proof g of conclusion C from hypothesis B (denoted by g: B → C) there is a uniquely defined composite proof g ∘ f of conclusion C from hypothesis A (denoted by g ∘ f: A → C),

• this composition of proofs is associative,

• for each formula A there is an identity proof 1_{A}: A → A such that for f: A → B we have f ∘ 1_{A} = f = 1_{B} ∘ f.

Under these assumptions the proofs are the arrows in a category whose objects are the formulae of the logic. What remains is to provide the right axioms for the “category of proofs”.

It seems that finding these axioms is particularly difficult for the case of Boolean logic. For intuitionistic logic, Prawitz [Pra71] proposed the notion of proof normalization for identifying proofs. It was soon discovered that this notion of identity coincides with the notion of identity that results from the axioms of a Cartesian closed category (see, e.g., [LS86]). In fact, one can say that the proofs of intuitionistic logic are the arrows in the free (bi-)Cartesian closed category generated by the set of propositional variables. An alternative way of representing the arrows in that category is via terms in the simply-typed λ-calculus: arrow composition is normalization of terms. This observation is well-known as the Curry-Howard-correspondence [How80].

In the case of linear logic, the relation to ∗-autonomous categories [Bar79] was noticed immediately after its discovery [Laf88, See89]. In the sequent calculus linear logic proofs are identified when they can be transformed into each other via “trivial” rule permutations [Laf95]. For multiplicative linear logic this coincides with the proof identifications induced by the axioms of a ∗-autonomous category [Blu93, SL04]. Therefore, we can safely say that a proof in multiplicative linear logic is an arrow in the free ∗-autonomous category generated by the propositional variables [BCST96, LS06, Hug05a].

But for classical logic no such well-accepted category of proofs exists. We can distinguish two main reasons. First, if we start from a Cartesian closed category and add an involutive negation^{1}, we get the collapse into a Boolean algebra, i.e., any two proofs f, g: A → B are identified. For every formula there would be at most one proof (see, e.g., [LS86, p.67] or the appendix of [Gir91] for details). Alternatively, starting from a ∗-autonomous category and adding natural transformations A → A ∧ A and A → t, i.e., the proofs for weakening and contraction, yields the same collapse.^{2}

1i.e., a natural isomorphism between A and the double-negation of A (in this paper denoted by ¯ Ā)

2Since we are dealing with Boolean logic, we will use the symbols ∧ and t for the tensor operation (usually ⊗) and the unit (usually 1 or I) in a ∗-autonomous category.

The second reason is that cut elimination in the sequent calculus for classical logic is not confluent. Since cut elimination is the usual way of composing proofs, this means that there is no canonical way of composing two proofs, let alone associativity of composition.

Consequently, for avoiding these two problems, we have to accept that (i) Cartesian closed categories do not provide an abstract algebraic axiomatisation for proofs in classical logic, and that (ii) the sequent calculus is not the right framework for investigating the identity of proofs in classical logic.

There have already been several accounts for a proof theory for classical logic based on the axioms of Cartesian closed categories. The first were probably Parigot’s λμcalculus [Par92] and Girard’s LC [Gir91]. The work on polarized proof nets by Laurent [Lau99, Lau03] shows that there is in fact not much difference between the two. Later, the category-theoretic axiomatisations underlying this proof theory has been investigated and the close relationship to continuations [Thi97, SR98] has been established, culminating in Selinger’s control categories [Sel01]. However, by sticking to the axioms of Cartesian closed categories, one has to sacrifice the perfect symmetry of Boolean logic.

In this paper, we will go the opposite way. In the attempt of going from a Boolean algebra to a Boolean category we insist on keeping the symmetry between ∧ and ∨. By doing this we have to leave the realm of Cartesian closed categories. That this is very well possible has recently been shown by several authors [DP04, FP04c, LS05a]. However, the fact that all three proposals considerably differ from each other suggests that there might be no canonical way of giving a categorical axiomatisation for proofs in classical logic.

We will provide a series of possible such axiomatisations with increasing strength. They will all build on the structure of a ∗-autonomous category in which every object has a monoid (and a comonoid) structure. In this respect it will closely follow the work of [FP04c] and [LS05a], but will differ from [DP04].

The approach that we take here is mainly motivated by the investigation in the complexity of proofs. Eventually, a good theory of proof identification should never identify two proofs if one is exponentially bigger than the other.

The main proof-theoretic inspiration for this work comes from the system SKS [BT01], which is a deductive system for Boolean logic within the formalism of the calculus of structures [Gug07, GS01, BT01]. A remarkable feature of the cut-free version of SKS, which is called KS, is that it can (cut-free) polynomially simulate not only sequent calculus and tableaux systems but also resolution and Frege-Hilbert systems [Gug04a, BG07]. This means that if a tautology has a polynomial size proof in any of these systems, then it has a cut-free polynomial size proof in KS. This ability of KS is a consequence of two features:

1. Deep inference: Instead of decomposing the formulae along their root connectives into subformulae during the construction of a proof, in KS inference rules are applied deep inside formulae in the same way as we know it from term rewriting.

2. The two inference rules switch and medial, which look as follows:

\begin{aligned}& F \{(A ∨ B) ∧ C\} \\ s \\ & F \{A ∨ (B ∧ C)\} \end{aligned}  and \begin{aligned}& F \{(A ∧ B) ∨ (C ∧ D)\} \\ m \\ & F \{(A ∨ C) ∧ (B ∨ D)\} \end{aligned} ,  (1)

where F { } stands for an arbitrary (positive) formula context and A, B, C, and D are formula variables.

From deep inference to algebra. Deep inference allows us to establish the relationship between proof theory and algebra in a much cleaner way than this is possible with shallow inference formalisms like the sequent calculus. The reason is that from a derivation in a deep inference formalism one can directly “read off the morphisms”. Take for example the following derivation in system KS:

\begin{aligned}& (A′ ∧ B) ∨ (C ∧ D) \\ r \\ & (A ∧ B) ∨ (C ∧ D) \end{aligned} ; m ; (A ∨ C) ∧ (B ∨ D)  (2)

where A, A′, B, C, and D are arbitrary formulae, and r is any inference rule taking A′ to A. In category-theoretic language this would be written as a composition of maps:

\xymatrix{(A′ ∧ B) ∨ (C ∧ D) \ar[r]^{(r∧B)∨(C∧D)} & (A ∧ B) ∨ (C ∧ D) \ar[r]^{m_{A,B,C,D}} & (A ∨ C) ∧ (B ∨ D)}

where m_{A,B,C,D}: (A ∧ B) ∨ (C ∧ D) → (A ∨ C) ∧ (B ∨ D) is called the medial map, and r: A′ → A is the map corresponding to the rule r. System KS also allows the derivation

\begin{aligned}& (A′ ∧ B) ∨ (C ∧ D) \\ m \\ & (A′ ∨ C) ∧ (B ∨ D) \end{aligned} ; r ; (A ∨ C) ∧ (B ∨ D)  (3)

From the proof-theoretic point of view it makes perfect sense to identify the two derivations in (2) and (3) because they do “essentially” the same. This is what Guglielmi calls bureaucracy of type B [Gug04c]. In the language of category theory, the identification of (2) and (3) is saying that the diagram

[figure: (A′ ∧ B) ∨ (C ∧ D); m_{A′,B,C,D}; (A′ ∨ C) ∧ (B ∨ D); (r∨C)∧(B∨D); (A ∧ B) ∨ (C ∧ D); (r∧B)∨(C∧D); (A ∨ C) ∧ (B ∨ D); m_{A,B,C,D}]  (4)

has to commute, which exactly means that the medial map has to be natural.

For deep inference, Guglielmi also introduces the notion of bureaucracy of type A [Gug04b], which is the formal distinction between the derivations

\begin{aligned}& A′ ∧ B′ \\ r_{2} \\ & A′ ∧ B \end{aligned} ; r_{1} ; A ∧ B  and \begin{aligned}& A′ ∧ B′ \\ r_{1} \\ & A ∧ B′ \end{aligned} ; r_{2} ; A ∧ B  (5)

where rule r_{1} takes A′ to A, and rule r_{2} takes B′ to B. Proof-theoretically, the two derivations in (5) are “essentially” the same, so it makes sense to identify them. Translating this into category theory means to say that the operation ∧ is a bifunctor.

However, it is not always the case that the demands of algebra and proof theory coincide so nicely. Sometimes they contradict each other, which causes “creative tensions” [LS06]. One example is the treatment of units. Proof-theoretically it might be desirable to distinguish between the following two proofs in the sequent calculus (here t stands for “truth” and f for “falsum”):

axiom(true) ; ⊢ t weakening  and ⊢ t, f  axiom(identity) ⊢ t, f  (6)

This distinction is made, for example, by the proof nets presented in [LS05b]. From the algebraic point of view, this causes certain difficulties: In [LS05a] the concept of weak units has been introduced in order to give a clean algebraic treatment to the distinction in (6). However, in this paper we will depart from this and use proper units instead. This is from the algebraic point of view more reasonable and simplifies the theory considerably. But it forces the identification of the two proofs in (6).

Some remarks about switch and medial. The inference rule switch in (1), or the switch map s_{A,B,C}: (A∨B)∧C → A∨(B ∧C) has already been well investigated from the viewpoint of proof theory [Gug07], as well as from the viewpoint of category theory, where it is also called weak distributivity [HdP93, CS97b], linear distributivity, or dissociativity [DP04]. On the other hand, the medial rule or medial map m_{A,B,C,D}: (A∧B)∨(C ∧D) → (A ∨ C) ∧ (B ∨ D) has not yet been so thoroughly investigated. Only very recently Lamarche [Lam07] started to study the consequences of the presence of the medial map in a ∗-autonomous category, and Došen and Petrić [DP07] investigate it under the name intermutation from the viewpoint of coherence (but without taking the switch map into account).

Seen from the deductive point of view, the two rules switch and medial have certain similarities:

• switch allows the reduction of the identity rule and the cut rule to atomic form, and medial allows the reduction of the contraction rule (and the cocontraction rule) to atomic form (see [BT01] for details),

• switch and medial are both self-dual, and

• they look similar, as can bee seen in (1). In fact, recent work shows that they can both be seen as instance of a single more general inference rule [Gug02, Gug05].

However, from the algebraic point of view, they are quite different: Switch is a consequence of more primitive properties, namely the associativity of ∧ and ∨ and the de Morgan duality between the two operations^{3}, whereas medial has to be put as additional primitive, if we want it in the category.^{4}

Outline of the paper. In this work we will present a series of axioms that seem reasonable (from the proof-theoretic as well as from the algebraic points of view) to have in a Boolean category. While introducing axioms, we will also show their consequences. Some of the axioms presented here coincide with axioms given in the accompanying paper [Lam07] which has been written at the same time as this paper and appears in the same issue of this journal. This overlap is certainly not surprising. However, there are two main differences between the two papers. First, while [Lam07] works in the minimal setting of a ∗-autonomous category with medial (or with “linear logic plus medial”), we assume from the beginning full classical propositional logic, i.e., the presence of weakening and contraction. Second (and more importantly) we are staying in the realm of syntax, whereas [Lam07] is primarily concerned with the construction of concrete models for classical proofs.

It is in fact a problem of the subject in general that there are only very few concrete examples of (symmetric) models of classical proofs. One of them is the category Rel of sets and relations [Hyl04], but it has the common problem that it identifies disjunction and conjunction. From the proof-theoretic point of view this kind of degenerate model is not very interesting. In fact, the investigation of medial is pointless in this setting.^{5} Here the work in [Lam07] provides some breakthroughs towards new kind of models in which disjunction and conjunction do not coincide.

In the end of this paper, we will also give a concrete example of a Boolean category, namely a variation of the proof nets of [LS05b]. Although this example might be considered “only syntactic”, it nonetheless shows that the axioms presented here do not lead to the collapse into a Boolean algebra. Furthermore, this last section can be read independently by the reader interested only in proof nets and not in category theory.

This paper is another attempt to be accessible to both the category theorist and the proof theorist. Since it is mainly about algebra, we use here the language of category theory. Nonetheless, the seasoned proof theorist might find it easier to understand if he substitutes everywhere “object” by “formula” and “map”/“morphism”/“arrow” by “proof”. Every commuting diagram in the paper is nothing but an equation between proofs written in a deep inference formalism. In order to make the paper easier accessible to proof theorists, all statements are proved in more detail than the seasoned category theorist might find appropriate.

3Nonetheless it has been investigated in [CS97b] from the category theoretic viewpoint under the assumption that negation (and therefore the de Morgan duality) is absent.

4This fact raises an open problem: can we find simple primitives from which medial arises naturally, in the same way as switch arises naturally from associativity and duality?

5For this reason, we will leave it as an exercise to the reader to verify that Rel fulfills all the axioms presented in this paper.

2. What is a Boolean Category ?

Recall the analogy mentioned in the abstract: A Boolean category should be for categories, what a Boolean algebra is for posets. This leads to the following definition:

2.1. Definition. We say a category 𝒞 is a B0-category if there is a Boolean algebra ℬ and a mapping F: 𝒞 → ℬ from objects of 𝒞 to elements of ℬ, such that for all objects A and B in 𝒞, we have F (A) ≤ F (B) in ℬ if and only if there is an arrow f: A → B in 𝒞.

In other words, a B0-category is a category whose image under the forgetful functor from the category of categories to the category of posets is a Boolean algebra. From the proof-theoretic point of view one should have that there is a proof from A to B if and only if A ⇒ B is a valid implication. However, from the algebraic point of view there are many models, including the category Rel of sets and relations, as well as the models constructed in the in the accompanying paper [Lam07], which have a map between any two objects A and B. Note that these models are not ruled out by Definition 2.1 because there is the trivial one-element Boolean algebra. In any case, we can make the following (trivial) observation.

2.2. Observation. In a B0-category, we can for any pair of objects A and B, provide objects A ∧ B and A ∨ B and Ā, and there are objects t and f, such that there are maps

α̂_{A,B,C}: A ∧ (B ∧ C) → (A ∧ B) ∧ C  α̌_{A,B,C}: A ∨ (B ∨ C) → (A ∨ B) ∨ C
σ̂_{A,B}: A ∧ B → B ∧ A  σ̌_{A,B}: A ∨ B → B ∨ A
ϱ̂_{A}: A ∧ t → A  ϱ̌_{A}: A ∨ f → A
λ̂_{A}: t ∧ A → A  λ̌_{A}: f ∨ A → A
î_{A}: A ∧ Ā → f  ǐ_{A}: t → Ā ∨ A
s_{A,B,C}: (A ∨ B) ∧ C → A ∨ (B ∧ C)
m_{A,B,C,D}: (A ∧ B) ∨ (C ∧ D) → (A ∨ C) ∧ (B ∨ D)
Δ_{A}: A → A ∧ A  ∇_{A}: A ∨ A → A
Π^{A}: A → t  ⨿^{A}: f → A

(7)

for all objects A, B, and C. This can easily be shown by verifying that all of them correspond to valid implications in Boolean logic. Conversely, a category in which every arrow can be given as a composite of the ones given above by using only the operations of ∧, ∨, and the usual arrow composition, is a B0-category. This is a consequence of the completeness of system SKS [BT01], which is a deep inference deductive system for Boolean logic incorporating the maps in (7) as inference rules.

Note that Definition 2.1 is neither enlightening nor useful. It is necessary to add some additional structure in order to obtain a “nicely behaved” theory of Boolean categories. However, as already mentioned in the introduction, the naive approach of adding structure, namely adding the structure of a bi-Cartesian closed category (also called Heyting category) with an involutive negation leads to collapse: Every Boolean category in that strong sense is a Boolean algebra. The hom-sets are either singletons or empty. This observation has first been made by André Joyal, and the proof can be found, for example, in [LS86], page 67. For the sake of completeness, we repeat the argument here: First, recall that in a Cartesian closed category, we have, among other properties, (i) binary products, that we (following the notation of this paper) denote by ∧, (ii) a terminal object t with the property that t ∧ A ≅ A for all objects A, and (iii) a natural bijection between the maps f: A ∧ B → C and f^{∗}: A → B ⇒ C, where B ⇒ C denotes the exponential of B and C. Going from f to f^{∗} is also known as currying. Adding an involutive negation means adding a contravariant endofunctor \overline{(−)} such that there is a natural bijection between maps f: A → B and f̄: B̄ → Ā. It also means that there is an initial object f = t̄. Hence, we have in particular for all objects A and B, that

Hom(A, B) ≅ Hom(t ∧ A, B) ≅ Hom(t, A ⇒ B) ≅ Hom(\overline{A ⇒ B}, f) .  (8)

Now observe that whenever we have an object X such that the two projections

π_{1}, π_{2} : X ∧ X → X

are equal, then for all objects Y, any two maps f, g: Y → X are equal, because

f = π_{1} ∘ ⟨f, g⟩ = π_{2} ∘ ⟨f, g⟩ = g .  (9)

Now note that since f is initial, there is exactly one map f → f ⇒ f, hence, by uncurrying there is exactly one map f ∧ f → f. Therefore, for every Y, there is at most one map Y → f. By (8), for all A, B, we have Hom(A, B) is either singleton or empty.

Recapitulating the situation, we have here two extremes of Boolean categories: no structure and too much structure. Neither of them is very interesting, neither for proof theory nor for category theory. But there is a whole universe between the two, which we will start to investigate now. On our path, we will stick to (8) and carefully avoid to have (9). This is what makes our approach different from control categories [Sel01], in which the equation f = π_{1} ∘ ⟨f, g⟩ holds, but the rightmost bijection in (8) is absent.

3. ∗-Autonomous categories

Let us stress the fact that in a plain B0-category there is no relation between the maps listed in (7). In particular, there is no functoriality of ∨ and ∧, no naturality of α̂, σ̂, …, and no de Morgan duality. Adding this structure means exactly adding the structure of a ∗-autonomous category [Bar79].

Since we are working in classical logic, we will here use the symbols ∧, ∨, t, f for the usual ⊗, ⅋, 1, ⊥.

3.1. Definition. A B0-category 𝒞 is symmetric ∧-monoidal if the operation −∧− : 𝒞 × 𝒞 → 𝒞 is a bifunctor and the maps α̂_{A,B,C}, σ̂_{A,B}, ϱ̂_{A}, λ̂_{A} in (7) are natural isomorphisms that obey the following equations:

[figure: A ∧ (B ∧ (C ∧ D)); A∧α̂_{B,C,D}; A ∧ ((B ∧ C) ∧ D); α̂_{A,B∧C,D}; (A ∧ B) ∧ (C ∧ D); α̂_{A,B,C∧D}; (A ∧ (B ∧ C)) ∧ D; α̂_{A,B,C}∧D; ((A ∧ B) ∧ C) ∧ D; α̂_{A∧B,C,D}]

[figure: A ∧ (B ∧ C); α̂_{A,B,C}; A ∧ (C ∧ B); A∧σ̂_{B,C}; (A ∧ B) ∧ C; σ̂_{A∧B,C}; (A ∧ C) ∧ B; α̂_{A,C,B}; C ∧ (A ∧ B); α̂_{C,A,B}; (C ∧ A) ∧ B; σ̂_{A,C}∧B]

[figure: A ∧ (t ∧ B); α̂_{A,t,B}; (A ∧ t) ∧ B; ϱ̂_{A}∧B; A ∧ B; A∧λ̂_{B}]

[figure: A ∧ B; σ̂_{A,B}; B ∧ A; σ̂_{B,A}; A ∧ B; 1_{A∧B}]

The notion of symmetric ∨-monoidal is defined in a similar way.

An important property of symmetric monoidal categories is the coherence theorem [Mac63], which says that every diagram containing only natural isomorphisms built out of α̂, σ̂, ϱ̂, λ̂, and the identity 1 via ∧ and ∘ must commute (for details, see [Mac71] and [Kel64]).^{6}

As a consequence of the coherence theorem, we can omit certain parentheses to ease the reading. For example, we will write A ∧ B ∧ C ∧ D for (A ∧ B) ∧ (C ∧ D) as well as for A ∧ ((B ∧ C) ∧ D). This can be done because there is a uniquely defined “coherence isomorphism” between any two of these objects.

6In [Kel64], Kelly provides some simplifications to MacLane’s conditions in [Mac63]. For example, the equations ϱ̂_{t} = λ̂_{t} : t ∧ t → t and ϱ̂_{A} ∘ σ̂_{t,A} = λ̂_{A}: t ∧ A → A follow from the ones in Definition 3.1.

Let us now turn our attention to a very important feature of Boolean logic: the duality between ∧ and ∨. We can safely say that it is reasonable to ask for this duality also in a Boolean category. That means, we are asking for ¯ Ā ≅ A and \overline{A ∧ B} ≅ Ā∨B̄. At the same time we ask for the possibility of transposition (or currying): The proofs of A ∧ B → C are in one-to-one correspondence with the proofs of A → B̄ ∨ C. This is exactly what makes a monoidal category ∗-autonomous.

3.2. Definition. A B0-category 𝒞 is ∗-autonomous if it is symmetric ∧-monoidal and is equipped with a contravariant functor \overline{(−)} : 𝒞 → 𝒞, such that \overline{\overline{(−)}}: 𝒞 → 𝒞 is a natural isomorphism and such that for any three objects A, B, C there is a natural bijection

Hom_{𝒞} (A ∧ B, C) ≅ Hom_{𝒞} (A, B̄ ∨ C) .  (⋆)

where the bifunctor − ∨ − is defined via A ∨ B = \overline{B̄ ∧ Ā}.^{7} We also define f = t̄.

Clearly, if a B0-category 𝒞 is ∗-autonomous, then it is also ∨-monoidal with α̌_{A,B,C} = \overline{α̂_{C̄,B̄,Ā}}, σ̌_{A,B} = \overline{σ̂_{B̄,Ā}}, ϱ̌_{A} = \overline{λ̂Ā}, λ̌_{A} = \overline{ϱ̂Ā}.

Note that our definition is not the original one, but it is not difficult to show the equivalence, and this was already done in [Bar79]. For further information, see also [BW99, Bar91, Hug05a, LS06].

Let us continue with stating some well-known facts about ∗-autonomous categories (for proofs of these facts, see e.g. [LS06]). Via the bijection (⋆) we can assign to every map f: A → B ∨ C a map g: A ∧ B̄ → C, and vice versa. We say that f and g are transposes of each other if they determine each other via (⋆). We will use the term “transpose” in a very general sense: given objects A, B, C, D, E such that D ≅ A ∧ B and E ≅ B̄ ∨ C, then any f: D → C uniquely determines a g: A → E, and vice versa. Also in that general case we will say that f and g are transposes of each other. For example, λ̂_{A}: t ∧ A → A and ϱ̌_{A}: A → A ∨ f are transposes of each other, and another way of transposing them yields the maps

ǐ_{A}: t → Ā ∨ A and î_{A}: A ∧ Ā → f .

If we have f: A → B ∨ C and b: B′ → B, then

\xymatrix{A ∧ B′ \ar[r]^{A∧b} & A ∧ B \ar[r]^{f} & C & is transpose of & A \ar[r]^{g} & B̄ ∨ C \ar[r]^{b̄∨C} & \overline{B′} ∨ C}  (10)

where g is transpose of f.

Let us now transpose the identity 1_{B∨C}: B ∨ C → B ∨ C. This yields the evaluation map eval : (B ∨ C) ∧ C̄ → B. Taking the ∧ of this with 1_{A}: A → A and transposing back determines a map s_{A,B,C}: A∧(B∨C) → (A∧B)∨C that is natural in all three arguments, and that we call the switch map [Gug07, BT01]^{8}. In a similar fashion we obtain maps (A∨B)∧C → A∨(B ∧C) and A∧(B ∨C) → B ∨(A∧C) and (A∨B)∧C → (A∧C)∨B. Alternatively these maps can be obtained from s by composing with σ̂ and σ̌. For this reason we will use the term “switch” for all of them, and denote them by s_{A,B,C} if it is clear from context which one is meant, as for example in the two diagrams

7Although we live in the commutative world, we invert the order of the arguments when taking the negation.

8To category theorists it is probably better known under the names weak distributivity [HdP93, CS97b] or linear distributivity. However, strictly speaking, it is not a form of distributivity. An alternative is the name dissociativity [DP04].

[figure: (A ∨ B) ∧ (C ∨ D); s_{A,B,C∨D}; A ∨ (B ∧ (C ∨ D)); A∨s_{B,C,D}; ((A ∨ B) ∧ C) ∨ D; s_{A∨B,C,D}; A ∨ (B ∧ C) ∨ D; s_{A,B,C}∨D]  (11)

and

[figure: A ∧ (B ∨ C) ∧ D; A∧s_{B,C,D}; A ∧ (B ∨ (C ∧ D)); s_{A,B,C∧D}; ((A ∧ B) ∨ C) ∧ D; s_{A,B,C}∧D; (A ∧ B) ∨ (C ∧ D); s_{A∧B,C,D}]  (12)

which commute in any ∗-autonomous category. Sometimes we will denote the map defined by (11) by t̂_{A,B,C,D}: (A ∨ B) ∧ (C ∨ D) → A ∨ (B ∧ C) ∨ D, called the tensor map^{9} and the one of (12) by ť_{A,B,C,D}: A ∧ (B ∨ C) ∧ D → (A ∧ B) ∨ (C ∧ D), called the cotensor map.

Note that the switch map is self-dual, while the two maps t̂ and ť are dual to each other, i.e.,

[figure: \overline{(A ∧ B) ∨ C}; \overline{s_{A,B,C}}; \overline{A ∧ (B ∨ C)}; ≅; C̄ ∧ (B̄ ∨ Ā); ≅; (C̄ ∧ B̄) ∨ Ā; s_{C̄,B̄,Ā}]  (13)

and

[figure: \overline{(A ∧ B) ∨ (C ∧ D)}; \overline{ť_{A,B,C,D}}; \overline{A ∧ (B ∨ C) ∧ D}; ≅; (D̄ ∨ C̄) ∧ (B̄ ∨ Ā); ≅; D̄ ∨ (C̄ ∧ B̄) ∨ Ā; t̂_{D̄,C̄,B̄,Ā}]  (14)

where the vertical maps are the canonical isomorphisms determined by the ∗-autonomous structure. Another property of switch that we will use later is the commutativity of the following diagrams:

[figure: (A ∨ B) ∧ t; s_{A,B,t}; A ∨ B; ϱ̂_{A∨B}; A ∨ (B ∧ t); A∨ϱ̂_{B}; (f ∨ A) ∧ B; s_{f,A,B}; A ∧ B; λ̌_{A}^{−1}∧B; f ∨ (A ∧ B); λ̌_{A∨B}^{−1}]  (15)

9This map describes precisely the tensor rule in the sequent system for linear logic.

4. Some remarks on mix

In this section we will recall what it means for a ∗-autonomous category to have mix. Although most of the material of this section can also be found in [CS97a], [FP04a], [DP04], and [Lam07], we give here a complete survey since the main result, Corollary 4.3, is rather crucial for the following sections. This corollary essentially says that the mix-rule in the sequent calculus

\begin{aligned}⊢ Γ & ⊢ Δ \\ mix \\ & ⊢ Γ, Δ \end{aligned}

is a consequence of the fact that false implies true. Although this is not a very deep result, it might be surprising for logicians that a property of sequents (if two sequents can be proved independently, then they can be proved together) which does not involve any units comes out of an algebraic property concerning only the units.

4.1. Theorem. Let 𝒞 be a ∗-autonomous category and e: f → t be a map in 𝒞. Then

[figure: f ∧ f; e∧f; t ∧ f; λ̂_{f}; f ∧ t; f∧e; f; ϱ̂_{f}]  (16)

if and only if

[figure: t; λ̌_{t}^{−1}; f ∨ t; e∨t; t ∨ f; ϱ̌_{t}^{−1}; t ∨ t; t∨e]  (17)

if and only if

[figure: A ∧ B; A∧λ̌_{B}^{−1}; A ∧ (f ∨ B); s_{A,f,B}; (A ∧ f) ∨ B; (A∧e)∨B; (A ∨ f) ∧ B; ϱ̌_{A}^{−1}∧B; (A ∧ t) ∨ B; ϱ̂_{A}∨B; A ∨ (f ∧ B); s_{A,f,B}; A ∨ (t ∧ B); A∨(e∧B); A ∨ B; A∨λ̂_{B}]  (18)

for all objects A and B.

Proof. First we show that (16) implies (18). For this, chase

[figure: A ∧ B; λ̌_{B}^{−1}; ϱ̌_{A}^{−1}; (A ∨ f) ∧ B; s; λ̌_{B}^{−1}; A ∧ (f ∨ B); ϱ̌_{A}^{−1}; s; A ∨ (f ∧ B); e; λ̌_{B}^{−1}; (A ∨ f) ∧ (f ∨ B); s; s; (A ∧ f) ∨ B; ϱ̌_{A}^{−1}; e; A ∨ (t ∧ B); λ̌_{B}^{−1}; A ∨ (f ∧ (f ∨ B)); e; s; ((A ∨ f) ∧ f) ∨ B; s; e; (A ∧ t) ∨ B; ϱ̌_{A}^{−1}; A ∨ (t ∧ (f ∨ B)); s; A ∨ (f ∧ f) ∨ B; e; e; ((A ∨ f) ∧ t) ∨ B; s; A ∨ (t ∧ f) ∨ B; λ̂_{f}; A ∨ (f ∧ t) ∨ B; ϱ̂_{f}; A ∨ f ∨ B; λ̂_{f∨B}; λ̌_{B}; A ∨ f ∨ B; ϱ̂_{A∨f}; ϱ̌_{A}; A ∨ B; λ̂_{B}; λ̌_{B}^{−1}; A ∨ B; A ∨ B; ϱ̂_{A}; ϱ̌_{A}^{−1}]  (19)

The big triangle at the center is an application of (16). The two little triangles next to it are (variations of) (15), and the triangles at the bottom are trivial. The topmost square is functoriality of ∧, the square in the center is (11), and all other squares commute because of naturality of s, λ̂, ϱ̂, λ̌, and ϱ̌. Now observe that (18) commutes if and only if

[figure: A ∧ B; A∧λ̌_{B}^{−1}; A ∧ (f ∨ B); A∧(e∨B); A ∧ (t ∨ B); s_{A,t,B}; (A ∨ f) ∧ B; ϱ̌_{A}^{−1}∧B; (A ∧ t) ∨ B; ϱ̂_{A}∨B; (A ∨ t) ∧ B; (A∨e)∧B; A ∨ (t ∧ B); s_{A,t,B}; A ∨ B; A∨λ̂_{B}]  (20)

commutes (because of naturality of switch), and that the diagonals of (18) and (20) are the same map mix_{A,B}: A ∧ B → A ∨ B. Note that by the dual of (19) we get that (17) implies (20). Therefore we also get that (17) implies (18). Now we show that (20) implies (17). We will do this by showing that

\xymatrix{ & t \ar[dl]_{ϱ̌_{t}^{−1}} \ar[d]^{ϱ̂_{t}^{−1}=λ̂_{t}^{−1}} \ar[dr]^{λ̌_{t}^{−1}} \\ t ∨ f \ar[dr]_{t∨e} & t ∧ t \ar[d]^{_{mix_{t,t}}} & f ∨ t \ar[dl]^{e∨t} \\  & t ∨ t}  (21)

commutes. For this, consider

[figure: t; ϱ̂_{t}^{−1}; t ∧ t; ϱ̂_{t}; ϱ̌_{t}^{−1}∧t; t; (t ∨ f) ∧ t; ϱ̂_{t∨f}; (t∨e)∧t; t ∨ f; ϱ̌_{t}^{−1}; (t ∨ t) ∧ t; ϱ̂_{t∨t}; s_{t,t,t}; t ∨ t; t∨e; t ∨ (t ∧ t); t∨λ̂_{t}; t∨ϱ̂_{t}; t ∨ t]  (22)

which says that the left triangle in (21) commutes because the right down path in (22) is exactly the lower left path in (20). Similarly we obtain the commutativity of the right triangle in (21). In the same way we show that (18) implies (16), which completes the proof.

Therefore, in a ∗-autonomous category every map e: f → t obeying (16) uniquely determines a map mix_{A,B}: A ∧ B → A ∨ B which is natural in A and B. It can be shown that this mix map goes well with the twist, associativity, and switch maps:

4.2. Proposition. The map mix_{A,B}: A ∧ B → A ∨ B obtained from (18) is natural in both arguments and obeys the equations

[figure: A ∧ B; ^{mix^{A,B}}; A ∨ B; σ̌_{A,B}; B ∧ A; σ̂_{A,B}; B ∨ A; _{mix_{B,A}}]  (mix-σ̂)

and

[figure: A ∧ (B ∧ C); A∧mix_{B,C}; A ∧ (B ∨ C); ^{mix^{A,B∨C}}; s_{A,B,C}; A ∨ (B ∨ C); α̌_{A,B,C}; (A ∧ B) ∧ C; α̂_{A,B,C}; (A ∧ B) ∨ C; _{mix_{A∧B,C}}; (A ∨ B) ∨ C; mix_{A,B}∨C]  (mix-α̂)

Proof. Naturality of mix follows immediately from the naturality of switch. Equation (mix-σ̂) follows immediately from the definition of switch, and (mix-α̂) can be shown with a similar diagram as (19).

4.3. Corollary. In a ∗-autonomous category there is a one-to-one correspondence between the maps e: f → t obeying (16) and the natural transformations mix_{A,B}: A ∧ B → A ∨ B obeying (mix-σ̂) and (mix-α̂).

Proof. Whenever we have a map mix_{A,B}: A ∧ B → A ∨ B for all A and B, we can form the map

\xymatrix{e: f \ar[r]^{ϱ̂_{f}^{−1}} & f ∧ t \ar[r]^{^{mix^{f,t}}} & f ∨ t \ar[r]^{λ̌_{t}} & t}  (23)

One can now easily show that naturality of mix, as well as (mix-σ̂) and (mix-α̂) are exactly what is needed to let the map e: f → t defined in (23) obey equation (16). We leave the details to the reader. Hint: Show that both maps of (16) are equal to

\xymatrix{f ∧ f \ar[r]^{^{mix^{f,f}}} & f ∨ f \ar[r]^{λ̌_{f} =ϱ̌_{f}} & f} .

It remains to show that plugging the map of (23) into (18) gives back the same natural transformation mix_{A,B}: A ∧ B → A ∨ B we started from. Similarly, plugging in the the mix defined via (18) into (23) gives back the same map e: f → t that has been plugged into (18). Again, we leave the details to the reader.

Note that a ∗-autonomous category can have many different maps e: f → t with the property of Theorem 4.1, each of them defining its own natural mix obeying (mix-σ̂) and (mix-α̂).

5. ∨-Monoids and ∧-comonoids

The structure investigated so far is exactly the same as for proofs in linear logic (with or without mix). For classical logic, we need to provide algebraic structure for the maps ∇_{A}: A ∨ A → A and ⨿^{A}: f → A, as well as Δ_{A}: A → A ∧ A and Π^{A}: A → t, which are listed in (7). This is done via monoids and comonoids.

5.1. Definition. A B0-category has commutative ∨-monoids if it is symmetric ∨-mo-noidal and for every object A, the maps ∇_{A} and ⨿^{A} obey the equations

[figure: A ∨ (A ∨ A); α̌_{A,A,A}; A ∨ A; A∨∇_{A}; A; ∇_{A}; (A ∨ A) ∨ A; ∇_{A}∨A; A ∨ A; ∇_{A}; A ∨ A; σ̌_{A,A}; A; ∇_{A}; A ∨ A; ∇_{A}; A ∨ f; A∨⨿^{A}; A; ϱ̌_{A}; A ∨ A; ∇_{A}] (24)

Dually, we say that a B0-category has cocommutative ∧-comonoids if it is symmetric ∧-monoidal and for every object A, the maps Δ_{A} and Π^{A} obey the equations

[figure: A ∧ A; Δ_{A}∧A; (A ∧ A) ∧ A; α̂_{A,A,A}^{−1}; A; Δ_{A}; A ∧ A; Δ_{A}; A ∧ (A ∧ A); A∧Δ_{A}; A ∧ A; σ̂_{A,A}^{−1}; A; Δ_{A}; A ∧ A; Δ_{A}; A ∧ A; A∧Π^{A}; A; Δ_{A}; A ∧ t; ϱ̂_{A}^{−1}] (25)

Translated into the language of the sequent calculus (cf. [FP04c]), having the structure of a ∨-monoid, i.e., the equations in (24), means

(i) to force the identification of the two possible proofs of the shape

Λ ⊢ A, A, A, Γ ; contraction ; Λ ⊢ A, A, Γ contraction

Λ ⊢ A, Γ

(ii) to identify the two proofs

Λ ⊢ A, A, Γ ; exchange ; Λ ⊢ A, A, Γ
contraction  and
Λ ⊢ A, Γ

Λ ⊢ A, A, Γ ; contraction ; Λ ⊢ A, Γ

(iii) to say that the derivation

Λ ⊢ A, Γ ; weakening ; Λ ⊢ A, A, Γ contraction

Λ ⊢ A, Γ

is the same as doing nothing (i.e., the identity).

The equations in (25), i.e., the structure of an ∧-comonoid, forces the same identification on the left-hand side of the turnstile. See [FP04c] for a detailed discussion of this correspondence.

5.2. Remark. The (co)associativity of the maps Δ_{A} and ∇_{A} allows us to use the notation Δ_{A}^{2} : A → A ∧ A ∧ A and ∇_{A}^{2} : A ∨ A ∨ A → A.

5.3. Proposition. Let 𝒞 be a category with commutative ∨-monoids, and let

[figure: A ∨ f; A∨f; A; ϱ̌_{A}; A ∨ A; ∇_{A}]

commute for some f: f → A. Then f = ⨿^{A}.

Proof. This is a well-known fact from algebra: in a monoid the unit is uniquely defined. Written as diagram, the standard proof looks as follows:

[figure: f; λ̌_{f}^{−1}=ϱ̌_{f}^{−1}; f; f ∨ f; λ̌_{f}; ϱ̌_{f}; f∨f; ⨿^{A}∨f; f; f ∨ A; ⨿^{A}∨A; λ̌_{A}; A ∨ A; ∇_{A}; A ∨ f; A∨f; ϱ̌_{A}; f; f; A; f; ⨿^{A}]

Note that in the same way it follows that the counit in a comonoid is uniquely defined.

Although the operations ∧ and ∨ are not the product and coproduct in the categorytheoretic sense, we use the notation:

⟨f, g⟩ = (f ∧ g) ∘ Δ_{A}: A → C ∧ D and [f, h] = ∇_{C} ∘ (f ∨ h): A ∨ B → C  (26)

where f: A → C and g: A → D and h: B → C are arbitrary maps.

Another helpful notation (see [LS05a]) is the following:

\begin{matrix}Π_{A^{⫾}}^{B} = ϱ̂_{A} ∘ (A ∧ Π^{B}): A ∧ B → A & Π_{^{⫾}B}^{A} = λ̂_{B} ∘ (Π^{A} ∧ B): A ∧ B → B \\ ⨿_{A^{⫾}}^{B} = (A ∨ ⨿^{B}) ∘ ϱ̌_{A}^{−1} : A → A ∨ B & ⨿_{^{⫾}B}^{A} = (⨿^{A} ∨ B) ∘ λ̌_{B}^{−1} : B → A ∨ B \end{matrix}  (27)

Note that

∇_{A} ∘ ⨿_{^{⫾}A}^{A} = 1_{A} = ∇_{A} ∘ ⨿_{A^{⫾}}^{A} and Π_{^{⫾}A}^{A} ∘ Δ_{A} = 1_{A} = Π_{A^{⫾}}^{A} ∘ Δ_{A}  (28)

5.4. Definition. Let f: A → B be a map in a B0-category with commutative ∨-monoids and cocommutative ∧-comonoids. Consider the following four diagrams:

[figure: A ∨ A; f∨f; B ∨ B; ∇_{B}; A; ∇_{A}; B; f; f; ⨿^{A}; A; f; B; ⨿^{B}; A; f; B; Π^{B}; t; Π^{A}; A; f; B; Δ_{B}; A ∧ A; Δ_{A}; B ∧ B; f∧f]

We say that

• f preserves the ∨-multiplication if the left square commutes,

• f preserves the ∨-unit if the left triangle commutes,

• f preserves the ∧-counit if the right triangle commutes,

• f preserves the ∧-comultiplication if the right square commutes,

• f is a ∨-monoid morphism if the two left diagrams commute,

• f is a ∧-comonoid morphism if the two right diagrams commute,

• f is a quasientropy if both triangles commute,

• f is clonable if both squares commute,

• f is strong if all four diagrams commute.

5.5. Definition. A B1-category is a B0-category that is ∗-autonomous and has cocommutative ∧-comonoids.

Clearly, a B1-category also has commutative ∨-monoids with ∇ dual to Δ, and ⨿ dual to Π.

5.6. Remark. Definition 5.5 exhibits another “creative tension” between algebra and proof theory. From the algebraic point of view one should add the phrase “and all isomorphisms preserve the ∧-comonoid structure” because in a semantics of proofs this will probably be inevitable. But here we do not assume it from the beginning, but systematically give conditions that will ensure it in the end (cf. Theorem 7.19 and Remark 7.20). From the proof-theoretic view point this is more interesting because when seen syntactically, these conditions are more primitive. The reason is that in syntax the morphisms (i.e., proofs) come after the objects (i.e., formulae), and the formulae can always be decomposed into subformulae, whereas in semantics we have no access to the outermost connective. Furthermore, forcing all isomorphisms to preserve the ∧-comonoid structure can cause identifications of proofs that might not necessarily be wanted by every proof theorist (see, e.g., Proposition 7.14).

5.7. Remark. For each object A in a B1-category 𝒞, the identity map 1_{A}: A → A is strong, and all kinds of maps defined in Definition 5.4 are closed under composition. Therefore, each kind defines a wide subcategory (i.e., a subcategory that has all objects) of 𝒞, e.g., the wide subcategory of quasientropies, or the wide subcategory of ∨-monoid morphisms.

In a B1-category we have two canonical maps f → t, namely Π^{f} and ⨿^{t}. Because of the ∧-comonoid structure on f and the ∨-monoid structure on t, we have

[figure: f ∨ t; ⨿^{t}∨t; t ∨ t; ∇_{t}; t ∨ f; t∨⨿^{t}; t; λ̌_{t}; ϱ̌_{t}; and; t ∧ f; Π^{f} ∧f; f ∧ f; Δ_{f}; f ∧ t; f∧Π^{f}; f; λ̂_{f}^{−1}; ϱ̂_{f}^{−1}]

(which hold even if the (co)monoids are not (co)commutative.) Since λ̌_{t}, ϱ̌_{t}, λ̂_{f}, and ϱ̂_{f} are isomorphisms, we immediately can conclude that the following two diagrams commute (cf. [FP04a]):

[figure: t; λ̌_{t}^{−1}; f ∨ t; ⨿^{t}∨t; t ∨ f; ϱ̌_{t}^{−1}; t ∨ t; t∨⨿^{t}; and; f ∧ f; f∧Π^{f}; f ∧ t; ϱ̂_{f}; t ∧ f; Π^{f} ∧f; f; λ̂_{f}]

By Section 4, this gives us two different mix maps A ∧ B → A ∨ B, and motivates the following definition:

5.8. Definition. A B1-category is called single-mixed if Π^{f} = ⨿^{t}.

In a single-mixed B1-category we have, as the name says, a single canonical mix map mix_{A,B}: A ∧ B → A ∨ B obeying (mix-σ̂) and (mix-α̂). The naturality of mix, i.e., the commutativity of

[figure: A ∧ B; ^{mix^{A,B}}; A ∨ B; f∨g; C ∧ D; f∧g; C ∨ D; _{mix_{C,D}}]  (29)

for all maps f: A → C and g: B → D, uniquely determines a map f ∨ ∧g: A∧B → C ∨D. Then, for every f, g: A → B we can define

f + g = ∇_{B} ∘ (f ∨ ∧ g) ∘ Δ_{A}: A → B .

It follows from (co)-associativity and (co)-commutativity of Δ and ∇, along with naturality of mix, that the operation + on maps is associative and commutative. This gives us for Hom(A, B) a commutative semigroup structure.

Note that in general the semigroup structure on the Hom-sets is not an enrichment, e.g., (f + g)h is in general not the same as fh + gh.

5.9. Definition. Let 𝒞 be a single-mixed B1-category. Then 𝒞 is called idempotent if for every A and B, the semigroup on Hom(A, B) is idempotent, i.e., for every f: A → B we have f + f = f.

In an idempotent B1-category the semigroup structure on Hom(A, B) is in fact a sup-semilattice structure, given by f ≤ g iff f + g = g.

One can argue that the structure of B1-categories is in some sense the minimum of algebraic structure that a Boolean category should have: ∗-autonomous categories provide the right structure for linear logic proofs, and the ∨-monoids and ∧-comonoids seem to be exactly what is needed to “model contraction and weakening” in classical logic. There are certainly reasons to argue against that, since it is by no means Godgiven that the proofs in classical logic obey the bijection (⋆) nor that “contraction is associative”. But let us, for the time being, assume that proofs in classical logic form a B1category. Then it is desirable that there is some more structure. This can be, for example, an agreement between the ∧-monoidal structure (Definition 3.1) and the ∧-comonoid structure (Definition 5.1), or, a more sophisticated condition like the commutativity of the diagram

[figure: ((A ∧ B) ∨ (A ∧ B)) ∧ (A ∨ B); ∇_{A∧B}∧(A∨B); A ∧ B ∧ (A ∨ B); ≅; (A ∧ B) ∨ (A ∧ B ∧ (A ∨ B)); s_{A∧B,A∧B,A∨B}; A ∧ (B ∨ A) ∧ B; ť_{A,B,A,B}; (A ∧ B) ∨ (A ∧ (B ∨ A) ∧ B); ≅; (A ∧ B) ∨ (A ∧ B); ∇_{A∧B}; (A ∧ B) ∨ (A ∧ B) ∨ (A ∧ B); (A∧B)∨ť_{A,B,A,B}; A ∧ B; ∇_{A∧B}^{2}]  (30)

for all objects A and B. We now start to add the axioms for this.

5.10. Proposition. Let 𝒞 be a B1-category in which the equation

Π^{t} = 1_{t} : t → t  (B2a)

holds. Then we have that

(i) Δ_{t} = ϱ̂_{t}^{−1} : t → t ∧ t

(ii) For all objects A, the map Π^{A} is a ∧-comonoid morphism.

Proof. The equation Δ_{t} = ϱ̂_{t}^{−1} follows immediately from Π^{t} = 1_{t} and the definition of ∧-comonoids. That Π^{A} preserves the ∧-counit is trivial and that it preserves the ∧- comultiplication follows from

[figure: A; Π^{A}; t; Δ_{t}=ϱ̂_{t}^{−1}; A ∧ t; ϱ̂_{A}^{−1}; A∧Π^{A}; Π^{A}∧t; A ∧ A; Δ_{A}; t ∧ t; Π^{A}∧Π^{A}]

where the left triangle is the definition of ∧-comonoids, the lower triangle is functoriality of ∧ and the big “triangle” is naturality of ϱ̂.

5.11. Lemma. If a B1-category is single-mixed and obeys (B2a), then

1_{t} + 1_{t} = 1_{t}  and  1_{f} + 1_{f} = 1_{f}  (31)

Proof. First, we show that

Π_{^{⫾}f}^{f} = ∇_{f} ∘ mix_{f,f} : f ∧ f → f  (32)

This is done by chasing the diagram

[figure: f ∧ f; λ̌_{f}^{−1}∧f; (f ∨ f) ∧ f; (f∧Π^{f} )∧f; t ∧ f; Π^{f} ∧f; λ̌_{t∧f}^{−1}; (f ∨ t) ∧ f; λ̌_{t}^{−1}∧f; s_{f,t,f}; f ∨ (t ∧ f); f∨λ̂_{f}; t ∧ f; λ̌_{t∧f}; f ∨ f; ∇_{f}; f; λ̂_{f}; λ̌_{f}; f]  (33)

The right-down path is ∇_{f} ∘ mix_{f,f} and the left down path is Π_{^{⫾}f}^{f}. The two squares commute because of naturality of λ̌, the upper triangle holds because (15), the big triangle in the center is trivial, and that the lower triangle commutes follows from (the dual of) Proposition 5.10 (i). Now we can proceed:

1_{f} = Π_{^{⫾}f}^{f} ∘ Δ_{f} = ∇_{f} ∘ mix_{f,f} ∘ Δ_{f} = 1_{f} + 1_{f}

The equation 1_{t} = 1_{t} + 1_{t} follows by duality.

Note that Lemma 5.11 is a consequence of having proper units. In the case of weak units (see [LS05b, LS05a]) it does not hold.

5.12. Proposition. In a B1-category that is single-mixed and obeys (B2a), we have

f + Π^{A} = f  (34)

for all maps f: A → t. Dually, we have

g + ⨿^{B} = g  (35)

for all maps g: f → B.

Proof. Chase the diagram

[figure: A; Δ_{A}; A ∧ A; A∧Π^{A}; A; A ∧ t; ϱ̂_{A}; f∧t; t; f; t ∧ t; ϱ̂_{t}; t ∧ t; Δ_{t}; _{mix_{t,t}}; t; t ∨ t; ∇_{t}]  (36)

The first square is the comonoid equation, the second one is naturality of ϱ̂, the triangle commutes because of Proposition 5.10 (i), and the lower quadrangle is (31).

5.13. Proposition. In a B1-category obeying (B2a), the equation

[figure: A ∧ B; Π^{A}∧Π^{B}; t ∧ t; ϱ̂_{t}; t; Π^{A∧B}]  (B2b)

holds if and only if

(i) Π^{t∧t} = ϱ̂_{t} : t ∧ t → t and

(ii) the maps that preserve the ∧-counit are closed under ∧.

Proof. We see that (i) follows from (B2a) and (B2b) by plugging in t for A and B in (B2b). That (ii) holds follows from

[figure: A ∧ B; f∧g; C ∧ D; Π^{C∧D}; t ∧ t; ϱ̂_{t}; Π^{A}∧Π^{B}; Π^{C}∧Π^{D}; t; Π^{A∧B}]  (37)

where f: A → B and g: C → D are maps that preserve the ∧-counit. Conversely, it follows from (ii) and Proposition 5.10 that Π^{A} ∧ Π^{B} preserves the ∧-counit. With (i) this yields (B2b).

5.14. Proposition. In a B1-category obeying (B2a) and (B2b) the maps α̂_{A,B,C}, σ̂_{A,B}, ϱ̂_{A}, λ̂_{A}, Π^{A}, Π_{B^{⫾}}^{A}, and Π_{^{⫾}B}^{A} all preserve the ∧-counit. And dually, the maps α̌_{A,B,C}, σ̌_{A,B}, ϱ̌_{A}, λ̌_{A}, ⨿^{A}, ⨿_{B^{⫾}}^{A}, and ⨿_{^{⫾}B}^{A} all preserve the ∨-unit.

Proof. We show the case for σ̂_{A,B}:

[figure: A ∧ B; σ̂_{A,B}; B ∧ A; Π^{B∧A}; t ∧ t; ϱ̂_{t}; σ̂_{t,t}; Π^{A}∧Π^{B}; t ∧ t; ϱ̂_{t}; Π^{B}∧Π^{A}; t; Π^{A∧B}]

The quadrangle in naturality of σ̂ and the commutativity of triangle in the center is a consequence of the coherence theorem for monoidal categories. The two slim triangles are just (B2b). The cases for α̂_{A,B,C}, ϱ̂_{A}, λ̂_{A} are similar. For Π^{A}, it follows directly from (B2a) and for Π_{B^{⫾}}^{A} and Π_{^{⫾}B}^{A} from Proposition 5.13 (ii) and from (27).

5.15. Proposition. If a B1-category obeys (B2a) and the equation

[figure: A ∧ B; Δ_{A}∧Δ_{B}; A ∧ A ∧ B ∧ B; A∧σ̂_{A,B}∧B; A ∧ B ∧ A ∧ B; Δ_{A∧B}]  (B2c)

then

(i) also the equation (B2b) holds,

(ii) for every A, the map Δ_{A} is a ∧-comonoid morphism, and

(iii) the maps that preserve the ∧-comultiplication are closed under ∧.

Proof. (i) For showing that (B2b) holds, consider the diagram

[figure: A ∧ B; A ∧ B; ϱ̂_{A∧B}^{−1}; A ∧ A ∧ B ∧ B; A∧Π^{A}∧B∧Π^{B}; Δ_{A}∧Δ_{B}; A∧σ̂_{A,B}∧B; A ∧ t ∧ B ∧ t; A∧σ̂_{t,B}∧t; ϱ̂_{A}^{−1}∧ϱ̂_{B}^{−1}; A ∧ B ∧ A ∧ B; Δ_{A∧B}; A ∧ B ∧ t ∧ t; A∧B∧Π^{A}∧Π^{B}; A ∧ B ∧ t; A∧B∧ϱ̂_{t}]

The triangle on the left is (B2c), the upper quadrangle is the comonoid equation, the lower quadrangle is naturality of σ̂ and the quadrangle on the right commutes because of the coherence in monoidal categories. The outer square says that ϱ̂_{t} ∘ (Π^{A} ∧ Π^{B}) is ∧-counit for Δ_{A∧B}. By Proposition 5.3 (uniqueness of units) it must therefore be equal to Π^{A∧B}. (ii) That Δ_{A} preserves the ∧-comultiplication follows from

[figure: A; Δ_{A}; A ∧ A; Δ_{A∧A}; A ∧ A ∧ A ∧ A; A∧σ̂_{A,A}∧A; Δ_{A}∧Δ_{A}; A ∧ A; Δ_{A}; A ∧ A ∧ A ∧ A; Δ_{A}∧Δ_{A}]  (38)

where the pentagon commutes because of the coassociativity and cocommutativity of Δ_{A}: A → A ∧ A. For showing that Δ_{A} preserves the ∧-counit, consider the diagram

[figure: A; Δ_{A}; A ∧ A; Π^{A∧A}; t ∧ t; Π^{A}∧Π^{A}; Δ_{t}; ϱ̂_{t}; t; Π^{A}; t]

The big and the lower triangle commute by Proposition 5.10, and the left triangle is (B2b) which has been shown before. For (iii) chase

[figure: A ∧ B; f∧g; C ∧ D; Δ_{C∧D}; A ∧ A ∧ B ∧ B; f∧f∧g∧g; Δ_{A}∧Δ_{B}; A∧σ̂_{A,B}∧B; C ∧ C ∧ D ∧ D; C∧σ̂_{C,D}∧D; Δ_{C}∧Δ_{D}; A ∧ B ∧ A ∧ B; Δ_{A∧B}; C ∧ D ∧ C ∧ D; f∧g∧f∧g]

where f: A → B and g: C → D are maps preserving the ∧-comultiplication.

5.16. Proposition. In a B1-category obeying (B2a) and (B2c) the maps α̂_{A,B,C}, σ̂_{A,B}, ϱ̂_{A}, λ̂_{A}, Π^{A}, Π_{A^{⫾}}^{B}, and Π_{^{⫾}B}^{A} all preserve the ∧-comultiplication. Dually, the maps α̌_{A,B,C}, σ̌_{A,B}, ϱ̌_{A}, λ̌_{A}, ⨿^{A}, ⨿_{A^{⫾}}^{B}, and ⨿_{^{⫾}B}^{A} all preserve the ∨-multiplication.

Proof. Again, we show the case only for σ̂:

[figure: A ∧ B; σ̂_{A,B}; B ∧ A; Δ_{B∧A}; A ∧ A ∧ B ∧ B; σ̂_{A∧A,B∧B}; Δ_{A}∧Δ_{B}; A∧σ̂_{A,B}∧B; B ∧ B ∧ A ∧ A; B∧σ̂_{B,A}∧A; Δ_{B}∧Δ_{A}; A ∧ B ∧ A ∧ B; Δ_{A∧B}; B ∧ A ∧ B ∧ A; σ̂_{A,B}∧σ̂_{A,B}]

The two triangles are (B2c), the upper square is naturality of σ̂ and the lower square commutes because of coherence in monoidal categories. For α̂, ϱ̂, and λ̂ the situation is similar. For Π^{A} it has been shown already in Proposition 5.10, and for Π_{A^{⫾}}^{B}, and Π_{^{⫾}B}^{A} it follows from Proposition 5.15.

Propositions 5.10–5.15 give rise to the following definition:

5.17. Definition. A B2-category is a B1-category which obeys equations (B2a) and (B2c) for all objects A and B.

The following theorem summarizes the properties of B2-categories.

5.18. Theorem. In a B2-category, the maps α̂_{A,B,C}, σ̂_{A,B}, ϱ̂_{A}, λ̂_{A}, Δ_{A}, Π^{A}, Π_{A^{⫾}}^{B}, and Π_{^{⫾}B}^{A}, all are ∧-comonoid morphisms, and the ∧-comonoid morphisms are closed under ∧. Dually, the maps α̌_{A,B,C}, σ̌_{A,B}, ϱ̌_{A}, λ̌_{A}, ∇_{A}, ⨿^{A}, ⨿_{A^{⫾}}^{B}, and ⨿_{^{⫾}B}^{A}, all are ∨-monoid morphisms, and the ∨-monoid morphisms are closed under ∨.

Proof. Propositions 5.10, 5.13, 5.14, 5.15, and 5.16.

5.19. Proposition. Let f: A → C and g: A → D and h: B → C and a: A′ → A and b: B′ → B and c: C → C′ and d: D → D′ be maps for some objects A, B, C, D, A′, B′, C′, D′ in a B2-category. Diagrammatically:

[figure: A′; a; A; f; C; C′; c; B′; b; B; g; D; h; D′; d]

Then we have:

(i) (c ∧ d) ∘ ⟨f, g⟩ = ⟨c ∘ f, d ∘ g⟩.

(ii) If a preserves the comultiplication, then ⟨f, g⟩ ∘ a = ⟨f ∘ a, g ∘ a⟩.

(iii) If g preserves the counit, then Π_{^{⫾}D}^{C} ∘ ⟨f, g⟩ = f. If f preserves the counit, then Π_{C^{⫾}}^{D} ∘ ⟨f, g⟩ = g.

(iv) ⟨Π_{C^{⫾}}^{D}, Π_{^{⫾}D}^{C}⟩ = 1_{C∧D}.

Dually, we also have:

(i) [f, h] ∘ (a ∨ b) = [f ∘ a, h ∘ b].

(ii) If c preserves the multiplication, then c ∘ [f, h] = [c ∘ f, c ∘ h].

(iii) If h preserves the unit, then [f, h] ∘ ⨿_{A^{⫾}}^{B} = f. If f preserves the unit, then [f, h] ∘ ⨿_{^{⫾}B}^{A} = h.

(iv) [⨿_{A^{⫾}}^{B}, ⨿_{^{⫾}B}^{A}] = 1_{A∨B}.

Proof. Straightforward calculation. Note that (i)–(iii) hold already in a B1-category, only for (iv) is the equation (B2c) needed.

As observed before, if a B1-category is single-mixed then Hom(A, B) carries a semigroup structure. If we additionally have the structure of a B2-category, then the bijection (⋆) of Definition 3.2 preserves this semigroup structure:

5.20. Proposition. In a single-mixed B2-category the bijection (⋆) is a semigroup isomorphism.

Proof. Let f, g: A ∧ B → C be two maps for some objects A, B, and C, and let f′, g′: A → B̄ ∨ C be their transposes. We have to show that f′ + g′ is the transpose of f + g. First note, that in any ∗-autonomous category the map

\xymatrix{A ∧ A ∧ B ∧ B \ar[r]^{A∧σ̂_{A,B}∧B} & A ∧ B ∧ A ∧ B \ar[r]^{f∧g} & C ∧ C}

is a transpose of

\xymatrix{A ∧ A \ar[r]^{f′∧g′} & (B̄ ∨ C) ∧ (B̄ ∨ C) \ar[r]^{t̂} & B̄ ∨ B̄ ∨ (C ∧ C)}

where t̂ is the canonical map obtained from two switches, cf. (11). Now, by definition, f + g is the map

\xymatrix{A ∧ B \ar[r]^{Δ_{A∧B}} \ar[dr]_{Δ_{A}∧Δ_{B}} & A ∧ B ∧ A ∧ B \ar[r]^{f∧g} & C ∧ C \ar[r]^{^{mix^{C,C}}} & C ∨ C \ar[r]^{∇_{C}} & C \\  & A ∧ A ∧ B ∧ B \ar[u]_{A∧σ̂_{A,B}∧B}}

By (10) and what has been said above, the transpose of the lower path is the outermost path of the following:

[figure: A; Δ_{A}; A ∧ A; f′∧g′; (B̄ ∨ C) ∧ (B̄ ∨ C); t̂; _{mix_{B̄∨C,B̄∨C}}; B̄ ∨ B̄ ∨ (C ∧ C); B̄∨B̄∨mix_{C,C}; B̄ ∨ C ∨ B̄ ∨ C; B̄∨σ̂_{C,B̄}∨C; B̄ ∨ B̄ ∨ C ∨ C; ∇B̄∨∇_{C}; B̄ ∨ C; ∇_{B̄∨C}]

The innermost path is by definition f′ + g′. The square commutes because of (mix-σ̂) and (mix-α̂), and the triangle is the dual of (B2c).

6. Order enrichment

In [FP04c], Führman and Pym equipped B2-categories with an order enrichment, such that the proof identifications induced by the axioms are exactly the same as the proof identifications made by Gentzen’s sequent calculus LK [Gen34], modulo “trivial rule permutations” (see [Laf95, Rob03]), and such that f ≼ g if g is obtained from f via cut elimination (which is not confluent in LK).

6.1. Definition. A B2-category is called an LK-category if for every A, B, the set Hom(A, B) is equipped with a partial order structure ≼ such that

(i) the arrow composition ∘, as well as the bifunctors ∧ and ∨ are monotonic in both arguments,

(ii) for every map f: A → B we have

Π^{B} ∘ f ≼ Π^{A}  (LK-Π)
Δ_{B} ∘ f ≼ (f ∧ f) ∘ Δ_{A}  (LK-Δ)

(iii) and the bijection (⋆) of Definition 3.2 is an order isomorphism for ≼.

Although in [FP04c, FP04b] Führmann and Pym use the term “classical category”, We use here the term LK-categories because—as worked out in detail in [FP04c]—they provide a category-theoretic axiomatisation of sequent calculus proofs in Gentzen’s system LK [Gen34]. However, it should be clear that LK-categories are only one particular example of a wide range of possible category-theoretic axiomatisations of proofs in classical logic.

6.2. Remark. Note that in [FP04c] Führmann and Pym give a different definition for LK-categories. Since they start from a weakly distributive category [CS97b] instead of a ∗-autonomous one, they do not have immediate access to transposition. For this reason, they have to give a larger set of inequalities, defining the order ≼:

Δ_{B} ∘ f ≼ (f ∧ f) ∘ Δ_{A}  f ∘ ∇_{A} ≼ ∇_{B} ∘ (f ∨ f)
Π^{B} ∘ f ≼ Π^{A}  f ∘ ⨿^{A} ≼ ⨿^{B}
A ∨ Δ_{B} ≼ (∇_{A} ∨ (B ∧ B)) ∘ t̂ ∘ Δ_{A∨B}  A ∧ ∇_{B} ≼ Δ_{A∧B} ∘ ť ∘ (Δ_{A} ∧ (B ∨ B))
A ∨ Π^{B} ≼ (⨿^{A} ∨ t) ∘ λ̌_{t}^{−1} ∘ Π^{A∨B}  A ∧ ⨿^{B} ≼ ⨿^{A∧B} ∘ λ̂_{f} ∘ (Π^{A} ∧ f)

(FP)

where f: A → B is an arbitrary map and t̂: (A ∨ B) ∧ (A ∨ B) → A ∨ A ∨ (B ∧ B) and ť: A∧A∧(B ∨B) → (A∧B)∨(A∧B) are the tensor and cotensor map, cf. (11) and (12). One can now easily show that both definitions are equivalent: Clearly the inequations on the right in (FP) are just transposes of the ones on the left. The two top ones on the left are just (LK-Π) and (LK-Δ), and the two bottom ones follow as follows. If we transpose

A ∨ B [figure: A∨Δ_{B}] A ∨ (B ∧ B) we get the map

Ā ∧ (A ∨ B) [figure: eval] B [figure: Δ_{B}] B ∧ B

By (LK-Δ), this is smaller or equal to

Ā ∧ (A ∨ B) [figure: Δ_{Ā∧(A∨B)}]Ā ∧ (A ∨ B) ∧ Ā ∧ (A ∨ B) [figure: eval∧eval]B ∧ B

By (B2c) this is the same map as

Ā∧(A∨B) [figure: ΔĀ∧Δ_{A∨B}]Ā∧Ā∧(A∨B)∧(A∨B) [figure: ≅] Ā∧(A∨B)∧Ā∧(A∨B) [figure: eval∧eval]B ∧B

Transposing back yields

A ∨ B [figure: Δ_{A∨B}] (A ∨ B) ∧ (A ∨ B) [figure: t̂] A ∨ A ∨ (B ∧ B) [figure: ∇_{A}] A ∨ (B ∧ B)

This shows the third inequation on the left in (FP). For the last one, we proceed similarly:

Transposing A ∨ B [figure: A∨Π^{B}] A ∨ t yields

Ā ∧ (A ∨ B) [figure: eval] B [figure: Π^{B}] t

which is by (LK-Π) smaller or equal to

Ā ∧ (A ∨ B) [figure: Π^{Ā∧(A∨B)}]t

which is by (B2b) and (27) the same as

Ā ∧ (A ∨ B) [figure: ΠĀ ; ^{⫾}A∨B] A ∨ B [figure: Π^{A∨B}] t

If transpose back, we get

A ∨ B [figure: Π^{A∨B}] t [figure: ⨿_{^{⫾}t}^{A}] A ∨ t

as desired. We do not show here the other direction because it is rather tedious: It is almost literally the same as the proof for showing that any weakly distributive category with negation is a ∗-autonomous category (see [CS97b, BCST96]).

The following theorem states the main properties of LK-categories. It has first been observed and proved by Führmann and Pym in [FP04a].

6.3. Theorem. Every LK-category is single-mixed and idempotent. Furthermore, for all maps f, g: A → B, we have f ≤ g iff g ≼ f.

Proof. Because of (B2a) and (LK-Π) we have that ⨿^{t} = 1_{t} ∘ ⨿^{t} = Π^{t} ∘ ⨿^{t} ≼ Π^{f}. By duality, we also get Π^{f} ≼ ⨿^{t}. Therefore Π^{f} = ⨿^{t}, i.e., the category is single-mixed. Next, we show that f + g ≼ f for all maps f, g: A → B. For this, note that

A ∧ B [figure: ^{mix^{A,B}}] A ∨ B ≼ A ∧ B [figure: Π_{^{⫾}B}^{A}] B [figure: ⨿_{^{⫾}B}^{A}] A ∨ B

because these are the transposes of

A ∧ Ā [figure: ^{ı^{}^{ˆ A}}] f [figure: Π^{f}] t [figure: ^{ı^{}^{ˇ B}}] B ∨ B̄ ≼ A ∧ Ā [figure: Π^{A∧Ā}] t [figure: ^{ı^{}^{ˇ B}}] B ∨ B̄

Now we can proceed as follows:

f + g = ∇_{B} ∘ (f ∨ g) ∘ mix_{A,A} ∘ Δ_{A}
≼ ∇_{B} ∘ (f ∨ g) ∘ ⨿_{^{⫾}A}^{A} ∘ Π_{^{⫾}A}^{A} ∘ Δ_{A}
= ∇_{B} ∘ (f ∨ g) ∘ ⨿_{^{⫾}A}^{A} ∘ 1_{A}
= ∇_{B} ∘ (f ∨ B) ∘ (A ∨ g) ∘ (A ∨ ⨿^{A}) ∘ ϱ̌_{A}
= ∇_{B} ∘ (f ∨ B) ∘ (A ∨ g ∘ ⨿^{A}) ∘ ϱ̌_{A}
≼ ∇_{B} ∘ (f ∨ B) ∘ (A ∨ ⨿^{B}) ∘ ϱ̌_{A}
= ∇_{B} ∘ ⨿_{^{⫾}B}^{B} ∘ f
= f

Similarly, we get f +g ≼ g. Now we show that f ≼ f +f for f: A → B. Let f̂: A∧B̄ → f be the transpose of f. Then we have

f̂ = 1_{f} ∘ f̂
= (1_{f} + 1_{f}) ∘ f̂
= ∇_{f} ∘ mix_{f,f} ∘ Δ_{f} ∘ f̂
≼ ∇_{f} ∘ mix_{f,f} ∘ (f̂∧ f̂) ∘ Δ_{A∧B̄}
= f̂+ f̂
= { \atop f + f}

The second equation is Lemma 5.11, the third one is the definition of +, the fourth one is (LK-Δ), the fifth again the definition of +, and the last equation uses Proposition 5.20. By transposing back, we get f ≼ f + f. From this together with f + f ≼ f we get idempotency. For showing that f ≤ g iff g ≼ f, we need to show that g ≼ f iff f + g = g. Since f + g ≼ f, we have that f + g = g implies g ≼ f. Now suppose g ≼ f. Then we have g = g + g ≼ f + g. This finishes the proof since f + g ≼ g has been shown already.

Note that the converse is not necessarily true. Not every single-mixed idempotent B2-category is an LK-category. Nonetheless, because of Proposition 5.12, in every singlemixed idempotent B2-category we have for every f: A → B that Π^{B} ∘ f + Π^{A} = Π^{B} ∘ f, and hence Π^{A} ≤ Π^{B} ∘ f which is exactly (LK-Π). However, the inequality (LK-Δ) does not follow from idempotency. One can easily construct countermodels along the lines of [Str05] (see also Section 9).

7. The medial map and the nullary medial map

That LK-categories are idempotent means that they are already at the degenerate end of the spectrum of Boolean categories. On the other hand, B2-categories have (apart from Theorem 5.18) very little structure. The question that arises now is therefore, how we can add additional structure to B2-categories without getting too much collapse. In particular, can we extend the structure such that all the maps mentioned in Theorem 5.18 become ∨-monoid morphisms and ∧-comonoid morphisms? This is where medial enters the scene.

7.1. Definition. We say, a B2-category 𝒞 has medial if for all objects A, B, C, and D there is a map m_{A,B,C,D}: (A ∧ B) ∨ (C ∧ D) → (A ∨ C) ∧ (B ∨ D) with the following properties:

• it is natural in A, B, C and D,

• it is self-dual, i.e.,

[figure: \overline{(A ∨ C) ∧ (B ∨ D)}; \overline{m_{A,B,C,D}}; \overline{(A ∧ B) ∨ (C ∧ D)}; ≅; (D̄ ∧ B̄) ∨ (C̄ ∧ Ā); ≅; (D̄ ∨ C̄) ∧ (B̄ ∨ Ā); m_{D̄,B̄,C̄,Ā}]  (39)

commutes, where the vertical maps are the canonical isomorphisms induced by Definition 3.2,

• and it obeys the equation

[figure: A ∨ B; Δ_{A}∨Δ_{B}; (A ∧ A) ∨ (B ∧ B); m_{A,A,B,B}; (A ∨ B) ∧ (A ∨ B); Δ_{A∨B}]  (B3c)

for all objects A and B. The following equation is a consequence of (B3c) and the self-duality of medial.

[figure: (A ∧ B) ∨ (A ∧ B); m_{A,B,A,B}; (A ∨ A) ∧ (B ∨ B); ∇_{A}∧∇_{B}; A ∧ B; ∇_{A∧B}]  (B3c′)

7.2. Theorem. Let 𝒞 be a B2-category that has medial. Then

(i) The maps that preserve the ∧-comultiplication are closed under ∨, and dually, the maps that preserve the ∨-multiplication are closed under ∧.

(ii) For all maps A →^{f} C, A →^{g} D, B →^{h} C, and B →^{k} D, we have that

[⟨f, g⟩, ⟨h, k⟩] = ⟨[f, h], [g, k]⟩: A ∨ B → C ∧ D .

(iii) For all objects A, B, C, and D,

m_{A,B,C,D} = [ ⟨ ⨿_{A^{⫾}}^{C} ∘ Π_{A^{⫾}}^{B}, ⨿_{B^{⫾}}^{D} ∘ Π_{^{⫾}B}^{A} ⟩ , ⟨ ⨿_{^{⫾}C}^{A} ∘ Π_{C^{⫾}}^{D}, ⨿_{^{⫾}D}^{B} ∘ Π_{^{⫾}D}^{C} ⟩ ]
= ⟨ [ ⨿_{A^{⫾}}^{C} ∘ Π_{A^{⫾}}^{B}, ⨿_{^{⫾}C}^{A} ∘ Π_{C^{⫾}}^{D} ] , [ ⨿_{B^{⫾}}^{D} ∘ Π_{^{⫾}B}^{A}, ⨿_{^{⫾}D}^{B} ∘ Π_{^{⫾}D}^{C} ] ⟩

(iv) For all objects A, B, C, and D, the following diagram commutes:

[figure: ((A ∧ B) ∨ (C ∧ D)) ∧ ((A ∧ B) ∨ (C ∧ D)); (Π_{A^{⫾}}^{B}∨Π_{C^{⫾}}^{D})∧(Π_{^{⫾}B}^{A}∨Π_{^{⫾}D}^{C}); (A ∧ B) ∨ (C ∧ D); Δ_{(A∧B)∨(C∧D)}; (A ∨ C) ∧ (B ∨ D); ∇_{(A∨C)∧(B∨D)}; ((A ∨ C) ∧ (B ∨ D)) ∨ ((A ∨ C) ∧ (B ∨ D)); (⨿_{A^{⫾}}^{C}∧⨿_{B^{⫾}}^{D})∨(⨿_{^{⫾}C}^{A}∧⨿_{^{⫾}D}^{B})] (40)

(v) The horizontal diagonal of (40) is equal to m_{A,B,C,D}. Proof. For (i), chase the following (compare with the proof of Proposition 5.15 (iii))

[figure: A ∨ B; f∨g; C ∨ D; Δ_{C∨D}; (A ∧ A) ∨ (B ∧ B); (f∧f)∨(g∧g); Δ_{A}∨Δ_{B}; m_{A,A,B,B}; (C ∧ C) ∨ (D ∧ D); m_{C,C,D,D}; Δ_{C}∨Δ_{D}; (A ∨ B) ∧ (A ∨ B); Δ_{A∨B}; (C ∨ D) ∧ (C ∨ D); (f∨g)∧(f∨g)]

ON THE AXIOMATISATION OF BOOLEAN CATEGORIES  567

For (ii) chase the diagram

[figure: A ∨ B; [⟨f,g⟩,⟨h,k⟩]; ⟨f,g⟩∨⟨h,k⟩; C ∧ D; (A ∧ A) ∨ (B ∧ B); (f∧g)∨(h∧k); m_{A,A,B,B}; (C ∧ D) ∨ (C ∧ D); ∇_{C∧D}; m_{C,D,C,D}; A ∨ B; Δ_{A}∨Δ_{B}; Δ_{A∨B}; C ∧ D; (A ∨ B) ∧ (A ∨ B); (f∨h)∧(g∨k); (C ∨ C) ∧ (D ∨ D); ∇_{C}∧∇_{D}; A ∨ B; ⟨[f,h],[g,k]⟩; C ∧ D; [f,h]∧[g,k]]

where the square in the center is naturality of medial, the two small triangles are (B3c) and (B3c′). The big triangles are just (26). Note the importance of naturality of medial in the two diagrams above. Let us now continue with (iv) and (v), which are proved by

\xymatrix{(A ∧ B) ∨ (C ∧ D) \ar[rr]^{Δ_{(A∧B)∨(C∧D)}} \ar[dr]_{Δ_{A∧B}∨Δ_{C∧D}} \ar[dd]_{(Δ_{A}∧Δ_{B})∨(Δ_{C}∧Δ_{D})} &  & ((A ∧ B) ∨ (C ∧ D)) ∧ ((A ∧ B) ∨ (C ∧ D)) \ar[dd]^{(Π_{A^{⫾}}^{B}∨Π_{C^{⫾}}^{D})∧(Π_{^{⫾}B}^{A}∨Π_{^{⫾}D}^{C})} \\  & (A ∧ B ∧ A ∧ B) ∨ (C ∧ D ∧ C ∧ D) \ar[ur]_{m} \ar[dd]^{(Π_{A^{⫾}}^{B}∧Π_{^{⫾}B}^{A})∨(Π_{C^{⫾}}^{D}∧Π_{^{⫾}D}^{C})} \\ (A ∧ A ∧ B ∧ B) ∨ (C ∧ C ∧ D ∧ D) \ar[ur]_{≅} \ar[dr]_{(Π_{A^{⫾}}^{A}∧Π_{^{⫾}B}^{B})∨(Π_{C^{⫾}}^{C}∧Π_{^{⫾}D}^{D})} &  & (A ∨ C) ∧ (B ∨ D) \\  & (A ∧ B) ∨ (C ∧ D) \ar[ur]_{m}}

and (28) and the self-duality of medial. It remains to show (iii). For this consider

[figure: (A ∧ B) ∨ (C ∧ D); m_{A,B,C,D}; ((A ∧ B) ∨ (C ∧ D)) ∧ ((A ∧ B) ∨ (C ∧ D)); Δ_{(A∧B)∨(C∧D)}; (A ∨ C) ∧ (B ∨ D); (⨿_{^{⫾}A}^{A}∨⨿_{C^{⫾}}^{C})∧(⨿_{^{⫾}B}^{B}∨⨿_{D^{⫾}}^{D}); (Π_{A^{⫾}}^{B}∨Π_{C^{⫾}}^{D})∧(Π_{^{⫾}B}^{A}∨Π_{^{⫾}D}^{C}); (⨿_{A^{⫾}}^{C}∨⨿_{^{⫾}C}^{A})∧(⨿_{B^{⫾}}^{D}∨⨿_{^{⫾}D}^{B}); (A ∨ C ∨ A ∨ C) ∧ (B ∨ D ∨ B ∨ D); \begin{matrix}(⨿_{A^{⫾}}^{C}∘Π_{A^{⫾}}^{B}∨⨿_{^{⫾}C}^{A}∘Π_{C^{⫾}}^{D})∧ \\ (⨿_{B^{⫾}}^{D}∘Π_{^{⫾}B}^{A}∨⨿_{^{⫾}D}^{B}∘Π_{^{⫾}D}^{C}) \end{matrix}; (A ∨ A ∨ C ∨ C) ∧ (B ∨ B ∨ D ∨ D); (∇_{A}∨∇_{C})∧(∇_{B}∨∇_{D}); (A∨σ̌_{A,C}∨C)∧(B∨σ̌_{B,D}∨D); (A ∨ C) ∧ (B ∨ D); ∇_{A∨C}∧∇_{B∨D}]

The topmost triangle is (v), the two middle ones are trivial, and the bottommost triangle is (B2c). Note that the first-right-then-down path is

⟨ [ ⨿_{A^{⫾}}^{C} ∘ Π_{A^{⫾}}^{B}, ⨿_{^{⫾}C}^{A} ∘ Π_{C^{⫾}}^{D} ] , [ ⨿_{B^{⫾}}^{D} ∘ Π_{^{⫾}B}^{A}, ⨿_{^{⫾}D}^{B} ∘ Π_{^{⫾}D}^{C} ] ⟩

by definition, and the first-down-then-right path is m_{A,B,C,D} because of (28). We get (iii) by self-duality of medial.

7.3. Remark. Because of (iii) and (v) in Theorem 7.2, we could obtain a weak medial map by adding (iv) or (ii) as axiom to a B2-category. This weak medial map would be self-dual. By also adding Theorem 7.2 (i) as axiom, we could even recover equations (B3c) and (B3c′), as the following diagram shows:

[figure: A ∨ B; Δ_{A∨B}; (A ∨ B) ∧ (A ∨ B); (Δ_{A}∨Δ_{B})∧(Δ_{A}∨Δ_{B}); (A ∨ B) ∧ (A ∨ B); (Π_{A^{⫾}}^{A}∨Π_{B^{⫾}}^{B})∧(Π_{^{⫾}A}^{A}∨Π_{^{⫾}B}^{B}); (A ∧ A) ∨ (B ∧ B); Δ_{A}∨Δ_{B}; ((A ∧ A) ∨ (B ∧ B)) ∧ ((A ∧ A) ∨ (B ∧ B)); Δ_{(A∧A)∨(B∧B)}]

where the left square says that Δ_{A} ∨ Δ_{B} preserves the ∧-comultiplication. However, by doing this, we would not get naturality of medial, which is crucial for algebraic as well as for proof-theoretic reasons (see also the introduction).

7.4. Definition. A B2-category 𝒞 has nullary medial if there is a map ňm: t ∨ t → t (called the nullary medial map) such that for all objects A, B, the following holds:

[figure: A ∨ B; Π^{A}∨Π^{B}; t ∨ t; ňm; t; Π^{A∨B}]  (B3b)

Clearly, if a a B2-category has nullary medial, then ňm = Π^{t∨t}. This can be seen by plugging in t for A and B in (B3b). By duality ⨿^{f∧f} = n̂m: f → f ∧ f (the nullary comedial map) obeys the dual of (B3b).

7.5. Proposition. In a B2-category 𝒞 that has nullary medial, we have that

(i) The maps that preserve the ∧-counit are closed under ∨, and dually, the maps that preserve the ∨-unit are closed under ∧.

(ii) For all objects A, B, C, the map s_{A,B,C} is a quasientropy.

Proof. For showing the first statement, replace in (37) every ∧ by an ∨, and ϱ̂_{t} by ňm. The second statement is shown by

\xymatrix{(A ∨ B) ∧ C \ar[rr]^{s_{A,B,C}} \ar[d]_{(Π^{A}∨Π^{B})∧Π^{C}} &  & A ∨ (B ∧ C) \ar[d]^{Π^{A}∨(Π^{B}∧Π^{C})} \\ (t ∨ t) ∧ t \ar[rr]^{s_{t,t,t}} \ar[d]_{ňm∧t} \ar[dr]_{ϱ̂_{t∨t}} &  & t ∨ (t ∧ t) \ar[dl]^{t∨ϱ̂_{t}} \\ t ∧ t \ar[dr]_{ϱ̂_{t}} & t ∨ t \ar[d]^{ňm} \\  & t}

where the left down-path is Π^{(A∨B)∧C} and the right down-path is Π^{A∨(B∧C)} (because of (B2b) and (B3b)). The two squares are naturality of s and ϱ̂, and the triangle at the center is just (15). Hence, switch preserves the ∧-counit, and by duality also the ∨-unit.

7.6. Proposition. Let 𝒞 be a B2-category with medial and nullary medial. Then 𝒞 obeys the equation

[figure: (A ∧ t) ∨ (B ∧ t); m_{A,t,B,t}; (A ∨ B) ∧ (t ∨ t); (A∨B)∧ňm; A ∨ B; ϱ̂_{A}∨ϱ̂_{B}; (A ∨ B) ∧ t; ϱ̂_{A∨B}^{−1}]  (m-ϱ̂)

Proof. Chase

[figure: (A ∧ t) ∨ (B ∧ t); m_{A,t,B,t}; Δ_{(A∧t)∨(B∧t)}; (A ∨ B) ∧ (t ∨ t); (A∨B)∧ňm; ((A ∧ t) ∨ (B ∧ t)) ∧ ((A ∧ t) ∨ (B ∧ t)); (ϱ̂_{A}∨ϱ̂_{B})∧(ϱ̂_{A}∨ϱ̂_{B}); (Π_{A^{⫾}}^{t}∨Π_{B^{⫾}}^{t})∧(Π_{^{⫾}t}^{A}∨Π_{^{⫾}t}^{B}); (A ∨ B) ∧ (A ∨ B); Δ_{A∨B}; (A∨B)∧(Π^{A}∨Π^{B}); (A∨B)∧(Π^{A∨B}); A ∨ B; ϱ̂_{A}∨ϱ̂_{B}; (A ∨ B) ∧ t; ϱ̂_{A∨B}^{−1}]

The upper triangle is Theorem 7.2 (v), the lower triangle is the comonoid equation, the left square says that ϱ̂_{A} ∨ϱ̂_{B} preserves the ∧-comultiplication (Theorems 5.18 and 7.2 (i)), the triangle on the right is (B3b), and the triangle in the middle commutes because Π_{A^{⫾}}^{t} = ϱ̂_{A} and Π_{^{⫾}t}^{A} = Π^{A} ∘ ϱ̂_{A}, where the latter equation holds because of (27) and naturality of ϱ̂.

7.7. Proposition. A B2-category with medial and nullary medial the following are equivalent:

(i) We have

Π^{t∨t} = ňm = ∇_{t} : t ∨ t → t  (B3a)

(ii) For all objects A, the map ϱ̂_{A} preserves the ∨-multiplication.

Proof. Chasing the diagram

[figure: (A ∧ t) ∨ (A ∧ t); ϱ̂_{A}∨ϱ̂_{A}; m_{A,t,B,t}; A ∨ A; ∇_{A}; (A ∨ A) ∧ (t ∨ t); (A∨A)∧ňm; ∇_{A}∧(t∨t); ∇_{A}∧∇_{t}; (A ∨ A) ∧ t; ϱ̂_{A∨A}; ∇_{A}∧t; A ∧ (t ∨ t); A∧ňm; A∧∇_{t}; A ∧ t; ϱ̂_{A}; A ∧ t; ∇_{A∧t}; A; ϱ̂_{A}]

shows that in the presence of medial, nullary medial, and (B3a) the map ϱ̂_{A} preserves the ∨-multiplication. Note that in that diagram the uppermost square is (m-ϱ̂) from the previous proposition. The lowermost square commutes because of (B3a), and the big left triangle is (B3c′). Conversely, consider the diagram

[figure: t ∨ t; Δ_{t∨t}; Δ_{t}∨Δ_{t}=ϱ̂_{t}^{−1}∨ϱ̂_{t}^{−1}; ⨿_{t^{⫾}}^{t}∨⨿_{^{⫾}t}^{t}; (t ∨ t) ∧ (t ∨ t); 1_{t∨t}∧∇_{t}; (t ∧ t) ∨ (t ∧ t); p; m_{t,t,t,t}; (⨿_{t^{⫾}}^{t}∧t)∨(⨿_{^{⫾}t}^{t}∧t); ((t ∨ t) ∧ (t ∨ t)) ∨ ((t ∨ t) ∧ (t ∨ t)); ∇_{(t∨t)∧(t∨t)}; (1_{t∨t}∧∇_{t})∨(1_{t∨t}∧∇_{t}); t ∨ t ∨ t ∨ t; ∇_{t∨t}; ϱ̂_{t∨t}^{−1}∨ϱ̂_{t∨t}^{−1}; ((t ∨ t) ∧ t) ∨ ((t ∨ t) ∧ t); ∇_{(t∨t)∧t}; t ∨ t; (t ∨ t) ∧ t; ϱ̂_{t∨t}^{−1}]

where p = (⨿_{t^{⫾}}^{t}∨⨿_{t^{⫾}}^{t})∧(⨿_{^{⫾}t}^{t}∨⨿_{^{⫾}t}^{t}). The upper two triangles are (B3c) and Theorem 7.2 (v). The left triangle commutes because of Proposition 5.19 (iv), and the triangle at the center is the monoid equation. The triangle-shaped square is the naturality of ϱ̂, and the rightmost square commutes because 1_{t∨t} ∧ ∇_{t} preserves the ∨-multiplication, which follows from (the dual of) Proposition 5.15 (ii) and Theorem 7.2 (i). Finally, the lower square commutes because we assumed that ϱ̂_{A} preserved the ∨-multiplication. Note that the commutativity of the outer square says that ∇_{t} is unit for Δ_{t∨t}. Therefore, by Proposition 5.3, we can conclude that ňm = Π^{t∨t} = ∇_{t}.

7.8. Definition. A B3-category is a B2-category that obeys (B3a) and has medial and nullary medial.

7.9. Corollary. In a B3-category, the maps ϱ̂_{A}, λ̂_{A}, ϱ̌_{A}, and λ̌_{A} are clonable for all objects A, i.e, they preserve both the ∨-multiplication and the ∧-comultiplication.

Proof. Theorem 5.18 and Proposition 7.7 suffice to show that ϱ̂_{A} is clonable. For λ̂_{A} it is similar, and for ϱ̌_{A} and λ̌_{A} it follows by duality.

It has first been observed by Lamarche [Lam07] that the presence of a natural and self-dual map m_{A,B,C,D}: (A ∧ B) ∨ (C ∧ D) → (A ∨ C) ∧ (B ∨ D) in a ∗-autonomous category induces two canonical maps e_{1}, e_{2} : f → t, namely

e_{1} : f [figure: λ̌_{f}^{−1}]f ∨ f [figure: ϱ̂_{f}^{−1}∨λ̂_{f}^{−1}](f ∧ t) ∨ (t ∧ f) [figure: m_{f,t,t,f}] (f ∨ t) ∧ (t ∨ f) [figure: λ̌_{t}∧ϱ̌_{t}] t ∧ t [figure: ϱ̂_{t}] t

and

e_{2} : f [figure: λ̌_{f}^{−1}]f ∨ f [figure: λ̂_{f}^{−1}∨ϱ̂_{f}^{−1}](t ∧ f) ∨ (f ∧ t) [figure: m_{t,f,f,t}] (t ∨ f) ∧ (f ∨ t) [figure: ϱ̌_{t}∧λ̌_{t}] t ∧ t [figure: ϱ̂_{t}] t

which are both self-dual (while Π^{f} and ⨿^{t} are dual to each other). By adding sufficient structure one can enforce that e_{1} = e_{2} and that this map has the properties of Theorem 4.1. In [Lam07], Lamarche shows how this can be done without the ∧-comonoid and ∨-monoid structure for every object by using equation (m-σ̂) that we will introduce in Proposition 7.13. In our case the structure of a B2-category is sufficient to obtain that e_{1} = e_{2}. But for letting this map have the properties of Theorem 4.1, as it is the case with Π^{f} and ⨿^{t}, we need all the structure of a B3-category. Then we have the following:

7.10. Theorem. In a B3-category we have Π^{f} = e_{1} = e_{2} = ⨿^{t}, i.e., every B3-category is single-mixed.

Proof. We will first show that Π^{f} = e_{1}. For this, note that

(λ̌_{t} ∧ ϱ̌_{t}) ∘ m_{f,t,t,f} ∘ (ϱ̂_{f}^{−1} ∨ λ̂_{f}^{−1})

= (λ̌_{t} ∧ ϱ̌_{t}) ∘ ⟨ [ ⨿_{f^{⫾}}^{t} ∘ Π_{f^{⫾}}^{t}, ⨿_{^{⫾}t}^{f} ∘ Π_{t^{⫾}}^{f} ] , [ ⨿_{t^{⫾}}^{f} ∘ Π_{^{⫾}t}^{f}, ⨿_{^{⫾}f}^{t} ∘ Π_{^{⫾}f}^{t} ] ⟩ ∘ (ϱ̂_{f}^{−1} ∨ λ̂_{f}^{−1})
= ⟨ [ λ̌_{t} ∘ ⨿_{f^{⫾}}^{t} ∘ Π_{f^{⫾}}^{t} ∘ ϱ̂_{f}^{−1}, λ̌_{t} ∘ ⨿_{^{⫾}t}^{f} ∘ Π_{t^{⫾}}^{f} ∘ λ̂_{f}^{−1} ] , [ ϱ̌_{t} ∘ ⨿_{t^{⫾}}^{f} ∘ Π_{^{⫾}t}^{f} ∘ ϱ̂_{f}^{−1}, ϱ̌_{t} ∘ ⨿_{^{⫾}f}^{t} ∘ Π_{^{⫾}f}^{t} ∘ λ̂_{f}^{−1} ] ⟩
= ⟨ [ ⨿^{t}, Π^{f} ] , [ Π^{f} , ⨿^{t} ] ⟩

The first equation is an application of Theorem 7.2 (iii), the second one uses Proposition 5.19 together with the fact that ϱ̂_{f} and λ̂_{f} preserve the ∧-comultiplication (Theorem 5.18) and that these maps are closed under ∨ (Theorem 7.2 (i)). The third equation is an easy calculation, involving (26) and the naturality of ϱ̂ and λ̂. Before we proceed, notice that:

Π_{^{⫾}t}^{t} = λ̂_{t} = ϱ̂_{t} = Π_{t^{⫾}}^{t} : t ∧ t → t and ⨿_{^{⫾}f}^{f} = λ̂_{f}^{−1} = ϱ̂_{f}^{−1} = ⨿_{f^{⫾}}^{f} : f → f ∨ f (41)

Now we have:

e_{1} = ϱ̂_{t} ∘ (λ̌_{t} ∧ ϱ̌_{t}) ∘ m_{f,t,t,f} ∘ (ϱ̂_{f}^{−1} ∨ λ̂_{f}^{−1}) ∘ λ̌_{f}^{−1}
= ϱ̂_{t} ∘ ⟨ [ ⨿^{t}, Π^{f} ] , [ Π^{f}, ⨿^{t} ] ⟩ ∘ λ̌_{f}^{−1}
= ϱ̂_{t} ∘ ⟨ [ ⨿^{t}, Π^{f} ] ∘ λ̌_{f}^{−1}, [ Π^{f}, ⨿^{t} ] ∘ λ̌_{f}^{−1} ⟩
= Π_{t^{⫾}}^{t} ∘ ⟨ [ ⨿^{t}, Π^{f} ] ∘ ⨿_{^{⫾}f}^{f}, [ Π^{f}, ⨿^{t} ] ∘ ⨿_{f^{⫾}}^{f} ⟩
= Π_{t^{⫾}}^{t} ∘ ⟨ Π^{f}, Π^{f} ⟩
= Π^{f}

The first two equations are just the definition of e_{1} and the previous calculation. The third equation uses Proposition 5.19 and the fact that λ̌_{f} = ϱ̌_{f} preserves the ∧-comultiplication (Corollary 7.9). The fourth equation applies (41), and the last two equations are again Proposition 5.19, together with the fact that ⨿^{t} preserves the ∨-unit and Π^{f} preserves the ∧-counit (Theorem 5.18). Similarly, we show that e_{2} = Π^{f} and dually, we obtain e_{1} = e_{2} = ⨿^{t}.

7.11. Theorem. In a B3-category, the strong maps (in fact, all types of maps defined in Definition 5.4) are closed under ∧ and ∨. Furthermore, the maps m_{A,B,C,D} and ňm and n̂m are strong.

Proof. By Propositions 5.13 and 5.15, the ∧-comonoid morphisms are closed under ∧, and by Proposition 7.5 and Theorem 7.2 they are closed under ∨. Dually, the ∨- monoid morphisms are closed under ∨ and ∧, and therefore also the strong maps have this property. Since by Theorem 7.2 (v), medial is ((Π_{A^{⫾}}^{B} ∨ Π_{C^{⫾}}^{D}) ∧ (Π_{^{⫾}B}^{A} ∨ Π_{^{⫾}D}^{C})) ∘ Δ_{(A∧B)∨(C∧D)} as well as ∇_{(A∨C)∧(B∨D)} ∘ ((⨿_{A^{⫾}}^{C} ∧ ⨿_{B^{⫾}}^{D}) ∨ (⨿_{^{⫾}C}^{A} ∧ ⨿_{^{⫾}D}^{B})), we have by Theorem 5.18 that it is a ∧-comonoid morphism and a ∨-monoid morphism, and therefore strong. Since ňm = Π^{t∨t} = ∇_{t}, we get again from Theorem 5.18 that it is a ∧-comonoid morphism and a ∨-monoid morphism. Similarly for n̂m = ⨿^{f∧f} = Δ_{f}.

7.12. Proposition. In a B3-category the maps α̌_{A,B,C}, σ̌_{A,B}, λ̌_{A}, and ϱ̌_{A} preserve the ∧-counit for all objects A, B, C. Dually, the maps α̂_{A,B,C}, σ̂_{A,B}, λ̂_{A}, and ϱ̂_{A} all preserve the ∨-unit.

Proof. As before, the cases for α̌_{A,B,C} and σ̌_{A,B} are similar. This time, we show the case for α̌_{A,B,C}:

\xymatrix{A ∨ (B ∨ C) \ar[rr]^{α̌_{A,B,C}} \ar[d]_{Π^{A}∨(Π^{B}∨Π^{C})} &  & (A ∨ B) ∨ C \ar[d]^{(Π^{A}∨Π^{B})∨Π^{C}} \\ t ∨ (t ∨ t) \ar[rr]_{α̌_{t,t,t}} \ar[d]_{t∨∇_{t}} &  & (t ∨ t) ∨ t \ar[d]^{∇_{t}∨t} \\ t ∨ t \ar[dr]_{∇_{t}} &  & t ∨ t \ar[dl]^{∇_{t}} \\  & t}

The square is naturality of α̌, and the pentagon is associativity of ∇. The left down path is Π^{A∨(B∨C)} and the right down path is Π^{(A∨B)∨C} (because of (B3b) and (B3a)). For ϱ̌_{A}, chase

[figure: A ∨ f; ϱ̌_{A}; Π^{A}∨f; Π^{A}∨Π^{f}; A; Π^{A}; t ∨ f; t∨⨿^{t}; ϱ̌_{t}; t ∨ t; ňm; ∇_{t}; t; Π^{A∨f}; t]

The upper right quadrangle is naturality of ϱ̌. The leftmost triangle is (B3b). The one in the center next to it commutes because of functoriality of ∨ and Π^{f} = ⨿^{t} (Theorem 7.10). The lower right triangle the the monoid equation and the triangle at the bottom is (B3a). The case for λ̌_{A} is similar.

7.13. Proposition. In a B3-category the following are equivalent:

(i) The equation

[figure: (A ∧ B) ∨ (C ∧ D); m_{A,B,C,D}; (B ∧ A) ∨ (D ∧ C); σ̂_{A,B}∨σ̂_{C,D}; (A ∨ C) ∧ (B ∨ D); σ̂_{A∨C,B∨D}; (B ∨ D) ∧ (A ∨ C); m_{B,A,D,C}]  (m-σ̂)

holds for all objects A, B, C, and D. (ii) The map σ̂_{A,B}: A ∧ B → B ∧ A preserves the ∨-multiplication. (iii) The map σ̌_{A,B}: A ∨ B → B ∨ A preserves the ∧-comultiplication. (iv) The equation

[figure: (A ∧ B) ∨ (C ∧ D); m_{A,B,C,D}; (C ∧ D) ∨ (A ∧ B); σ̌_{A∧B,C∧D}; (A ∨ C) ∧ (B ∨ D); σ̌_{A,C}∧σ̌_{B,D}; (C ∨ A) ∧ (D ∨ B); m_{C,D,A,B}]  (m-σ̌)

holds for all objects A, B, C, and D. Proof. Suppose (m-σ̂) does hold. Then we have

[figure: (A ∧ B) ∨ (A ∧ B); m_{A,B,A,B}; (B ∧ A) ∨ (B ∧ A); σ̂_{A,B}∨σ̂_{A,B}; (A ∨ A) ∧ (B ∨ B); ∇_{A}∧∇_{B}; σ̂_{A∨A,B∨B}; (B ∨ B) ∧ (A ∨ A); m_{B,A,B,A}; A ∧ B; σ̂_{A,B}; B ∧ A; ∇_{B}∧∇_{A}]

which together with (B3c′) says that σ̂_{A,B} preserves the ∨-multiplication. Conversely, we have The upper square is naturality of σ̂, and the lower square says that σ̂_{A,B} preserves the ∨-multiplication. Together with Theorem 7.2 (v), this is (m-σ̂). Hence (i) and (ii) are equivalent. The other equivalences follow because of duality.

[figure: (A ∧ B) ∨ (C ∧ D); (⨿_{A^{⫾}}^{C}∧⨿_{B^{⫾}}^{D})∨(⨿_{^{⫾}C}^{A}∧⨿_{^{⫾}D}^{B}); (B ∧ A) ∨ (D ∧ C); σ̂_{A,B}∨σ̂_{C,D}; ((A ∨ C) ∧ (B ∨ D)) ∨ ((A ∨ C) ∧ (B ∨ D)); ∇_{(A∨C)∧(B∨D)}; σ̂_{A∨C,B∨D}∨σ̂_{A∨C,B∨D}; ((B ∨ D) ∧ (A ∨ C)) ∨ ((B ∨ D) ∧ (A ∨ C)); (⨿_{B^{⫾}}^{D}∧⨿_{A^{⫾}}^{C})∨(⨿_{^{⫾}D}^{B}∧⨿_{^{⫾}C}^{A}); (A ∨ C) ∧ (B ∨ D); σ̂_{A∨C,B∨D}; (B ∨ D) ∧ (A ∨ C); ∇_{(B∨D)∧(A∨C)}]

7.14. Proposition. In a B3-category the following are equivalent:

(i) The equation

[figure: (A ∧ (B ∧ C)) ∨ (D ∧ (E ∧ F)); m_{A,B∧C,D,E∧F}; ((A ∧ B) ∧ C) ∨ ((D ∧ E) ∧ F); α̂_{A,B,C}∨α̂_{D,E,F}; (A ∨ D) ∧ ((B ∧ C) ∨ (E ∧ F)); (A∨D)∧m_{B,C,E,F}; ((A ∧ B) ∨ (D ∧ E)) ∧ (C ∨ F); m_{A∧B,C,D∧E,F}; (A ∨ D) ∧ ((B ∨ E) ∧ (C ∨ F)); α̂_{A∨D,B∨E,C∨F}; ((A ∨ D) ∧ (B ∨ E)) ∧ (C ∨ F); m_{A,B,D,E}∧(C∨F)] (m-α̂)

holds for all objects A, B, C, D, E, and F.

(ii) The map α̂_{A,B,C}: A ∧ (B ∧ C) → (A ∧ B) ∧ C preserves the ∨-multiplication.

Proof. Similar to the previous proposition. (Here the statements corresponding to (iii) and (iv) in Proposition 7.13 are omitted to save space, but obviously they hold accordingly.)

7.15. Remark. This proposition allows us to speak of uniquely defined maps

m̂_{A,B,C,D,E,F}^{2} : (A ∧ B ∧ C) ∨ (D ∧ E ∧ F) → (A ∨ D) ∧ (B ∨ E) ∧ (C ∨ F)

and dually

m̌_{A,B,C,D,E,F}^{2} : (A ∧ B) ∨ (C ∧ D) ∨ (E ∧ F) → (A ∨ C ∨ E) ∧ (B ∨ D ∨ F)

A more sophisticated and more general notation for composed variations of medial is introduced by Lamarche in [Lam07].

7.16. Proposition. In a a B3-category obeying (m-σ̂) and (m-α̂) the following are equivalent:

(i) The equation

[figure: ((A ∧ B) ∨ (C ∧ D)) ∧ E; m_{A,B,C,D}∧E; (A ∧ B) ∨ (C ∧ D ∧ E); s_{A∧B,C∧D,E}; (A ∨ C) ∧ (B ∨ D) ∧ E; (A∨C)∧s_{B,D,E}; (A ∨ C) ∧ (B ∨ (D ∧ E)); m_{A,B,C,D∧E}]  (m-s)

holds for all objects A, B, C, D, and E.

(ii) The map s_{A,B,C}: A ∧ (B ∨ C) → (A ∧ B) ∨ C preserves the ∧-comultiplication.

Proof. First note that if the equations (m-σ̂), (m-α̂), and (m-s) hold, we can compose them to get the commutativity of diagrams like

[figure: ((A ∧ B) ∨ (C ∧ D)) ∧ E ∧ F; (A ∧ B) ∨ (C ∧ E ∧ D ∧ F); m_{A,B,C∧E,D∧F}; (A ∨ C) ∧ (B ∨ D) ∧ E ∧ F; m_{A,B,C,D}∧E∧F; (A ∨ (C ∧ E)) ∧ (B ∨ (D ∧ F))]  (42)

where the horizontal maps are the canonical maps (composed of twist, associativity, and switch) that are uniquely determined by the ∗-autonomous structure. Now chase

\xymatrix{(A ∨ B) ∧ C \ar[d]_{(Δ_{A}∨Δ_{B})∧Δ_{C}} \ar[r]^{s_{A,B,C}} & A ∨ (B ∧ C) \ar[d]^{Δ_{A}∨(Δ_{B}∧Δ_{C})} \\ ((A ∧ A) ∨ (B ∧ B)) ∧ C ∧ C \ar[d]_{m_{A,A,B,B}∧C∧C} \ar[r]^{s_{A∧A,B∧B,C∧C}} \ar@{-->}[dr] & (A ∧ A) ∨ (B ∧ B ∧ C ∧ C) \ar[d]^{(A∧A)∨(B∧σ̂_{B,C}∧C)} \\ (A ∨ B) ∧ (A ∨ B) ∧ C ∧ C \ar[d]_{(A∨B)∧σ̂_{A∨B,C}∧C} \ar@{-->}[dr] & (A ∧ A) ∨ (B ∧ C ∧ B ∧ C) \ar[d]^{m_{A,A,B∧C,B∧C}} \\ (A ∨ B) ∧ C ∧ (A ∨ B) ∧ C \ar[r]_{s_{A,B,C}∧s_{A,B,C}} & (A ∨ (B ∧ C)) ∧ (A ∨ (B ∧ C))}

where the parallelogram is just (42), the upper square is naturality of switch and the two triangles are laws of ∗-autonomous categories. Note that, by (B2c) and (B3c), the vertical paths are just Δ_{(A∨B)∧C} and Δ_{A∨(B∧C)}. Therefore switch preserves the ∧-comultiplication. Conversely, consider the diagram

\xymatrix{((A∧B)∨(C∧D))∧E \ar[d]_{Δ_{((A∧B)∨(C∧D))∧E}} \ar[r]^{s_{A∧B,C∧D,E}} & (A∧B)∨(C∧D∧E) \ar[d]^{Δ_{(A∧B)∨(C∧D∧E)}} \\ ((A∧B)∨(C∧D))∧E∧((A∧B)∨(C∧D))∧E \ar[d]_{p} \ar[r]^{s∧s} & ((A∧B)∨(C∧D∧E))∧((A∧B)∨(C∧D∧E)) \ar[d]^{q} \\ ((A∧t)∨(C∧t))∧t∧((t∧B)∨(t∧D))∧E \ar[d]_{≅} \ar[r]^{s∧s} & ((A∧t)∨(C∧t∧t))∧((t∧B)∨(t∧D∧E)) \ar[d]^{≅} \\ (A∨C)∧(B∨C)∧E \ar[r]_{(A∨C)∧s_{B,D,E}} & (A∨C)∧(B∨(D∧E))}

where

p = ((A ∧ Π^{B}) ∨ (C ∧ Π^{D})) ∧ Π^{E} ∧ ((Π^{A} ∧ B) ∨ (Π^{C} ∧ D)) ∧ E
q = ((A ∧ Π^{B}) ∨ (C ∧ Π^{D} ∧ Π^{E})) ∧ ((Π^{A} ∧ B) ∨ (Π^{C} ∧ D ∧ E))

Note that the left vertical map is m_{A,B,C,D} ∧1_{E} while the right vertical map is m_{A,B,C,D∧E}. The upper square commutes because we assumed that switch preserves the ∧-comultipli-cation, the middle one is naturality of switch, and the lower one commutes because the category is ∗-autonomous (the isomorphisms are just compositions of ϱ̂ and λ̂).

7.17. Definition. A B4-category is a B3-category that obeys the equations (m-σ̂), (m-α̂), and (m-s).

7.18. Remark. Equivalently, one can define a B4-category as a B3-category in which σ̂, α̂, and s are strong. We have chosen the form of Definition (7.17) to show the resemblance to the work [Lam07] where the equations (m-σ̂), (m-α̂), and (m-s) are also considered as primitives.

7.19. Theorem. In a B4-category, the maps α̂_{A,B,C}, σ̂_{A,B}, ϱ̂_{A}, λ̂_{A} and α̌_{A,B,C}, σ̌_{A,B}, ϱ̌_{A}, λ̌_{A}, as well as s_{A,B,C} and mix_{A,B} are all strong.

Proof. That α̂_{A,B,C}, σ̂_{A,B}, ϱ̂_{A}, λ̂_{A} and α̌_{A,B,C}, σ̌_{A,B}, ϱ̌_{A}, λ̌_{A} are quasientropies follows from Theorem 5.18 and Proposition 7.12. That ϱ̂_{A}, λ̂_{A} and ϱ̌_{A}, λ̌_{A} are clonable has been said already in Corollary 7.9. For α̂_{A,B,C}, σ̂_{A,B} and α̌_{A,B,C}, σ̌_{A,B} this follows from Theorem 5.18 and Propositions 7.13 and 7.14 (and by duality). Hence, all these maps are strong. That s_{A,B,C} is strong follows from Proposition 7.5 and Proposition 7.16 (and self-duality of switch). For showing that mix_{A,B} is also strong it suffices to observe that mix is a composition of strong maps via ∘, ∧, and ∨. See (18), Theorem 7.10, and Theorem 7.11.

7.20. Remark. Theorem 7.19 gives justification to the algebraic concern raised in Remark 5.6. In a B4-category all isomorphisms that are imposed by the B4-structure do preserve the ∨-monoid and ∧-comonoid structure (and are therefore “proper isomorphisms”). Note that there might still be “improper isomorphisms” in a B4-category. But these live outside the B4-structure and are therefore not accessible to proof-theoretic investigations.

It has first been observed by Lamarche in [Lam07] that the equation (m-mix) (see below) is a consequence of the equations (m-α̂), (m-σ̂), and (m-s). Due to the presence of the ∨-monoids and ∧-comonoids, we can give here a simpler proof of that fact:

7.21. Corollary. In a B4-category, the diagram

[figure: A ∧ B ∧ C ∧ D; A∧σ̂_{B,C}∧D; A ∧ C ∧ B ∧ D; mix_{A,C}∧mix_{B,D}; (A ∧ B) ∨ (C ∧ D); _{mix_{A∧B,C∧D}}; (A ∨ C) ∧ (B ∨ D); m_{A,B,C,D}]  (m-mix)

commutes.

Proof. Chase

[figure: A ∧ B ∧ C ∧ D; A∧σ̂_{B,C}∧D; Δ_{A}∧Δ_{B}∧Δ_{C}∧Δ_{D}; A ∧ C ∧ B ∧ D; Δ_{A}∧Δ_{C}∧Δ_{B}∧Δ_{D}; A ∧ A ∧ B ∧ B ∧ C ∧ C ∧ D ∧ D; A∧A∧σ̂_{B∧B,C∧C}∧D∧D; A ∧ A ∧ C ∧ C ∧ B ∧ B ∧ D ∧ D; ≅; Π_{^{⫾}A}^{A}∧Π_{^{⫾}C}^{C}∧Π_{B^{⫾}}^{B}∧Π_{D^{⫾}}^{D}; A ∧ B ∧ C ∧ D; Δ_{A∧B∧C∧D}; A ∧ B ∧ C ∧ D ∧ A ∧ B ∧ C ∧ D; (Π_{A^{⫾}}^{B}∧Π_{C^{⫾}}^{D})∧Π_{^{⫾}B}^{A}∧Π_{^{⫾}D}^{C}; mix_{A∧B,C∧D}∧mix_{A∧B,C∧D}; A ∧ C ∧ B ∧ D; mix∧mix; ((A ∧ B) ∨ (C ∧ D)) ∧ ((A ∧ B) ∨ (C ∧ D)); (Π_{A^{⫾}}^{B}∨Π_{C^{⫾}}^{D})∧(Π_{^{⫾}B}^{A}∨Π_{^{⫾}D}^{C}); (A ∧ B) ∨ (C ∧ D); mix; Δ_{(A∧B)∨(C∧D)}; (A ∨ C) ∧ (B ∨ D); m_{A,B,C,D}]

The topmost quadrangle commutes because of naturality of σ̂. The pentagon below consists of several applications of (B2c). The two triangles on the right are trivial. The quadrangle on the lower left commutes because mix preserves the ∧-comultiplication, and the quadrangle on the lower right because of naturality of mix. Finally, the triangle on the bottom is Theorem 7.2 (v).

Obviously one can come up with more diagrams like (m-mix) or (m-ϱ̂) and ask whether they commute, for example the following due to McKinley [McK05]:

[figure: (A ∧ f) ∨ (B ∧ C); m_{A,f,B,C}; (A ∨ B) ∧ (f ∨ C); (A∨B)∧λ̌_{C}; (A ∧ t) ∨ (B ∧ C); (A∧Π^{f} )∨(B∧C); (A ∨ B) ∧ C; s_{A,B,C}; A ∨ (B ∧ C); ϱ̂_{A}∨(B∧C)]  (43)

It was soon discovered independently by several people that (43) is equivalent to:

[figure: (A ∧ B) ∨ (C ∧ D); m_{A,B,C,D}; A ∨ B ∨ (C ∧ D); mix_{A,B}∨(C∧D); (A ∨ C) ∧ (B ∨ D); t̂_{A,C,B,D}]  (mix-m-t̂)

Here are two other examples that do not contain the units:

[figure: ((A ∧ B) ∨ (C ∧ D)) ∧ (E ∨ F); s_{A∧B,C∧D,E∧F}; (A ∨ C) ∧ (B ∨ D) ∧ (E ∨ F); m_{A,B,C,D}∧(E∨F); (A ∧ B) ∨ (C ∧ D ∧ (E ∨ F)); (A∧B)∨ť_{C,D,E,F}; ((A ∨ C) ∧ F) ∨ (E ∧ (B ∨ D)); ť_{A∨C,B∨D,E,F}; (A ∧ B) ∨ (C ∧ F) ∨ (E ∧ D); m̌_{A,B,C,F,E,D}^{2}; (A ∨ C ∨ E) ∧ (F ∨ B ∨ D); m_{A∨C,F,E,B∨D}]  (m-ť-s)

[figure: (A′∨A)∧(B′∨B)∧(C′∨C)∧(D′∨D); p; ((A′∨B′)∧(C′∨D′))∨(D∧C)∨(B∧A); m̌_{A′∨B′,C′∨D′,D,C,B,A}^{2}; ((A′∨A)∧(B′∨C))∨(B∧D′)∨(D∨C′); q; (A′∨B′∨B∨D)∧(D′∨C′∨C∨A); t̂_{A′∨B′,B∨D,D′∨C′,C∨A}; (A′∨A∨B∨D)∧(D′∨C′∨B′∨C); m̌_{A′∨A,B′∨C,B,D′,D,C′}^{2}; A′∨B′∨((B∨D)∧(D′∨C′))∨C∨A; t̂_{A′∨A,B∨D,D′∨C′,B′∨C}] (m̌^{2}-s-m̌^{2})

where p and q are the canonical maps (composed of several switches, twists, and associativity) that are determined by the ∗-autonomous structure.

One usually speaks of “coherence” [Mac71] if all diagrams of this kind commute. Very often a “coherence theorem” is based on so-called “coherence graphs” [KM71, DP04]. In certain cases (see, e.g., [Str05]) the notion of coherence graph is too restricted. For this reason, in [LS05a], the notion of “graphicality” is introduced.

7.22. Definition. Let 𝒞 be a single-mixed B1-category, and let 𝒞^{∨ ∧} be the category obtained from 𝒞 by adding for each pair of objects A and B a map mix_{A,B}^{−1} : A ∨ B → A ∧ B which is inverse to mix_{A,B} (i.e., the two bifunctors −∧− and −∨− are naturally isomorphic in 𝒞^{∨ ∧}). We say that 𝒞 is graphical if the canonical forgetful functor F: 𝒞 → 𝒞^{∨ ∧} is faithful.

Note that 𝒞^{∨ ∧} is a ∗-autonomous category in which the two monoidal structures coincide, i.e., it is a compact closed category. In fact, the whole point of Definition 7.22 is to forget in a given ∗-autonomous category the difference between ∧ and ∨. The actual problem is usually to find a canonical way of making this collapse. But here, we can explore the fact that 𝒞 is single-mixed and that the structure of a B1-category does not induce any other natural maps A ∧ B → A ∨ B or A ∨ B → A ∧ B. Although in general inverting arrows in a category can destroy the structure, it is harmless here since it only makes mix an iso, and hence 𝒞^{∨ ∧} compact closed. We do not go into further details of inverting arrows in categories because the paper is already very long and Definition 7.22 does not play an important role in the paper. Its main purpose is to provide the means of formulating the following open problem.

7.23. Open Problem. Let ℰ be a set of equations and let 𝒞 be the free B1-category that is generated from a set 𝒜 of generators (e.g., propositional variables) and that obeys all of ℰ. Is 𝒞 graphical? This question is equivalent to asking for a general coherence result for Boolean categories. The present paper exhibits many equations that have to hold, but it gives no clue whether they are enough, or what could be missing.

Note that for example the freely generated ∗-autonomous category without units [LS05a, HHS05, DP05] is graphical. This can be shown by using traditional proof nets for multiplicative linear logic. However, the work of [LS06] can be used to show that the freely generated ∗-autonomous category with units is not graphical.

Clearly, in a graphical B4-category the equations (mix-m-t̂), (m-ť-s), and (m̌^{2}-s-m̌^{2}) all hold. However, at the current state of the art it is not known whether they hold in every B4-category.^{10} But what can easily be shown is the following proposition.

7.24. Proposition. In every B4-category

(i) the equation (43) holds if and only if equation (mix-m-t̂) holds, and

(ii) the equation (30) holds if and only if equation (m-ť-s) holds.

Proof. Since we do not need this later, we leave the proof as an exercise to the reader.

7.25. Definition. A B5-category is a B4-category that obeys equations (mix-m-t̂), (m-ť-s), and (m̌^{2}-s-m̌^{2}) for all objects.

The motivation for this definition is the following lemma which will be needed in the next section.

10The conjecture is that it is not the case, but so far no counterexample could be constructed.

ON THE AXIOMATISATION OF BOOLEAN CATEGORIES  581

7.26. Lemma. In a B5-category the following equation holds for all objects A, A′, B, B′, C, C′, D, and D′:

[figure: (A′∨A)∧(B′∨B)∧(C′∨C)∧(D′∨D); t̂_{A′,A,B′,B}∧t̂_{C′,C,D′,D}; (A′∨A)∧(B′∨(B∧C′)∨C)∧(D′∨D); (A′∨A)∧t̂_{B′,B,C′,C}∧(D′∨D); (A′∨B′∨(A∧B))∧(C′∨D′∨(C∧D)); t̂_{A′∨B′,A∧B,C′∨D′,C∧D}; (A′∨B′∨(B∧C′)∨C∨A)∧(D′∨D); mix_{A′∨A,B′∨(B∧C′)∨C}∧(D′∨D); ((A′∨B′)∧(C′∨D′))∨(D∧C)∨(B∧A); ((A′∨B′)∧(C′∨D′))∨m_{D,C,B,A}; A′∨B′∨(B∧(D′∨D)∧C′)∨C∨A; s_{A′∨B′∨C∨A,B∧C′,D′∨D}; ((A′∨B′)∧(C′∨D′))∨((D∨B)∧(C∨A)); m_{A′∨B′,C′∨D′,D∨B,C∨A}; A′∨B′∨(B∧D′)∨(D∧C′)∨C∨A; A′∨B′∨ť_{B,D′,D,C′}∨C∨A; (A′∨B′∨B∨D)∧(D′∨C′∨C∨A); t̂_{A′∨B′,B∨D,D′∨C′,C∨A}; A′∨B′∨((B∨D)∧(D′∨C′))∨C∨A; A′∨B′∨m_{B,D′,D,C′}∨C∨A]

Proof. Chase the following diagram:

\xymatrix{(A′∨A)∧(B′∨(B∧C′)∨C)∧(D′∨D) \ar[dd]_{mix} \ar[dr]^{s} &  & (A′∨A)∧(B′∨B)∧(C′∨C)∧(D′∨D) \ar[ll]_{t̂} \ar[rr]^{t̂∧t̂} &  & (A′∨B′∨(A∧B))∧(C′∨D′∨(C∧D)) \ar[dd]^{t̂} \\  & (((A′∨A)∧(B′∨C))∨(B∧C′))∧(D′∨D) \ar[dl]^{mix} \ar[dd]^{m} \ar[rr]^{s} &  & (((A′∨A)∧(B′∨C))∨(B∧C′∧(D′∨D)) \ar[dd]_{ť} \\ (A′∨B′∨(B∧C′)∨C∨A)∧(D′∨D) \ar[dd]_{s} &  &  &  & ((A′∨B′)∧(C′∨D′))∨(D∧C)∨(B∧A) \ar[dd]^{m} \\  & (A′∨A∨B)∧(B′∨C∨C′)∧(D′∨D) \ar[dd]^{ť} \ar[ul]_{t̂} &  & ((A′∨A)∧(B′∨C))∨(B∧D′)∨(C′∧D) \ar[dd]_{m̌^{2}} \\ A′∨B′∨(B∧(D′∨D)∧C′)∨C∨A \ar[dd]_{ť} &  &  &  & ((A′∨B′)∧(C′∨D′))∨((B∨D)∧(C∧A)) \ar[dd]^{m} \\  & ((A′∨A∨B)∧D′)∨(D∧(B′∨C∨C′)) \ar[rr]^{m} \ar[dl]^{s∨s} &  & (A′∨A∨B∨D)∧(D′∨B′∨C∨C′) \ar[dl]^{t̂} \\ A′∨B′∨(B∧D′)∨(D∧C′)∨C∨A \ar[rr]_{m} &  & A′∨B′∨((B∨D)∧(D′∨C′))∨C∨A &  & (A′∨B′∨B∨D)∧(D′∨C′∨C∨A) \ar[ll]^{t̂}}

The little triangle in the upper left commutes because of (mix-α̂). The little triangle below it is just (mix-m-t̂), and the pentagon below commutes because of the coherence in ∗-autonomous categories^{11} [BCST96, LS06]. The big square in the center is (m-ť-s) and the small parallelogram at the bottom is just two applications of (m-s) plugged together, and the big horse-shoe shape on the left is (m̌^{2}-s-m̌^{2}).

8. Beyond medial

The definition of monoidal categories settles how the maps α̂_{A,B,C}, σ̂_{A,B}, ϱ̂_{A}, and λ̂_{A} behave with respect to each other, and how the maps α̌_{A,B,C}, σ̌_{A,B}, ϱ̌_{A}, and λ̌_{A} behave with respect to each other. The notion of ∗-autonomous category then settles via the bijection (⋆) how the two monoidal structures interact. Then, the structure of a B1category adds ∨-monoids and ∧-comonoids, and the structure of B2-categories allows the ∨-monoidal structure to go well with the ∨-monoids and the ∧-monoidal structure to go well with the ∧-comonoids. Finally, the structure of B4-categories ensures that both monoidal structures go well with the ∨-monoids and the ∧-comonoids.

However, what has been neglected so far is how the ∨-monoids and the ∧-comonoids go along with each other. Recall that in any B2-category the maps ∇ and ⨿ preserve the ∨-monoid structure and the maps Δ and Π preserve the ∧-comonoid structure (Theorem 7.19).

8.1. Compatibility of ∨-monoids and ∧-comonoids. We have the following possibilities:

(i) The maps Π and ⨿ are quasientropies.

(ii) The maps Π and ⨿ are clonable.

(iii) The maps Δ and ∇ are quasientropies.

(iv) The maps Δ and ∇ are clonable.

Condition (i) says in particular that the following diagram commutes

[figure: f; ⨿^{A}; A; Π^{A}; t; Π^{f}]  (44)

Every B1-category obeying (B2a) and (44) is not only single-mixed but also for every

object A the composition f →^{⨿^{A}} A →^{Π^{A}} t yields the same result. In [LS05a] the equation (44) was used as basic axiom, and the mix map was constructed from that without the use proper units.

The next observation to make is that (ii) and (iii) of 8.1 are equivalent, provided (B3b) and (B3a) are present:

11It even commutes in the setting of weakly distributive categories.

8.2. Proposition. In a B2-category with nullary medial and (B3a) the following are equivalent for every object A:

(i) The map Π^{A} preserves the ∨-multiplication.

(ii) The map ∇_{A} preserves the ∧-counit.

(iii) The map ⨿Ā preserves the ∧-comultiplication.

(iv) The map ΔĀ preserves the ∨-unit.

Proof. The equivalence of (ii) and (i) follows from

[figure: A ∨ A; Π^{A∨A}; ∇_{A}; A; Π^{A}; t ∨ t; Π^{A}∨Π^{A}; t; ∇_{t}]

The lower triangle is (B3b) together with (B3a). The upper triangle is (ii), and the square is (i). The other equivalences follow by duality.

Condition 8.1 (iv) exhibits yet another example of a “creative tension” between algebra and proof theory. From the viewpoint of algebra, it makes perfect sense to demand that the ∨-monoid structure and the ∧-comonoid structure be compatible with each other, i.e., that 8.1 (i)–(iv) do all hold (see [Lam07]). However, from the proof-theoretic point of view it is reasonable to make some fine distinctions: We have to keep in mind that in the sequent calculus it is the “contraction-contraction-case”

[figure: π_{1}; ⊢ Γ, A, A; cont; ⊢ Γ, A; π_{2}; ⊢ Ā, Ā, Δ; cont; ⊢ Ā, Δ] cut ⊢ Γ, Δ

which spoils the confluence of cut elimination and which causes the exponential blow-up of the size of the proof. This questions 8.1 (iv), i.e., the commutativity of the diagram

[figure: A ∨ A; ∇_{A}; A; Δ_{A}; (A ∧ A) ∨ (A ∧ A); Δ_{A}∨Δ_{A}; A ∧ A; ∇_{A∧A}]  (45)

motivates the distinction made in the following definition.

8.3. Definition. We say a B1-category is weakly flat if for every object A, the maps Π^{A} and ⨿^{A} are strong and the maps Δ_{A} and ∇_{A} are quasientropies (i.e., 8.1 (i)–(iii) hold), and it is flat if for every object A, the maps Π^{A}, ⨿^{A}, Δ_{A} and ∇_{A} are all strong (i.e., all of 8.1 (i)–(iv) do hold).

8.4. Corollary. A B3-category is weakly flat, if and only if Π^{A} is a ∨-monoid morphism for every object A.

To understand the next (and final) axiom of this paper, recall that in every *-autono-mous category we have

[figure: t; ı^{}_{ˇ A}∧ı^{}_{ˇ A}; (Ā ∨ A) ∧ (Ā ∨ A); t̂; Ā ∨ A; _{ı^{}_{ˇ A}}; Ā ∨ (A ∧ Ā) ∨ A; Ā∨ı^{}_{ˆ A}∨A]  (46)

and that this equation is the reason why the cut elimination for multiplicative linear logic (proof nets as well as sequent calculus) works so well. The motivation for the following definition is to obtain something similar for classical logic (cf. [LS05a]).

8.5. Definition. A B1-category is contractible if the following diagram commutes for all objects A.

[figure: t; ^{ı^{}^{ˇ A}}; Ā ∨ A; Δ_{Ā∨A}; (Ā ∨ A) ∧ (Ā ∨ A); t̂; Ā ∨ A; _{ı^{}_{ˇ A}}; Ā ∨ (A ∧ Ā) ∨ A; Ā∨ı^{}_{ˆ A}∨A]  (47)

The following theorem states one of the main results of this paper. It explains the deep reasons why the cut elimination for the proof nets of [LS05b] is not confluent in the general case. It also shows that the combination of equations (45) and (47) together with the B5-structure leads to a certain collapse, which can be compared to the collapse made by an LK-category. Nonetheless, even with this collapse we can find reasonable models for proofs of Boolean logic, as it is shown in the next section.

8.6. Theorem. In a B5-category that is flat and contractible, we have

1_{A} + 1_{A} = 1_{A}

for all objects A.

Proof. The proof idea here is the same as in the proof of Theorem 2.4.7 in [LS05a]. The novelty is that here we do not need the sledge-hammer axiom of graphicality. Instead we make use of Lemma 7.26. We proceed by showing that ǐ_{A} + ǐ_{A} = ǐ_{A}: t → Ā ∨ A for all objects A. From this the result follows by Proposition 5.20. Note that in particular we have that ǐ_{A} + ǐ_{A} is the map

[figure: t; ^{ı^{}^{ˇ A∧A}}; Ā ∨ Ā ∨ (A ∧ A); Ā∨Ā∨mix_{A,A}; Ā ∨ Ā ∨ A ∨ A; ∇Ā∨∇_{A}; Ā ∨ A]

which is because of (mix-α̂) and the ∗-autonomous structure the same as the left-most down path in the following diagram.

[figure: t; ı^{}_{ˇ A}∧ı^{}_{ˇ A}∧ı^{}_{ˇ A}∧ı^{}_{ˇ A}; ı^{}_{ˇ A}∧ı^{}_{ˇ A}∧ı^{}_{ˇ A}; ı^{}_{ˇ A}∧ı^{}_{ˇ A}; (Ā∨A)∧(Ā∨A)∧(Ā∨A)∧(Ā∨A); t̂_{Ā,A,Ā,A}; (Ā∨A)∧(Ā∨A)∧(Ā∨A); t̂_{Ā,A,Ā,A}; _{ı^{}_{ˇ A}}; (Ā∨A)∧(Ā∨(A∧Ā)∨A)∧(Ā∨A); _{mix_{Ā∨A,Ā∨(A∧Ā)∨A}}; (Ā∨A)∧(Ā∨(A∧Ā)∨A); mix; _{ı^{}_{ˇ A}}; _{ı^{}_{ˆ A}}; (Ā∨Ā∨(A∧Ā)∨A∨A)∧(Ā∨A); s_{Ā∨Ā∨A∨A,A∧Ā,Ā∨A}; (Ā∨A)∧(Ā∨A); _{mix_{Ā∨A,Ā∨A}}; Ā∨Ā∨(A∧Ā)∨A∨A; _{ı^{}_{ˇ A}}; _{ı^{}_{ˇ A}}; _{ı^{}_{ˆ A}}; Ā∨Ā∨(A∧(Ā∨A)∧Ā)∨A∨A; ť_{A,Ā,A,Ā}; Ā∨Ā∨A∨A; ∇Ā∨∇_{A}; Ā∨Ā∨(A∧Ā)∨A∨A; ∇Ā∨∇_{A}; _{ı^{}_{ˆ A}}; Ā∨Ā∨(A∧Ā)∨(A∧Ā)∨A∨A; m_{A,Ā,A,Ā}; ∇_{A∧Ā}; Ā∨A; Ā∨(A∧Ā)∨A; _{ı^{}_{ˆ A}}; Ā∨Ā∨((A∨A)∧(Ā∨Ā))∨A∨A; ∇Ā∨(∇_{A}∧∇Ā)∨∇_{A}; ∇_{A}∧∇Ā]

The upper triangle commutes because of functoriality of ∧, the square in the lower left corner because of functoriality of ∨, and the parallelograms because of naturality of mix and t̂. The quadrangle in the upper left commutes because of (46), and the little triangle in the right center is just (15) together with naturality of switch. The pentagon below it is just the dual of (47), and the two little triangles at the lower right corner are (B3c′) and functoriality of ∨. Therefore, this diagram gives us a complicated way of writing just ǐ_{A} + ǐ_{A}. Similarly, the next diagram gives us a complicated way of writing ǐ_{A}:

[figure: t; ı^{}_{ˇ A}∧ı^{}_{ˇ A}∧ı^{}_{ˇ A}∧ı^{}_{ˇ A}; _{ı^{}_{ˇ A}}; _{ı^{}_{ˇ (A∧A)∨(A∧A)}}; (Ā∨A)∧(Ā∨A)∧(Ā∨A)∧(Ā∨A); t̂_{Ā,A,Ā,A}∧t̂_{Ā,A,Ā,A}; (Ā∨Ā∨(A∧A))∧(Ā∨Ā∨(A∧A)); t̂_{Ā∨Ā,A∧A,Ā∨Ā,A∧A}; Ā∨A; ΔĀ∨Δ_{A}; ((Ā∨Ā)∧(Ā∨Ā))∨(A∧A)∨(A∧A); m_{A,A,A,A}; (∇Ā∧∇Ā)∨∇_{A∧A}; (Ā∧Ā)∨(A∧A); m_{Ā,Ā,A,A}; ((Ā∨Ā)∧(Ā∨Ā))∨((A∨A)∧(A∨A)); m_{Ā∧Ā,Ā∨Ā,A∨A,A∨A}; (∇Ā∧∇Ā)∨(∇_{A}∧∇_{A}); (Ā∨A)∧(Ā∨A); t̂_{Ā,A,Ā,A}; (Ā∨Ā∨A∨A)∧(Ā∨Ā∨A∨A); t̂_{Ā∧Ā,A∨A,Ā∨Ā,A∨A}; (∇Ā∨∇_{A})∧(∇Ā∨∇_{A}); Ā∨A; _{ı^{}_{ˇ A}}; Ā∨(A∧Ā)∨A; _{ı^{}_{ˆ A}}; Ā∨Ā∨((A∨A)∧(Ā∨Ā))∨A∨A; ∇Ā∨(∇_{A}∧∇Ā)∨∇_{A}]

Here the big upper right “triangle” commutes because of the ∗-autonomous structure. The irregular quadrangle in the center is a transposed version of (45), the little triangle below it is (B3c′), the two squares at the bottom are naturality of m and t̂, and the left-most part of the diagram commutes because of (47) and (B3c). Finally, we apply Lemma 7.26 to paste the two diagrams together, which yields ǐ_{A} + ǐ_{A} = ǐ_{A} as desired.

In Figure 1 the basic idea of this proof is shown. The first four equations in that figure express the idea behind the first big diagram in the proof of Theorem 8.6, and the last three equations in Figure 1 express the idea of the second diagram. More explanations on this will follow in the next section.

8.7. Corollary. Let 𝒜 be a set of propositional variables and let 𝒞 be the free flat and contractible B5-category generated by 𝒜. Then 𝒞 is idempotent.

9. A concrete example: proof nets

In this section we will construct a concrete example of a category which has almost all the properties discussed in this paper. Its existence shows that this paper actually makes sense: The equations presented here do not lead to the collapse into a Boolean algebra. In fact, this category was the main source of motivation for introducing the equations presented in Sections 3, 5, 7, and 8.

We are going to present two versions of proof nets:

1. The simple proof nets are a slight modification of the proof nets introduced in [LS05b, LS05a]. The difference is that the categories of proof nets defined in these papers had only weak units, while here we are assuming from the beginning that t and f are proper unit objects.

2. The extended proof nets have a richer structure than the simple nets. From the algebraic point of view the main difference to the simple nets is that the category of extended nets does not obey equation (45) and is not idempotent (and is therefore not an LK-category). From the proof theoretic point of view, the extended nets keep more information about the proofs. In particular the size of proofs can captured.

9.1. Definition. Let 𝒜 be a set of propositional variables. The set ℱ of formulae is generated via

ℱ ::= 𝒜 | 𝒜̄| t | f | ℱ ∧ ℱ | ℱ ∨ ℱ .

A sequent is a finite list of formulae, separated by comma. A formula can be seen as a tree and a sequent as a forest whose leaves are labeled by elements of the set 𝒜 ∪𝒜̄∪{f, t} and whose inner nodes are labeled by elements of {∧, ∨}. For a sequent Γ, let ℒ (Γ) denote the set of its leaves. For a leaf i ∈ ℒ (Γ) let ℓ(i) ∈ 𝒜 ∪ 𝒜̄∪ {f, t} denote its labeling. A linking for a sequent Γ is a binary relation P ⊆ ℒ (Γ) × ℒ (Γ) such that

(i) for every i ∈ ℒ (Γ) with ℓ(i) = t we have (i, i) ∈ P, and

(ii) if (i, j) ∈ P, then one of the following cases must hold:

• i = j and ℓ(i) = t, or

• i ≠ j and ℓ(i) = ā and ℓ(j) = a for some a ∈ 𝒜.

A simple prenet^{12} consists of a sequent Γ and a linking P for it. It will be denoted by P ▷ Γ.

In this paper, we will write prenets by simply writing down the sequent and by putting the linking as (directed) graph above it, as in these two examples^{13}:

b̄ ∧ a , ā ∧ b̄ , b ∧ a , ā ∧ b  (48)

12What we call prenet is in the literature sometimes also called a proof structure.

13Here we make two modifications to the proof nets used in [LS05b, LS05a]: (i) We force every t to be linked to itself and we do not allow links between t and f. The reason is that we deal in this paper with proper units in the categorical sense, while [LS05b, LS05a] used “weak units” (see also the introduction).

The observation that linking every t to itself and disallowing t-f-links is enough to get proper units is due to François Lamarche. (ii) We use here directed links between complementary pairs of atoms (instead of undirected links as in [LS05b, LS05a]). This brings a slight simplification of cut elimination via path composition. The idea for this has been taken from Dominic Hughes [Hug05b, Hug05a].

and

b̄ ∨ a , ((ā ∧ t) ∧ ā) ∧ b , b ∨ ((a ∧ c) ∨ f) , t ∨ ((c̄ ∧ f) ∧ b)  (49)

Now we will define when a simple prenet is correct, i.e., comes from an actual proof. A conjunctive pruning of a prenet P ▷Γ is the result of removing one of the two subformulae of each ∧ in Γ and restricting the linking P accordingly. Here are two (of 16 possible) conjunctive prunings of (48):

b̄ ∧ a , ā ∧ b̄ , b ∧ a , ā ∧ b  b̄ ∧ a , ā ∧ b̄ , b ∧ a , ā ∧ b

A simple prenet is correct if each of its conjunctive prunings contains at least one link (i.e, the linking is not empty). A simple proof net is a correct simple prenet. The two examples in (48) and (49) are proof nets. Here is a prenet, which is not a proof net because there is a pruning in which all links disappear:

b̄ ∧ a , ā ∧ b  ⟶  b̄ ∧ a , ā ∧ b

Now we show how simple proof nets can be composed. As in [LS05b, LS05a, Str05] this is done via cut elimination. But we use here a notational trick to make it even more intuitive: we allow to write proof nets in two-sided form: Instead of putting the linking above a sequent A_{1}, …, A_{n}, B_{1}, …, B_{m}, we put it in between Ā_{n}, …, Ā_{1} and B_{1}, …, B_{m}, where the negation Ā of a formula A is inductively defined as follows^{14}:

ā = ā , ¯ ā = a , t̄ = f , f̄ = t , \overline{(A ∧ B)} = B̄ ∨ Ā , \overline{(A ∨ B)} = B̄ ∧ Ā .

Here are three different ways of writing example (48) in two-sided form:

\begin{matrix}ā ∨ b \\ ā ∧ b̄ , b ∧ a , ā ∧ b \end{matrix}  \begin{matrix}b ∨ a , ā ∨ b \\ b ∧ a , ā ∧ b \end{matrix}  \begin{matrix}ā ∨ b̄ , b ∨ a , ā ∨ b \\ ā ∧ b \end{matrix} (50)

14We invert the order when taking the negation in order to reduce the number of crossings in the pictures.

And here is a different way of writing example (49):

\begin{matrix}ā ∧ b , (b̄ ∨ (t ∨ c) ∧ f \\ ((ā ∧ t) ∧ ā) ∧ b , b ∨ ((a ∧ c) ∨ f) \end{matrix}  (51)

Note that for defining the direction of the links and for checking correctness we always have to consider the negation of the formula on the top. This is equivalent to pretending we had not taken the negation of that formula when going from the one-sided to the twosided version. One can make this formally precise by using polarities [Lam01]. What is important is the fact that the objects in (48) and in (50) denote the same net. Similarly,

(49) and in (51) are just different ways of drawing the same proof net.

Cut elimination can now be defined by plugging nets together, as in the following example which is a composition of (the middle) net in (50) and the one in (51):

\begin{matrix}b ∨ a , ā ∨ b \\ b ∧ a , ā ∧ b , (b̄ ∨ (t ∨ c) ∧ f \\ ((ā ∧ t) ∧ ā) ∧ b , b ∨ ((a ∧ c) ∨ f) \end{matrix} ⟶ \begin{matrix}b ∨ a , ā ∨ b , (b̄ ∨ (t ∨ c) ∧ f \\ b ∧ a , ((ā ∧ t) ∧ ā) ∧ b , b ∨ ((a ∧ c) ∨ f) \end{matrix} (52)

There is a link in the resulting net if and only if there is a corresponding path in the nonreduced composition. Writing it in the two-sided version makes it more intuitive than in the one-sided version, where (52) would be written as:

b̄ ∧ a , ā ∧ b̄ , b ∧ a , (ā ∧ b) ♢ (b̄ ∨ a) , ((ā ∧ t) ∧ ā) ∧ b , b ∨ ((a ∧ c) ∨ f) , t ∨ ((c̄ ∧ f) ∧ b)

↓

b̄ ∧ a , ā ∧ b̄ , b ∧ a , ((ā ∧ t) ∧ ā) ∧ b , b ∨ ((a ∧ c) ∨ f) , t ∨ ((c̄ ∧ f) ∧ b)

This is the way it has been done in [LS05b] where it has been shown that this operation is associative and preserves correctness. In [LS05b] it has also been shown how sequent calculus derivations are translated into proof nets. After what has been said here, it might be more intuitive to think of them as flow graphs [Bus91, Car97] of derivations in SKS [BT01]. From the historical perspective it should be mentioned that the basic idea of the simple proof nets discussed here appeared in the literature already in [And76] as matings and in [Bib81] as matrix proofs^{15}, and that this idea goes even back to the coherence graphs of [KM71].

If we now restrict ourselves to proof nets with only two conclusions, then we have a category^{16}: the objects are the formulae and the arrows A → B are the proof nets P ▷ Ā, B. Arrow composition is defined as above, and the identities are the trivial proof nets P ▷ Ā, A. Let us call this category SNet(𝒜) where 𝒜 is the set of propositional variables from which we started.

9.2. Theorem. The category SNet(𝒜) is a B5-category that is flat and contractible.

Proof. The maps α̂, σ̂, ϱ̂, λ̂, s, m, Π, and Δ are given by the obvious nets. We show here as example the nets for m_{A,B,C,D}, ϱ̂_{A}, Π^{A}, and Δ_{A} (the others being similar, cf. [Str05]):

\begin{matrix}( A ∧ B) ∨ ( C ∧ D) \\ ( A ∨ C) ∧ ( B ∨ D) \end{matrix}  \begin{matrix}A ∧ t \\ A \end{matrix}  \begin{matrix}A \\ t \end{matrix}  \begin{matrix}A \\ A ∧ A \end{matrix}

In these drawings the bold links between formulae represent bundles of several links, one for each leaf of the formula tree. Note that the arrows have to have the right direction, and that there are no links connecting f and t. There are four cases:

\begin{matrix}A \\ A \end{matrix}  ⇝  \begin{matrix}a \\ a \end{matrix}  ā ; ā  {t \atop t}  {f \atop f}  (53)

15Note, however, that there is a subtle but crucial difference between our simple nets and the work of [And76, Bib81]: in this early work links between atoms in a conjunction relation were not allowed (because they are irrelevant for correctness), but these links are crucial for obtaining an associative cut elimination operation (see [LS05b]).

16Without the restriction to two formulae we would obtain a polycategory [Lam69, Sza75].

It is an easy exercise to check that all the equations demanded by the definitions do indeed hold. We show here only the case of the contractibility axiom (47):

\begin{matrix}t \\ Ā ∨ A \end{matrix}  =  \begin{matrix}t \\ Ā ∨ A \\ ( Ā ∨ A) ∧ ( Ā ∨ A) \\ Ā ∨ ( A ∧ Ā) ∨ A \\ Ā ∨ A \end{matrix}

As above, the bold links represent bundles of normal links:

Ā ∨ A ⇝ ā ∨ a  a ∨ ā  f ∨ t  t ∨ f (54)

The transposition (⋆) of proof nets is obtained by simply drawing the net in the transposed way, as it has been done with (48) and (50). That this has the desired properties should be clear from inspecting (53) and (54).

9.3. Theorem. The category SNet(𝒜) is graphical.

Proof. Trivial (cf. [LS05a]).

Note that in SNet(𝒜) the sum f + g: A → B of two proofs f, g: A → B is obtained by taking the (set-theoretic) union of the two corresponding linkings. Hence, SNet(𝒜) is idempotent, and we have that f ≤ g iff the linking for f is a subset of the linking for g.

9.4. Theorem. The category SNet(𝒜) is an LK-category.

Proof. Let f, g: A → B be two maps in SNet(𝒜). Let f be given by the proof net P ▷ Ā, B and g be given by Q ▷ Ā, B. Then, by what has been said above, we define f ≼ g iff Q ⊆ P. After Theorem 9.2 it only remains to show that equation (LK-Δ) holds for all f. But this follows immediately from the definition of composition of proof nets.

It should be clear, that the category SNet(𝒜) is quite a degenerate model for proofs of Boolean propositional logic. The size of a proof net is at most quadratic in the size of the sequent. This means in particular, that the information how often a certain link is used in a proof is not present in the proof net. For this reason we will now allow more than one link between a pair of complementary atoms.^{17} But as shown in [LS05b], doing this naively means losing confluence of cut elimination via path composition. I.e., we do not get a category with associative arrow composition. A possible solution has been suggested in [Str05]:

17In terms of [LS05b] this means stepping from the Boolean semiring of weights to the natural numbers semiring of weights.

9.5. Definition. An extended prenet consists of a sequent Γ, a finite set K of anchors, an anchor labeling ℓ: K → 𝒜, and a linking (which is now no longer a binary relation, but a binary function to the naturals) P: (ℒ (Γ) ∪ K) × (ℒ (Γ) ∪ K) → ℕ, such that

(i) for every i ∈ ℒ (Γ) with ℓ(i) = t we have P (i, i) = 1,

(ii) for every k ∈ K we have

∑_{i∈ℒ (Γ)∪K} P (i, k) ≥ 2  and  ∑_{j∈ℒ (Γ)∪K} P (k, j) ≥ 2

(iii) if P (i, j) ≥ 1, then one of the following cases must hold:

• i = j and ℓ(i) = t and P (i, i) = 1, or

• i ≠ j and i ∈ ℒ (Γ) and j ∈ ℒ (Γ) ∪ K and ℓ(i) = ā and ℓ(j) = a for some

a ∈ 𝒜, or

• i ≠ j and i ∈ K and j ∈ ℒ (Γ) ∪ K and ℓ(i) = ℓ(j) = a for some a ∈ 𝒜.

As before, every t has to be linked to itself. That we allow only one and not many such links is due to Lemma 5.11 (which is a consequence of having proper units, cf. [Str05]). But contrary to what we had before, we do now allow not only many links between two atoms but also “non-direct” links visiting anchors on their way. But each anchor can only serve links between atoms of the same name. Furthermore, an anchor must have at least two incoming and at least two outgoing links. Here are two examples of extended prenets:

\begin{matrix}b ∨ a , ā ∨ b \\ • \\ b ∧ a , ā ∧ b \end{matrix}  and  \begin{matrix}b ∨ a , ā ∨ b \\ • \\ • \\ • \\ b ∧ a , ā ∧ b \end{matrix}  (55)

The labellings of the anchors are not shown because they are clear from the linkings. Observe that while in a simple proof net the number of links is at most quadratic in the size of the sequent, in an extended net things can get arbitrarily large, as the second example in (55) shows.

The correctness of extended nets is defined similarly as for simple nets. But now the condition is not that every pruning must contain a link, but it must contain a complete path from one leaf to another (in a conjunctive pruning the anchors remain and behave as big disjunctions). A correct extended prenet is an extended proof net. The examples in (55) are extended proof nets.

9.6. Cut elimination for extended nets. The composition of two extended proof nets is again defined via cut elimination, which can again be understood as path composition. But this time we have to be careful to treat the anchors correctly if we want a well-defined and associative composition. To be formally precise, we define it in two steps:

1.) Replace every leaf of the cut formula by an anchor, while the links remain unchanged.

2.) Remove all anchors that have no right to exist (i.e., that have less than two incoming or outgoing links). This is done by repeatedly performing the following reduction steps until no further reduction is possible:

• Remove every anchor without any outcoming links, and remove all links coming into it.

• Remove every anchor without any incoming links, and remove all links coming out of it.

• If there is an anchor k with only one link coming out, i.e., there is exactly one i ∈ ℒ (Γ) ∪ K with P (k, i) = 1, and P (k, j) = 0 for all j ∈ ℒ (Γ) ∪ K with j ≠ i, then

– for every l ∈ ℒ (Γ) ∪ K increase the value of P (l, i) by P (l, k), i.e, all links going into k are redirected to i, and

– remove k.

• If there is an anchor k with only one link going in, i.e., there is exactly one i ∈ ℒ (Γ) ∪ K with P (i, k) = 1, and P (j, k) = 0 for all j ∈ ℒ (Γ) ∪ K with j ≠ i, then

– for every l ∈ ℒ (Γ) ∪ K increase the value of P (i, l) by P (k, l), i.e, all links coming out of k are replaced by links coming out of i, and

– remove k.

• Set P (k, k) = 0 for all k ∈ K.

• Set P (i, i) = 1 for all i with ℓ(i) = t.

This sounds more complicated than it actually is. As first example, we show here the

594  LUTZ STRASSBURGER

case of the contractibility axiom (applied to a single atom):

\begin{matrix}t \\ ā ∨ a \\ ( ā ∨ a) ∧ ( ā ∨ a) \\ ā ∨ ( a ∧ ā) ∨ a \\ ā ∨ a \end{matrix} ⇝ \begin{aligned}& t \\ • & • \\ • & • & • & • \\ • & • & • & • \\ & ā ∨ a \end{aligned} ⇝ \begin{matrix}t \\ • & • \\ ā ∨ a \end{matrix} ⇝ \begin{matrix}t \\ • \\ ā ∨ a \end{matrix} ⇝ \begin{matrix}t \\ • \\ ā ∨ a \end{matrix} ⇝ \begin{matrix}t \\ ā ∨ a \end{matrix}

Here are two other examples (compare with (52)):

\begin{matrix}b ∨ a , ā ∨ b \\ b ∧ a , ā ∧ b , (b̄ ∨ (t ∨ c) ∧ f \\ ((ā ∧ t) ∧ ā) ∧ b , b ∨ ((a ∧ c) ∨ f) \end{matrix} ⟶ \begin{matrix}b ∨ a , ā ∨ b , (b̄ ∨ (t ∨ c) ∧ f \\ • \\ b ∧ a , ((ā ∧ t) ∧ ā) ∧ b , b ∨ ((a ∧ c) ∨ f) \end{matrix} (56)

and

\begin{matrix}b ∨ a , ā ∨ b \\ • \\ b ∧ a , ā ∧ b , (b̄ ∨ (t ∨ c) ∧ f \\ ((ā ∧ t) ∧ ā) ∧ b , b ∨ ((a ∧ c) ∨ f) \end{matrix} ⟶ \begin{matrix}b ∨ a , ā ∨ b , (b̄ ∨ (t ∨ c) ∧ f \\ • \\ b ∧ a , ((ā ∧ t) ∧ ā) ∧ b , b ∨ ((a ∧ c) ∨ f) \end{matrix} (57)

The whole point of the construction of the extended proof nets is, that we again get a category, which we denote by ENet(𝒜).^{18} This category is again a B5-category and it is graphical. But it is not flat because the following two nets are obviously not equal:

18The restrictions made to the anchors in Definition 9.5 are chosen such that we indeed get a welldefined and associative composition.

\begin{matrix}a ∨ a \\ a ∧ a \end{matrix}  and  \begin{matrix}a ∨ a \\ • \\ a ∧ a \end{matrix}  (58)

which means that diagram (45) does not commute. It is also easy to see that ENet(𝒜) is not idempotent, and is therefore not an LK-category. However, we have:

9.7. Theorem. The category ENet(𝒜) is a B5-category that is weakly flat and contractible.

Proof. Again, the maps α̂, σ̂ ϱ̂, λ̂, s, m, Π, and Δ are given by the obvious nets. It is an easy exercise to check that the equations demanded by the definitions do still hold.

9.8. Theorem. The category ENet(𝒜) is graphical.

Proof. Trivial.

In Figure 1 we use the notation of the extended proof nets to illustrate the idea behind the proof of Theorem 8.6. The middle equation in the second line is (45), i.e, the identity of the two nets in (58). The left-most equation in the second line and the right-most equation in the first line are both the contractibility equation (47). Everything else in Figure 1 is rather trivial from the viewpoint of proof nets. However, since we do not have a “coherence theorem”, Figure 1 cannot tell us whether the equations are really consequences of the axioms. For this, the proper proof in Section 8 is necessary.

10. More thoughts on order enrichment

Although ENet(𝒜) is not an LK-category, we can enrich it with a partial order which is induced by cut elimination according to the ideas of [FP04c, FP04a]. This means that f ≼ g if g is obtained from f via cut elimination in some formal system (not necessarily LK or another sequent system).

In category-theoretic terms, this is achieved by keeping properties (i) and (iii) in Definition 6.1, but by dropping (LK-Π) and (LK-Δ). It should be clear that there is a wide range of possibilities of providing such a partial order. As an example we will sketch here the idea which has been proposed in [Str05].

Let f: A → B be a map in ENet(𝒜), i.e., an extended proof net, and let k ∈ K_{f} be an anchor in f, and let P_{f} be the linking of f. Then we can remove k according to the cut elimination for simple proof nets (as defined in [LS05b]). Let K′ be K_{f} \ {k} and for all i, j ∈ ℒ (Γ) ∪ K′ let P′(i, j) = P_{f}(i, j) + P_{f}(i, k) · P_{f}(k, j). Now define g: A → B to be the result of applying the second step of 9.6 to P′, K′.

ā ∨ a = \begin{aligned}• & • & • & • \\ & • & & • \\ & & ā ∨ a \end{aligned} = \begin{aligned}• & • & • & • & • & • \\ • & • & & • & • \\ & • & & • \\ & & ā ∨ a \end{aligned} = \begin{aligned}• & • & • & • & • & • & • & • \\ • & • & • & • & • & • & • & • \\ • & • & • & • \\ & & & & ā ∨ a \end{aligned}

∥

ā ∨ a = \begin{aligned}• & • \\ • & • & • & • \\ • & • & • & • \\ & ā ∨ a \end{aligned} = \begin{aligned}• & • & • & • \\ • & • & • & • \\ & ā ∨ a \end{aligned} = \begin{aligned}• & • & • & • & • & • & • & • \\ • & • & • & • & • & • & • & • \\ • & • & • & • \\ & & & & ā ∨ a \end{aligned}

Figure 1: The idea of the proof of Theorem 8.6

For example the net on the left in (58) is the result of eliminating the anchor of the net on the right in (58).

Note that this anchor elimination process is not confluent, i.e., in a net with many anchors, the result of eliminating all of them depends on the order in which they are eliminated. This has been shown in [LS05b], but morally it is a consequence of Theorem 8.6.

There is also a close relationship to cut elimination in the calculus of structures. There is work in progress to nail down the precise relation between the anchor elimination for proof nets defined above and the splitting technique [Gug07] for elimination the cuts in system SKS [Brü03].

Let us finish this paper by proposing yet another way of enriching ENet(𝒜) with a partial order: Since maps in that category are just directed graphs, we can define f ≼ g if g is a minor of f in the graph-theoretic sense. We have to leave it as problem for future work to investigate the proof-theoretic implications of this.

Acknowledgments

Some essential parts of the research described here have been carried out while the author was working at Saarland University, Programming Systems Lab.

I am grateful to François Lamarche for many fruitful discussions and helpful comments on early drafts of this paper. Kai Brünnler, Alessio Guglielmi, and Richard McKinley contributed indirectly to this work by asking the right questions at the right time. Furthermore I would thank the anonymous referee for several significant comments that helped to improve the paper.

References

[And76] Peter B. Andrews. Refutations by matings. IEEE Transactions on Computers, C-25:801–807, 1976.

[Bar79] Michael Barr. *-Autonomous Categories, volume 752 of Lecture Notes in Mathematics. Springer-Verlag, 1979.

[Bar91] Michael Barr. *-autonomous categories and linear logic. Mathematical Structures in Computer Science, 1:159–178, 1991.

[BCST96] Richard Blute, Robin Cockett, Robert Seely, and Todd Trimble. Natural deduction and coherence for weakly distributive categories. Journal of Pure and Applied Algebra, 113:229–296, 1996.

[BG07] Paola Bruscoli and Alessio Guglielmi. On the proof complexity of deep inference. In Proof, Computation, Complexity (PCC 2007), 2007.

[Bib81] Wolfgang Bibel. On matrices with connections. Journal of the ACM, 28:633–645, 1981.

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

[Brü03] Kai Brünnler. Deep Inference and Symmetry for 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 LNAI, pages 347–361. Springer-Verlag, 2001.

[Bus91] Samuel R. Buss. The undecidability of k-provability. Annals of Pure and Applied Logic, 53:72–102, 1991.

[BW99] Michael Barr and Charles Wells. Category Theory for Computing Science. Les Publications CRM, Montréal, third edition, 1999.

[Car97] Alessandra Carbone. Interpolants, cut elimination and flow graphs for the propositional calculus. Annals of Pure and Applied Logic, 83:249–299, 1997.

[CR79] Stephen A. Cook and Robert A. Reckhow. The relative efficiency of propositional proof systems. The Journal of Symbolic Logic, 44(1):36–50, 1979.

[CS97a] J.R.B. Cockett and R.A.G. Seely. Proof theory for full intuitionistic linear logic, bilinear logic, and mix categories. Theory and Applications of Categories, 3(5):85–131, 1997.

[CS97b] J.R.B. Cockett and R.A.G. Seely. Weakly distributive categories. Journal of Pure and Applied Algebra, 114:133–173, 1997.

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

[DP05] Kosta Došen and Zoran Petrić. Proof-net categories. preprint, Mathematical Institute, Belgrade, 2005.

[DP07] Kosta Došen and Zoran Petrić. Intermutation. preprint, Mathematical Institute, Belgrade, 2007.

[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 IEEE Symposium on Logic in Computer Science (LICS 2004), pages 211–220, 2004.

[FP04c] Carsten Führmann and David Pym. Order-enriched categorical models of the classical sequent calculus. To appear in Journal of Pure and Applied Algebra, 2004.

[Gen34] Gerhard Gentzen. Untersuchungen über das logische Schließen. I. Mathematische Zeitschrift, 39:176–210, 1934.

[Gir91] Jean-Yves Girard. A new constructive logic: Classical logic. Mathematical Structures in Computer Science, 1:255–296, 1991.

[GS01] Alessio Guglielmi and Lutz Straßburger. Non-commutativity and MELL in the calculus of structures. In Laurent Fribourg, editor, Computer Science Logic, CSL 2001, volume 2142 of LNCS, pages 54–68. Springer-Verlag, 2001.

[Gug02] Alessio Guglielmi. Subatomic logic. note, November 2002.

[Gug04a] Alessio Guglielmi. Deep inference and speed-up in proof search. Email to the frogs mailinglist on 2004-08-08, archived at http://news.gmane.org/gmane.

science.mathematics.frogs, 2004.

[Gug04b] Alessio Guglielmi. Formalism A. note, April 2004.

[Gug04c] Alessio Guglielmi. Formalism B. note, December 2004.

[Gug05] Alessio Guglielmi. Some news on subatomic logic. note, July 2005.

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

[HdP93] J. Martin E. Hyland and Valeria de Paiva. Full intuitionistic linear logic (extended abstract). Annals of Pure and Applied Logic, 64(3):273–291, 1993.

[HHS05] Robin Houston, Dominic Hughes, and Andrea Schalk. Modelling linear logic without units (preliminary results). Preprint, available at http://arxiv.org/

abs/math/0504037, 2005.

[How80] W. A. Howard. The formulae-as-types notion of construction. In J. P. Seldin and J. R. Hindley, editors, To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, pages 479–490. Academic Press, 1980.

[Hug05a] Dominic Hughes. Simple free star-autonomous categories and full coherence.

Preprint, available at http://arxiv.org/abs/math.CT/0506521, 2005.

[Hug05b] Dominic Hughes. Simple multiplicative proof nets with units. Preprint, available

at http://arxiv.org/abs/math.CT/0507003, 2005.

[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.

[Kel64] Gregory Maxwell Kelly. On MacLane’s conditions for coherence of natural associativities, commutativities, etc. Journal of Algebra, 4:397–402, 1964.

[KM71] Gregory Maxwell Kelly and Saunders Mac Lane. Coherence in closed categories. Journal of Pure and Applied Algebra, 1:97–140, 1971.

[Laf88] Yves Lafont. Logique, Catégories et Machines. PhD thesis, Université Paris 7, 1988.

[Laf95] Yves Lafont. From proof nets to interaction nets. In J.-Y. Girard, Y. Lafont, and L. Regnier, editors, Advances in Linear Logic, volume 222 of London Mathematical Society Lecture Notes, pages 225–247. Cambridge University Press, 1995.

[Lam68] Joachim Lambek. Deductive systems and categories. I: Syntactic calculus and residuated categories. Math. Systems Theory, 2:287–318, 1968.

[Lam69] Joachim Lambek. Deductive systems and categories. II. standard constructions and closed categories. In P. Hilton, editor, Category Theory, Homology Theory and Applications, volume 86 of Lecture Notes in Mathematics, pages 76–122. Springer, 1969.

[Lam01] François Lamarche. On the algebra of structural contexts. Accepted at Mathematical Structures in Computer Science, 2001.

[Lam07] François Lamarche. Exploring the gap between linear and classical logic, 2007. Theory and Applications of Categories, 18:473–535, 2007.

[Lau99] Olivier Laurent. Polarized proof-nets: proof-nets for LC (extended abstract). In Jean-Yves Girard, editor, Typed Lambda Calculi and Applications (TLCA 1999), volume 1581 of LNCS, pages 213–227. Springer-Verlag, 1999.

[Lau03] Olivier Laurent. Polarized proof-nets and λμ-calculus. Theoretical Computer Science, 290(1):161–188, 2003.

[LS86] Joachim Lambek and Phil J. Scott. Introduction to higher order categorical logic, volume 7 of Cambridge studies in advanced mathematics. Cambridge University Press, 1986.

[LS05a] François Lamarche and Lutz Straßburger. Constructing free Boolean categories. In Proceedings of the Twentieth Annual IEEE Symposium on Logic in Computer Science (LICS’05), pages 209–218, 2005.

[LS05b] François Lamarche and Lutz Straßburger. Naming proofs in classical propositional logic. In Paweł Urzyczyn, editor, Typed Lambda Calculi and Applications, TLCA 2005, volume 3461 of LNCS, pages 246–261. Springer-Verlag, 2005.

[LS06] François Lamarche and Lutz Straßburger. From proof nets to the free *- autonomous category. Logical Methods in Computer Science, 2(4:3):1–44, 2006.

[Mac63] Saunders Mac Lane. Natural associativity and commutativity. Rice University Studies, 49:28–46, 1963.

[Mac71] Saunders Mac Lane. Categories for the Working Mathematician. Number 5 in Graduate Texts in Mathematics. Springer-Verlag, 1971.

[McK05] Richard McKinley. New bureacracy/coherence. Email to the frogs mail-

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

[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.

[Pra71] Dag Prawitz. Ideas and results in proof theory. In J. E. Fenstad, editor, Proceedings of the Second Scandinavian Logic Symposium, pages 235–307. North-Holland Publishing Co., 1971.

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

[See89] R.A.G. Seely. Linear logic, *-autonomous categories and cofree coalgebras. Contemporary Mathematics, 92, 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.

[SL04] Lutz Straßburger and François Lamarche. On proof nets for multiplicative linear logic with units. In Jerzy Marcinkowski and Andrzej Tarlecki, editors, Computer Science Logic, CSL 2004, volume 3210 of LNCS, pages 145–159. Springer-Verlag, 2004.

[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 Paola Bruscoli and François Lamarche, editors, Structures and Deduction 2005 (Satellite Workshop of ICALP’05), 2005.

[Sza75] M. E. Szabo. Polycategories. Comm. Alg., 3:663–689, 1975.

[Thi97] Hayo Thielecke. Categorical Structure of Continuation Passing Style. PhD thesis, University of Edinburgh, 1997.

Lutz Straßburger INRIA Futurs & École Polytechnique LIX Rue de Saclay 91128 Palaiseau Cedex France

http://www.lix.polytechnique.fr/Labo/Lutz.Strassburger/
Email: lutz@lix.polytechnique.fr

This article may be accessed via WWW at http://www.tac.mta.ca/tac/ or by anony-

mous ftp at ftp://ftp.tac.mta.ca/pub/tac/ html/volumes/18/18/18-18.{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. The method of distribution of the journal is via the Internet tools WWW/ftp. The journal is archived electronically and in printed paper format.

Subscription information. Individual subscribers receive (by e-mail) abstracts of articles as they are published. Full text of published articles is available in .dvi, Postscript and PDF. Details will be e-mailed to new subscribers. 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 is the preferred flavour. TEX source of articles for publication should be submitted by e-mail directly to an appropriate Editor. They are listed below. Please obtain detailed information on submission format and style files from the journal’s WWW server at http://www.tac.mta.ca/tac/. You may also write to tac@mta.ca to receive details by e-mail.

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

TEXnical editor. Michael Barr, McGill University: barr@math.mcgill.ca

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