An algebraic theory of normal forms

Abstract

In this paper we present a general theory of normal forms , based on a categorial result (Dubuc, 1974) for the free monoid construction. We shall use the theory mainly for proposictional modal logic, although it seems to have a wider range of applications. We shall formally represent normal forms as combinatorial objects, basically labelled trees and forests. This geometric conceptualization is implicit in (Fine, 1975) and our approach will extend it to other cases and make it more direct: operations of a purely geometric and combinatorial nature (cuts of leaves and roots, renaming labels and more generally segment-by-label replacements) will be introduced in order to give a mathematical description of the basic logical/algebraic constructions (free algebras, morphisms among them, canonical models, the lattice of varieties). We begin (Section 1) by recalling the above-mentioned categorial construction: we need a careful inspection of it because in the various examples considered later (Sections 2 and 3) we plan to deduce from it in a uniform way the normal forms and the description of finitely generated free algebras. This method always works whenever we can describe the category of algebras corresponding to the logic under consideration as a T-objects category . When this simple description seems not to be available, still the general theory might be of some interest, because a description of the category of algebras as a T -objects category plus equation is possible (we shall give examples in Section 5). The central part of the paper (Sections 4 and 5) is more advanced and specific: we show how the general approach presented here can provide some insights even in the basic case of the modal system K . Section 4 contains a contribution to the theory of normal forms, namely the description of the uniform substitution . This result will enable us to give a duality theorem for the category of finitely generated free modal algebras and in Section 5 to provide a characterization of the collections of normal forms which happen to be normal forms for a logic, thus giving a description of the lattice of modal logics . Section 6 (that can be read independently on Section 5) deals with some applications: we shall show how to use normal forms in order to prove for the modal system K the definability of higher-order propositional quantifiers and of the tense operator F (the parallel results for intuitionistic logic are in Pitts, 1992; Ghilardi, 1992; Ghilardi and Zawadowski, 1993). As to the prerequisites, the paper is almost self-contained. The reader is only assumed to have familiarity with standard techniques in algebraic logic (a possible reference is Rasiowa (1974)). Knowledge of the basic facts about adjoint functors is required too, see e.g. McLane (1971) or the appendix.