Completeness

This chapter is about the completeness — and incompleteness — of normal modal logics. As we saw in Section 1.6, normal modal logics are collections of formulas satisfying certain simple closure conditions. They can be specified either syntactically or semantically, and this gives rise to the questions which dominate the chapter: Given a semantically specified logic, can we give it a syntactic characterization, and if so, how? And: Given a syntactically specified logic, can we give it a semantic characterization (and in particular, a characterization in terms of frames), and if so, how? To answer either type of question we need to know how to prove (soundness and) completeness theorems, and the bulk of the chapter is devoted to developing techniques for doing so. The chapter has two major parts. The first, comprising the first four sections, is an introduction to basic completeness theory. It introduces canonical models, explains and applies the completeness-via-canonicity proof technique, discusses the Sahlqvist Completeness Theorem, and proves two fundamental limitative results. The material introduced in these sections (which are all on the basic track) is needed to follow the second part and the algebraic investigations of Chapter 5. In the second part of the chapter we turn to the following question: what are we to do when canonicity fails? (As will become clear, canonicity failure is a fact of life for temporal logic, propositional dynamic logic, and other applied modal languages.)