PUBLICATIONS DE L’INSTITUT MATHÉMATIQUE Nouvelle série, tome 78(92) (2005), 1–33

COHERENCE OF PROOF-NET CATEGORIES

Kosta Došen and Zoran Petrić

Communicated by Žarko Mijajlović

Abstract. The notion of proof-net category defined in this paper is closely related to graphs implicit in proof nets for the multiplicative fragment without constant propositions of linear logic. Analogous graphs occur in Kelly’s and Mac Lane’s coherence theorem for symmetric monoidal closed categories. A coherence theorem with respect to these graphs is proved for proof-net categories. Such a coherence theorem is also proved in the presence of arrows corresponding to the mix principle of linear logic. The notion of proof-net category catches the unit free fragment of the notion of star-autonomous category, a special kind of symmetric monoidal closed category.

1. Introduction

In this paper we introduce the notion of proof-net category, for which we will show that it is closely related to graphs implicit in proof nets for the multiplicative fragment without constant propositions of linear logic (see [14] and [7] for the notion of proof net). Analogous graphs occur in Kelly’s and Mac Lane’s coherence theorem for symmetric monoidal closed categories of [17].

The notion of proof-net category is based on the notion of symmetric net category of [11, Section 7.6]; these are categories with two multiplications, ∧ and ∨, associative and commutative up to isomorphism, which have moreover arrows of the dissociativity type A ∧ (B ∨ C) → (A ∧ B) ∨ C (called linear or weak distribution in [6]). The symmetric net category freely generated by a set of objects is called DS. To obtain proof-net categories we add to symmetric net categories an operation on objects corresponding to negation, which is involutive up to isomorphism. With these operations come appropriate arrows. A number of equations between

2000 Mathematics Subject Classification: Primary 03F07, 03F52, 18D10, 18D15, 19D23. Key words and phrases: generality of proofs, linear logic, mix, proof nets, linear distribution,

dissociativity, categorial coherence, Kelly–Mac Lane graphs, Brauerian graphs, split equivalences, symmetric monoidal closed category, star-autonomous category.

arrows, of the kind called coherence conditions in category theory, are satisfied in proof-net categories.

A notion amounting to the notion of star-autonomous category of [2] is obtained in a similar manner in [6]. Star-autonomous categories, which stem from [1], are a special kind of symmetric monoidal closed categories. In contradistinction to symmetric net and proof-net categories they involve unit objects.

We introduce next a category Br whose arrows are called Brauerian split equivalences of finite ordinals. These equivalence relations, which stem from results in representation theory of [3], amount to the graphs used by Kelly and Mac Lane for their coherence theorem of symmetric monoidal categories mentioned above. Brauerian split equivalences express generality of proofs in linear logic (see [9], [10]).

For proof-net categories we prove a coherence theorem that says that there is a faithful functor from the proof-net category PN^{¬} freely generated by a set of objects into Br. The coherence theorem for PN^{¬} yields an elementary decision procedure for verifying whether a diagram of arrows commutes in PN^{¬}, and hence also in every proof-net category. This is a very useful result, which enables us in [12] to obtain other coherence results with respect to Br, in particular a coherence result for star-autonomous categories, involving the units. It is also shown in [12] with the help of coherence for PN^{¬} that the notion of proof-net category catches the unit-free fragment of star-autonomous categories. (A different attempt to catch this fragment is made in [18] and [15].)

The coherence theorem for PN^{¬} is proved by finding a category PN, equivalent to PN^{¬}, in which negation can be applied only to the generating objects, and coherence is first established for PN by relying on coherence for symmetric net categories, previously established in [11, Chapter 7], and on an additional normalization procedure involving negation.

In the last two sections of the paper we consider proof-net categories that have mix arrows of the type A ∧ B ⊢ A ∨ B. We prove coherence with respect to Br for the appropriate notion of proof-net category with these arrows, which we call mix-proof-net category.

2. The category DS

The objects of the category DS are the formulae of the propositional language L_{∧,∨}, generated from a set P of propositional letters, which we call simply letters, with the binary connectives ∧ and ∨. We use p, q, r, …, sometimes with indices, for letters, and A, B, C, …, sometimes with indices, for formulae. As usual, we omit the outermost parentheses of formulae and other expressions later on.

To define the arrows of DS, we define first inductively a set of expressions called the arrow terms of DS. Every arrow term of DS will have a type, which is an ordered pair of formulae of L_{∧,∨}. We write f: A ⊢ B when the arrow term f is of type (A, B). (We use the turnstile ⊢ instead of the more usual →, which we reserve for a connective and a biendofunctor.) We use f, g, h, …, sometimes with indices, for arrow terms.

For all formulae A, B and C of L_{∧,∨} the following primitive arrow terms:

1_{A}: A ⊢ A,

b^{∧}\overrightarrow{A,B,C} : A ∧ (B ∧ C) ⊢ (A ∧ B) ∧ C, b^{∨}\overrightarrow{A,B,C} : A ∨ (B ∨ C) ⊢ (A ∨ B) ∨ C,

b^{∧}\overleftarrow{A,B,C} : (A ∧ B) ∧ C ⊢ A ∧ (B ∧ C), b^{∨}\overleftarrow{A,B,C} : (A ∨ B) ∨ C ⊢ A ∨ (B ∨ C),

c^{∧}_{A,B} : A ∧ B ⊢ B ∧ A,  c^{∨}_{A,B} : B ∨ A ⊢ A ∨ B,
d_{A,B,C}: A ∧ (B ∨ C) ⊢ (A ∧ B) ∨ C

are arrow terms of DS. If g: A ⊢ B and f: B ⊢ C are arrow terms of DS, then f ^{∘} g: A ⊢ C is an arrow term of DS; and if f: A ⊢ D and g: B ⊢ E are arrow terms of DS, then f ξ g: A ξ B ⊢ D ξ E, for ξ ∈ {∧, ∨}, is an arrow term of DS. This concludes the definition of the arrow terms of DS.

Next we define inductively the set of equations of DS, which are expressions of the form f = g, where f and g are arrow terms of DS of the same type. We stipulate first that all instances of f = f and of the following equations are equations of DS:

(cat 1) f ^{∘} 1_{A} = 1_{B} ^{∘} f = f: A ⊢ B,

(cat 2) h^{∘} (g^{∘} f) = (h^{∘} g)^{∘} f,

for ξ ∈ {∧, ∨},

(ξ 1) 1_{A} ξ 1_{B} = 1_{A^{ξ}B},

(ξ 2) (g_{1} ^{∘} f_{1}) ξ (g_{2} ^{∘} f_{2}) = (g_{1} ξ g_{2})^{∘} (f_{1} ξ f_{2}),

for f: A ⊢ D, g: B ⊢ E and h: C ⊢ F,

(b^{ξ}^{→} nat) ((f ξ g) ξ h)^{∘} b^{ξ}\overrightarrow{A,B,C} = b^{ξ}\overrightarrow{D,E,F} ^{∘} (f ξ (g ξ h)),

(c^{∧} nat) (g ∧ f)^{∘} c^{∧}_{A,B} = c^{∧}_{D,E} ^{∘} (f ∧ g),

(c^{∨} nat) (g ∨ f)^{∘} c^{∨}_{B,A} = c^{∨}_{E,D} ^{∘} (f ∨ g),

(d nat) ((f ∧ g) ∨ h)^{∘} d_{A,B,C} = d_{D,E,F} ^{∘} (f ∧ (g ∨ h)),

(b^{ξ}b^{ξ}) b^{ξ}\overleftarrow{A,B,C} ^{∘} b^{ξ}\overrightarrow{A,B,C} = 1_{A^{ξ}(B^{ξ}C)},  b^{ξ}\overrightarrow{A,B,C} ^{∘} b^{ξ}\overleftarrow{A,B,C} = 1_{(A^{ξ}B)^{ξ}C},

(b^{ξ} 5) b^{ξ}\overleftarrow{A,B,C^{ξ}D} ^{∘} b^{ξ}\overleftarrow{A^{ξ}B,C,D} = (1_{A} ξ b^{ξ}\overleftarrow{B,C,D})^{∘} b^{ξ}\overleftarrow{A,B^{ξ}C,D} ^{∘} (b^{ξ}\overleftarrow{A,B,C} ξ 1_{D}),

(c^{∧} c^{∧}) c^{∧}_{B,A} ^{∘} c^{∧}_{A,B} = 1_{A∧B},

(c^{∨} c^{∨}) c^{∨}_{A,B} ^{∘} c^{∨}_{B,A} = 1_{A∨B},

(b^{∧} c^{∧}) (1_{B} ∧ c^{∧}_{C,A})^{∘} b^{∧}\overleftarrow{B,C,A} ^{∘} c^{∧}_{A,B∧C} ^{∘} b^{∧}\overleftarrow{A,B,C} ^{∘} (c^{∧}_{B,A} ∧ 1_{C}) = b^{∧}\overleftarrow{B,A,C},

(b^{∨} c^{∨}) (1_{B} ∨ c^{∨}_{A,C})^{∘} b^{∨}\overleftarrow{B,C,A} ^{∘} c^{∨}_{B∨C,A} ^{∘} b^{∨}\overleftarrow{A,B,C} ^{∘} (c^{∨}_{A,B} ∨ 1_{C}) = b^{∨}\overleftarrow{B,A,C},

(d∧) (b^{∧}\overleftarrow{A,B,C} ∨ 1_{D})^{∘} d_{A∧B,C,D} = d_{A,B∧C,D} ^{∘} (1_{A} ∧ d_{B,C,D})^{∘} b^{∧}\overleftarrow{A,B,C∨D},

(d∨) d_{D,C,B∨A} ^{∘} (1_{D} ∧ b^{∨}\overleftarrow{C,B,A}) = b^{∨}\overleftarrow{D∧C,B,A} ^{∘} (d_{D,C,B} ∨ 1_{A})^{∘} d_{D,C∨B,A},

for d_{C,B,A}^{R} =_{df} c^{∨}_{C,B∧A} ^{∘} (c^{∧}_{A,B} ∨ 1_{C})^{∘} d_{A,B,C} ^{∘} (1_{A} ∧ c^{∨}_{B,C})^{∘} c^{∧}_{C∨B,A}:

(C ∨ B) ∧ A ⊢ C ∨ (B ∧ A),

(d b^{∧}) d_{A∧B,C,D}^{R} ^{∘} (d_{A,B,C} ∧ 1_{D}) = d_{A,B,C∧D} ^{∘} (1_{A} ∧ d_{B,C,D}^{R})^{∘} b^{∧}\overleftarrow{A,B∨C,D},

(d b^{∨}) (1_{D} ∨ d_{C,B,A})^{∘} d_{D,C,B∨A}^{R} = b^{∨}\overleftarrow{D,C∧B,A} ^{∘} (d_{D,C,B}^{R} ∨ 1_{A})^{∘} d_{D∨C,B,A}.

The set of equations of DS is closed under symmetry and transitivity of equality and under the rules

(cong ξ) \frac{f = f_{1} g = g_{1}}{f ξ g = f_{1} ξ g_{1}}

where ξ ∈ {^{∘} , ∧, ∨}, and if ξ is ^{∘}, then f ^{∘} g is defined (namely, f and g have appropriate, composable, types).

On the arrow terms of DS we impose the equations of DS. This means that an arrow of DS is an equivalence class of arrow terms of DS defined with respect to the smallest equivalence relation such that the equations of DS are satisfied (see [11, Section 2.3]).

The equations (ξ 1) and (ξ 2) are called bifunctorial equations. They say that ∧ and ∨ are biendofunctors (i.e. 2-endofunctors in the terminology of [11, Section 2.4]).

It is easy to show that for DS we have the equations

(b^{ξ}^{←} nat) (f ξ (g ξ h))^{∘} b^{ξ}\overleftarrow{A,B,C} = b^{ξ}\overleftarrow{D,E,F} ^{∘} ((f ξ g) ξ h),

(d^{R} nat) (h ∨ (g ∧ f))^{∘} d_{C,B,A}^{R} = d_{F,E,D}^{R} ^{∘} ((h ∨ g) ∧ f). We call these equations and other equations with “nat” in their names, like those in the list above, naturality equations. Such equations say that b^{∧}^{→}, b^{∧}^{←}, c^{∧}, etc. are natural transformations.

The equations (d∧), (d∨), (d b^{∧}) and (d b^{∨}) stem from [6, Section 2.1] (see [5, Section 2.1] for an announcement). The equation (d b^{∨}) of [11, Section 7.2] amounts with (b^{∨}b^{∨}) to the present one.

3. The category PN^{¬}

The category PN^{¬} is defined as DS save that we make the following changes and additions. Instead of L_{∧,∨}, we have the propositional language L_{¬,∧,∨}, which has in addition to what we have for L_{∧,∨} the unary connective ¬.

To define the arrow terms of PN^{¬}, in the inductive definition we had for the arrow terms of DS we assume in addition that for all formulae A and B of L_{¬,∧,∨} the following primitive arrow terms:

Δ^{∧}_{B,A}: A ⊢ A ∧ (¬B ∨ B),

Σ^{∨}_{B,A}: (B ∧ ¬B) ∨ A ⊢ A,

are arrow terms of PN^{¬}. We call the index B, of Δ^{∧}_{B,A} and Σ^{∨}_{B,A} the crown index, and A the stem index. The crown of Δ^{∧}_{B,A} ic the right conjunct ¬B ∨ B in the target of Δ^{∧}_{B,A}: A ⊢ A ∧ (¬B ∨ B), and the crown of Σ^{∨}_{B,A} is the left disjunct B ∧ ¬B in the source of Σ^{∨}_{B,A}: (B ∧ ¬B) ∨ A ⊢ A. We have analogous definitions of crown and stem indices, and crowns for Σ^{∧}, Δ^{∧}′, Σ^{∧}′, Δ^{∨}, Σ^{∨}′ and Δ^{∨}′, which will be defined below. (The symbol Δ should be associated with the Latin dexter, because in Δ^{∧}_{B,A}, Δ^{∧}′_{B,A}, Δ^{∨}_{B,A} and Δ^{∨}′_{B,A} the crown is on the right-hand side of the stem; analogously, Σ should be associated with sinister.)

To define the arrows of PN^{¬}, we assume in the inductive definition we had for the equations of DS the following additional equations, which we call the PN equations (and not PN^{¬} equations):

