Propiedad de modelo finito

En lógica matemática , una lógica L tiene la propiedad de modelo finito (pff, por sus siglas en inglés) si cualquier no teorema de L es refutado por algún modelo finito de L. Otra forma de expresarlo es decir que L tiene la pff si para cada fórmula A de L , A es un teorema de L si y solo si A es un teorema de la teoría de modelos finitos de L.

Si L es finitamente axiomatizable (y posee un conjunto recursivo de reglas de inferencia ) y tiene el fmp, entonces es decidible . Sin embargo, el resultado no se cumple si L es meramente recursivamente axiomatizable. Incluso si solo hay un número finito de modelos finitos entre los que elegir (salvo isomorfismo ), persiste el problema de comprobar si los marcos subyacentes de dichos modelos validan la lógica, y esto puede no ser decidible cuando la lógica no es finitamente axiomatizable, incluso cuando es recursivamente axiomatizable. (Cabe destacar que una lógica es recursivamente enumerable si y solo si es recursivamente axiomatizable, un resultado conocido como el teorema de Craig ).

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 ]}

• Semántica de Kripke

• Patrick Blackburn, Maarten de Rijke , Yde Venema Lógica modal . Prensa de la Universidad de Cambridge, 2001.
• Alasdair Urquhart . Decidibilidad y la propiedad del modelo finito. Journal of Philosophical Logic , 10 (1981), 367-370.