Finite model property

In logic, a logic L has the finite model property (fmp for short) if any non-theorem of L is falsified by some finite model of L. Another way of putting this is to say that L has the fmp if for every formula A of L, A is an L-theorem iff A is a theorem of the theory of finite models of L.

If L is finitely axiomatizable (and has a recursive set of recursive rules) and has the fmp, then it is decidable. However, the result does not hold if L is merely recursively axiomatizable. Even if there are only finitely many finite models to choose from (up to isomorphism) there is still the problem of checking whether the underlying frames of such models validate the logic, and this may not be decidable when the logic is not finitely axiomatizable, even when it is recursively axiomatizable. (Note that a logic is recursively enumerable if and only if it is recursively axiomatizable, a result known as Craig's theorem.)

Example

A first-order formula with one universal quantification has the fmp. A first-order formula without function symbols, where all existential quantifications appear first in the formula, also has the fmp.[1]

gollark: Why would people get *more* customers if they scammed people out of money?
gollark: That one.
gollark: no.
gollark: If you do reset it why do you expect it to work out better?
gollark: I've decided to throw my own metaphorical hat into the ring of today's suggestions, since it seems to be descending further into insanity *anyway*.

See also

References
  • Blackburn P., de Rijke M., Venema Y. Modal Logic. Cambridge University Press, 2001.
  • A Urquhart. Decidability and the Finite Model Property. Journal of Philosophical Logic, 10 (1981), 367-370.
  1. Leonid Libkin, Elements of finite model theory, chapter 14
This article is issued from Wikipedia. The text is licensed under Creative Commons - Attribution - Sharealike. Additional terms may apply for the media files.