(Δ^{∧} nat) (f ∧ 1_{¬B∨B})^{∘} Δ^{∧}_{B,A} = Δ^{∧}_{B,D} ^{∘} f,

(Σ^{∨} nat) f ^{∘} Σ^{∨}_{B,A} = Σ^{∨}_{B,D} ^{∘} (1_{B∧¬B} ∨ f),

(b^{∧}Δ^{∧})  b^{∧}\overleftarrow{A,B,¬C∨C} ^{∘} Δ^{∧}_{C,A∧B} = 1_{A} ∧ Δ^{∧}_{C,B},
(b^{∨}Σ^{∨})  Σ^{∨}_{C,B∨A} ^{∘} b^{∨}\overleftarrow{C∧¬C,B,A} = Σ^{∨}_{C,B} ∨ 1_{A},

for Σ^{∧}_{B,A} =_{df} c^{∧}_{A,¬B∨B} ^{∘} Δ^{∧}_{B,A} : A ⊢ (¬B ∨ B) ∧ A,

(dΣ^{∧}) d_{¬A∨A,B,C} ^{∘} Σ^{∧}_{A,B∨C} = Σ^{∧}_{A,B} ∨ 1_{C},

for Δ^{∨}_{B,A} =_{df} Σ^{∨}_{B,A} ^{∘} c^{∨}_{B∧¬B,A} : A ∨ (B ∧ ¬B) ⊢ A,

(dΔ^{∨})  Δ^{∨}_{A,C∧B} ^{∘} d_{C,B,A∧¬A} = 1_{C} ∧ Δ^{∨}_{A,B},
(Σ^{∨}Δ^{∧})  Σ^{∨}_{A,A} ^{∘} d_{A,¬A,A} ^{∘} Δ^{∧}_{A,A} = 1_{A},

for Δ^{∧}′_{B,A} =_{df} (1_{A} ∧ c^{∨}_{B,¬B})^{∘} Δ^{∧}_{B,A} : A ⊢ A ∧ (B ∨ ¬B) and

Σ^{∨}′_{B,A} =_{df} Σ^{∨}_{B,A} ^{∘} (c^{∧}_{¬B,B} ∨ 1_{A}) : (¬B ∧ B) ∨ A ⊢ A,

(Σ^{∨}′ Δ^{∧}′) Σ^{∨}′_{A,¬A} ^{∘} d_{¬A,A,¬A} ^{∘} Δ^{∧}′_{A,¬A} = 1_{¬A}.

It is easy to show that for PN^{¬} we have the equations

(Σ^{∧} nat) (1_{¬B∨B} ∧ f)^{∘} Σ^{∧}_{B,A} = Σ^{∧}_{B,D} ^{∘} f,

(Δ^{∨} nat) f ^{∘} Δ^{∨}_{B,A} = Δ^{∨}_{B,D} ^{∘} (f ∨ 1_{B∧¬B}).

The naturality equations (Δ^{∧} nat) and (Σ^{∨} nat) together with these say that Δ^{∧}, Σ^{∨}, Σ^{∧} and Δ^{∨} are natural transformations in the stem index only, i.e. in the second index.

We also have the following abbreviations:

Σ^{∧}′_{B,A} =_{df} c^{∧}_{A,B∨¬B} ^{∘} Δ^{∧}′_{B,A} : A ⊢ (B ∨ ¬B) ∧ A,

Δ^{∨}′_{B,A} =_{df} Σ^{∨}′_{B,A} ^{∘} c^{∨}_{¬B∧B,A} : A ∨ (¬B ∧ B) ⊢ A.

If Ξ stands for either Δ or Σ and ξ ∈ {∧, ∨}, then for every (Ξ^{ξ} nat) equation we

have in PN^{¬} the equation (Ξ^{ξ}′ nat), which differs from (Ξ^{ξ} nat) by replacing Ξ^{ξ} by

Ξ^{ξ}′, and the index of 1 by the appropriate index. For example, we have

(Δ^{∧}′ nat) (f ∧ 1_{B∨¬B})^{∘} Δ^{∧}′_{B,A} = Δ^{∧}′_{B,D} ^{∘} f.

As alternative primitive arrow terms for defining PN^{¬} we could take one of Ξ^{∧} or Ξ^{∧}′ and one of Ξ^{∨} or Ξ^{∨}′.

We can also derive for PN^{¬} the following equations:

(b^{∧}Δ^{∧}Σ^{∧})  b^{∧}\overleftarrow{A,¬B∨B,C} ^{∘} (Δ^{∧}_{B,A} ∧ 1_{C}) = 1_{A} ∧ Σ^{∧}_{B,C},
(b^{∧}Σ^{∧})  b^{∧}\overrightarrow{¬C∨C,B,A} ^{∘} Σ^{∧}_{C,B∧A} = Σ^{∧}_{C,B} ∧ 1_{A}.

For the first equation, with indices omitted, we have

b^{∧}^{←} ^{∘} (Δ^{∧} ∧ 1) = b^{∧}^{←} ^{∘} c^{∧} ^{∘} (1 ∧ Δ^{∧})^{∘} c^{∧}, by (c^{∧} c^{∧}) and (c^{∧} nat),

= b^{∧}^{←} ^{∘} c^{∧} ^{∘} b^{∧}^{←} ^{∘} Δ^{∧} ^{∘} c^{∧}, by (b^{∧}Δ^{∧}),

= (1 ∧ c^{∧})^{∘} b^{∧}^{←} ^{∘} Δ^{∧}, with (Δ^{∧} nat) and (b^{∧} c^{∧}),

= 1 ∧ Σ^{∧}, by (b^{∧}Δ^{∧}),

and for the second equation we have

b^{∧}^{→} ^{∘} Σ^{∧} = b^{∧}^{→} ^{∘} c^{∧} ^{∘} b^{∧}^{→} ^{∘} (1 ∧ Δ^{∧}), with (b^{∧}Δ^{∧}),

= (c^{∧} ∧ 1)^{∘} b^{∧}^{→} ^{∘} (1 ∧ c^{∧})^{∘} (1 ∧ Δ^{∧}), by (b^{∧} c^{∧}),

= Σ^{∧} ∧ 1, with (b^{∧}Δ^{∧}Σ^{∧}).

We derive analogously with the help of (b^{∨}Σ^{∨}) the equations

(b^{∨}Δ^{∨}Σ^{∨}) (Δ^{∨}_{B,A} ∨ 1_{C})^{∘} b^{∨}\overrightarrow{A,B∧¬B,C} = 1_{A} ∨ Σ^{∨}_{B,C},

(b^{∨}Δ^{∨})  Δ^{∨}_{C,A∨B} ^{∘} b^{∨}\overrightarrow{A,B,C∧¬C} = 1_{A} ∨ Δ^{∨}_{C,B}.

The arrows Δ^{∧}_{B,A}: A ⊢ A ∧ (¬B ∨ B) and Σ^{∧}_{B,A}: A ⊢ (¬B ∨ B) ∧ A are analogous to the arrows of types A ⊢ A ∧ ⊤ and A ⊢ ⊤ ∧ A that one finds in monoidal categories. However, Δ^{∧}_{B,A} and Σ^{∧}_{B,A} do not have inverses in PN^{¬}. The equations (b^{∧}Δ^{∧}), (b^{∧}Δ^{∧}Σ^{∧}), (b^{∧}Σ^{∧}) are analogous to equations that hold in monoidal categories (see [19, Section VII.1], [11, Section 4.6]). An analogous remark can be made for

Σ^{∨}_{B,A} and Δ^{∨}_{B,A}.

We can also derive for PN^{¬} the following equations by using essentially (dΣ^{∧})

and (dΔ^{∨}):

(d^{R} Δ^{∧}) d_{C,B,¬A∨A}^{R} ^{∘} Δ^{∧}_{A,C∨B} = 1_{C} ∨ Δ^{∧}_{A,B},

(d^{R} Σ^{∨})  Σ^{∨}_{A,B∧C} ^{∘} d_{A∧¬A,B,C}^{R} = Σ^{∨}_{A,B} ∧ 1_{C}.

These two equations could replace (dΣ^{∧}) and (dΔ^{∨}) for defining PN^{¬}. The analogues of the equations (dΣ^{∧}), (dΔ^{∨}), (d^{R} Δ^{∧}) and (d^{R} Σ^{∨}) may be found in [6, Section 2.1], where they are assumed for linearly (alias weakly) distributive categories with negation (cf. [11, Section 7.9]).

It is easy to infer that in PN^{¬} we have analogues of the equations (b^{∧}Δ^{∧}), (b^{∧}Δ^{∧}Σ^{∧}),

(b^{∧}Σ^{∧}), (b^{∨}Σ^{∨}), (b^{∨}Δ^{∨}Σ^{∨}), (b^{∨}Δ^{∨}), (dΣ^{∧}), (dΔ^{∨}), (d^{R} Δ^{∧}) and (d^{R} Σ^{∨}) obtained by replacing Ξ^{ξ}

by Ξ^{ξ}′, and the indices of the form ¬B ∨ B and B ∧ ¬B by B ∨ ¬B and ¬B ∧ B respectively. For example, we have

(b^{∧}Δ^{∧}′)  b^{∧}\overleftarrow{A,B,C∨¬C} ^{∘} Δ^{∧}′_{C,A∧B} = 1_{A} ∧ Δ^{∧}′_{C,B}.

We can also derive for PN^{¬} the following equations by using essentially (Σ^{∨}Δ^{∧})

and (Σ^{∨}′ Δ^{∧}′):

(Δ^{∨}′ Σ^{∧}′)  Δ^{∨}′_{A,A} ^{∘} d_{A,¬A,A}^{R} ^{∘} Σ^{∧}′_{A,A} = 1_{A},
(Δ^{∨}Σ^{∧})  Δ^{∨}_{A,¬A} ^{∘} d_{¬A,A,¬A}^{R} ^{∘} Σ^{∧}_{A,¬A} = 1_{¬A}.

These two equations could replace (Σ^{∨}Δ^{∧}) and (Σ^{∨}′ Δ^{∧}′) for defining PN^{¬}. The equations (Σ^{∨}Δ^{∧}), (Σ^{∨}′ Δ^{∧}′), (Δ^{∨}′ Σ^{∧}′) and (Δ^{∨}Σ^{∧}) are related to the triangular equations of an adjunction (see [19, Section IV.1]; see also the next section). The analogues of these equations may be found in [6, Section 4].

A proof-net category is a category with two biendofunctors ∧ and ∨, a unary operation ¬ on objects, and the natural transformations b^{∧}^{→}, b^{∧}^{←}, b^{∨}^{→}, b^{∨}^{←}, c^{∧}, c^{∨}, d,

Δ^{∧} and Σ^{∨} that satisfy the equations (b^{ξ} 5), (b^{ξ}b^{ξ}), …, (Σ^{∨}′ Δ^{∧}′) of PN^{¬}. The category PN^{¬} is up to isomorphism the free proof-net category generated by the set of letters P (the set P may be understood as a discrete category).

If β is a primitive arrow term of PN^{¬} except 1_{B}, then we call β-terms of PN^{¬} the set of arrow terms defined inductively as follows: β is a β-term; if f is a βterm, then for every A in L_{∧,∨} we have that 1_{A} ξ f and f ξ 1_{A}, where ξ ∈ {∧, ∨}, are β-terms.

In a β-term the subterm β is called the head of this β-term. For example, the

head of the b^{∧}\overrightarrow{B,C,D}-term 1_{A} ∧ (b^{∧}\overrightarrow{B,C,D} ∨ 1_{E}) is b^{∧}\overrightarrow{B,C,D}.

We define 1-terms as β-terms by replacing β in the definition above by 1_{B}. So 1-terms are headless.

An arrow term of the form f_{n} ^{∘} … ^{∘} f_{1}, where n ⩾ 1, with parentheses tied to ^{∘} associated arbitrarily, such that for every i ∈ {1, …, n} we have that f_{i} is composition-free is called factorized. In a factorized arrow term f_{n} ^{∘} … ^{∘} f_{1} the arrow terms f_{i} are called factors. A factor that is a β-term for some β is called a headed factor. A factorized arrow term is called headed when each of its factors is either headed or a 1-term. A factorized arrow term f_{n} ^{∘} … ^{∘} f_{1} is called developed when f_{1} is a 1-term and if n > 1, then every factor of f_{n} ^{∘} … ^{∘} f_{2} is headed. It is sometimes useful to write the factors of a headed arrow term one above the other, as it is done for example in Figure 1 at the end of §6.

By using the categorial equations (cat 1) and (cat 2) and bifunctorial equations we can easily prove by induction on the length of f the following lemma.

Development Lemma. For every arrow term f there is a developed arrow term f′ such that f = f′ in PN^{¬}.

Analogous definitions of β-term and developed arrow term can be given for DS, and an analogous Development Lemma can be proved for DS.

4. The category Br

We are now going to introduce a category called Br, which will serve to prove our main coherence result for proof-net categories. We will show that there is a faithful functor from PN^{¬} to Br. The name of the category Br comes from “Brauerian”. The arrows of this category correspond to graphs, or diagrams, that were introduced in [3] in connection with Brauer algebras. Analogous graphs were investigated in [13], and in [17] Kelly and Mac Lane relied on them to prove their coherence result for symmetric monoidal closed categories.

Let M be a set whose subsets are denoted by X, Y, Z, … For i ∈ {s, t} (where s stands for “source” and t for “target”), let M^{i} be a set in one-to-one correspondence with M, and let i: M → M^{i} be a bijection. Let X^{i} be the subset of M^{i} that is the image of the subset X of M under i. If u ∈ M, then we use u_{i} as an abbreviation for i(u). We assume also that M, M^{s} and M^{t} are mutually disjoint.

For X, Y ⊆ M, let a split relation of M be a triple ⟨R, X, Y ⟩ such that R ⊆ (X^{s} ∪ Y^{t})^{2}. The set X^{s} ∪ Y^{t} may be conceived as the disjoint union of X and Y. We denote a split relation ⟨R, X, Y ⟩ more suggestively by R: X ⊢ Y.

A split relation R: X ⊢ Y is a split equivalence when R is an equivalence relation. We denote by part(R) the partition of X_{s} ∪ Y_{t} corresponding to the split equivalence R: X ⊢ Y.

