mathematical logic Mathematical logic is the study of formal logic within mathematics. Major subareas include model theory, proof theory, set theory, and recursion theory. Research in mathematical logic commonly addresses the mathematical properties of formal ...

, a logic L has the finite model property (fmp for short) if any non-

theorem In mathematics, a theorem is a statement that has been proved, or can be proved. The ''proof'' of a theorem is a logical argument that uses the inference rules of a deductive system to establish that the theorem is a logical consequence of t ...

of L is falsified by some ''finite''

model A model is an informative representation of an object, person or system. The term originally denoted the plans of a building in late 16th-century English, and derived via French and Italian ultimately from Latin ''modulus'', a measure. Models c ...

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

if and only if In logic and related fields such as mathematics and philosophy, "if and only if" (shortened as "iff") is a biconditional logical connective between statements, where either both statements are true or both are false. The connective is b ...

''A'' is a theorem of the theory of finite models of L. If L is finitely axiomatizable (and has a

recursive Recursion (adjective: ''recursive'') occurs when a thing is defined in terms of itself or of its type. Recursion is used in a variety of disciplines ranging from linguistics to logic. The most common application of recursion is in mathematics ...

set of

inference rule In the philosophy of logic, a rule of inference, inference rule or transformation rule is a logical form consisting of a function which takes premises, analyzes their syntax, and returns a conclusion (or conclusions). For example, the rule of ...

s) 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 In mathematics, an isomorphism is a structure-preserving mapping between two structures of the same type that can be reversed by an inverse mapping. Two mathematical structures are isomorphic if an isomorphism exists between them. The word i ...

) 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 In mathematical logic, Craig's theorem states that any recursively enumerable set of well-formed formulas of a first-order language is (primitively) recursively axiomatizable. This result is not related to the well-known Craig interpolation theore ...

Example

first-order In mathematics and other formal sciences, first-order or first order most often means either: * "linear" (a polynomial of degree at most one), as in first-order approximation and other calculus uses, where it is contrasted with "polynomials of high ...

formula with one

universal quantification In mathematical logic, a universal quantification is a type of quantifier, a logical constant which is interpreted as "given any" or "for all". It expresses that a predicate can be satisfied by every member of a domain of discourse. In other ...

has the fmp. A first-order formula without function symbols, where all

existential quantification In predicate logic, an existential quantification is a type of quantifier, a logical constant which is interpreted as "there exists", "there is at least one", or "for some". It is usually denoted by the logical operator symbol ∃, which, ...

s appear first in the formula, also has the fmp. Leonid Libkin, ''Elements of finite model theory'', chapter 14

References

* Patrick Blackburn,

Maarten de Rijke Maarten de Rijke (born 1 August 1961) is a Dutch computer scientist. His work initially focused on modal logic and knowledge representation, but since the early years of the 21st century he has worked mainly in information retrieval. His work is ...

, Yde Venema ''Modal Logic''. Cambridge University Press, 2001. * Alasdair Urquhart. Decidability and the Finite Model Property. ''

Journal of Philosophical Logic The ''Journal of Philosophical Logic'' is a bimonthly peer-reviewed academic journal covering all aspects of logic. It was established in 1972 and is published by Springer Science+Business Media. The editors-in-chief are Rosalie Iemhoff (Utrecht ...

'', 10 (1981), 367-370. {{Reflist Logic Modal logic

Example

See also

References