Finite model property
Encyclopedia
In logic
, we say a logic L has the finite model property (fmp for short) if there is a class of models M of L (i.e. each model M is a model of L) such that any non-theorem of L is falsified by some finite model in M. 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 strengthened claim that if L is recursively axiomatizable and the fmp then it is decidable, is false. 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 iff it is recursively axiomatizable, a result known as Craig's theorem
.)
Logic
In philosophy, Logic is the formal systematic study of the principles of valid inference and correct reasoning. Logic is used in most intellectual activities, but is studied primarily in the disciplines of philosophy, mathematics, semantics, and computer science...
, we say a logic L has the finite model property (fmp for short) if there is a class of models M of L (i.e. each model M is a model of L) such that any non-theorem of L is falsified by some finite model in M. 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
IFF
IFF, Iff or iff may refer to:Technology/Science:* Identification friend or foe, an electronic radio-based identification system using transponders...
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 strengthened claim that if L is recursively axiomatizable and the fmp then it is decidable, is false. 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 iff it is recursively axiomatizable, a result known as Craig's theorem
Craig's theorem
In mathematical logic, Craig's theorem states that any recursively enumerable set of well-formed formulas of a first-order language is recursively axiomatizable. This result is not related to the well-known Craig interpolation theorem....
.)