Propiedad de una fórmula o conjunto de fórmulas que existe al menos una interpretación, modelo o asignación de valores de verdad que hace verdaderas todas las fórmulas del conjunto.

Principio

Una fórmula o teoría es satisfacible si y solo si existe un modelo en el que todas sus oraciones se evalúan como verdaderas según la semántica de la lógica considerada.

Demostración

En lógica proposicional, el conjunto de cláusulas {p ∨ q, ¬p} es satisfacible porque la asignación p = falso, q = verdadero hace verdaderas ambas cláusulas; en lógica de primer orden, una teoría con ∃x P(x) es satisfacible si existe una interpretación con al menos un elemento que satisfaga P.

Aplicación incorrecta

Confundir satisfacibilidad con demostrabilidad sintáctica desde axiomas: un conjunto puede ser consistente desde el punto de vista de la prueba pero insatisfacible en ciertas semánticas no estándar, o satisfacible sin ser derivable en un sistema de prueba restringido.

Consecuencia

Si un conjunto es satisfacible se puede exhibir o razonar sobre al menos un modelo concreto; la satisfacibilidad posibilita métodos basados en modelos como la búsqueda de contraejemplos y la verificación mediante modelos.

Inversión

La negación de la satisfacibilidad es la insatisfacibilidad (no existe modelo); por contraste, la validez no es simplemente la negación de la satisfacibilidad sino una condición de verdad universal en todos los modelos.

Límite

La satisfacibilidad es semántica y depende de la lógica elegida y de sus modelos admisibles; en algunas lógicas no clásicas cambia lo que cuenta como modelo y la existencia de modelos finitos frente a infinitos puede diferir.

Tensión semántica

Satisfacibilidad vs demostrabilidad: la satisfacibilidad trata sobre la existencia de modelos, mientras que la demostrabilidad se ocupa de derivaciones sintácticas — los teoremas de completitud unen ambos pero no eliminan las diferencias prácticas.

Síntesis

La satisfacibilidad identifica cuándo existe al menos una interpretación que hace verdaderas todas las oraciones; es una afirmación semántica que respalda la construcción de modelos, la búsqueda de contraejemplos y muchas técnicas de razonamiento automatizado.