  Basic ideas are presented semantically rather than proof-theoretically, though both axiom systems and tableau systems exist. Even so, technical details can become baroque, so as far as possible, we will separate informal presentation, which is enough to get the general idea, from its formal counterpart, which is of more specialized interest. A general acquaintance with modal logic is assumed (though there is a very brief discussion to establish notation, which varies some from author to author). It should be noted that modal semantics is used here, and generally, in two different ways. Often one has a particular Kripke model in mind, though it may be specified informally. For instance, we might consider a Kripke model in which the states are the present instant and all past ones, with later states accessible from earlier ones. Such a model is enlightening when discussing “the King of France” for instance, even though the notion of instant is somewhat vaguely determined. But besides this use of informally specified concrete models, there is formal Kripke semantics which is a mathematically precise thing. If it is established that something, say \(\Box (X \supset Y) \supset (\Box X \supset \Box Y)\), is valid in all formal Kripke models, we can assume it will be so in our vaguely specified, intuitive models, no matter how we attempt to make them more precise. Informal models pervade our discussions—their fundamental properties come from the formal semantics.