The Principle of Categorical Harmony

In this section, we first see how logical constants can be regarded as adjoint functors, and finally lead to the principle of categorical harmony. Although I do not explain the concept of categories from the scratch, from a logical point of view, you may

conceive of a category as a sort of proof-theoretic consequence relation: suppose we have the following concepts given.

• The concept of formulae ϕ.

• The concept of hypothetical proofs (or deductions) from formulae ϕ to ψ . For any

formula ϕ there must be an identity proof idϕ from ϕ to ϕ.

• The concept of proof-decorated relation p :

ϕ p ψ (2)

where p is a proof from ϕ to ψ .

• The concept of sequential composition ◦ of proofs: composing ϕ p ψ and ψ q

ξ , we obtain

ϕ q◦ p ξ. (3)

If we think of a monodical category for substructural logic, we additionally have parallel composition ⊗:

ϕ ⊗ ϕ! p⊗ p! ψ ⊗ ψ ! (4)

where ϕ p ψ and ϕ! p! ψ !.

• The concept of reduction of proofs such that the identity proofs may be canceled

out (i.e., idϕ ◦ p equals p modulo reducibility; q ◦idϕ equals q modulo reducibility), and proofs may locally be reduced in any order (i.e., ( p ◦ q) ◦ r equals p ◦ (q ◦ r )

modulo reducibility). Moreover, reduction must respect composition (i.e., if p equals q and r equals s modulo reducibility, p ◦ q must equal r ◦ s modulo reducibility).

The concept of a proof-theoretic consequence relation (resp. with parallel composition) thus defined is basically the same as the concept of a category (resp. monoidal category): a formula corresponds to an object in a category, and a proof to a morphism in it. To be precise, a proof-theoretic consequence relation is a way of presenting a category rather than category per se. In most parts of the article, however, full-fledged category theory shall not be used, for simplicity and readability, and it suffices for the reader to know some basic logic and order theory, apart from occasional exceptions.

From the perspective of Schroeder-Heister [23], categorical logic (or categorial logic to avoid confusion) places primary emphasis on hypothetical judgements, which are concerned with the question “what follows from what?”, rather than categorical judgements in the philosopher's sense, which are concerned with the question “what holds on their own?”. In the traditional accounts of both model-theoretic and prooftheoretic semantics, the categorical is prior to the hypothetical, and the hypothetical is reduced to the categorical via the so-called transmission view of logical consequence. These are called dogmas of standard semantics, whether model-theoretic or prooftheoretic, in Schroeder-Heister [23]. His theory takes the hypothetical to precede the categorical, and it is in good harmony with the idea of categorical logic, in which the hypothetical, i.e., the concept of morphisms, is conceptually prior to the

categorical, i.e., the concept of morphisms with their domains being a terminal object (or monoidal unit in the case of substructural logic).

Some authors have discussed how logical constants can be derived from logical consequence relations (see, e.g., Westerståhl [25]). To that end, category theory allows us to derive logical constants from abstract proof-theoretic consequence relations (i.e., categories) through the concept of adjunctions, which even give us inferential rules for the derived logical constants, and hence a proof system as a whole (in the case of intuitionistic logic, for example, the proof system thus obtained is indeed equivalent to standard ones, such as NJ and LJ). Given a category (abstract prooftheoretic consequence relation), we can always mine logical constants (if any) in the category via the generic criteria of adjunctions. In such a way, category-theoretical logic elucidates a generic link between logical constants and logical consequence, without focusing on a particular system of logic.

In the following, let us review the concept of adjoint functors in the simple case of preorders, which is basically enough for us, apart from occasional exceptions. A preorder

(L , L ) (5)

consists of a set P with a reflexive and transitive relation L on L. Especially, the deductive relations of most logical systems form preorders; note that reflexivity and transitivity amount to identity and cut in logical terms. It is well known that a preorder can be seen as a category in which the number of morphisms between fixed two objects in it are at most one. Then, a functor F : L → L! between preorders L and L! is just a monotone map: i.e., ϕ L ψ implies F (ϕ) L! F (ψ ). Now, a functor

