Propiedad de una fórmula o conjunto de fórmulas para la cual ninguna interpretación, modelo o asignación hace verdaderas todas las fórmulas del conjunto; equivalentemente, la clase de modelos es vacía.

Principio

Un conjunto es insatisfacible cuando las condiciones semánticas de la lógica excluyen cualquier mundo posible o estructura que hiciera verdaderas todas sus fórmulas simultáneamente.

Demostración

En lógica proposicional, el conjunto {p, ¬p} es insatisfacible porque ninguna asignación de verdad puede hacer verdaderos a la vez p y ¬p; en lógica de primer orden, {∀x P(x), ∃x ¬P(x)} es insatisfacible en semántica estándar.

Aplicación incorrecta

Afirmar que una teoría es insatisfacible porque carece de pruebas de una oración concreta: la ausencia de derivaciones no implica necesariamente la ausencia de modelos, y problemas de decidibilidad pueden ocultar el estado de satisfacibilidad.

Consecuencia

La insatisfacibilidad permite la prueba por contradicción: derivar una contradicción explícita muestra que ningún modelo puede satisfacer las premisas; también impulsa métodos automáticos de refutación como la detección SAT/UNSAT.

Inversión

El concepto inverso es la satisfacibilidad; la insatisfacibilidad corresponde semánticamente a la imposibilidad de un modelo, mientras que sintácticamente suele corresponder a la derivabilidad de una contradicción explícita.

Límite

La insatisfacibilidad depende de la semántica y de las hipótesis sobre el dominio (por ejemplo, modelos finitos frente a arbitrarios); las lógicas paraconsistentes alteran el vínculo entre contradicción e insatisfacibilidad.

Tensión semántica

Insatisfacibilidad vs inconsistencia sintáctica: la insatisfacibilidad es una noción semántica (ausencia de modelo), mientras que la inconsistencia suele indicar que se deriva una contradicción bajo una relación de consecuencia particular; coinciden en sistemas sónicos y completos pero divergen en otros.

Síntesis

La insatisfacibilidad declara que no existe interpretación que haga verdaderas todas las fórmulas; es la señal semántica de una contradicción en sentido modelístico y sustenta la refutación y el razonamiento mediante contra‑modelos.