Un método en lógicas modales y relacionadas que construye un modelo canónico cuyos mundos son conjuntos máximamente consistentes (o teorías saturadas) de fórmulas y cuyas relaciones de accesibilidad se definen a partir de condiciones sintácticas; se usa para probar teoremas de completitud estableciendo un lema de verdad que vincula fórmulas con pertenencia en mundos.

Principio

Utilizar una maximización al estilo Lindenbaum (o saturación) para extender conjuntos consistentes a conjuntos maximalmente consistentes, definir los mundos como esos conjuntos y definir relaciones de modo que las fórmulas modales se preserven; luego se prueba por inducción el lema de verdad que muestra que una fórmula es verdadera en un mundo si y solo si pertenece al conjunto maximalmente consistente correspondiente.

Demostración

Para la lógica modal normal K, partir de un conjunto consistente Γ, extenderlo a un conjunto maximal K-consistente w, tomar como marco canónico el conjunto de todos esos conjuntos máximos, definir wRv si para todo □φ ∈ w se tiene φ ∈ v, y demostrar el lema de verdad para concluir que toda fórmula válida en K es válida en el modelo canónico, obteniendo la completitud.

Aplicación incorrecta

Suponer que el modelo canónico es pequeño o posee propiedades de marco deseadas (p. ej. finito, bien fundado o satisface ciertas condiciones) sin comprobar que los axiomas de la lógica imponen esas propiedades; aplicar la construcción incorrectamente a sistemas no normales sin adaptar la definición de accesibilidad.

Consecuencia

Genera resultados de completitud (y frecuentemente de correspondencia): si una fórmula no es demostrable, su negación es consistente y se extiende a un mundo en el modelo canónico que falsifica la fórmula, produciendo un contra-modelo; también aclara la relación entre axiomas sintácticos y condiciones de marco semántico.

Inversión

En contraste con la construcción directa de modelos o la filtración: los modelos canónicos son sintácticos y a menudo grandes o no finitos, mientras que la filtración produce aproximaciones finitas que preservan la verdad para un lenguaje acotado — alternar entre ellas intercambia completitud general por finitud o decidibilidad.

Límite

Eficaz para lógicas modales normales y muchos sistemas relacionados donde los conjuntos maximalmente consistentes y la accesibilidad definida cumplen las propiedades requeridas; falla o necesita modificación para lógicas sin un lema de maximización aplicable, para ciertas lógicas no normales o cuando se necesita propiedad de modelo finito sin técnicas adicionales.

Tensión semántica

Tensión con la filtración y los modelos generados por bisimulación: los modelos canónicos son muy sintácticos y a menudo no finitos; la filtración busca modelos finitos que preserven fórmulas específicas, y la bisimulación captura la invariancia modal — la elección depende de si se precisa completitud, finitud o invariancia.

Síntesis

La construcción de modelo canónico convierte la consistencia sintáctica en contraejemplos semánticos empaquetando conjuntos maximalmente consistentes como mundos y codificando los operadores modales en relaciones de accesibilidad; el lema de verdad enlaza sintaxis y semántica, dando completitud y clarificando cómo los axiomas restringen los marcos.