Home Philosophy Advances in Proof-Theoretic Semantics

## Deductions in Multicategories and PolycategoriesLet 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 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 In multicategories instead of composition we have arrows:
which correspond to Gentzen's cut of singular sequents. The notation In multicategories, besides the associativity of insertion that corresponds to the associativity of composition in categories:
we have another kind of associativity of insertion, which involves also commutativity:
This other associativity is interesting algebraically and combinatorially. It is also related to interesting polyhedra (see [11], Sect. 13). In 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. |

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

Related topics |

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