Substructural Logics: A Primer

Substructural logics owe their name to the fact that an especially immediate and intuitive way to introduce them is by means of sequent calculi à la Gentzen where one or more of the structural rules (weakening, contraction, exchange, cut) are suitably restricted or even left out. We do not assume the reader to be familiar with the terminology of the preceding sentence, which will be subsequently explained in full detail — but if only she has some acquaintance with the history of twentieth century logic, at least the name of Gerhard Gentzen should not be completely foreign to her.

In this chapter, we shall introduce sequent calculi and Hilbert-style calculi for several substructural logics. A standard way to accomplish such tasks, in handbooks whose scope comprises various logical systems, is to focus on a basic system and then consider its extensions. Such extensions can be either axiomatic (the language remains the same as in the basic calculus, but more postulates are added) or linguistic (the language is enriched by new logical constants and, possibly, some postulates governing these new symbols are introduced). The choice of such a basic system must perforce be, to some extent, arbitrary. However, a delicate tradeoff is involved: this system must be neither too weak, for it would lack any intrinsic interest, nor too strong, since its extensions would be too limited in number.

In Chapter 1, we discussed at some length the importance of cut elimination, both from a philosophical and from a technical viewpoint. Hitherto, however, we did not prove the cut elimination theorem for any of the systems so far introduced. This will be exactly the task of the present chapter. For a start, we shall present Gentzen’s proof of the Haupsatz for LK; coming to know how such a proof works is essential also from our perspective, for it allows to appreciate the role that structural rules play in it. Subsequently, we shall assess how Gentzen’s strategy should be modified in order to obtain the elimination of cuts for systems lacking some of the structural rules. We shall also show, with the aid of appropriate counterexamples, that not all of our sequent systems are cut-free.

In Chapter 2, we examined two different kinds of formalisms whose role is undoubtedly central in the proof theory of substructural logics: sequent calculi, on the one hand, and Hilbert-style systems, on the other. On that occasion, we noticed that there are at least six well-motivated axiomatic calculi — HRW, HR, HRMI, HRM, HLuk, and HLuk ₃ — which do not have any sequential counterpart, in that they seem scarcely amenable to a treatment by means of traditional sequents. As we already remarked, Hilbert-style calculi are defmitely not the best one could hope for when it comes to engaging in proof search and theorem proving tasks. As a consequence, it seems desirable to find efficient and manageable formalisms also for the above-mentioned logics.

When studying a logical calculus S of any kind, it is extremely important to be in a position to fmd a class of adequate models for it — i.e. a class of algebraic structures which verify exactly the provable formulae of S. Thus, for example, it turns out that the algebraic counterpart of classical propositional logic are Boolean algebras, while intuitionistic propositional logic corresponds to Heyting algebras. As a rule, these correspondences pave the way for a profitable interaction: the investigation of models may yield several fruitful insights on the structure of the given calculus, and, conversely, it may even happen that proof-theoretical techniques be of some avail in proving purely algebraic results (Grishin 1982; Kowalski and Ono 2000).

In the preceding chapter, we introduced and investigated at some length several classes of algebraic structures, claiming that there exists a correspondence between the diagram of logics in Table 2.2 and the diagram of algebras in Table 5.1. Our present task will be to show that our claim was sound. In fact, we shall prove completeness theorems for most of the Hilbert-style calculi of Chapter 2 using the algebraic structures of Chapter 5. Subsequently, we shall see that — at least in some cases — such classes of structures are even too large for our purposes: due to the representation results of Chapter 5, in fact, the theorems of the logics at issue coincide with the formulae which are valid in a smaller (and usually much easier to tinker with) class of structures. In a few lucky cases, it will be sufficient to consider a single manageable structure, just as it happens for classical logic (even though this structure may not be just as simple and wieldy). Finally, we shall quickly browse through some applications of algebraic semantics to the solution of purely syntactical problems concerning our substructural calculi.

We have traced back the conceptual roots of algebraic semantics to Frege’s idea according to which sentences are names for truth values. But there is another standpoint one can assume about the semantic value of sentences. In fact, a true sentence like “Brutus killed Caesar” could have been false if Brutus had not killed Caesar; it is true in the light of what actually happened, but could have been false if human history had been different — in another “possible world”, so to speak. In this perspective, it seems natural to view sentences as names not for truth values, but rather for sets of possible worlds. According to this approach, in fact, the meaning of a sentence A is given by specifying which states of affairs, courses of events etc. render A true.