PUBLICATIONS DE L’INSTITUT MATHÉMATIQUE Nouvelle série, tome 82(96) (2007), 17–23 DOI 102298/PIM0796017D

RELEVANT CATEGORIES AND PARTIAL FUNCTIONS

Kosta Došen and Zoran Petrić

To the memory of Aleksandar Kron

Abstract. A relevant category is a symmetric monoidal closed category with a diagonal natural transformation that satisfies some coherence conditions. Every cartesian closed category is a relevant category in this sense. The denomination relevant comes from the connection with relevant logic. It is shown that the category of sets with partial functions, which is isomorphic to the category of pointed sets, is a category that is relevant, but not cartesian closed.

1. Introduction

It is well known that the category of pointed sets with point-preserving functions as arrows is a symmetric monoidal closed category (see [5, Section IV.1]). The symmetric monoidal closed structure in this category is provided by the smash product and internal hom-sets (see Section 3 below). This category, which is isomorphic to the category of sets with partial functions, has however a richer structure than just symmetric monoidal closed.

If to the assumptions for symmetric monoidal categories we add a diagonal natural transformation with appropriate equations between arrows, then one obtains a notion of monoidal category for which a coherence theorem is proved in [10] with respect to relations on finite ordinals. We will call these categories relevant monoidal categories, because the types of arrows in the relevant monoidal category freely generated by a set of propositional letters corresponds to sequents in the multiplicative (i.e. intensional) conjunction (i.e. fusion) fragment of relevant logic, including the multiplicative constant true proposition ⊤. This fragment, which is the same both in intuitionistic and in classical versions of relevant logic, catches essentially the structural rules of relevant logic, on which the whole structure of this logic rests. The equations for relevant monoidal categories stem from [2]. (An incomplete set of these equations may be found in [7, Definition 2.1(i)].)

2000 Mathematics Subject Classification: 03B47, 03F52, 03G30, 18D10, 18D15.

Key words and phrases: symmetric monoidal closed categories, diagonal natural transformation, intuitionistic relevant logic, partial functions, pointed sets.

Symmetric monoidal closed categories that are also relevant monoidal with respect to the same monoidal structure will be called relevant monoidal closed categories. The relevant monoidal closed category RMC freely generated by a set of propositional letters corresponds to the multiplicative conjunction-⊤-implication fragment (both intuitionistic and classical) of relevant logic. We have that A is the source and B the target of an arrow of RMC iff A → B is a theorem of the multiplicative conjunction-⊤-implication fragment of the relevant logic R (see [1], where multiplicative conjunction, i.e. fusion, is called co-tenability).

The category of pointed sets has a diagonal natural transformation with respect to the smash product, which makes of it a relevant monoidal closed category. Moreover, it has also finite products and coproducts (including the empty ones), where product is different from the smash product. With this additional structure, we obtain also operations corresponding to the additive (lattice) connectives of relevant logic, without distribution of additive conjunction over additive disjunction. The relevant logic R has this distribution, but a version of R without it also exists. (Linear logic lacks this distribution.) We are still within a fragment of relevant logic common to its intuitionistic and classical versions. This fragment catches presumably the whole positive fragment of intuitionistic relevant logic.

The connection between relevant logic and the category of pointed sets is reminiscent of the connection that exists between intuitionistic logic and the category Set of sets with functions. As intuitionistic propositional logic may be identified with the bicartesian closed category (see [8, Section I.8]) freely generated by a set of propositional letters, so the positive fragment of intuitionistic relevant logic may be identified with a free relevant category such as we will introduce. And as Set is the prime example of a bicartesian closed category, so the category of pointed sets may be the prime example of a relevant category.

