Home Philosophy Advances in Proof-Theoretic Semantics
Deductions in Categories
One can surmise the following. The specificity of transitions that are deductions is not made uniquely of the things these transitions connect. Deductions are not singled out by specifying what can be premises and conclusions. Something having to do with these transitions themselves, independently of the premises and conclusions, determines that we have to do with deductions.
What could that be? What are anyway the transitions, the passages, that deductions are? Is the active, dynamic, component in the word transition essential?
One can next surmise the following. The specificity of transitions that are deductions does not consist in this active component. That side of the matter is psychological and is not essential from a mathematical, and logical, point of view. (The dangers of psychologism that lurk here are considered in .) Reified in mathematics, deductions are like arrows in a category.
A category is made of a class whose elements are called arrows, and another class whose elements are called objects, and two functions from arrows to objects—one that assigns to every arrow an object that is its source, and the other that assigns to every arrow an object that is its target. We also have operations on arrows, about which we will speak in a moment. Otherwise, arrows are not specified more closely. They can be anything, provided they have sources and targets, and the required operations. The notion of arrow is very abstract, like the notion of point or the notion of line in geometry. It is anything that satisfies the assumptions, which are very abstract too.
In the same way, deductions have a source, called a premise, and a target, called a conclusion, and they make a structure given by operations on them. It happens that on deductions such as we have envisaged them here, with a single premise and a single conclusion, the main operations are exactly like the main operations on arrows in categories.
These are the operations that enter into the definition of a category, and they are the binary operation of composition
f : A → B g : B → C g ◦ f : A → C
which in terms of deductions is a simple form of cut of sequent systems, and the nullary operations of identity arrows 1A : A → A, which as deductions are the triv-
ial identity deductions where the premise and conclusion coincide—the primordial deductions, the axiomatic sequents. The operation of composition is partial; the target of f must be the source of g for g ◦ f to be defined.
For categories, one assumes associativity of composition:
f : A → B g : B → C
g ◦ f : A → C h : C → D
h ◦ (g ◦ f ) : A → D
g : B → C h : C → D
f : A → B h ◦ g : B → D
(h ◦ g) ◦ f : A → D
h ◦ (g ◦ f ) = (h ◦ g) ◦ f,
which makes perfect sense as an equality of deductions—it is about permuting cut with cut in sequent systems. This permuting is involved in usual cut elimination procedures (see , Sect. 2), and less usual ones (see , Chap. 1). It is however interesting in its own right, independently of these procedures. It is a perfectly natural assumption about deductions, with which they make the deepest kind of mathematical structure—a structure one finds in all categories, and in particular in the category of sets (which we will consider below).
Let us note that if, as in the Curry–Howard correspondence, one designates deductions by typed lambda terms, which is congenial with understanding proofs in the categorical, and not the hypothetical, i.e. categorial, way (see , Sect. 4), then composition of deductions is represented by substitution. With that, associativity of composition becomes invisible, unless one introduces, as it is sometimes done, an explicit substitution operator (see ). This unary operator is obtained by currying binary
composition. Instead of g ◦ f , we have something like g(x , f ), which corresponds
to “g where for x one substitutes f ”, and where (x , f ) is a unary operator applied
to g. Analogously, h(y, g) corresponds to “h where for y one substitutes g”, and
associativity of composition becomes
h(y, g(x , f )) = h(y, g)(x , f ).
It does not seem we will get closer to associativity with other notations for explicit substitution (like, for example, the notation with inverse order suggested by ,
where g(x , f ) is replaced by something like ( f, x )g, and our equation becomes
(( f, x )g, y)h = ( f, x )(g, y)h, or a vertical notation like gx , with which our equation
becomes h y
f = hgf ) . It is improbable that one could have reached the notion of category, and realized its importance, by conceiving and representing matters pertaining to composition in that manner.
In categories one assumes moreover identity laws, i.e. laws of composing with identity arrows:
1 A : A → A f : A → B
f ◦ 1A : A → B
f : A → B 1 B : B → B
1B ◦ f : A → B
f ◦ 1A = 1B ◦ f = f,
which in terms of deductions say that composing a deduction with an identity deduction, either on the side of the premise or on the side of the conclusion, leaves the deduction unchanged. This again makes perfect sense as an equality of deductions, and is an essential ingredient of cut elimination. When the cuts have been pushed to the top of the derivation, where they are performed with axiomatic sequents, they disappear.
Lambek (see ) called deductive system the notion generalizing categories by not assuming the associativity of composition and the laws of composing with identity arrows. In  and  (Sect. 1.9) one can see how this notion of deductive system is characterized proof-theoretically by a representation result in the style of Stone, and how the notion of category is characterized proof-theoretically by a representation result in the style of Cayley.
There may be further operations on arrows, with which we enter into the field of categories with additional structure. One such operation is tied to the biendofunctor of product, which corresponds to conjunction, both in classical and intuitionistic logic. Coproduct, with which another such operation is tied, corresponds to disjunction, in both logics again. With product and coproduct we obtain equations between deductions that make perfect sense in proof theory. They stem from adjointness of functors, and are related to normalization in natural deduction and cut elimination in sequent systems (see ,  and ). Other equations, like those involving distributivity of product over coproduct, i.e. conjunction over disjunction, may, but need not, be based on adjointness. Intuitionistic logic will differ essentially from classical logic by tying implication to adjointness (see  and ), which should not be done for classical, material, implication (see , Chap. 14). We will not go further into categorial proof theory, which deals with the equations between deductions suggested by such categories with additional structure. Let it be said only that it is remarkable how equations important in mathematics in general, or in particular fields of mathematics, reemerge as perfectly sensible equations between deductions (see ).
What was surmised above is that the structure that deductions make with such operations is an essential ingredient in the notion of deduction. Could one go as far as to take this as the main ingredient? As in category theory, the structure of arrows would be the main thing. And, as in category theory, the arrows would be more important than the objects. With deductions the objects are the premises and conclusions, and these premises and conclusions, whatever they are precisely— propositions, commands, questions, problems, or something else—would not precede the arrows. Deducing would not be preceded by asserting, or another function of language.
When functions are reified as sets of ordered pairs, the active, dynamic, component in the notion of function is lost. This component, which comes from psychology, is also lost in the reification brought by the categorial notion of function, where a function is an arrow in a category. Categorially, functions in the category Set, where the objects are sets and the arrows are functions, are characterized through composition and identity functions. The same operations characterize deductions in general.
Although Set has the structure that deductions make, it is not natural for its objects to be called premises and conclusions, and for its arrows to be called deductions. One reason may be the nature of these objects, which are not in the field of propositions (see the end of the preceding section). Another reason might be that we have too many of these deductions. Any two objects would be connected by a deduction, except when the premise is not empty while the conclusion is empty. Deductions, in the categories where arrows may be more naturally designated by that term, are usually more discriminatory. There are more objects not connected by arrows.
The structure of deductions imitates the structure of the category Set even more when they involve the binary connectives of conjunction, disjunction and implication, together with the nullary connectives T and ⊥. This structure, appropriate for intuitionistic propositional logic, imitates Set with the biendofunctors of product, coproduct and exponentiation (for exponentiation we have covariance in the base and contravariance in the exponent), together with the terminal and initial objects, i.e. a singleton and the empty set. Still, the arrows of the category Set could not be taken as deductions, but only as their model. (The question of models of deductions was discussed in .) This is the model that stands behind the standard proof-theoretic semantics for intuitionistic logic, which through the Curry–Howard correspondence is tied to the typed lambda calculus.
Matters become clearer when in conceiving this semantics we do not conform to the dogma mentioned at the beginning. When we look upon this semantics hypothetically, and not categorically, as in the typed lambda calculus, we will end up in the categorial setting of Set. With the typed lambda calculus we also end up in the sets of Set, but the categorial setting is hidden.
In  one may find a categorial setting for the proof theory of classical conjunctivedisjunctive logic different from that of Set, which leads to a categorial setting for the proof theory of the whole of classical propositional logic where a characterization through adjunction for classical implication is relinquished. Implication is again characterized through adjunction in the categorial setting for the proof theory of linear propositional logic without modalities, which is investigated in .
|< Prev||CONTENTS||Next >|