Construcción modelo‑teórica en lógica modal que cuocienta un modelo de Kripke (posiblemente infinito) por una equivalencia definida a partir de un conjunto finito de fórmulas de modo que el cociente finito resultante (la filtración) preserva la verdad de cada fórmula en ese conjunto finito, permitiendo argumentos de modelo finito para satisfacibilidad y completitud.

Principio

Particionar los estados por sus valoraciones sobre el conjunto finito de subfórmulas relevante y colapsar estados equivalentes en clases de equivalencia, definiendo relaciones de sucesor entre clases para preservar la satisfacibilidad de las fórmulas elegidas mientras se reduce el tamaño del modelo.

Demostración

Para probar la propiedad de modelo finito de una lógica modal normal en una clase restringida de marcos, tomar un modelo que satisface una fórmula, recopilar el conjunto finito de subfórmulas, construir la equivalencia de filtración sobre estados que coinciden en esas subfórmulas y formar el modelo cociente finito que sigue satisfaciendo la fórmula original.

Aplicación incorrecta

Suponer que una filtración preserva la verdad de fórmulas fuera del conjunto de subfórmulas elegido, o aplicar la filtración estándar sin tener en cuenta condiciones del marco (como transitividad o simetría) que el cociente puede violar, conducente a afirmaciones incorrectas de completitud o preservación de marcos.

Consecuencia

Cuando es válida, la filtración produce modelos finitos para fórmulas satisfacibles (propiedad de modelo finito), simplifica pruebas de completitud reduciendo modelos canónicos a cocientes finitos y proporciona testigos finitos algorítmicos de satisfacibilidad en muchos sistemas modales.

Inversión

La idea inversa es el desenrollado en árbol (unravelling), que transforma un modelo en una estructura arbórea preservando verdades locales pero posiblemente expandiéndolo; invertir resalta el compromiso entre colapsar para obtener finitud y expandir para regularidad arbórea.

Límite

La filtración está ligada a un conjunto finito de fórmulas elegido y a lógicas donde la preservación de subfórmulas y las condiciones de marco son compatibles con la cociente; puede fallar o requerir modificación para lógicas con modalidades globales, operadores de punto fijo, rasgos híbridos o cuando las condiciones de marco no se preservan por el cociente.

Tensión semántica

La tensión aparece entre usar la filtración para obtener modelos canónicos pequeños y emplear métodos automata‑teóricos o algebraicos que evitan el colapso de modelos; también entre preservar sintácticamente subfórmulas y perder otras restricciones semánticas del marco en el cociente.

Síntesis

El Método de Filtración colapsa un modelo según la equivalencia inducida por un conjunto finito de fórmulas para producir un modelo más pequeño que preserva la verdad de dichas fórmulas; es una forma semántica concreta de lograr resultados de modelo finito y testigos constructivos de satisfacibilidad, sujeto a un manejo cuidadoso de condiciones de marco y características del lenguaje.