Non-associativeness of composition in deductive systems?

85 Views Asked by At

WARNING: The first three and last two paragraphs of this question concern historical/philosophical matters related to a secondary aim of the question. If you are more interested in the properly mathematical part of it, you are invited to skip them as you wish.

BEGINNING OF THE HISTORICAL/PHILOSOPHICAL PART OF THE QUESTION

I begin with a small and (probably excessively, but also harmlessly) simplified introduction. The notion of category seems to have been historically inspired by a common pattern emerging everywhere in the mathematical 'zoo' after the notion of function between sets had been sufficiently established. Since the composition of functions turns out to be associative in virtually all historical examples (and how could it not be?!), the composition of morphisms in a category is axiomatized to be associative as well.

After being properly abstracted from such examples, category theory found its way of application in a much broader class of situations. In particular, there are the notions of enrichment and internalization, which permit some 'animals' that have been historically thought as objects in a category, to be treated as categories themselves, allowing quite fruitful generalizations and better understanding. This clearly surpasses the original aim of category theory (even under a less simplified perspective on its historical development, I believe).

At this point, however, the associativeness axiom seems to start charging its price: it's much more difficult, if not impossible, to apply the notions of enrichment and internalization when dealing with objects that involve some kind of non-associativeness. Thus, it sounds quite natural to ask: is it possible to relax the definition of a category with respect to the associativeness of composition and still get some reasonable theory to deal with? Curiously, such a notion of 'non-associative category' happens to appear in another application that category theory has found in its history: Logic.

END OF THE HISTORICAL/PHILOSOPHICAL PART OF THE QUESTION

Indeed, a deductive system (as defined, for example, in the book 'Introduction to higher order categorical logic' by Lambek and Scott) is precisely a category without the associativeness axiom. As the authors put it,

'Logicians will think of the objects of a deductive system as formulas, of the arrows as proofs (or deductions) and of an operation on arrows as a rule of inference.' (p.47)

And they stress:

'Logicians should note that a deductive system is concerned not just with unlabelled entailments or sequents $A\rightarrow B$ (as in Gentzen's proof theory), but with deductions or proofs of such entailments.' (p.47)

In other words, as I understand it, deductive systems should be thought as being accompanied by some concrete 'models' of the systems themselves. Unfortunately, I was not able to find examples of such deductive systems and their concrete 'models' that put in relief the non-associativeness of the composition in this framework. Indeed, the authors add that

'(...) from any deductive system one may obtain a category by imposing a suitable equivalence relation between proofs.' (p.52)

The first aim of this question is to ask:

What are some good examples of the role played by non-associativeness in the framework of deductive systems?

Let me elaborate on an attempt I made to imagine what such examples might look like. (I'll now possibly enter a totally amateurish way of expression; hopefully logicians won't despise me because of that! =] )

Imagine you have a formula that can be proved easily by using some induction step, or less easily without using it. Then these proofs are clearly not equivalent, but this non-equivalence doesn't have anything to do with non-associativeness of the composition of inferences: rather, the distinction between them lies much earlier than that, on the assumptions you make before starting your reasoning.

Now, imagine you have a formula that can be proved easily by using two induction steps, and less easily by using only one induction step, but starting with the same assumptions in both cases. Would this example be suitable for reflecting the non-associativeness of composition in a deductive system? What a relation making these two proofs equivalent would look like? Are there examples of concrete 'models' of deductive systems for which there are proofs that can't be made equivalent by any reasonable relation, thus making non-associativeness unavoidable? Evidently, 'reasonable' here is to be understood in relation to the concrete 'model'.

EPILOGUE OF THE HISTORICAL/PHILOSOPHICAL PART OF THE QUESTION

Finally, the secondary aim of this question: why is it so difficult to find some natural phenomena for which the appropriate notion of composition is non-associative? Is it just our still prevalent addiction to the language of sets, or there's something more subtle about that? How would you put in words your intuition about the associativeness of composition in general?

Comments about any aspects of the question as a whole will also be appreciated.