ABSTRACT

In the previous chapter, we defined propositional structures and we showed that they are suitable models for a wide range of our logics. In this chapter, we will examine a number of algebraic techniques for manipulating and constructing propositional structures. These techniques help us to clarify the nature of substructural logics. In particular, the main results of this chapter will be conservative extension results. Suppose we have a logic L over some language £, and we are interested in extending the language C to form a new language £' by adding some new connectives. We add new rules to L, giving us a new logic L' on the new language. Now we have a question to answer: is this a good extension? One way the extension can be good is as follows: DEFINITION 9.1 (CONSERVATIVE EXTENSION) The logic L' on the language £' is a conservative extension of the logic L on the language C if and only if

<> L' extends L: if something is provable in Lit is also provable in L', and <> L' is conservative over L: if something is provable in L' and it features none

of the new vocabulary in £', then it was already provable in L. If L' conservatively extends L then we know that the rules governing the additions to the language truly govern that addition, and do not tell us anything new about our original vocabulary. As one example, we will show that substructural logics on the languages [---., +--, o] are conservatively extended, in general, by the distributive lattice connectives: [A, v, T, ..l].