En la lógica matemática , una lógica L tiene la propiedad de modelo finito (FMP para abreviar) si alguno no teorema de L está falseada por alguna finitos modelo de L . Otra forma de expresar esto es decir que L tiene el FMP si para cada fórmula A de L , A es un L -theorem si y sólo si A es un teorema de la teoría de los modelos finitos de L .
Si L es finitamente axiomatizable (y tiene un conjunto recursivo de reglas de inferencia ) y tiene el fmp, entonces es decidible . Sin embargo, el resultado no es válido si L es simplemente axiomatizable de forma recursiva. Incluso si solo hay un número finito de modelos finitos para elegir (hasta el isomorfismo ), todavía existe el problema de verificar si los marcos subyacentes de tales modelos validan la lógica, y esto puede no ser decidible cuando la lógica no es finitamente axiomatizable, incluso cuando es recursivamente axiomatizable. (Tenga en cuenta que una lógica es recursivamente enumerable si y solo si es recursivamente axiomatizable, un resultado conocido como teorema de Craig ).
Ejemplo
Una fórmula de primer orden con una cuantificación universal tiene el fmp. Una fórmula de primer orden sin símbolos de función , donde todas las cuantificaciones existenciales aparecen primero en la fórmula, también tiene el fmp. [1]
Ver también
Referencias
- Patrick Blackburn, Maarten de Rijke , Yde Venema Modal Logic . Cambridge University Press, 2001.
- Alasdair Urquhart . Decidibilidad y propiedad del modelo finito. Revista de lógica filosófica , 10 (1981), 367-370.
- ^ Leonid Libkin , Elementos de la teoría de modelos finitos , capítulo 14