Inspired by some ideas of Belnap, which are derived from Scott’s models for the untyped lambda calculus, Helman found in [6] that typed lambda terms in betanormal form that code proofs in the additive conjunction-implication fragment of the relevant logic R can be interpreted in the hierarchy of pointed sets with product and sets of point-preserving functions. A connection between relevant logic and the category of pointed sets was also investigated by Szabo in [12], but with an approach different from ours—in particular as far as distribution of product over coproduct is concerned. It was prefigured by Jacobs in [7, Example 2.3(i)] that the category of pointed sets is a relevant monoidal category, though the notion of relevant monoidal category of that paper differs from ours.

2. Relevant categories

The objects of the category SyMon are the formulae of the propositional language L_{⊤,∧}, generated from a set P of propositional letters with the nullary connective, i.e. propositional constant, ⊤ and the binary connective ∧. We use p, q, r, …, sometimes with indices, for propositional 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 SyMon, we define first inductively a set of expressions called the arrow terms. Every arrow term of SyMon 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^{∧}\overleftarrow{A,B,C} : (A ∧ B) ∧ C ⊢ A ∧ (B ∧ C),

c^{∧}_{A,B} : A ∧ B ⊢ B ∧ A,

δ^{∧}\overrightarrow{A}: A ∧ ⊤ ⊢ A, δ^{∧}\overleftarrow{A}: A ⊢ A ∧ ⊤

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

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

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

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

(∧ 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),

(δ^{∧}^{→} nat) f ^{∘} δ^{∧}\overrightarrow{A} = δ^{∧}\overrightarrow{B}^{∘} (f ∧ 1_{⊤}),

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

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

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

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

(δ^{∧} δ^{∧}) δ^{∧}\overrightarrow{A} ^{∘} δ^{∧}\overleftarrow{A} = 1_{A},  δ^{∧}\overleftarrow{A} ^{∘} δ^{∧}\overrightarrow{A} = 1_{A∧⊤},

(b^{∧} δ^{∧}) b^{∧}\overrightarrow{A,B,⊤} = δ^{∧}\overleftarrow{A∧B} ^{∘} (1_{A} ∧ δ^{∧}\overrightarrow{B}).

The set of equations of SyMon 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 ξ ∈ {^{∘} , ∧}; if ξ is ^{∘}, then f ^{∘} g is defined (namely, f and g have appropriate, composable, types), and analogously for f_{1} ^{∘} g_{1}. This concludes the definition of the equations of SyMon.

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

The equations (∧ 1) and (∧ 2) say that ∧ is a biendofunctor (a 2-endofunctor, in the terminology of [4, Section 2.4]). Equations with “nat” in their names, like

those in the list above, say that b^{∧}^{→}, c^{∧}, etc. are natural transformations.

The category SyMon is the free symmetric monoidal category in the sense of [9, Chapter VII] generated by the set P.

The category ReMon is defined as the category SyMon with the following additions. We have the additional primitive arrow terms w^{∧}_{A}: A ⊢ A ∧ A, and the following additional equations:

(w^{∧} nat) (f ∧ f)^{∘} w^{∧}_{A} = w^{∧}_{D} ^{∘} f,

(b^{∧}w^{∧})  b^{∧}\overrightarrow{A,A,A} ^{∘} (1_{A} ∧ w^{∧}_{A})^{∘} w^{∧}_{A} = (w^{∧}_{A} ∧ 1_{A})^{∘} w^{∧}_{A},
(c^{∧}w^{∧})  c^{∧}_{A,A} ^{∘} w^{∧}_{A} = w^{∧}_{A},

for c^{∧}_{A,B,C,D}^{m} =_{df} b^{∧}\overrightarrow{A,C,B∧D} ^{∘} (1_{A} ∧ (b^{∧}\overleftarrow{C,B,D} ^{∘} (c^{∧}_{B,C} ∧1_{D})^{∘} b^{∧}\overrightarrow{B,C,D}))^{∘} b^{∧}\overleftarrow{A,B,C∧D} :

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