A split equivalence R: X ⊢ Y is Brauerian when every member of part(R) is a two-element set. For R: X ⊢ Y a Brauerian split equivalence, every member of part(R) is either of the form {u_{s}, v_{t}}, in which case it is called a transversal, or of the form {u_{s}, v_{s}}, in which case it is called a cup, or, finally, of the form {u_{t}, v_{t}}, in which case it is called a cap.

For X, Y, Z ∈ M, we want to define the composition P ∗ R: X ⊢ Z of the split relations R: X ⊢ Y and P: Y ⊢ Z of M. For that we need some auxiliary notions.

For X, Y ⊆ M, let the function φ^{s}: X ∪ Y^{t} → X^{s} ∪ Y^{t} be defined by

φ^{s}(u) = \{ \begin{matrix}u_{s} & if u ∈ X \\ u & if u ∈ Y^{t}, \end{matrix}

and let the function φ^{t}: X^{s} ∪ Y → X^{s} ∪ Y^{t} be defined by

φ^{t}(u) = \{ \begin{matrix}u & if u ∈ X^{s} \\ u_{t} & if u ∈ Y. \end{matrix}

For a split relation R: X ⊢ Y, let the two relations R^{−s} ⊆ (X ∪ Y^{t})^{2} and R^{−t} ⊆ (X^{s} ∪ Y)^{2} be defined by

(u, v) ∈ R^{−i} iff (φ^{i}(u), φ^{i}(v)) ∈ R

for i ∈ {s, t}. Finally, for an arbitrary binary relation R, let Tr(R) be the transitive closure of R.

Then we define P ∗ R by

P ∗ R =_{df} Tr(R^{−t} ∪ P^{−s}) ∩ (X^{s} ∪ Z^{t})^{2}.

It is easy to conclude that P ∗ R: X ⊢ Z is a split relation of M, and that if R: X ⊢ Y and P: Y ⊢ Z are (Brauerian) split equivalences, then P ∗ R is a (Brauerian) split equivalence.

We now define the category Br. The objects of Br are the members of the set of finite ordinals N. (We have 0 = ∅ and n+1 = n ∪ {n}, while N is the ordinal ω.) The arrows of Br are the Brauerian split equivalences R: m ⊢ n of N. The identity arrow 1_{n}: n ⊢ n of Br is the Brauerian split equivalence such that

part(1_{n}) = {{m_{s}, m_{t}} | m < n}.

Composition in Br is the operation ∗ defined above.

That Br is indeed a category (i.e. that ∗ is associative and that 1_{n} is an identity arrow) is proved in [9] and [10]. This proof is obtained via an isomorphic representation of Br in the category Rel, whose objects are the finite ordinals and whose arrows are all the relations between these objects. Composition in Rel is the ordinary composition of relations. A direct formal proof would be more involved, though what we have to prove is rather clear if we represent Brauerian split equivalences geometrically (as this is done in [3], [13], and also in categories of tangles; see [16, Chapter 12] and references therein).

For example, for R ⊆ (3^{s} ∪ 9^{t})^{2} and P ⊆ (9^{s} ∪ 1^{t})^{2} such that

part(R) = {{0_{s}, 0_{t}}, {1_{s}, 3_{t}}, {2_{s}, 6_{t}}} ∪ {{n_{t}, (n+1)_{t}} | n ∈ {1, 4, 7}},
part(P) = {{2_{s}, 0_{t}}} ∪ {{n_{s}, (n+1)_{s}} | n ∈ {0, 3, 5, 7}},

the composition P ∗ R ⊆ (3^{s} ∪ 1^{t})^{2}, for which we have

part(P ∗ R) = {{0_{s}, 0_{t}}, {1_{s}, 2_{s}}},

is obtained from the following diagram:

[figure: 0; 0; 1; 2; 3; 4; 5; 6; 7; 8; 0; 1; 2; R; P]

Every bijection f from X^{s} to Y^{t} corresponds to a Brauerian split equivalence R: X ⊢ Y such that the members of part(R) are of the form {u, f(u)}. The composition of such Brauerian split equivalences, which correspond to bijections, is then a simple matter: it amounts to composition of these bijections. If in Br we keep as arrows only such Brauerian split equivalences, then we obtain a subcategory of Br isomorphic to the category Bij whose objects are again the finite ordinals and whose arrows are the bijections between these objects. The category Bij is a subcategory of the category Rel (which played an important role in [11]), whose objects are the finite ordinals and whose arrows are all the relations between these objects. Composition in Bij and Rel is the ordinary composition of relations. The category Rel (which played an important role in [11]) is isomorphic to a subcategory of the category whose arrows are split relations of finite ordinals, of whom Br is also a subcategory.

We define a functor G from PN^{¬} to Br in the following way. On objects, we stipulate that GA is the number of occurrences of letters in A. (If A has n = {0, 1, …, n−1} occurrences of letters, then the first occurrence corresponds to 0, the second to 1, etc.) On arrows, we have first that Gα is an identity arrow of

Br for α being 1_{A}, b^{ξ}\overrightarrow{A,B,C}, b^{ξ}\overleftarrow{A,B,C} and d_{A,B,C}, where ξ ∈ \{∧, ∨\}.

Next, for i, j ∈ {s, t}, we have that {m_{i}, n_{j}} belongs to part(G c^{∧}_{A,B}) iff {n_{i}, m_{j}} belongs to part(G c^{∨}_{A,B}), iff i is s and j is t, while m, n < GA+GB and

(m−n−GA)(m−n+GB) = 0.

In the following example, we have G(p ∨ q) = 2 = {0, 1} and G((q ∨ ¬r) ∨ q)= 3 = {0, 1, 2}, and we have the diagrams

[figure: 0; 1; 2; 3; 4; 0; 1; 2; 3; 4; 0; 1; 2; 3; 4; 0; 1; 2; 3; 4; G c^{∧}_{p∨q,(q∨¬r)∨q}; G c^{∨}_{p∨q,(q∨¬r)∨q}; (p ∨ q) ∧ ((q ∨ ¬r) ∨ q); ((q ∨ ¬r) ∨ q) ∧ (p ∨ q); ((q ∨ ¬r) ∨ q) ∨ (p ∨ q); (p ∨ q) ∨ ((q ∨ ¬r) ∨ q)]

We have that {m_{i}, n_{j}} belongs to part(GΔ^{∧}_{B,A}) iff either

i is s and j is t, while m, n < GA and m = n, or

i and j are both t, while m, n ∈ {GA, …, GA+2GB−1} and |m−n| = GB.

In the following example, for A being (q ∨ ¬r) ∨ q and B being p ∨ q, we have

[figure: 0; 1; 2; 3; 4; 5; 6; 0; 1; 2; GΔ^{∧}_{p∨q,(q∨¬r)∨q}; ((q ∨ ¬r) ∨ q) ∧ (¬(p ∨ q) ∨ (p ∨ q)); (q ∨ ¬r) ∨ q]

We have that {m_{i}, n_{j}} belongs to part(GΣ^{∨}_{B,A}) iff either

i is s and j is t, while m ∈ {2GB, …, 2GB+GA−1}, n < GA and m−2GB = n, or

i and j are both s, while m, n < 2GB and |m−n| = GB.

For A and B being as in the previous example, we have

[figure: 0; 1; 2; 3; 4; 5; 6; 0; 1; 2; GΣ^{∨}_{p∨q,(q∨¬r)∨q}; (q ∨ ¬r) ∨ q; ((p ∨ q) ∧ ¬(p ∨ q)) ∨ ((q ∨ ¬r) ∨ q)]

Let G(f ^{∘} g) = Gf ∗ Gg. To define G(f ξ g), for ξ ∈ {∧, ∨}, we need an auxiliary notion.

Suppose b_{X} is a bijection from X to X_{1} and b_{Y} a bijection from Y to Y_{1}. Then for R ⊆ (X^{s} ∪ Y^{t})^{2} we define R_{b_{Y}}^{b_{X}} ⊆ (X_{1}^{s} ∪ Y_{1}^{t})^{2} by

(u_{i}, v_{j}) ∈ R_{b_{Y}}^{b_{X}} iff (i(b_{U}^{−1}(u)), j(b_{V}^{−1}(v))) ∈ R,

where (i, U), (j, V) ∈ {(s, X), (t, Y)}.

If f: A ⊢ D and g: B ⊢ E, then for ξ ∈{∧, ∨} the set of ordered pairs G(f ξg) is

Gf ∪ Gg_{+GD}^{+GA}

where +GA is the bijection from GB to {n+GA | n ∈ GB} that assigns n+GA to n, and +GD is the bijection from GE to {n+GD | n ∈ GE} that assigns n+GD to n.

It is not difficult to check that G so defined is indeed a functor from PN^{¬} to Br. For that, we determine by induction on the length of derivation that for every equation f = g of PN^{¬} we have Gf = Gg in Br.

Consider, for example, the following diagram, which illustrates an instance of

(Σ^{∨}Δ^{∧}):

[figure: Σ^{∨}_{p∧q,p∧q}; d_{p∧q,¬(p∧q),p∧q}; Δ^{∧}_{p∧q,p∧q}; p ∧ q; ((p ∧ q) ∧ ¬(p ∧ q))∨(p ∧ q); (p ∧ q)∧(¬(p ∧ q) ∨ (p ∧ q)); p ∧ q]

This diagram shows that the equation (Σ^{∨}Δ^{∧}), as well as the equation (Σ^{∨}′ Δ^{∧}′), which is illustrated by analogous diagrams, is related to triangular equations of adjunctions (cf. [8, Section 4.10]). The triangular equations of adjunctions are essentially about “straightening a serpentine”, and this straightening is based on planar ambient isotopies of knot theory (cf. [4, Section 1.A], ).

We have shown by this induction that Br is a proof-net category, and the existence of a structure-preserving functor G from PN^{¬} to Br follows from the freedom of PN^{¬}.

We can define analogously to G a functor, which we also call G, from the category DS to Br. We just omit from the definition of G above the clauses involving Δ^{∧}_{B,A} and Σ^{∨}_{B,A}. The image of DS by G in Br is the subcategory of Br isomorphic to Bij, which we mentioned above. The following is proved in [11, Section 7.6].

DS Coherence. The functor G from DS to Br is faithful.

It follows immediately from this coherence result that DS is isomorphic to a subcategory of PN^{¬} (cf. [11, Section 14.4]).

Up to the end of §8 we will be occupied with proving the following.

PN^{¬} Coherence. The functor G from PN^{¬} to Br is faithful.

For this proof, we must deal first with some preliminary matters.

5. Some properties of DS

In this section we will prove some results about the category DS, which we will be use to ascertain that particular equations hold in PN^{¬}. We need these results also for the proof of PN^{¬} Coherence.

First we introduce a definition. Suppose x is the n-th occurrence of a letter (counting from the left) in a formula A of L_{¬,∧,∨}, and y is the m-th occurrence of the same letter in a formula B of L_{¬,∧,∨}. Then we say that x and y are linked in an arrow f: A ⊢ B of PN^{¬} when in the partition part(Gf) we have {(n−1)_{s}, (m−1)_{t}} as a member. (Note that to find the n-th occurrence, we count starting from 1, but the ordinal n > 0 is {0, …, n−1}.) We have an analogous definition of linked occurrences of the same letter for DS: we just replace L_{¬,∧,∨} by L_{∧,∨} and PN^{¬} by DS.

It is easy to established by induction on the complexity of f that for every arrow term f: A ⊢ B of DS we have GA = GB. Moreover, every occurrence of letter in A is linked to exactly one occurrence of the same letter in B, and vice versa. This is related to the fact that every arrow term f: A ⊢ B of DS may be obtained by substituting letters for letters out of an arrow term f′: A′ ⊢ B′ of DS such that every letter occurs in A′ at most once, and the same for B′ (see [11, Sections 3.3 and 7.6]).

Suppose for Lemmata 1D and 2D below that f: A ⊢ B is an arrow term of DS such that A has a subformula D in which ∧ does not occur and B has a subformula D′ in which ∧ does not occur, and suppose that every occurrence of a letter in D is linked to an occurrence of a letter in D′ and vice versa. Then we can prove the following.

Lemma 1D. The source A of f is D iff the target B of f is D′.

This follows from the fact, noted above, that GA = GB. The arrow term f in this case can have as subterms that are primitive arrow terms only arrow terms of the forms 1_{E}, b^{∨}\overrightarrow{E,F,G}, b^{∨}\overleftarrow{E,F,G} or c^{∨}_{E,F}. We also have the following.

Lemma 2D. If D ∧ A′ or A′ ∧ D is a subformula of A, then D′ ∧ B′ or B′ ∧ D′ is a subformula of B for some B′.

This is easily proved by induction on the complexity of the arrow term f, with the help of Lemma 1D.

Suppose for Lemmata 1C and 2C below that f: A ⊢ B is an arrow term of DS such that B has a subformula C in which ∨ does not occur and A has a subformula C′ in which ∨ does not occur, and suppose that every occurrence of a letter in C is linked to an occurrence of a letter in C′ and vice versa. Then we can prove the following duals of Lemmata 1D and 2D, in an analogous manner.

Lemma 1C. The target B of f is C iff the source A of f is C′.

Lemma 2C. If C ∨ B′ or B′ ∨ C is a subformula of B, then C′ ∨ A′ or A′ ∨ C′ is a subformula of A for some A′.

Suppose for the following lemma, which is a corollary of either Lemma 2D or Lemma 2C, that f: A ⊢ B is an arrow term of DS such that an occurrence x of a letter p in A is linked to an occurrence y of p in B.

Lemma 2. It is impossible that A has a subformula x ∧ A′ or A′ ∧ x and B has a subformula y ∨ B′ or B′ ∨ y.

Suppose for Lemmata 3D, 3C, 3 and 4 below that f: A ⊢ B is an arrow term of DS, and for i ∈ {1, 2} let x_{i} in A and y_{i} in B be occurrences of the letter p_{i} linked in f (here p_{1} and p_{2} may also be the same letter).

Lemma 3D. If in A we have a subformula A_{1} ∨ A_{2} such that x_{i} occurs in A_{i}, then in B we have a subformula B_{1} ∨ B_{2} or B_{2} ∨ B_{1} such that y_{i} occurs in B_{i}.

This is easily proved by induction on the complexity of the arrow term f. We prove analogously the following.

Lemma 3C. If in B we have a subformula B_{1} ∧ B_{2} such that y_{i} occurs in B_{i}, then in A we have a subformula A_{1} ∧ A_{2} or A_{2} ∧ A_{1} such that x_{i} occurs in A_{i}.

As a corollary of either Lemma 3D or Lemma 3C we have the following.

Lemma 3. It is impossible that A has a subformula x_{1} ∨ x_{2} or x_{2} ∨ x_{1} and B has a subformula y_{1} ∧ y_{2} or y_{2} ∧ y_{1}.

The following lemma, dual to Lemma 3, is a corollary of Lemma 2.

Lemma 4. It is impossible that A has a subformula x_{1} ∧ x_{2} or x_{2} ∧ x_{1} and B has a subformula y_{1} ∨ y_{2} or y_{2} ∨ y_{1}.

Lemma 3 is related to the acyclicity condition of proof nets, while Lemma 4 is related to the connectedness condition (see [7]).

Next we can prove the following lemma.

p-q-r Lemma. Let f: A ⊢ B be an arrow of DS, let x_{i} for i ∈ {1, 2, 3} be occurrences of the letters p, q and r, respectively, in A, and let y_{i} be occurrences of the letters p, q and r, respectively, in B, such that x_{i} and y_{i} are linked in f. Let, moreover, x_{2} ∨ x_{3} be a subformula of A and y_{1} ∧ y_{2} a subformula of B. Then there is a d_{p,q,r}-term h: A′ ⊢ B′ such that x′_{i} are occurrences of the letters p, q and r, respectively, in the source p ∧ (q ∨ r) of the head of h and y′_{i} are occurrences of the letters p, q and r, respectively, in the target (p ∧ q) ∨ r of the head of h, such that for some arrows f_{x}: A ⊢ A′ and f_{y}: B′ ⊢ B of DS we have f = f_{y} ^{∘} h^{∘} f_{x} in DS, and x_{i} is linked to x′_{i} in f_{x}, while y′_{i} is linked to y_{i} in f_{y}.

Proof. The proof of this lemma, of which we give just a sketch, relies on a cutelimination and related results of [11, Sections 7.7-8]. We first find in the category GDS introduced in [11, Section 7.7] a cut-free Gentzen term f′: X ⊢ Y, which corresponds to f, by the relationship that exists between DS and GDS. According to the equations at the beginning of Section 7.8 of [11], which are used for the proof of the Invertibility Lemmata in the same section, in GDS we have the equation f′ = f′′ for a Gentzen term f′′ that has as a subterm either ∧_{p,q}(1_{p}, ∨_{q,r}(1_{q}, 1_{r})) or ∨_{q,r}(∧_{p,q}(1_{p}, 1_{q}), 1_{r}) both of type p ∧ (q ∨ r) ⊢ (p ∧ q) ∨ r. By the relationship that exists between DS and GDS, we can find starting from f′′ an arrow term f_{y} ^{∘} h^{∘} f_{x} equal to f in DS, which satisfies the conditions of the lemma. ⊣

The full force of the Cut-Elimination Theorem of Section 7.7 of [11] is not essential for this proof, but applying this theorem simplifies the proof.

6. The category PN

We now introduce a category called PN, which is equivalent to PN^{¬}. In the objects of PN, the negation connective ¬ will be prefixed only to letters, and hence Δ^{∧}_{B,A} and Σ^{∨}_{B,A} will be primitive only for the crown index B being a letter. Here is the formal definition of PN.

For P being the set of letters that we used to generate L_{∧,∨} and L_{¬,∧,∨} in §§2-3, let P^{¬} be the set {¬p | p ∈ P}. The objects of PN are the formulae of the propositional language L_{∧,∨}^{¬p} generated from P ∪ P^{¬} with the binary connectives ∧ and ∨. To define the arrow terms of PN, in the inductive definition we had for the arrow terms of DS we assume in addition that for every formula A of L_{∧,∨}^{¬p} and every letter p

Δ^{∧}_{p,A}: A ⊢ A ∧ (¬p ∨ p),

Σ^{∨}_{p,A}: (p ∧ ¬p) ∨ A ⊢ A,

are primitive arrow terms of PN.

To define the arrows of PN, we assume as additional equations in the inductive definition we had for the equations of DS the PN equations of §3 restricted to the arrow terms Δ^{∧}_{p,A} and Σ^{∨}_{p,A}. This means that in (Δ^{∧} nat) and (Σ^{∨} nat) the crown index B will be p, in (b^{∧}Δ^{∧}) and (b^{∨}Σ^{∨}) the crown index C will be p, and in (dΣ^{∧}), (dΔ^{∨}), (Σ^{∨}Δ^{∧}) and (Σ^{∨}′ Δ^{∧}′) the crown index A will be p. We define Σ^{∧}_{p,A}, Δ^{∨}_{p,A}, Δ^{∧}′_{p,A},

Σ^{∨}′_{p,A}, Σ^{∧}′_{p,A} and Δ^{∨}′_{p,A} for PN as they were defined in PN^{¬} in terms of Δ^{∧}_{p,A} and

Σ^{∨}_{p,A}.

The following equations of PN, and hence also of PN^{¬}, which we call stemincreasing equations, enable us to have in developed arrow terms only Δ^{∧}_{A,B}-terms and Σ^{∨}_{A,B}-terms that coincide with their heads:

(1 ∧ Δ^{∧}) 1_{A} ∧ Δ^{∧}_{p,B} = b^{∧}\overleftarrow{A,B,¬p∨p} ^{∘} Δ^{∧}_{p,A∧B}, by (b^{∧}Δ^{∧}),

(Δ^{∧} ∧ 1) Δ^{∧}_{p,B} ∧ 1_{A} = c^{∧}_{A,B∧(¬p∨p)} ^{∘} b^{∧}\overleftarrow{A,B,¬p∨p} ^{∘} (c^{∧}_{B,A} ∧ 1_{¬p∨p})^{∘} Δ^{∧}_{p,B∧A},

by (c^{∧} c^{∧}), (c^{∧} nat), (1 ∧ Δ^{∧}) and (Δ^{∧} nat),

(1 ∨ Δ^{∧}) 1_{A} ∨ Δ^{∧}_{p,B} = d_{A,B,¬p∨p}^{R} ^{∘} Δ^{∧}_{p,A∨B}, by (d^{R} Δ^{∧}),

(Δ^{∧} ∨ 1) Δ^{∧}_{p,B} ∨ 1_{A} = c^{∨}_{B∧(¬p∨p),A} ^{∘} d_{A,B,¬p∨p}^{R} ^{∘} (c^{∨}_{A,B} ∧ 1_{¬p∨p})^{∘} Δ^{∧}_{p,B∨A},

by (c^{∨} c^{∨}), (c^{∨} nat), (1 ∨ Δ^{∧}) and (Δ^{∧} nat),

(Σ^{∨} ∨ 1) Σ^{∨}_{p,B} ∨ 1_{A} = Σ^{∨}_{p,B∨A} ^{∘} b^{∨}\overleftarrow{p∧¬p,B,A}, by (b^{∨}Σ^{∨}),

(1 ∨ Σ^{∨}) 1_{A} ∨ Σ^{∨}_{p,B} = Σ^{∨}_{p,A∨B} ^{∘} (1_{p∧¬p}∨ c^{∨}_{A,B})^{∘} b^{∨}\overleftarrow{p∧¬p,B,A} ^{∘} c^{∨}_{(p∧¬p)∨B,A},

by (c^{∨} c^{∨}), (c^{∨} nat), (Σ^{∨} ∨ 1) and (Σ^{∨} nat),

(Σ^{∨} ∧ 1) Σ^{∨}_{p,B} ∧ 1_{A} = Σ^{∨}_{p,B∧A} ^{∘} d_{p∧¬p,B,A}^{R}, by (d^{R} Σ^{∨}),

(1 ∧ Σ^{∨}) 1_{A} ∧ Σ^{∨}_{p,B} = Σ^{∨}_{p,A∧B} ^{∘} (1_{p∧¬p} ∨ c^{∧}_{B,A})^{∘} d_{p∧¬p,B,A}^{R} ^{∘} c^{∧}_{A,(p∧¬p)∨B},

by (c^{∧} c^{∧}), (c^{∧} nat), (Σ^{∨} ∧ 1) and (Σ^{∨} nat).

Note that in the stem-increasing equations the stem index B of Δ^{∧} and Σ^{∨} becomes more complex on the right-hand sides, whereas the crown index p does not change. We have analogous stem-increasing equations for Σ^{∧}, Δ^{∧}′, Σ^{∧}′, Δ^{∨}, Σ^{∨}′ and Δ^{∨}′.

We will next prove several lemmata concerning PN, which we will find useful for calculations later on. For these lemmata we need the following.

Let DS^{¬p} be the category defined as DS save that it is generated not by P, but by P ∪ P^{¬}. So the objects of DS^{¬p} are formulae of L_{∧,∨}^{¬p}, i.e. the objects of PN. For A and B formulae of L_{∧,∨}^{¬p}, we define when an occurrence of p in A is linked to an occurrence of p in B in an arrow f: A ⊢ B of DS^{¬p} analogously to what we had at the beginning of the preceding section.

Let Ξ^{ξ} for ξ ∈ {∧, ∨} stand for either Δ^{ξ}, or Δ^{ξ}′, or Σ^{ξ}, or Σ^{ξ}′, and let a Ξ^{ξ}_{B,A}-term

be defined as a β-term in §3, save that β is replaced by Ξ^{ξ}_{B,A}. We use also Θ as a variable alternative to Ξ. Then we have the following.

Ξ^{∧}-Permutation Lemma. Let g: C ⊢ D be a Ξ^{∧}_{p,B}-term of PN such that x_{1} and ¬x_{2} are respectively the occurrences within D of p and ¬p in the crown of the head Ξ^{∧}_{p,B} of g, and let f: D ⊢ E be an arrow term of DS^{¬p} such that we have an occurrence y_{1} of p and an occurrence ¬y_{2} of ¬p within a subformula of E of the form y_{1} ∨ ¬y_{2} or ¬y_{2} ∨ y_{1}, and x_{i} is linked to y_{i} for i ∈ {1, 2} in f. Then there is a Θ^{∧}_{p,B′}-term g′: D′ ⊢ E of PN the crown of whose head is y_{1} ∨ ¬y_{2} or ¬y_{2} ∨ y_{1}, and there is an arrow term f′: C ⊢ D′ of DS^{¬p} such that in PN we have f ^{∘} g = g′ ^{∘} f′.

Proof. By the Development Lemma we can assume that f is a developed arrow term, and then it is enough to consider the case when f is either a β-term for β a primitive arrow term of DS^{¬p} or f is 1_{E}. Note that in the developed arrow term f_{n} ^{∘} … ^{∘} f_{1}, which is equal to f, we have that f_{1} is 1_{D}, and that f_{2}, if it exists, cannot be a d_{B,p,¬p}-term or a d_{B,¬p,p}-term such that x_{1} and ¬x_{2} are the occurrences of p and ¬p in the right conjunct of the source B ∧ (¬p ∨ p) or B ∧ (p ∨ ¬p) of the head of f_{2}. Otherwise, in the target of the head of f_{2} we would obtain as the left disjunct B ∧ ¬p or B ∧ p, which together with Lemma 2 would contradict the conditions put on f, and hence also on f_{n} ^{∘} … ^{∘} f_{1}, in the formulation of the Ξ^{∧}-Permutation Lemma.

The case when f is 1_{E} is trivial, and there are also many easy cases settled by bifunctorial and naturality equations. The remaining, more interesting, cases are settled by the following equations of PN:

b^{∧}\overrightarrow{A,B,¬p∨p} ^{∘} (1_{A} ∧ Δ^{∧}_{p,B}) = Δ^{∧}_{p,A∧B},  by (b^{∧}Δ^{∧}),
b^{∧}\overleftarrow{B_{1},B_{2},¬p∨p} ^{∘} Δ^{∧}_{p,B_{1}∧B_{2}} = 1_{B_{1}} ∧ Δ^{∧}_{p,B_{2}},  by (b^{∧}Δ^{∧}),
b^{∧}\overrightarrow{A,¬p∨p,B} ^{∘} (1_{A} ∧ Σ^{∧}_{p,B}) = Δ^{∧}_{p,A} ∧ 1_{B},  by (b^{∧}Δ^{∧}Σ^{∧}),
b^{∧}\overleftarrow{B,¬p∨p,A} ^{∘} (Δ^{∧}_{p,B} ∧ 1_{A}) = 1_{B} ∧ Σ^{∧}_{p,A},  by (b^{∧}Δ^{∧}Σ^{∧}),
b^{∧}\overrightarrow{¬p∨p,B_{1},B_{2}} ^{∘} Σ^{∧}_{p,B_{1}∧B_{2}} = Σ^{∧}_{p,B_{1}} ∧ 1_{B_{2}},  by (b^{∧}Σ^{∧}),
b^{∧}\overleftarrow{¬p∨p,B,A} ^{∘} (Σ^{∧}_{p,B} ∧ 1_{A}) = Σ^{∧}_{p,B∧A},  by (b^{∧}Σ^{∧}),
c^{∧}_{B,¬p∨p} ^{∘} Δ^{∧}_{p,B} = Σ^{∧}_{p,B},  by definition,
c^{∧}_{¬p∨p,B} ^{∘} Σ^{∧}_{p,B} = Δ^{∧}_{p,B},  by definition and (c^{∧} c^{∧}),
(1_{B} ∧ c^{∨}_{p,¬p})^{∘} Δ^{∧}_{p,B} = Δ^{∧}′_{p,B},  by definition,
(c^{∨}_{p,¬p} ∧ 1_{B})^{∘} Σ^{∧}_{p,B} = Σ^{∧}′_{p,B},  by definition and (c^{∧} nat),
d_{¬p∨p,B_{1},B_{2}} ^{∘} Σ^{∧}_{p,B_{1}∨B_{2}} = Σ^{∧}_{p,B_{1}} ∨ 1_{B_{2}},  by (dΣ^{∧}).

Besides these equations, we have analogous equations where ¬p ∨ p is replaced by p ∨ ¬p, while Δ^{∧} and Σ^{∧} are replaced by Δ^{∧}′ and Σ^{∧}′ respectively, and vice versa. ⊣ We prove analogously the following dual of the preceding lemma.

Ξ^{∨}-Permutation Lemma. Let g: D ⊢ C be a Ξ^{∨}_{p,B}-term of PN such that x_{1} and ¬x_{2} are respectively the occurrences within D of p and ¬p in the crown of the head Ξ^{∨}_{p,B} of g, and let f: E ⊢ D be an arrow term of DS^{¬p} such that we have an occurrence y_{1} of p and an occurrence ¬y_{2} of ¬p within a subformula of E of the form y_{1} ∧ ¬y_{2} or ¬y_{2} ∧ y_{1}, and y_{i} is linked to x_{i} for i ∈ {1, 2} in f. Then there is a Θ^{∨}_{p,B′}-term g′: E ⊢ D′ of PN the crown of whose head is y_{1} ∧ ¬y_{2} or ¬y_{2} ∧ y_{1}, and there is an arrow term f′: D′ ⊢ C of DS^{¬p} such that in PN we have g^{∘} f = f′ ^{∘} g′.

Next we prove the following lemma, which involves the p-q-r Lemma of the preceding section.

p-¬p-p Lemma. Let x_{1}, ¬x_{2} and x_{3} be occurrences of p, ¬p and p, respectively, in a formula A of L_{∧,∨}^{¬p}, and let y_{1}, ¬y_{2} and y_{3} be occurrences of p, ¬p and p, respectively in a formula B of L_{∧,∨}^{¬p}. Let ¬x_{2} ∨ x_{3} or x_{3} ∨ ¬x_{2} be a subformula of A and y_{1} ∧ ¬y_{2} or ¬y_{2} ∧ y_{1} a subformula of B. Let g_{1} : A′ ⊢ A be a Ξ^{∧}_{p,C}-term of PN such that ¬x_{2} ∨ x_{3} or x_{3} ∨ ¬x_{2} is the crown of the head of g_{1}, let g_{2} : B ⊢ B′ be a Θ^{∨}_{p,D}-term of PN such that y_{1} ∧ ¬y_{2} or ¬y_{2} ∧ y_{1} is the crown of the head of g_{2}, and let f: A ⊢ B be an arrow term of DS^{¬p} such that x_{i} and y_{i} are linked in f for i ∈ {1, 2, 3}. Then g_{2} ^{∘} f ^{∘} g_{1} is equal in PN to an arrow term of DS^{¬p}.

Proof. By the p-q-r Lemma, f: A ⊢ B is equal in DS^{¬p}, and hence also in PN, to an arrow term of the form f_{y} ^{∘} h^{∘} f_{x}, where h is a d_{p,¬p,p}-term, and the other conditions of the p-q-r Lemma are satisfied. So in PN we have

g_{2} ^{∘} f ^{∘} g_{1} = g_{2} ^{∘} f_{y} ^{∘} h^{∘} f_{x} ^{∘} g_{1} = f′_{y} ^{∘} g′_{2} ^{∘} h^{∘} g′_{1} ^{∘} f′_{x},

by the Ξ^{ξ}-Permutation Lemmata above. Here the head of g′_{1} must be Δ^{∧}_{p,p}: p ⊢ p ∧ (¬p ∨ p), the head of h is d_{p,¬p,p}: p ∧ (¬p ∨ p) ⊢ (p ∧ ¬p) ∨ p, and the head of g′_{2} must be Σ^{∨}_{p,p}: (p ∧ ¬p) ∨ p ⊢ p. By applying (Σ^{∨}Δ^{∧}), and perhaps bifunctorial equations, we obtain that g′_{2} ^{∘} h^{∘} g′_{1} is equal in PN to an arrow term of the form 1_{A}, and hence we have g_{2} ^{∘} f ^{∘} g_{1} = f′_{y} ^{∘} f′_{x} in PN, which proves the lemma. ⊣

To give an example of the application of the p-¬p-p Lemma, consider the diagram in Figure 1. This diagram corresponds to G(Σ^{∨}_{q,p∧q} ^{∘} h^{∘} Δ^{∧}_{q,p∧q}) for an arrow term h of PN, which is of the form g_{2} ^{∘} f ^{∘} g_{1} for the arrow term g_{1} being 1_{p∧q} ∧ (1_{¬q} ∨ Σ^{∧}_{p,q}), the arrow term g_{2} being (1_{q}∧ Σ^{∨}_{p,¬q}) ∨ 1_{p∧q} and f an arrow term of DS^{¬p}. Then by applying the p-¬p-p Lemma we obtain an arrow term f′ of DS^{¬p} equal to g_{2} ^{∘} f ^{∘} g_{1} in PN, and next by applying the p-¬p-p Lemma (as a matter of fact, the q-¬q-q Lemma), we obtain an arrow term h′ of DS^{¬p} equal to Σ^{∨}_{q,p∧q} ^{∘} f′ ^{∘} Δ^{∧}_{q,p∧q} in PN. By DS Coherence of §4, we may conclude that h′, and hence also Σ^{∨}_{q,p∧q} ^{∘} h^{∘} Δ^{∧}_{q,p∧q}, is equal to 1_{p∧q} in PN.

[figure: p ∧ q; (q ∧ ¬q) ∨ (p ∧ q); (q ∧ ((p ∧ ¬p) ∨ ¬q)) ∨ (p ∧ q); (q ∧ (p ∧ (¬p ∨ ¬q))) ∨ (p ∧ q); ((q ∧ p) ∧ (¬p ∨ ¬q)) ∨ (p ∧ q); ((p ∧ q) ∧ (¬p ∨ ¬q)) ∨ (p ∧ q); (p ∧ q) ∧ ((¬p ∨¬q) ∨ (p ∧ q)); (p ∧ q) ∧ ((¬q ∨ ¬p) ∨ (p ∧ q)); (p ∧ q) ∧ (¬q ∨ (¬p ∨ (p ∧ q))); (p ∧ q) ∧ (¬q∨ ((¬p ∨ p)∧q)); (p ∧ q) ∧ (¬q ∨ q); p ∧ q; Σ^{∨}_{q,p∧q}; (1_{q} ∧ Σ^{∨}_{p,¬q}) ∨ 1_{p∧q}; (1_{q} ∧ d_{p,¬p,¬q}) ∨ 1_{p∧q}; b^{∧}\overleftarrow{q,p,¬p∨¬q} ∨ 1_{p∧q}; (c^{∧}_{p,q} ∧ 1_{¬p∨¬q}) ∨ 1_{p∧q}; d_{p∧q,¬p∨¬q,p∧q}; 1_{p∧q} ∧ (c^{∨}_{¬p,¬q} ∨ 1_{p∧q}); 1_{p∧q} ∧ b^{∨}\overrightarrow{¬q,¬p,p∧q}; 1_{p∧q} ∧ (1_{¬q} ∨ d_{¬p,p,q}^{R}); 1_{p∧q} ∧ (1_{¬q} ∨ Σ^{∧}_{p,q}); Δ^{∧}_{q,p∧q}]

Figure 1

Here is a lemma analogous to the p-¬p-p Lemma.

¬p-p-¬p Lemma. Let ¬x_{1}, x_{2} and ¬x_{3} be occurrences of ¬p, p and ¬p, respectively, in a formula A of L_{∧,∨}^{¬p}, and let ¬y_{1}, y_{2} and ¬y_{3} be occurrences of ¬p, p and ¬p, respectively, in a formula B of L_{∧,∨}^{¬p}. Let g_{1} : A′ ⊢ A be a Ξ^{∧}_{p,C}-term of PN such that x_{2} ∨ ¬x_{3} or ¬x_{3} ∨ x_{2} is the crown of the head of g_{1}, let g_{2} : B ⊢ B′ be a Θ^{∨}_{p,D}-term of PN such that ¬y_{1} ∧ y_{2} or y_{2} ∧ ¬y_{1} is the crown of the head of g_{2}, and let f: A ⊢ B be an arrow term of DS^{¬p} such that x_{i} and y_{i} are linked in f for i ∈ {1, 2, 3}. Then g_{2} ^{∘} f ^{∘} g_{1} is equal in PN to an arrow term of DS^{¬p}.

To prove this lemma we proceed as for the p-¬p-p Lemma, relying on the equation (Σ^{∨}′ Δ^{∧}′) of PN.

7. The equivalence of PN^{¬} and PN

In this section we show that the categories PN^{¬} and PN are equivalent categories. We define inductively a functor F from the category PN^{¬} to PN in the following manner. On objects we have

F p = p, for p a letter, F (A ξ B) = F A ξ F B, for ξ ∈ {∧, ∨}, F ¬p = ¬p, for p a letter, F ¬¬A = F A, F ¬(A ∧ B) = F ¬A ∨ F ¬B, F ¬(A ∨ B) = F ¬A ∧ F ¬B.

On arrows we have F α_{A_{1},...,A_{n}} = α_{F A_{1},...,F A_{n}},

for α_{A_{1},...,A_{n}} being 1_{A}, b^{ξ}\overrightarrow{A,B,C}, b^{ξ}\overleftarrow{A,B,C}, c^{ξ}_{A,B} or d_{A,B,C} where ξ ∈ \{∧, ∨\},

F Δ^{∧}_{p,A} = Δ^{∧}_{p,F A}: F A ⊢ F A ∧ (¬p ∨ p),

F Σ^{∨}_{p,A} = Σ^{∨}_{p,F A}: (p ∧ ¬p) ∨ F A ⊢ F A,

F Δ^{∧}_{¬B,A} = (1_{F A} ∧ c^{∨}_{F B,F ¬B})^{∘} F Δ^{∧}_{B,A}: F A ⊢ F A ∧ (F B ∨ F ¬B),

F Σ^{∨}_{¬B,A} = F Σ^{∨}_{B,A} ^{∘} (c^{∧}_{F ¬B,F B} ∨ 1_{F A}): (F ¬B ∧ F B) ∨ F A ⊢ F A,

F Δ^{∧}_{B∧C,A} = (1_{F A} ∧ ((c^{∨}_{F ¬B,F ¬C} ∨ 1_{F B∧F C})^{∘} b^{∨}\overrightarrow{F ¬C,F ¬B,F B∧F C} ^{∘}

∘ (1_{F ¬C} ∨ (d_{F ¬B,F B,F C}^{R} ^{∘} c^{∧}_{F C,F ¬B∨F B} ^{∘} F Δ^{∧}_{B,C}))))^{∘} F Δ^{∧}_{C,A}:

F A ⊢ F A ∧ ((F ¬B ∨ F ¬C) ∨ (F B ∧ F C)),

F Σ^{∨}_{B∧C,A} = F Σ^{∨}_{C,A} ^{∘} ((1_{F C} ∧ (F Σ^{∨}_{B,¬C} ^{∘} d_{F B,F ¬B,F ¬C}))^{∘}

∘ b^{∧}\overleftarrow{F C,F B,F ¬B∨F ¬C} ^{∘} (c^{∧}_{F B,F C} ∧1_{F ¬B∨F ¬C})) ∨ 1_{F A}):

((F B ∧ F C) ∧ (F ¬B ∨ F ¬C)) ∨ F A ⊢ F A,

F Δ^{∧}_{B∨C,A} = (1_{F A} ∧ ((c^{∧}_{F ¬C,F ¬B} ∨ 1_{F B∨F C})^{∘} b^{∨}\overleftarrow{F ¬C∧F ¬B,F B,F C} ^{∘}

∘ ((d_{F ¬C,F ¬B,F B} ^{∘} F Δ^{∧}_{B,¬C}) ∨ 1_{F C})))^{∘} F Δ^{∧}_{C,A}:

F A ⊢ F A ∧ ((F ¬B ∧ F ¬C) ∨ (F B ∨ F C)),

F Σ^{∨}_{B∨C,A} = F Σ^{∨}_{C,A}^{∘} (((F Σ^{∨}_{B,C} ^{∘} c^{∨}_{F B∧F ¬B,F C} ^{∘} d_{F C,F B,F ¬B}^{R})∧1_{F ¬C})^{∘}

∘ b^{∧}\overrightarrow{F C∨F B,F ¬B,F ¬C} ^{∘} (c^{∨}_{F C,F B} ∧ 1_{F ¬B∧F ¬C})) ∨ 1_{F A}):

