Desktop version

Home arrow Philosophy arrow Advances in Proof-Theoretic Semantics

Deductions in Multicategories and Polycategories

Let us consider now the deductions where we can have more than one premise, though we still have a single conclusion. Such deductions, which correspond to Gentzen's singular sequents, with not more than one formula on the right-hand side, correspond to arrows f : ΓA in Lambek's multicategories, sometimes called multiarrows, where capital Greek letters like Γ stand for finite sequences of objects. A particular kind of multicategory is an operad, where Γ in multiarrows f : ΓA is a finite sequence every member of which is A. The algebraic notion of operad, which has arisen in algebraic topology, has been much investigated lately. (References concerning the notions of operad and multicategory, and a discussion of matters concerning them, may be found in [11].)

Multicategories can be mimicked by categories with additional structure like monoidal categories, which have a binary operation on objects like conjunction, enabling us to bind the objects in Γ into a single object. The particular structure of multicategories is however important and interesting, and we shall now examine one aspect of it.

In multicategories instead of composition we have insertion operations on multi-

arrows:

f : Γ A g : Δ, A B

g <] f : Δ, Γ , ΘB

which correspond to Gentzen's cut of singular sequents. The notation g<] f is ambiguous, because it does not specify the cut formula. This ambiguity is remedied with the more precise notation of [11], but for the comments we will make here we can do with the less precise notation we have just introduced.

In multicategories, besides the associativity of insertion that corresponds to the associativity of composition in categories:

f : Γ A g : Δ, A B

g <] f : Δ, Γ , Θ B h : IT, B ,'£ C

h <] (g <] f ) : IT, Δ, Γ , Θ, '£C

g : Δ, A B h : IT, B ,'£ C

f : Γ A h <] g : IT, Δ, A ,Θ,'£ C

(h <] g) <] f : IT, Δ, Γ , Θ, '£C

h <] (g <] f ) = (h <] g) <] f,

we have another kind of associativity of insertion, which involves also commutativity:

f : Γ A h : Δ, A ,Θ, B ,IT C

g : B h <] f : Δ, Γ , Θ , B ,IT C

(h <] f ) <] g : Δ, Γ , Θ, '£, ITC

g : B h : Δ, A ,Θ, B ,IT C

f : Γ A h <] g : Δ, A ,Θ,'£,IT C

(h <] g) <] f : Δ, Γ , Θ, '£, ITC

(h <] f ) <] g = (h <] g) <] f,

This other associativity is interesting algebraically and combinatorially. It is also related to interesting polyhedra (see [11], Sect. 13).

In polycategories we have arrows ΓΔ, which correspond to the plural

sequents of Gentzen, where there may be several formulae on the right-hand side

too. The arrows of polycategories correspond to the deductions of classical logic, which are investigated graph-theoretically in [12]. For polycategories and their operations of insertions, which correspond to Gentzen's cut for plural sequents, we have besides the associativity and the associativity involving commutativity on the lefthand side, analogous to those we have just given for multicategories, another associativity involving commutativity on the right-hand side (see [12], Propositions 2.1–3).

These plural deductions of classical logic are not very natural. They have been invented following Gentzen's suggestion, and not found by describing deduction in real life. They provide however the best means to understand classical logic prooftheoretically. They are implicit in the categorial approach to the proof theory of classical logic of [9], and in the categorial approach to the proof theory of linear logic of [10].

The remarks made here on deduction lead to the following tentative characterization of this notion. A deduction is an arrow in a category, a multicategory, or a polycategory, where the objects are more or less akin to propositions—something in the field of propositions.

 
Found a mistake? Please highlight the word and press Shift + Enter  
< Prev   CONTENTS   Next >

Related topics