Editing Kripke semantics (section)

===Finite model property===

A logic has the '''[[finite model property]]''' (FMP) if it is complete
with respect to a class of finite frames. An application of this
notion is the [[decidability (logic)|decidability]] question: it
follows from
[[Post's theorem]] that a recursively axiomatized modal logic ''L''
which has FMP is decidable, provided it is decidable whether a given
finite frame is a model of ''L''. In particular, every finitely
axiomatizable logic with FMP is decidable.

There are various methods for establishing FMP for a given logic.
Refinements and extensions of the canonical model construction often
work, using tools such as [[#Model constructions|filtration]] or
[[#Model constructions|unravelling]]. As another possibility,
completeness proofs based on [[cut-elimination|cut-free]]
[[sequent calculus|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 with respect to a class of
[[modal algebra]]s, 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.