((F B ∨ F C) ∧ (F ¬B ∧ F ¬C)) ∨ F A ⊢ F A,

F (f ^{∘} g) = F f ^{∘} F g, F (f ξ g) = F f ξ F g, for ξ ∈ {∧, ∨}.

It is easy to infer

F Δ^{∧}_{¬B,A} = F Δ^{∧}′_{B,A}, F Σ^{∨}_{¬B,A} = F Σ^{∨}′_{B,A},

F Δ^{∧}′_{¬B,A} = F Δ^{∧}_{B,A}, F Σ^{∨}′_{¬B,A} = F Σ^{∨}_{B,A},

F Δ^{∧}_{B,A} = F Δ^{∧}_{B,F A}, F Σ^{∨}_{B,A} = F Σ^{∨}_{B,F A}.

To ascertain that F so defined is indeed a functor, we have to verify that if f = g is an instance of one of the PN equations, then F f = F g holds in PN. This is done by induction on the number od occurrences of connectives in the crown indices occurring in these equations.

For (Δ^{∧} nat) and (Σ^{∨} nat) this is a very easy matter. For (b^{∧}Δ^{∧}), (b^{∨}Σ^{∨}), (dΣ^{∧}) and (dΔ^{∨}) we use essentially naturality equations. (In that context, it might be easier to rely on the equations (d^{R} Δ^{∧}) and (d^{R} Σ^{∨}), which are alternative to (dΣ^{∧}) and (dΔ^{∨}).)

