work, using tools such as filtration or unravelling. As another possibility, completeness proofs based on cut-free sequent calculi usually produce finite models directly. Most of the modal systems used in practice (including all listed above) have FMP. In some cases, we can use FMP to prove Kripke completeness of a logic: every normal modal logic is complete wrt a class of modal algebras, and a finite modal algebra can be transformed into a Kripke frame. As an example, Robert Bull proved using this method that every normal extension of S4.3 has FMP, and is Kripke complete. Kripke semantics has a straightforward generalization to logics with more than one modality. A Kripke frame for a language with as the set of its necessity operators consists of a non-empty set W equipped with binary relations Ri for each i ∈ I. The definition of a satisfaction relation is modified as follows: if and only if Carlson models A simplified semantics, discovered by Tim Carlson, is often used for polymodal provability logics. A Carlson model is a structure with a single accessibility relation R, and subsets Di ⊆ W for each modality. Satisfaction is defined as: if and only if Carlson models are easier to visualize and to work with than usual polymodal Kripke models; there are, however, Kripke complete polymodal logics which are Carlson incomplete. In Semantical Considerations on Modal Logic, published in 1963, Kripke responded to a difficulty with classical quantification theory. The motivation for the world-relative approach was to represent the possibility that objects in one world may fail to exist in another. But if standard quantifier rules are used, every term must refer to something that exists in all the possible worlds. This seems incompatible with our ordinary practice of using terms to refer to things that exist contingently. Kripke's response to this difficulty was to eliminate terms. He gave an example of a system that uses the world-relative interpretation and preserves the classical rules. But the costs are severe. First, his language is artificially impoverished, and second, the rules for the propositional modal logic must be weakened. Kripke's possible worlds theory has been used by narratologists (beginning with Pavel and Dolezel) to understand "reader's manipulation of alternative plot developments, or the characters' planned or fantasized alternative action series." This application has become especially useful in the analysis of hyperfiction. Intuitionistic logic Kripke semantics for intuitionistic logic follows the