F : L → L! (6)

is called left adjoint to G : L! → L (7)

(or G is right adjoint to F ) if and only if

F (ϕ) L! ψ ⇔ ϕ L G(ψ ) (8) for any ϕ ∈ L and ψ ∈ L!. This situation of adjunction is denoted by F -G. Note

that a left or right adjoint of a given functor does not necessarily exist.

In this formulation, it would already be evident that an adjunction F -G is equivalent to a sort of bi-directional inferential rule:

F (ϕ ) L ! ψ

ϕ L G(ψ ) (9)

where the double line means that we can infer the above “sequent” from the one below, and vice versa.

Let us look at several examples to illustrate how logical constants are characterised by adjunctions, and to articulate the inferential nature of them. Suppose that L is intuitionistic logic. We define the diagonal functor Δ : L → L × L by

Δ(ϕ) = (ϕ, ϕ) (10)

where × denotes binary product on categories (in this case just preorders) or in the category of (small) categories. Then, the right adjoint of Δ is conjunction ∧ : L × L → L:

Δ ∧. (11)

The left adjoint of Δ is disjunction ∨ : L × L → L:

∨ Δ. (12)

The associated bi-directional rule for ∧ turns out to be the following:

Δ(ϕ1 ) L × L (ϕ2 ,ϕ3 )

ϕ1 L ϕ2 ∧ ϕ3 (13)

which, by the definition of product on categories, boils down to the following familiar rule:

ϕ1 L ϕ2 ϕ1 L ϕ3

ϕ1 L ϕ2 ∧ ϕ3 (14)

This is the inferential rule for conjunction ∧ that is packed in the adjunction Δ ∧. We omit the case of ∨. Now, implication ϕ → (-) : L → L for each ϕ is the right adjoint of ϕ ∧ (-), where the expressions “ϕ → (-)” and “ϕ ∧ (-)” mean that ϕ is fixed, and (-) is an argument:

ϕ ∧ (-) -ϕ → (-). (15)

The derived inferential rule is the following:

ϕ ∧ ξ ψ

ξ ϕ → ψ (16)

Note that we may replace ∧ by comma in the format of sequent calculus. Quantifiers can be treated in a similar (but more heavily categorical) way using indexed or fibrational structures (LC )C∈C (intuitively, each object C in a category C is a collection of variables or a so-called context) rather than single L as in the above discussion (see, e.g., Pitts [16] for the case of intuitionistic logic; for a general variety of substructural logics over full Lambek calculus, categorical treatment of quantifiers is presented in Maruyama [15]). The corresponding double-line rules are the following:

ϕ ψ ϕ ∀x ψ ∃ x ϕ ψ

ϕ ψ (17)

with the obvious eigenvariable conditions (which naturally emerge from a categorical setting). Categorical logicians say that ∀ is a right adjoint, and ∃ is a left adjoint of substitution (or pullback in categorical terms). Finally, truth constants ⊥ and T are left and right adjoints of the unique operation from L to the one-element set {∗}, with the following double-line rules:

⊥ ϕ

∗ ∗ ∗ ∗

ϕ T (18)

which come down to: ⊥ ϕ ϕ T (19)

All the double-line rules above yield a sound and complete axiomatisation of intuitionistic logic; equivalence with other standard systems can easily be verified.

Building upon these observations, we can articulate the categorical inferentialistic process of introducing a logical constant in a meaning-conferring manner:

• At the beginning, there are universally definable operations, i.e., those operations that are definable in the general language of category theory.

– We may replace “the general language of category theory” by “the general language of monoidal category theory” if we want to account for substructural logics as well as logics with unrestricted structural rules.

– For example, diagonal Δ above is a universally definable operation. As observed in the above case of the double-line rule for ∧, the existence of Δ amounts to our meta-theoretical capacity to handle multiple sequents at once (in particular, ability to put two sequents in parallel in the case of ∧).