(b^{∧} c^{∧}w^{∧})  w^{∧}_{A∧B} = c^{∧}_{A,A,B,B}^{m} ^{∘} (w^{∧}_{A} ∧ w^{∧}_{B}),
(w^{∧} δ^{∧})  w^{∧}_{⊤} = δ^{∧}\overleftarrow{⊤}.

(These equations may be found in [2]; they are also in [7, Definition 2.1(i)], but

with (b^{∧} c^{∧}w^{∧}) lacking.)

A relevant monoidal category is a symmetric monoidal category that has in addition a natural transformation w^{∧} that satisfies the equations of ReMon. The category ReMon is the free relevant monoidal category generated by the set P. A coherence theorem is proved for this category in [10] with respect to the category whose arrows are relations between finite ordinals. This means that there is a faithful functor from ReMon into the latter category.

The category SMC is defined as the category SyMon with the following additions. We have an additional binary connective →, and the additional primitive arrow terms

ε_{A,B}: A ∧ (A → B) ⊢ B, η_{A,B}: B ⊢ A → (A ∧ B);

on arrow terms we have the additional unary operations A →, for every object A, such that for f: B ⊢ C we have the arrow term A → f: A → B ⊢ A → C.

The equations of SMC are obtained by assuming the following additional equations:

(A → 1) A → 1_{B} = 1_{A→B},
(A → 2) A → (f ^{∘} g) = (A → f)^{∘} (A → g),
(ε nat) f ^{∘} ε_{A,B} = ε_{A,C} ^{∘} (1_{A} ∧ (A → f)),
(η nat) (A → (1_{A} ∧ f))^{∘} η_{A,B} = η_{A,C} ^{∘} f,
(εη ∧) ε_{A,A∧B} ^{∘} (1_{A} ∧ η_{A,B}) = 1_{A∧B},
(εη →) (A → ε_{A,B})^{∘} η_{A,A→B} = 1_{A→B},

and the following additional rule:

\frac{f = g}{A → f = A → g}

The equations (A → 1) and (A → 2) say that A → is a functor, while (εη ∧) and (εη →) are the triangular equations of an adjunction (see [9, Section IV.1]). The category SMC is the free symmetric monoidal closed category generated by the set P (see [9, Section VII.7]).

The category RMC is defined by combining the definitions of ReMon and SMC. Relevant monoidal closed categories are symmetric monoidal closed categories that are also relevant monoidal with respect to the same monoidal structure. The category RMC is the free relevant monoidal closed category generated by the set P.

A positive intuitionistic relevant category is a relevant monoidal closed category that has all finite products and coproducts (including the empty ones).

3. The category of pointed sets

3.1. The category of pointed sets Set_{∗} is the category whose objects are sets with a distinguished element ∗, and whose arrows are functions f such that f(∗) = ∗. This category is isomorphic to the category of sets with partial functions, i.e. relations that are single-valued, but not necessarily defined on the whole domain.

We have the following special objects and operations on objects in Set_{∗}:

I = {∗},  a′ = {(x, ∗) | x ∈ a − I},  b′′ = {(∗, y) | y ∈ b − I},
a ⊗ b = ((a − I) × (b − I)) ∪ I,
a ⊠ b = (a ⊗ b) ∪ a′ ∪ b′′,
a ⊞ b = a′ ∪ b′′ ∪ I.

Let ⊤ in Set_{∗} be I ∪ {x}, where x ≠ ∗, and let ∧ be ⊗, which is the smash product. For a and b objects of Set_{∗}, let a → b be the union of I with the set of arrows of Set_{∗} from a to b without the arrow with constant value ∗. It is well known that with these operations on objects Set_{∗} is a symmetric monoidal closed category (see [5, Section IV.1]; see [3, Section 6], for more details). The importance of Set_{∗} for checking equations between arrows in SMC is demonstrated by Soloviev in [11].

It can also be easily shown that with w^{∧}_{a}(x) being (x, x) for x ≠ ∗, and ∗ otherwise, Set_{∗} is a relevant monoidal closed category. It was prefigured in [7, Example 2.3(i)] that Set_{∗} is a relevant monoidal category, though the notion of relevant monoidal category of that paper differs from ours, as explained in the preceding section.

