La relación formal |= (o ⊧) entre una estructura (o modelo), una asignación de variables (cuando procede) y una fórmula, que se cumple exactamente cuando la fórmula es verdadera en esa estructura bajo esa asignación según las reglas semánticas del lenguaje.

Principio

La satisfacción se define inductivamente sobre la estructura de la fórmula: las fórmulas atómicas se evalúan aplicando la interpretación de la estructura a términos y relaciones; los conectivos booleanos combinan valores de verdad de la manera habitual; los cuantificadores cuantifican sobre elementos del dominio mediante actualizaciones de la asignación; los operadores modales y otros usan las primitivas semánticas pertinentes (p. ej., accesibilidad en la semántica de Kripke).

Demostración

En lógica de primer orden, para la estructura M y asignación g, M,g |= ∃x P(x) si y sólo si existe un elemento a en el dominio de M tal que M,g[x↦a] |= P(x). En semántica proposicional de Kripke, M,w |= □φ se cumple si para todo v con wRv se tiene M,v |= φ.

Aplicación incorrecta

Tratar la relación de satisfacción como sinónimo de demostrabilidad sintáctica (confundir |= con ⊢), ignorar el papel de las asignaciones para variables libres, o aplicar cláusulas de satisfacción de una lógica a otra sin ajustar las primitivas semánticas.

Consecuencia

La relación de satisfacción sustenta nociones de la teoría de modelos como consecuencia lógica, entailment, validez, equivalencia elemental y transferencia de propiedades entre estructuras; proporciona el puente formal entre sintaxis y verdad semántica.

Inversión

La demostrabilidad (⊢) es la inversión: es una relación sintáctica entre fórmulas (y posiblemente premisas) y conclusiones dentro de un sistema deductivo, no una evaluación en modelos y asignaciones; los teoremas de completitud relacionan ambos pero siguen siendo conceptos distintos.

Límite

Se aplica solo donde se define una interpretación semántica precisa (estructuras, valoraciones, dominios); no captura nociones informales de verdad, interpretaciones pragmáticas o procesos de búsqueda de prueba salvo que se formalicen explícitamente como estructuras y relaciones.

Tensión semántica

Existe tensión entre la satisfacción modelo‑teórica y la consecuencia proof‑teórica: la satisfacción es semántica y conserva referencia, mientras que la demostrabilidad es sintáctica y basada en reglas; la confusión práctica aparece cuando herramientas confunden verificar verdad en un modelo con probar un teorema.

Síntesis

La relación de satisfacción es el predicado semántico definido inductivamente que especifica exactamente cuándo una fórmula se cumple en una estructura bajo una asignación, sirviendo de base para la teoría de modelos y enunciados precisos sobre verdad, consecuencia y equivalencia.