Em lógica, dizemos que a estrutura L tem a propriedade do modelo finito (ou, PMF) se existe uma classe de modelos M de L (isto é, cada modelo em M é um modelo de L) de tal forma que qualquer não-teorema de L seja falso segundo algum modelo finito de M. Uma outra forma de interpretação, é dizer que a estrutura L tem a PMF se, para cada fórmula A de L, A é um L-teorema se, e somente se, A é um teorema da teoria de modelos finitos de L.
Se L é axiomatizável (e tem um conjunto de regras recursivas) e tem a PMF, então L é decidível. No entanto, a afirmação de que se L é recursivamente axiomatizável, tem a PMF e é decidível, é falsa. Mesmo se houver um número finito de modelos finitos para escolher (a menos de isomorfismos) ainda há o problema de verificar se a estrutura de tais modelos valida a lógica, e isso não pode ser decidível quando a lógica não é finitamente axiomatizável, mesmo quando é recursivamente axiomatizável. (Note que a lógica é recursivamente enumerável se, e somente se, for recursivamente axiomatizável, resultado conhecido como o teorema de Craig.)
Exemplo
Uma fórmula de primeira ordem com um quantificador universal tem a PMF. Uma fórmula de primeira ordem sem símbolos funcionais, em que todos os quantificadores existenciais aparecem primeiro na fórmula, também tem a PMF.[1]
Veja Mais
Referências
- 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.
