Filtrations and Basic Proof Theory Notes for Lecture 5
Note that !Σ is an equivalence relation. Let |w|Σ = {v | w !Σ v} denote the equivalence class of w under !Σ. Definition 1.1 (Filtration) Let M = 〈W,R, V 〉 be a Kripke model. Given a set of formulas closed under subformulas, a model Mf = 〈W f , Rf , V f 〉 is said to be a filtration of M through Σ provided • W f = {|w|Σ | w ∈W} • If wRv then |w|ΣR |v|Σ • If |w|ΣR |v|Σ then for each 3φ ∈ Σ, if M, v |= φ then M, w |= 3φ • V f (p) = {|w|Σ | w ∈ V (p)} /
FINITE MODELS CONSTRUCTED FROM CANONICAL FORMULAS
This paper obtains the weak completeness and decidability results for standard systems of modal logic using models built from formulas themselves. This line of work began with Fine (Notre Dame J. Form. Log. 16:229–237, 1975). There are two ways in which our work advances on that paper: First, the definition of our models is mainly based on the relation Kozen and Parikh used in their proof of the completeness of PDL, see (Theor. Comp. Sci. 113–118, 1981). The point is to develop a general model-construction method based on this definition. We do this and thereby obtain the completeness of most of the standard modal systems, and in addition apply the method to some other systems of interest. None of the results use filtration, but in our final section we explore the connection.
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.