The development of Kripke semantics was a breakthrough in the theory of non-classical logics, because the model theory of such logics was almost non-existent before Kripke (algebraic semantics existed, but were considered 'syntax in disguise').
A modal logic (i.e., a set of formulas) L is sound with respect to a class of frames C, if L ⊆ Thm(C).
Semantics is useful for investigating a logic (i.e. a derivation system) only if the semantic consequence relation reflects its syntactical counterpart, the syntactic consequence relation (derivability).
For any class C of Kripke frames, Thm(C) is a normal modal logic (in particular, theorems of the minimal normal modal logic, K, are valid in every Kripke model).
However, the converse does not hold in general: while most of the modal systems studied are complete of classes of frames described by simple conditions, Kripke incomplete normal modal logics do exist.
A normal modal logic L corresponds to a class of frames C, if C = Mod(L).
since w R w. On the other hand, a frame which validates T has to be reflexive: fix w ∈ W, and define satisfaction of a propositional variable p as follows:
generates an incomplete logic, as it corresponds to the same class of frames as GL (viz.
The following table lists common modal axioms together with their corresponding classes.
, which logically establishes modus ponens as a rule of inference in every possible world.
is similar to the implicit implication by existential quantifier on the range of quantification.
A set of formulas is L-consistent if no contradiction can be derived from it using the theorems of L, and Modus Ponens.
Properties of the canonical model of K immediately imply completeness of K with respect to the class of all Kripke frames.
It follows from the preceding discussion that any logic axiomatized by a canonical set of formulas is Kripke complete, and compact.
Refinements and extensions of the canonical model construction often work, using tools such as filtration or unravelling.
As another possibility, completeness proofs based on cut-free sequent calculi usually produce finite models directly.
As an example, Robert Bull proved using this method that every normal extension of S4.3 has FMP, and is Kripke complete.
The definition of a satisfaction relation is modified as follows: A simplified semantics, discovered by Tim Carlson, is often used for polymodal provability logics.
Satisfaction is defined as 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.
Intuitionistic logic is sound and complete with respect to its Kripke semantics, and it has the finite model property.
is an intuitionistic Kripke frame, Mw is a (classical) L-structure for each node w ∈ W, and the following compatibility conditions hold whenever u ≤ v: Given an evaluation e of variables by elements of Mw, we define the satisfaction relation
: Here e(x→a) is the evaluation which gives x the value a, and otherwise agrees with e.[9] As part of the independent development of sheaf theory, it was realised around 1965 that Kripke semantics was intimately related to the treatment of existential quantification in topos theory.
Though this development was the work of a number of people, the name Kripke–Joyal semantics is often used in this connection.
The natural homomorphisms in Kripke semantics are called p-morphisms (which is short for pseudo-epimorphism, but the latter term is rarely used).
is a relation B ⊆ W × W’, which satisfies the following “zig-zag” property: A bisimulation of models is additionally required to preserve forcing of atomic formulas: The key property which follows from this definition is that bisimulations (hence also p-morphisms) of models preserve the satisfaction of all formulas, not only propositional variables.
for a propositional variable p. The definition of the accessibility relation R’ varies; in the simplest case we put but many applications need the reflexive and/or transitive closure of this relation, or similar modifications.
It can be remedied by equipping Kripke frames with extra structure which restricts the set of possible valuations, using ideas from algebraic semantics.
As an example from theoretical computer science, they give labeled transition systems, which model program execution.
Blackburn et al. thus claim because of this connection that modal languages are ideally suited in providing "internal, local perspective on relational structures."
(p. xii) Similar work that predated Kripke's revolutionary semantic breakthroughs:[11]