To verify (Σ^{∨}Δ^{∧}) in cases where A is of the form B ∧ C or B ∨ C, we rely on the induction hypothesis that if f = g is an instance of a PN equation such that the crown indices are B and C, then we have F f = F g in PN. This induction hypothesis entails that we can proceed as in the proof of the p-¬p-p Lemma in the preceding section, first for p replaced by B, and then for p replaced by C. Finally, we apply DS Coherence (see the example at the end of the preceding section). To verify (Σ^{∨}Δ^{∧}) in case A is of the form ¬B, we rely on the induction hypothesis for the equation (Σ^{∨}′ Δ^{∧}′).

To verify (Σ^{∨}′ Δ^{∧}′) we proceed analogously. In case A is B ∧ C or B ∨ C, we rely on the proof of the ¬p-p-¬p Lemma in the preceding section, and in case A is ¬B we rely on the induction hypothesis for the equation (Σ^{∨}Δ^{∧}). This concludes the verification that F is a functor from PN^{¬} to PN.

In the definition of F, there is some freedom in choosing the clauses for F Ξ^{ξ}_{BψC,A}, where Ξ ∈ {Δ, Σ} and ξ, ψ ∈ {∧, ∨}. Ours enable us to apply easily the p-¬p-p and ¬p-p-¬p Lemmata in verifying that F is a functor.

