Home Philosophy Advances in Proof-Theoretic Semantics

## The Principle of Categorical HarmonyIn 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 formula • The concept of proof-decorated relation
where • The concept of sequential composition ◦ of proofs: composing
If we think of a monodical category for substructural logic, we additionally have parallel composition ⊗:
where • The concept of reduction of proofs such that the identity proofs may be canceled out (i.e., modulo reducibility). Moreover, reduction must respect composition (i.e., if 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 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
consists of a set
is called left adjoint to (or
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
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
where × denotes binary product on categories (in this case just preorders) or in the category of (small) categories. Then, the right adjoint of
The left adjoint of ∨ The associated bi-directional rule for ∧ turns out to be the following:
which, by the definition of product on categories, boils down to the following familiar rule:
ϕ2 ϕ1 L ϕ3
This is the inferential rule for conjunction ∧ that is packed in the adjunction
The derived inferential rule is the following:
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
x ψ ∃ x ϕ ψ
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
∗ ∗
which come down to: ⊥ 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 • 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 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. |

< Prev | CONTENTS | Next > |
---|

Related topics |

Academic library - free online college e textbooks - info{at}ebrary.net - © 2014 - 2020