We also have arrows of the type of projections for the smash product, which are defined in an obvious way, but these arrows do not make natural transformations. The category Set_{∗} is not a cartesian category with the smash product. But Set_{∗} is a bicartesian category (i.e. a category with all finite products and coproducts) with binary product being ⊠ (which corresponds to cartesian product) and binary coproduct being ⊞, while I is both the terminal and the initial object, i.e. the empty product and coproduct. It is shown in [4, Sections 9.7, 12.4 and 13.4] that Set_{∗} is a bicartesian category of a particular kind, called there zero-dicartesian.

So Set_{∗} is a positive intuitionistic relevant category in the sense of the preceding section.

3.2. In [3] one can find a characterization of the objects isomorphic in SMC, and hence also in every symmetric monoidal closed category. Two objects A and B of SMC are isomorphic iff one can derive A = B in the equational calculus S whose axioms are the axioms of commutative monoids with respect to ∧ and ⊤ and the following two equations:

⊤ → C = C,
(A ∧ B) → C = B → (A → C).

The proof of this equivalence in [3] is based on a proof of an analogous equivalence where SMC is replaced by FinSet_{∗}, which is the category of finite pointed sets with point-preserving functions (a full subcategory of Set_{∗}), and A and B are diversified, which means that no propositional letter occurs more than once in these formulae. The equational calculus S axiomatizes all the equations between diversified formulae that hold in natural numbers, where formulae are understood as arithmetical terms such that propositional letters are variables ranging over natural numbers, ⊤ is 1, the operation ∧ is multiplication, and m → n is (n+1)^{m}−1.

We conjecture that these two assertions concerning S, its arithmetical interpretation and FinSet_{∗} are also true when the restriction to diversified formulae is lifted. If this conjecture were true, then the calculus S would characterize not only all the formulae isomorphic in SMC, but also in RMC.

References

[1] A. R. Anderson and N. D. Belnap, Entailment: The Logic of Relevance and Necessity, Vol. I, Princeton University Press, Princeton, 1975

[2] K. Došen and Z. Petrić, Modal functional completeness, in: H. Wansing (ed.), Proof Theory of Modal Logic, Kluwer, Dordrecht, 1996, pp. 167–211 [3] Isomorphic objects in symmetric monoidal closed categories, Mathematical Structures

in Computer Science 7 (1997), 639–662

[4] , Proof-Theoretical Coherence, KCL Publications, London, 2004 (revised version avail-

able at: http://www.mi.sanu.ac.yu/~kosta/coh.pdf)

[5] S. Eilenberg and G. M. Kelly, Closed categories, in: S. Eilenberg et al. (eds), Proceedings of the Conference on Categorical Algebra, La Jolla 1965, Springer-Verlag, Berlin, 1966, 421–562

[6] G. Helman, Completeness of the normal typed fragment of the λ-system U^{∗}, J. Philos. Logic 6 (1977), 33–46

[7] B. Jacobs, Semantics of weakening and contraction, Annals of Pure and Applied Logic 69 (1994), 73–106

[8] J. Lambek and P. J. Scott, Introduction to Higher Order Categorical Logic, Cambridge University Press, Cambridge, 1986

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

[10] Z. Petrić, Coherence in substructural categories, Studia Logica 70 (2002), 271–296 (available

at: http://arXiv.org/math.CT/0006061)

[11] S. V. Soloviev, Proof of a conjecture of S. Mac Lane, Annals of Pure and Applied Logic 90 (1997), 101–162

[12] M. E. Szabo, The continuous realizability of entailment, Zeitschrift für mathematische Logik und Grundlagen der Mathematik 29 (1983), 219–233

Mathematički institut, SANU Knez Mihailova 36 11001 Beograd, p.p. 367 Serbia

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