We define a functor F^{¬} from PN to PN^{¬} by stipulating that F^{¬}A = A and F^{¬}f = f. It is clear that if f = g in PN, then F^{¬}f = F^{¬}g in PN^{¬}; so F^{¬} is indeed a functor.

Our purpose is to show that PN^{¬} and PN are equivalent categories via the functors F and F^{¬}. It is clear that F F^{¬}A = A and F F^{¬}f = f. Since F^{¬}F A = F A, we have to define in PN^{¬} an isomorphism i_{A}: A ⊢ F A. For that we need the following auxiliary definitions in PN^{¬}:

n\overrightarrow{A} =_{df} Σ^{∨}′_{¬A,A} ^{∘} d_{¬¬A,¬A,A} ^{∘} Δ^{∧}_{A,¬¬A} : ¬¬A ⊢ A,

n\overleftarrow{A} =_{df} Σ^{∨}_{A,¬¬A} ^{∘} d_{A,¬A,¬¬A} ^{∘} Δ^{∧}′_{¬A,A} : A ⊢ ¬¬A,

r^{∧}\overrightarrow{A,B} =_{df} Σ^{∨}′_{A∧B,¬A∨¬B} ^{∘} d_{¬(A∧B),A∧B,¬A∨¬B}^{∘} (1_{¬(A∧B)} ∧ ((1_{A∧B}∨ c^{∨}_{¬A,¬B})^{∘}

∘ b^{∨}\overleftarrow{A∧B,¬B,¬A}^{∘} ((d_{A,B,¬B} ^{∘} Δ^{∧}′_{B,A}) ∨ 1_{¬A})))^{∘} Δ^{∧}′_{A,¬(A∧B)} :

¬(A ∧ B) ⊢ ¬A ∨ ¬B,

r^{∧}\overleftarrow{A,B} =_{df} Σ^{∨}′_{A,¬(A∧B)} ^{∘} ((((Δ^{∨}′_{B,¬A} ^{∘} d_{¬A,¬B,B}^{R}) ∧ 1_{A})^{∘} b^{∧}\overrightarrow{¬A∨¬B,B,A}^{∘}

∘ (1_{¬A∨¬B} ∧ c^{∧}_{A,B})) ∨ 1_{¬(A∧B)})^{∘} d_{¬A∨¬B,A∧B,¬(A∧B)} ^{∘} Δ^{∧}′_{A∧B,¬A∨¬B} :

¬A ∨ ¬B ⊢ ¬(A ∧ B),

r^{∨}\overrightarrow{A,B} =_{df} Σ^{∨}′_{A∨B,¬A∧¬B} ^{∘} d_{¬(A∨B),A∨B,¬A∧¬B} ^{∘} (1_{¬(A∨B)}∧((c^{∨}_{A,B} ∨1_{¬A∧¬B})^{∘}

∘ b^{∨}\overrightarrow{B,A,¬A∧¬B} ^{∘} (1_{B} ∨ (d_{A,¬A,¬B}^{R} ^{∘} Σ^{∧}′_{A,¬B}))))^{∘} Δ^{∧}′_{B,¬(A∨B)} :

¬(A ∨ B) ⊢ ¬A ∧ ¬B,

r^{∨}\overleftarrow{A,B} =_{df} Σ^{∨}′_{B,¬(A∨B)} ^{∘} (((1_{¬B} ∧ (Σ^{∨}′_{A,B} ^{∘} d_{¬A,A,B}))^{∘} b^{∧}\overleftarrow{¬B,¬A,A∨B} ^{∘}

∘ (c^{∧}_{¬A,¬B} ∧ 1_{A∨B})) ∨ 1_{¬(A∨B)})^{∘} d_{¬A∧¬B,A∨B,¬(A∨B)} ^{∘} Δ^{∧}′_{A∨B,¬A∧¬B} :

¬A ∧ ¬B ⊢ ¬(A ∨ B).

It can be shown that in PN^{¬} we have the following equations:

n\overrightarrow{A} ^{∘} n\overleftarrow{A} = 1_{A}, n\overleftarrow{A} ^{∘} n\overrightarrow{A} = 1_{¬¬A},
r^{∧}\overrightarrow{A,B} ^{∘} r^{∧}\overleftarrow{A,B} = 1_{¬A∨¬B},  r^{∧}\overleftarrow{A,B} ^{∘} r^{∧}\overrightarrow{A,B} = 1_{¬(A∧B)},
r^{∨}\overrightarrow{A,B} ^{∘} r^{∨}\overleftarrow{A,B} = 1_{¬A∧¬B},  r^{∨}\overleftarrow{A,B} ^{∘} r^{∨}\overrightarrow{A,B} = 1_{¬(A∨B)},

which means that n^{→} and n^{←}, as well as r^{ξ}^{→} and r^{ξ}^{←} are inverses of each other. To derive these equations in PN^{¬}, we use essentially (Δ^{∧} nat), (Σ^{∨} nat), the p-¬p-p and ¬p-p-¬p Lemmata, and DS Coherence. (If an equation holds in PN, then every substitution instance of it obtained by replacing letters uniformly by formulae of L_{¬,∧,∨} holds in PN^{¬}; this enables us to apply the p-¬p-p and ¬p-p-¬p Lemmata.) The definitions of n^{→}, n^{←}, r^{ξ}^{→} and r^{ξ}^{←}, for ξ ∈ {∧, ∨}, are such that they enable an easy application of the p-¬p-p and ¬p-p-¬p Lemmata.

Then we define i_{A}: A ⊢ F A and its inverse i_{A}^{−1} : F A ⊢ A by induction on the complexity of the formula A of L_{¬,∧,∨} (cf. [11, Section 14.1]):

i_{A} = i_{A}^{−1} = 1_{A}, if A is p or ¬p, for p a letter,
i_{A_{1}^{ξ}A_{2}} = i_{A_{1}} ξ i_{A_{2}},  i_{A_{1}^{ξ}A_{2}}^{−1} = i_{A_{1}}^{−1} ξ i_{A_{2}}^{−1},  for ξ ∈ {∧, ∨},

i_{¬¬B} = i_{B} ^{∘} n\overrightarrow{B}, i_{¬¬B}^{−1} = n\overleftarrow{B} ^{∘} i_{B}^{−1},

i_{¬(A_{1}∧A_{2})} = (i_{¬A_{1}} ∨ i_{¬A_{2}})^{∘} r^{∧}\overrightarrow{A_{1},A_{2}}, i_{¬(A_{1}∧A_{2})}^{−1} = r^{∧}\overleftarrow{A_{1},A_{2}} ^{∘} (i_{¬A_{1}}^{−1} ∨ i_{¬A_{2}}^{−1}),

i_{¬(A_{1}∨A_{2})} = (i_{¬A_{1}} ∧ i_{¬A_{2}})^{∘} r^{∨}\overrightarrow{A_{1},A_{2}}, i_{¬(A_{1}∨A_{2})}^{−1} = r^{∨}\overleftarrow{A_{1},A_{2}} ^{∘} (i_{¬A_{1}}^{−1} ∧ i_{¬A_{2}}^{−1}).

We can then prove the following (cf. [11, Section 14.1]).

Auxiliary Lemma. For every arrow term f: A ⊢ B of PN^{¬} we have f = i_{B}^{−1} ^{∘} F f ^{∘} i_{A} in PN^{¬}.

Proof. We proceed by induction on the complexity of the arrow term f. If f

is a primitive arrow term 1_{A}, b^{ξ}\overrightarrow{A,B,C}, b^{ξ}\overleftarrow{A,B,C}, c^{ξ}_{A,B} or d_{A,B,C}, for ξ ∈ \{∧, ∨\}, then we use naturality equations, and the fact that i_{D} is an isomorphism.

If f is Δ^{∧}_{D,A}, then we proceed by induction on the complexity of D. (This is an auxiliary induction in the basis of the main induction.) If D is p, then we use (Δ^{∧} nat) and the fact that i_{A} is an isomorphism.

If D is ¬B, then we rely on the following equation of PN^{¬}:

(Δ^{∧}n)  Δ^{∧}_{¬B,A} = (1_{A} ∧ (n\overleftarrow{B} ∨ 1_{¬B}))^{∘} Δ^{∧}′_{B,A},

together with the induction hypothesis. To derive (Δ^{∧}n) we have

(1_{A} ∧ (n\overleftarrow{B} ∨ 1_{¬B}))^{∘} Δ^{∧}′_{B,A}

= (1_{A} ∧ (Σ^{∨}_{B,¬¬B} ∨ 1_{¬B}))^{∘} (1_{A} ∧ (d_{B,¬B,¬¬B} ∨ 1_{¬B}))^{∘}

∘ (1_{A} ∧ (Δ^{∧}′_{¬B,B} ∨ 1_{¬B}))^{∘} Δ^{∧}′_{B,A}, by bifunctorial equations,

= (1_{A} ∧ (Σ^{∨}_{B,¬¬B} ∨1_{¬B}))^{∘} (1_{A} ∧ ((d_{B,¬B,¬¬B} ∨ 1_{¬B})^{∘}

∘ c^{∨}_{B∧(¬B∨¬¬B),¬B} ^{∘} d_{¬B,B,¬B∨¬¬B}^{R} ^{∘} (c^{∨}_{¬B,B} ∧ 1_{¬B∨¬¬B})))^{∘}

∘ b^{∧}\overleftarrow{A,¬B,B∨¬B} ^{∘} (Δ^{∧}′_{B,A} ∧ 1_{¬B∨¬¬B})^{∘} (1_{A} ∧ c^{∨}_{¬B,¬¬B})^{∘} Δ^{∧}_{¬B,A},

by stem-increasing equations involving Δ^{∧}′ analogous to (1 ∨ Δ^{∧}) and (1 ∧ Δ^{∧}) of the preceding section, and also (Δ^{∧}′ nat). The equation (Δ^{∧}n) follows by applying the ¬p-p-¬p Lemma (with p replaced by A), and DS Coherence.

If D is B ∧ C, then we rely on the following equation of PN^{¬}:

(Δ^{∧}r)  Δ^{∧}_{B∧C,A} = (1_{A} ∧ (((r^{∧}\overleftarrow{B,C} ^{∘} c^{∨}_{¬B,¬C}) ∨ 1_{B∧C})^{∘} b^{∨}\overrightarrow{¬C,¬B,B∧C} ^{∘}

∘ (1_{¬C} ∨ (d_{¬B,B,C}^{R} ^{∘} Σ^{∧}_{B,C}))))^{∘} Δ^{∧}_{C,A},

together with the induction hypothesis. To show that (Δ^{∧}r) holds in PN^{¬} we proceed as above, by applying essentially stem-increasing equations together with the p-¬p-p Lemma. We proceed analogously when D is B ∨ C.

The cases we have if f is Σ^{∨}_{D,A} are dual to those we had above for f being Δ^{∧}_{D,A}. In all these cases we proceed in an analogous manner. This concludes the basis of the induction.

If f is f_{2} ^{∘} f_{1}, then by the induction hypothesis we have

f_{2} ^{∘} f_{1} = i_{B}^{−1} ^{∘} F f_{2} ^{∘} i_{C} ^{∘} i_{C}^{−1} ^{∘} F f_{1} ^{∘} i_{A}

which yields f = i_{B}^{−1} ^{∘} F f ^{∘} i_{A}, by the fact that i_{C} is an isomorphism and by the functoriality of F.

If f is f_{1} ξ f_{2}, for ξ ∈ {∧, ∨}, then i_{A_{1}^{ξ}A_{2}} is i_{A_{1}} ξ i_{A_{2}} and i_{B_{1}^{ξ}B_{2}}^{−1} is i_{B_{1}}^{−1} ξ i_{B_{2}}^{−1}; we obtain f = i_{B}^{−1} ^{∘} F f ^{∘} i_{A} by using bifunctorial equations. ⊣

The Auxiliary Lemma shows that i_{A} is an isomorphism natural in A, and so we may conclude that PN^{¬} and PN are equivalent categories.

8. PN Coherence

We define a functor G from PN to Br as we defined it from PN^{¬} to Br. In the clauses for Δ^{∧}_{B,A} and Σ^{∨}_{B,A} we just restrict B to a letter p. For f an arrow term of PN^{¬} we have that GF f coincides with Gf where F is the functor from PN^{¬} to PN of the preceding section, G in GF f is the functor G from PN to Br and G in Gf is the functor G from PN^{¬} to Br. To show that, it is essential to check that GF Δ^{∧}_{B,A} and GF Σ^{∨}_{B,A} coincide with GΔ^{∧}_{B,A} and GΣ^{∨}_{B,A} respectively.

In this section we will prove that G from PN to Br is faithful. This will imply that G from PN^{¬} to Br is faithful too.

Analogously to what we had at the beginning of §5, we define when an occurrence x of a letter p in A is linked to an occurrence y of the same letter p in B in an arrow f: A ⊢ B of PN. We say that x and y are directly linked in a headed factorized arrow term f_{n} ^{∘} … ^{∘} f_{1} of PN when x and y are linked in the arrow f_{n} ^{∘} … ^{∘} f_{1}, and for every i ∈ {2, …, n} if f_{i} is a Σ^{∨}_{p,C}-term and z is one of the two occurrences of p in the crown p ∧ ¬p of the head of f_{i}, then x and z are not linked in the arrow f_{i−1} ^{∘} … ^{∘} f_{1} (see the end of §3 for the definition of headed factorized arrow term).

An alternative definition of directly linked x and y in a headed factorized arrow term f_{1} ^{∘} … ^{∘} f_{n} of PN is obtained by stipulating that x and y are linked in the arrow f_{1} ^{∘} … ^{∘} f_{n}, and for every i ∈ {2, …, n} if f_{i} is a Δ^{∧}_{p,D}-term and z is one of the two occurrences of p in the crown ¬p ∨ p of the head of f_{i}, then z and y are not linked in the arrow f_{1} ^{∘} … ^{∘} f_{i−1}.