• Logical constants are introduced step by step, by requiring the existence of right or left adjoints of existing operations, i.e., universally definable operations or already introduced logical constants.

– In other words, we define logical constants by bi-directional inferential rules corresponding to adjunctions concerned. Thus, this may be conceived of as a special sort of inferentialistic process to confer meaning on connectives. The condition of adjointness bans non-meaning-conferring rules like tonk's (discussed later).

– For example, conjunction and disjunction above can be introduced as adjoints of a universally definable operation (i.e., diagonal); after that, implication can be introduced as an adjoint of an existing logical constant (i.e., conjunction).

• Genuine logical constants are those introduced according to the above principle, namely the principle of categorical harmony. Others are pseudo-logical constants.

According to this view, logical constants in a logical system must be constructed step by step, from old simple to new complex ones, based upon different adjunctions. This

may be called the iterative conception of logic. The rôle of the powerset operation (or making a set of already existing sets) in the iterative conception of sets is analogous to the rôle of the operation of taking adjoint functors.

A remark on monoidal categories for substructural logics is that the language of monoidal categories is more general than the language of (plain) categories in the sense that monoidal products ⊗ encompass cartesian products ×. Formally, we have the fact that a monoidal product ⊗ is a cartesian product if and only if there

are both diagonals δ : C → C ⊗ C and projections p1 : C ⊗ D → C and p2 : C ⊗ D → D where ⊗ is assumed to be symmetric. The logical counterpart of this fact is that multiplicative conjunction ⊗ is additive conjunction if and only if both contraction and weakening hold where exchange is assumed. Since contraction may be formulated as ϕ ϕ ⊗ ϕ, and weakening as ϕ ⊗ ψ ϕ and ϕ ⊗ ψ ψ , it is evident that diagonals correspond to contraction, and projections to weakening (this correspondence can be given a precise meaning in terms of categorical semantics).

There are different conceptions of harmony in proof-theoretic semantics, discussed by different authors. In the present article, adjointness is conceived of as a sort of proof-theoretic harmony, and it is somehow akin to Prawitz's inversion principle in that both put emphasis on (different sorts of) “invertibility” of rules; recall that an adjunction amounts to the validity of a “bi-directional” rule of certain form. Categorically speaking, adjointness exhibits harmony between two functors; logically speaking, adjointness tells us harmony between the upward and the downward rules of the induced bi-directional rule. The precise procedure of introducing logical constants according to categorical harmony has already been given above. Let us summarise the main point of categorical harmony as follows.

• A logical constant must be introduced by (the double-line rule of) an adjunction with respect to an existing operation.

As we observed above, standard logical constants can be characterised by adjunctions or adjunction-induced double-line rules. The idea of capturing logicality by double-line rules was pursued by Došen [8, 9]. It seems, however, that his focus was not on harmony, but rather on logicality only (as pointed out by Schroeder-Heister [21]), and moreover he did not really use adjointness as a criterion to ban pathological, non-meaning-conferring rules. Indeed, Bonnay and Simmenauer [4] show that Došen's theory of logicality cannot ban a weird connective “blonk”; nonetheless, the adjointness harmony of the present paper is immune to blonk, since it is not definable by an adjunction, even though it is defined by a double-line rule. The approach of this paper takes adjointness as the primary constituent of harmony, analysing issues in proof-theoretic semantics from that particular perspective. Although the double-line and adjointness approaches are quite similar at first sight, however, they are considerably different as a matter of fact, as seen in the case of Bonnay and Simmenauer's blonk. There are actually several subtleties lurking behind the formulation above:

• It turns out that definability via one adjunction is crucial, since tonk can be defined via two adjunctions.

• A logical constant must be defined as an adjoint of an existing operation, since Russell-type paradoxical constants can be defined as adjoints of themselves.

These points shall be addressed later in detail. Before getting into those issues, in the next section, we briefly compare and contrast categorical harmony with other principles.