Propiedad de una lógica o teoría formal que afirma que toda fórmula o sentencia satisfacible (que tiene un modelo) posee un modelo finito.

Principio

Restringir la satisfacibilidad a estructuras finitas: si una fórmula es realizable, lo es en alguna estructura finita; esto relaciona la semántica con procedimientos algorítmicos mediante la búsqueda en dominios finitos.

Demostración

Muchas lógicas modales tienen esta propiedad porque la filtración construye, para cualquier fórmula satisfacible, un modelo de Kripke finito; concretamente, una fórmula modal satisfacible admite un marco finito que la valida.

Aplicación incorrecta

Suponer que la propiedad del modelo finito implica completitud o decidibilidad para teorías arbitrarias: la FMP ayuda a la decidibilidad en muchos casos pero no la garantiza sin una axiomatización efectiva o enumerabilidad.

Consecuencia

Con FMP y un lenguaje/axiomas efectivamente enumerables, se suele obtener decidibilidad buscando modelos finitos; la FMP también restringe los contramodelos posibles a un espacio de búsqueda finito.

Inversión

La inversión es la propiedad de modelo infinito: existen fórmulas satisfacibles que solo admiten modelos infinitos, de modo que ninguna estructura finita las realiza.

Límite

Se aplica a lógicas o teorías y a sus sentencias satisfacibles; depende de la firma y de los modelos permitidos (por ejemplo firmas relacionales vs. funcionales) y no es una afirmación sobre estructuras finitas concretas ni sobre el conteo de modelos de tamaño acotado.

Tensión semántica

Hay tensión entre satisfacibilidad finita (existencia de modelos finitos) y satisfacibilidad general (existencia de modelos arbitrarios); una lógica puede ser satisfacible sin tener FMP si la realización exige construcciones infinitas.

Síntesis

La Propiedad del Modelo Finito afirma que toda satisfacibilidad puede ser atestiguada por estructuras finitas; organiza procedimientos de búsqueda semántica y media entre la satisfacibilidad abstracta y la decidibilidad efectiva al limitar los contramodelos a dominios finitos.