For example, the occurrence of q in the source p ∧ q and the occurrence of q in the target q ∧ p of

c^{∧}_{p,q} ^{∘} (Σ^{∨}_{p,p} ∧ 1_{q})^{∘} (d_{p,¬p,p} ∧ 1_{q})^{∘} (Δ^{∧}_{p,p} ∧ 1_{q})

are directly linked in this headed factorized arrow term of PN, while the two occurrences of p in its source and target are not directly linked.

Take a headed factorized arrow term of PN of the form g_{2} ^{∘} f ^{∘} g_{1} where g_{1} is a Δ^{∧}_{p,D}-term and g_{2} is Σ^{∨}_{p,C}-term. Let ¬x_{1} ∨ x_{2} be the crown of the head of g_{1} (so x_{1} and x_{2} are both occurrences of p) and let y_{2} ∧ ¬y_{1} be the crown of the head of g_{2} (so y_{1} and y_{2} are also occurrences of the same letter p). We say that g_{1} and g_{2} are confronted through f when x_{i} and y_{i} are directly linked for some i ∈ {1, 2} in the arrow term f.

Let a Δ^{∧}_{p,A}-term that is a factor of a factorized arrow term f be called a Δ^{∧}- factor. We have an analogous definition of Σ^{∨}-factor obtained by replacing Δ^{∧} by Σ^{∨}. We can then prove the following lemma.

Confrontation Lemma. For every headed factorized arrow term g_{2} ^{∘} f ^{∘} g_{1} of PN such that g_{1} and g_{2} are confronted through f there is a headed factorized arrow term h of PN with a subterm of the form g′_{2} ^{∘} f′ ^{∘} g′_{1} such that g′_{1} is a Δ^{∧}-factor, g′_{2} is a Σ^{∨}-factor, g′_{1} and g′_{2} are confronted through f′, and, moreover,

(1) f′ is an arrow term of DS^{¬p},

(2) g_{2} ^{∘} f ^{∘} g_{1} = h in PN,

(3) the number of Δ^{∧}-factors is equal in g_{2} ^{∘} f ^{∘} g_{1} and h, and the same for the number of Σ^{∨}-factors.

Proof. We proceed by induction on the number n of factors of f that are Δ^{∧}-factors or Σ^{∨}-factors. If n = 0, then the arrow term f′ coincides with the arrow term f.

If n > 0, then let g_{2} ^{∘} f ^{∘} g_{1} be of the form f_{2} ^{∘} g^{∘} f_{1} for g a Δ^{∧}_{q,E}-term (we proceed analogously when g is a Σ^{∨}_{q,E}-term). According to the stem-increasing equations of §6, we may assume that g coincides with its head Δ^{∧}_{q,E}. Then by (Δ^{∧} nat) we obtain in PN

g_{2} ^{∘} f ^{∘} g_{1} = f_{2} ^{∘} (f_{1} ∧ 1_{¬q∨q})^{∘} Δ^{∧}_{q,E′} .

After f_{1} ∧ 1_{¬q∨q} in f_{2} ^{∘} (f_{1} ∧ 1_{¬q∨q}) is replaced by a headed factorized arrow term g_{2} ^{∘} f′′ ^{∘} (g_{1} ∧ 1_{¬q∨q}), we may apply the induction hypothesis to this arrow term, because it can easily be seen that g_{1} ∧ 1_{¬q∨q} and g_{2} are confronted through f′′, and f′′ has one Δ^{∧}-factor less than f. ⊣

A headed factorized arrow term of PN that has no subterm of the form g_{2} ^{∘} f ^{∘} g_{1} with g_{1} and g_{2} confronted through f is called pure. For a pure arrow term f there is a one-to-one correspondence, which we call the Δ^{∧}-cap bijection, between the Δ^{∧}-factors of f and the caps of the partition part(Gf). In this bijection, a cap ties, in an obvious sense, the occurrences of p in the crown ¬p ∨ p of the head of the corresponding Δ^{∧}-factor. There is an analogous one-to-one correspondence, which we call the Σ^{∨}-cup bijection, between the Σ^{∨}-factors of f and the cups of part(Gf) (see §4 for the notions of cup and cap). Intuitively speaking, this follows from the fact that in a sequence of cups and caps tied to each other as in the following example:

[figure: ∗; ∗]

cups and caps must alternate. For a pair made of a cap and a cup that is its immediate neighbour, like those marked with ∗ in the picture, we can find a subterm g_{2} ^{∘} f ^{∘} g_{1} such that g_{1} and g_{2} are confronted through f.

We can then prove the following.

Purification Lemma. Every arrow term of PN is equal in PN to a pure arrow term of PN.

Proof. We apply first the Development Lemma of §3. If in the resulting developed arrow term h we have a subterm g_{2} ^{∘} f ^{∘} g_{1} with g_{1} and g_{2} confronted through f, then we apply first the Confrontation Lemma to obtain a developed arrow term h′ with a subterm of the form g′_{2} ^{∘} f′ ^{∘} g′_{1} where g′_{1} and g′_{2} are confronted through f′, and f′ is an arrow term of DS^{¬p}.

Suppose that ¬x_{2} ∨ x_{3} is the crown of the head of g′_{1}, and y_{1} ∧ ¬y_{2} is the crown of the head of g′_{2}. Suppose x_{2} is linked to y_{2} in f′. Then, by Lemma 3 of §5, it is impossible that x_{3} is linked to y_{1}, and so there must be an occurrence x_{1} of p different from x_{3} in the source of f′ such that x_{1} is linked to y_{1} in f′, and there must be an occurrence y_{3} of p different from y_{1} in the target of f′ such that x_{3} is linked to y_{3} in f′. Next we apply the p-¬p-p Lemma of §6 to conclude that g′_{2} ^{∘} f′ ^{∘} g′_{1} is equal to an arrow term h′′ of DS^{¬p}.

After replacing g′_{2} ^{∘} f′ ^{∘} g′_{1} in h′ by h′′, we obtain a headed factorized arrow term in which there is one Δ^{∧}-factor and one Σ^{∨}-factor less than in h′, and hence also than in h, by clause (3) of the Confrontation Lemma.

If x_{3} is linked to y_{1}, then we reason analogously by applying Lemma 3 of §5 and the ¬p-p-¬p Lemma of §6.

We can iterate this procedure, which must terminate, because the number of Δ^{∧}-factors and Σ^{∨}-factors in h is finite. ⊣

We can then prove the following.

PN Coherence. The functor G from PN to Br is faithful.

Proof. Suppose for f and g arrow terms of PN of the same type A ⊢ B we have Gf = Gg. By the Purification Lemma, we can assume that f and g are pure arrow terms. Since Gf = Gg, by the Δ^{∧}-cap and Σ^{∨}-cup bijections we must have the same number n ⩾ 0 of Δ^{∧}-factors in f and g and the same number m ⩾ 0 of Σ^{∨}-factors in f and g. We proceed by induction on n+m.

If n+m = 0, then we just apply DS Coherence. Suppose now n > 0. So there is a Δ^{∧}-factor in f and a Δ^{∧}-factor in g that correspond by the Δ^{∧}-cap bijections to the same cap of part(Gf), which is equal to part(Gg). By using the head increasing equations of §6, together with (Δ^{∧} nat), we obtain in PN

f = f′ ^{∘} Δ^{∧}_{p,A}, g = g′ ^{∘} Δ^{∧}_{p,A}

for f′ and g′ pure arrow terms of the same type A ∧ (¬p ∨ p) ⊢ B, and such that the number of Δ^{∧}-factors in f′ and g′ is n−1 in each, and the number of Σ^{∨}-factors in f′ and g′ is m in each, the same number we had for the Σ^{∨}-factors in f and g. So we have

G(f′ ^{∘} Δ^{∧}_{p,A}) = Gf = Gg = G(g′ ^{∘} Δ^{∧}_{p,A}).

We can show that Gf′ = Gg′. We obtain Gf′ out of G(f′ ^{∘} Δ^{∧}_{p,A}) in the following manner. We first remove from the partition part(G(f′ ^{∘} Δ^{∧}_{p,A})) a cap {k_{t}, l_{t}}, where the k+1-th occurrence of letter in B is an occurrence of p in a subformula ¬p of B, and the l+1-th occurrence of letter in B is an occurrence of p that is not in a subformula ¬p of B (here we have either k < l or l < k). After this removal, we add two new transversals:

{GA_{s}, k_{t}}, {(GA+1)_{s}, l_{t}},

and this yields part(Gf′). Since Gg′ is obtained from G(g′ ^{∘} Δ^{∧}_{p,A}), which is equal to G(f′ ^{∘} Δ^{∧}_{p,A}) in exactly the same manner, we obtain that Gf′ = Gg′.

Then, by the induction hypothesis, we have that f′ = g′ in PN, which implies that f = g in PN. We proceed analogously in the induction step when m > 0, via Σ^{∨}-factors. ⊣

From PN Coherence and the equivalence between the categories PN^{¬} and PN, proved in the preceding section, we may conclude in the following manner that the functor G from PN^{¬} to Br is faithful.

Proof of PN^{¬} Coherence. Suppose that for f and g arrows of PN^{¬} of the same type we have Gf = Gg. Then, as we noted at the beginning of this section, we have GF f = GF g, and hence F f = F g in PN by PN Coherence. It follows that f = g in PN^{¬} by the equivalence of the categories PN^{¬} and PN. ⊣

So we have proved PN^{¬} Coherence, announced at the end of §4.

9. The category MDS

In this and in the next section we add mix arrows of the type A ∧ B ⊢ A ∨ B to proof-net categories, together with appropriate conditions that will enable us to prove coherence with respect to Br for the resulting categories, which we call mix-proof-net categories. The mix arrows, which underly the mix principle of linear logic, were treated extensively in [11, Chapters 8, 10, 11, 13]. The proof of coherence for mix-proof-net categories is an adaptation of the proof of coherence for proof-net categories given in the preceding sections.

The category MDS is defined as the category DS in §2 save that we have the additional primitive arrow terms m_{A,B}: A ∧ B ⊢ A ∨ B for all objects, i.e. for all formulae, A and B of L_{∧,∨}, and we assume the following additional equations:

(m nat) (f ∨ g)^{∘} m_{A,B} = m_{D,E} ^{∘} (f ∧ g), for f: A ⊢ D and g: B ⊢ E,

(b^{∧} m) m_{A∧B,C} ^{∘} b^{∧}\overrightarrow{A,B,C} = d_{A,B,C} ^{∘} (1_{A} ∧ m_{B,C}),

(b^{∨} m)  b^{∨}\overrightarrow{C,B,A} ^{∘} m_{C,B∨A} = (m_{C,B} ∨ 1_{A})^{∘} d_{C,B,A},

(cm) m_{B,A} ^{∘} c^{∧}_{A,B} = c^{∨}_{B,A} ^{∘} m_{A,B}.

The proof-theoretical principle underlying m_{A,B} is called mix (see [11, Section 8.1] and references therein).

To obtain the functor G from MDS to Br, we extend the definition of the functor G from DS to Br (see §4) by adding the clause that says that Gm_{A,B} is the identity arrow 1_{GA+GB} of Br. We have the following result of [11, Section 8.4].

MDS Coherence. The functor G from MDS to Br is faithful.

In the remainder of this section we will prove some lemmata concerning MDS, which we will use for the proof of coherence in the next section. For that we need some preliminaries.

For x a particular proper subformula of a formula A of L_{∧,∨}, and ξ ∈ {∧, ∨}, we define A^{−x} inductively as follows:

(B ξ x)^{−x} = (x ξ B)^{−x} = B,

for x a proper subformula of C,

(B ξ C)^{−x}= B ξ C^{−x},
(C ξ B)^{−x}= C^{−x} ξ B.

For i ∈ {1, 2}, let A_{i} be a formula of L_{∧,∨} with a proper subformula x_{i}, which is an occurrence of a letter q, and let x_{i} be the n_{i}-th occurrence of letter counting from the left. We define the following functions μ_{i}: N − {n_{i}−1} → N:

μ_{i}(n) =_{df} \{ \begin{matrix}n & if n < n_{i}−1 \\ n−1 & if n > n_{i}−1. \end{matrix}

The definition of linked occurrence of a letter in an arrow of MDS is analogous to what we had in §5. Then we can prove the following.

Lemma 1. For every arrow term f: A_{1} ⊢ A_{2} of MDS such that x_{1} and x_{2} are linked in the arrow f, there is an arrow term f^{−q}: A_{1}^{−x_{1}} ⊢ A_{2}^{−x_{2}} of MDS such that the members of part(Gf^{−q}) are {s(μ_{1}(m_{1})), t(μ_{2}(m_{2}))} for each {s(m_{1}), t(m_{2})} in part(Gf), provided m_{i} ≠ n_{i}−1.

Proof. We proceed by induction on the complexity of the arrow term f. If f is a primitive arrow term α_{B_{1},...,B_{m}}, then for some j ∈ {1, …, m} we have that x_{i} occurs in a subformula B_{j} of A_{i}. If x_{i} is a proper subformula of this subformula B_{j}, then B_{j}^{−x_{i}} is defined, and f^{−q} is

α_{B_{1},...,B_{j−1},B_{j}^{−x_{i}} ,B_{j+1},...,B_{m}}

(note that B_{j}^{−x_{1}} and B_{j}^{−x_{2}} are the same formula). If x_{i} is not a proper subformula of the subformula B_{j}, then f^{−q} is 1_{A_{i}^{−x_{i}}}.

If f is g^{∘} h, then f^{−q} is g^{−q} ^{∘} h^{−q}, and if f is g ξ h for ξ ∈ {∧, ∨}, then f^{−q} is either g^{−q} ξ h, or g ξ h^{−q}, or g when h is 1_{x_{1}}, or h when g is 1_{x_{1}}. ⊣

Here is an example of the application of Lemma 1. If f: A_{1} ⊢ A_{2} is

((m_{q,p∧q} ^{∘} (1_{q} ∧ c^{∧}_{q,p})^{∘} c^{∧}_{q∧p,q}) ∨ 1_{p})^{∘} d_{q∧p,q,p} ^{∘} b^{∧}\overrightarrow{q,p,q∨p} ^{∘} c^{∧}_{p∧(q∨p),q}:

(p ∧ (q ∨ p)) ∧ q ⊢ (q ∨ (p ∧ q)) ∨ p,

where x_{1} is the second (rightmost) occurrence of q in (p ∧ (q ∨ p)) ∧ q, while x_{2} is the second occurrence of q in (q ∨ (p ∧ q)) ∨ p, then f^{−q}: A_{1}^{−q} ⊢ A_{2}^{−q} is

((m_{q,p} ^{∘} (1_{q} ∧ 1_{p})^{∘} c^{∧}_{p,q}) ∨ 1_{p})^{∘} d_{p,q,p} ^{∘} 1_{p∧(q∨p)} ^{∘} 1_{p∧(q∨p)} : p ∧ (q ∨ p) ⊢ (q ∨ p) ∨ p,

which is equal to ((m_{q,p} ^{∘} c^{∧}_{p,q}) ∨ 1_{p})^{∘} d_{p,q,p}.

We define inductively a notion we call a context:

□ is a context;

if Z is a context and A a formula of L_{∧,∨}, then Z ξ A and A ξ Z are contexts for ξ ∈ {∧, ∨}.

Next we define inductively what it means for a context Z to be applied to an object B of MDS, which we write Z(B), or to an arrow term f of MDS, which we write Z(f):

□(B) = B, □(f) = f,

(Z ξ A)(B) = Z(B) ξ A, (Z ξ A)(f) = Z(f) ξ 1_{A},
(A ξ Z)(B) = A ξ Z(B); (A ξ Z)(f) = 1_{A} ξ Z(f).

We use X, Y, Z, … for contexts.

For f: A ⊢ C an arrow of MDS, we say that an occurrence x of a formula B as a subformula of A and an occurrence y of the same formula B as a subformula of C are linked in f when the n-th letter in x is linked in f to the n-th letter in y.

Let f: X(p) ∧ B ⊢ Y (p ∧ B) be an arrow term of MDS such that the displayed occurrences of p in the source and target, and also the displayed occurrences of B, are linked in the arrow f. Then, by successive applications of Lemma 1, for each occurrence of a letter in B, we obtain the arrow term f^{−B}: X(p) ⊢ Y (p) of MDS, and the displayed occurrences of p in X(p) and Y (p) are linked in the arrow f^{−B}.

Let f^{†}: X(p ∧ B) ⊢ Y (p ∧ B) be the arrow term of MDS obtained from f^{−B} by replacing the occurrences of p that correspond to those displayed in X(p) and Y (p) by occurrences of p ∧ B. This replacement is made in the indices of primitive arrow terms that occur in f^{−B}, and it need not involve all the occurrences of p in these indices. For example, if X is □ ∧ (q ∨ p) and Y is (q ∨ □) ∨ p, while f^{−B} is

((m_{q,p} ^{∘} c^{∧}_{p,q}) ∨ 1_{p})^{∘} d_{p,q,p}: p ∧ (q ∨ p) ⊢ (q ∨ p) ∨ p,

then f^{†} is

((m_{q,p∧B} ^{∘} c^{∧}_{p∧B,q}) ∨ 1_{p})^{∘} d_{p∧B,q,p}: (p ∧ B) ∧ (q ∨ p) ⊢ (q ∨ (p ∧ B)) ∨ p.

Then we can prove the following.

Lemma 2∧. Let f: X(p) ∧ B ⊢ Y (p ∧ B) and f^{†}: X(p ∧ B) ⊢ Y (p ∧ B) be as above. Then there is an arrow term h_{X}: X(p) ∧ B ⊢ X(p ∧ B) of DS such that f = f^{†} ^{∘} h_{X} in MDS.

Proof. We construct the arrow term h_{X} of DS by induction on the complexity of the context X. For the basis we have that h_{□} is 1_{p∧B}. In the induction step we have

h_{Z∧A} = (h_{Z} ∧ 1_{A})^{∘} c^{∧}_{A,Z(p)∧B} ^{∘} b^{∧}\overleftarrow{A,Z(p),B} ^{∘} (c^{∧}_{Z(p),A} ∧ 1_{B}),

h_{Z∨A} = (h_{Z} ∨ 1_{A})^{∘} c^{∨}_{Z(p)∧B,A} ^{∘} d_{A,Z(p),B}^{R} ^{∘} (c^{∨}_{A,Z(p)} ∧ 1_{B}),

h_{A∧Z} = (1_{A} ∧ h_{Z})^{∘} b^{∧}\overleftarrow{A,Z(p),B},

h_{A∨Z} = (1_{A} ∨ h_{Z})^{∘} d_{A,Z(p),B}^{R}.

It is easy to see that Gf = G(f^{†} ^{∘} h_{X}), and then the lemma follows by applying MDS Coherence. ⊣

Let f: Y (B ∨ p) ⊢ B ∨ X(p) be an arrow term of MDS such that the displayed occurrences of p in the source and target, and also the displayed occurrences of B, are linked in the arrow f. Then, as above by Lemma 1, we obtain the arrow term f^{−B}: Y (p) ⊢ X(p) of MDS, and the displayed occurrences of p in Y (p) and X(p) are linked in the arrow f^{−B}.

Let f^{†}: Y (B ∨ p) ⊢ X(B ∨ p) be the arrow term of MDS obtained from f^{−B} by replacing the occurrences of p that correspond to those displayed in Y (p) and X(p) by occurrences of B ∨ p (cf. the example above). Then we can prove the following, analogously to Lemma 2∧.

Lemma 2∨. Let f: Y (B ∨ p) ⊢ B ∨ X(p) and f^{†}: Y (B ∨ p) ⊢ X(B ∨ p) be as above. Then there is an arrow term h_{X}: X(B ∨ p) ⊢ B ∨ X(p) of DS such that f = h_{X} ^{∘} f^{†} in MDS.

10. MPN^{¬} Coherence

The category MPN^{¬} is defined as the category PN^{¬} in §3 save that we have the additional primitive arrow terms m_{A,B}: A ∧ B ⊢ A ∨ B for all objects A and B of PN^{¬}, and we assume as additional equations (m nat), (b^{∧} m), (b^{∨} m) and (cm) of the preceding section. To obtain the functor G from MPN^{¬} to Br, we extend the definition of the functor G from PN^{¬} to Br by adding the clause that says that Gm_{A,B} is the identity arrow 1_{GA+GB} of Br.

A mix-proof-net category is defined as a proof-net category (see §3) that has in addition a natural transformation m satisfying the equations (b^{∧} m), (b^{∨} m) and (cm). The category MPN^{¬} is up to isomorphism the free mix-proof-net category generated by P.

The category MPN is defined as the category PN in §6 save that we have the additional primitive arrow terms m_{A,B} for all objects of PN, and we assume as additional equations (m nat), (b^{∧} m), (b^{∨} m) and (cm). We can prove that MPN^{¬} and MPN are equivalent categories as in §7. (We have an additional case involving m_{A,B} in the proof of the analogue of the Auxiliary Lemma of §7, and similar trivial additions elsewhere; otherwise the proof is quite analogous.)

We have a functor G from MPN to Br defined by restricting the definition of the functor G from MPN^{¬} to Br (cf. the beginning of §8), and we will prove the following.

MPN Coherence. The functor G from MPN to Br is faithful.

The proof of this coherence proceeds as the proof of PN Coherence in §8. The only difference is in the Ξ^{∧}-Permutation and Ξ^{∨}-Permutation Lemmata of §6.

The formulation of the Ξ^{∧}-Permutation Lemma is modified by replacing PN and DS^{¬p} by respectively MPN and MDS^{¬p}, where the category MDS^{¬p} is defined as MDS save that it is generated not by P, but by P ∪ P^{¬} (cf. §6); moreover, we assume that y_{1} and ¬y_{2} occur in E within a subformula of the form p ∧ (¬y_{2} ∨ y_{1}) or ¬p ∧ (y_{1} ∨ ¬y_{2}). We modify the proof of this lemma as follows.

If in E we have p ∧ (¬y_{2} ∨ y_{1}), then by the stem-increasing equations of §6 we have that the Ξ^{∧}_{p,B}-term g: C ⊢ D is equal to f′′ ^{∘} Δ^{∧}_{p,C} for f′′: C ∧ (¬p ∨ p) ⊢ D an arrow term of DS^{¬p}, and so for f: D ⊢ E an arrow term of MDS^{¬p} satisfying the conditions of the lemma we have in MPN

f ^{∘} g = f ^{∘} f′′ ^{∘} Δ^{∧}_{p,C} .

Then we apply Lemma 2∧ of the preceding section to

f ^{∘} f′′: C ∧ (¬p ∨ p) ⊢ E,

where C is X(p), ¬p ∨ p is B and E is Y (p ∧ (¬p ∨ p)). So for

h_{X}: X(p) ∧ (¬p ∨ p) ⊢ X(p ∧ (¬p ∨ p))

an arrow term of DS^{¬p}, and

(f ^{∘} f′′)^{†}: X(p ∧ (¬p ∨ p)) ⊢ Y (p ∧ (¬p ∨ p))

we have

f ^{∘} f′′ = (f ^{∘} f′′)^{†} ^{∘} h_{X}.

By the Ξ^{∧}-Permutation Lemma of §6 we have

h_{X} ^{∘} Δ^{∧}_{p,C} = g′ ^{∘} f′

where g′ is the Δ^{∧}_{p,p}-term X(Δ^{∧}_{p,p}), and by bifunctorial and naturality equations we have

(f ^{∘} f′′)^{†} ^{∘} X(Δ^{∧}_{p,p}) = Y (Δ^{∧}_{p,p})^{∘} (f ^{∘} f′′)^{−(¬p∨p)}.

Note that (f ^{∘} f′′)^{†} is obtained from (f ^{∘} f′′)^{−(¬p∨p)} : X(p) ⊢ Y (p) by replacement of p.

So we have in MPN

f ^{∘} g = f ^{∘} f′′ ^{∘} Δ^{∧}_{p,C}

= (f ^{∘} f′′)^{†} ^{∘} h_{X} ^{∘} Δ^{∧}_{p,C}

= (f ^{∘} f′′)^{†} ^{∘} X(Δ^{∧}_{p,p})^{∘} f′

= Y (Δ^{∧}_{p,p})^{∘} f′′′

for f′′′, which is (f ^{∘} f′′)^{−(¬p∨p)} ^{∘} f′, an arrow term of MDS^{¬p}.

We proceed analogously if in E we have ¬p ∧ (y_{1} ∨ ¬y_{2}); instead of Δ^{∧}_{p,p} we then have Δ^{∧}′_{p,p}. We have an analogous reformulation of the Ξ^{∨}-Permutation Lemma of §6, with a proof based on Lemma 2∨ of the preceding section.

Instead of Lemma 2∧ of the preceding section, we could have proved, with more difficulty, an analogous lemma where f is of type

Z(X_{1}(p) ∧ X_{2}(B)) ⊢ Y (p ∧ B),

and f^{†} is of one of the following types:

\begin{matrix}Z(X_{1}(p ∧ B) ∧ (X_{2}(B))^{−B}) ⊢ Y (p ∧ B), \\ Z(X_{1}(p ∧ B)) ⊢ Y (p ∧ B). \end{matrix}

Then in the proof of the Ξ^{∧}-Permutation Lemma modified for MPN we would not need to pass from g to f′′ ^{∘} Δ^{∧}_{p,C} via stem-increasing equations, but this alternative approach is altogether less clear.

Note that we have no analogue of Lemma 2 of §5 for MDS. The lack of this lemma, on which we relied in §6 for the proof of the Ξ^{∧}-Permutation and Ξ^{∨}- Permutation Lemmata, is tied to the modifications we made for these lemmata with MPN. We have also no analogue of Lemma 4 of §5, but the analogue of Lemma 3 of §5 does hold.

From MPN Coherence and the equivalence of the categories MPN^{¬} and MPN we can then infer the following.

MPN^{¬} Coherence. The functor G from MPN^{¬} to Br is faithful.

References

[1] M. Barr, ∗-Autonomous Categories, Lecture Notes in Mathematics 752, Springer-Verlag, Berlin, 1979

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

[3] R. Brauer, On algebras which are connected with the semisimple continuous groups, Annals of Mathematics 38 (1937), 857–872

[4] G. Burde and H. Zieschang, Knots, de Gruyter, Berlin, 1985

[5] J. R. B. Cockett and R. A. G. Seely, Weakly distributive categories, in: M. P. Fourman et al., (editors) Applications of Categories in Computer Science, Cambridge University Press, Cambridge, 1992, pp. 45-65

[6] , Weakly distributive categories, J. Pure Appl. Algebra 114 (1997), 133–173 (updated version available at: http://www.math.mcgill.ca/rags)

[7] V. Danos and L. Regnier, The structure of multiplicatives, Archive for Mathematical Logic 28 (1989), 181–203

[8] K. Došen, Cut Elimination in Categories, Kluwer, Dordrecht, 1999

[9] K. Došen and Z. Petrić, Generality of proofs and its Brauerian representation, J. Symbolic Logic 68 (2003), 740–750 (available at: http://arXiv.org/math.LO/0211090)

[10] , A Brauerian representation of split preorders, Math. Logic Quart. 49 (2003), 579–586 (misprints corrected in text available at: http://arXiv.org/math.LO/0211277)

[11] , Proof-Theoretical Coherence, KCL Publications, London, 2004

[12] , Proof-Net Categories, preprint, 2005

[13] S. Eilenberg and G. M. Kelly, A generalization of the functorial calculus, J. Algebra 3 (1966), 366–375

[14] J.-Y. Girard, Linear logic, Theoret. Comput. Sci. 50 (1987), 1–101

[15] R. Houston, D. Hughes and A. Schalk, Modelling linear logic without units (Preliminary results), preprint, 2005 (available at: http://arXiv.org/math.CT/0504037)

[16] C. Kassel, Quantum Groups, Springer-Verlag, Berlin, 1995

[17] G. M. Kelly and S. Mac Lane, Coherence in closed categories, J. Pure Appl. Algebra 1 (1971), 97–140, 219

[18] F. Lamarche and L. Straßburger, Constructing free Boolean categories, preprint, 2005

[19] S. Mac Lane, Categories for the Working Mathematician, Springer-Verlag, Berlin, 1971 (expanded second edition, 1998)

Matematički institut SANU (Received 16 03 2005) Kneza Mihaila 35 (Revised 05 09 2005) 11000 Beograd, p.p. 367 Serbia and Montenegro

{kosta, zpetric}@mi.sanu.ac.yu