Propriété d'une formule ou d'un ensemble de formules pour laquelle aucune interprétation, aucun modèle ou aucune affectation ne rend toutes les formules de l'ensemble vraies ; équivalemment, la classe des modèles est vide.

Principe

Un ensemble est insatisfaisable lorsque les conditions sémantiques de la logique excluent tout monde possible ou structure susceptible de rendre simultanément vraies toutes ses formules.

Démonstration

En logique propositionnelle, l'ensemble {p, ¬p} est insatisfaisable car aucune affectation de vérité ne peut rendre p et ¬p vraies ensemble ; en logique du premier ordre, {∀x P(x), ∃x ¬P(x)} est insatisfaisable en sémantique standard.

Mauvaise application

Qualifier une théorie d'insatisfaisable parce qu'elle ne permet pas de prouver une phrase particulière : l'absence de dérivations n'implique pas nécessairement l'absence de modèles, et des problèmes de décidabilité peuvent masquer l'état de satisfaisabilité.

Conséquence

L'insatisfaisabilité permet la preuve par contradiction : dériver une contradiction explicite montre qu'aucun modèle ne peut satisfaire les prémisses ; elle motive aussi des méthodes de réfutation automatisées comme la détection SAT/UNSAT.

Inversion

Le concept inverse est la satisfaisabilité ; l'insatisfaisabilité correspond sémantiquement à l'impossibilité d'un modèle, tandis que sur le plan syntaxique elle correspond souvent à la dérivabilité d'une contradiction explicite.

Limite

L'insatisfaisabilité dépend de la sémantique et des hypothèses sur le domaine (par exemple modèles finis vs arbitraires) ; les logiques paraconsistantes modifient le lien entre contradiction et insatisfaisabilité.

Tension sémantique

Insatisfaisabilité vs incohérence syntaxique : l'insatisfaisabilité est une notion sémantique (absence de modèle), alors que l'incohérence signifie souvent qu'une contradiction est dérivable selon une relation de conséquence particulière ; elles coïncident dans des systèmes sonores et complets mais divergent sinon.

Synthèse

L'insatisfaisabilité affirme qu'aucune interprétation ne peut rendre toutes les formules vraies ; c'est le signal sémantique d'une contradiction en théorie des modèles et la base des techniques de réfutation et de recherche de contre‑modèles.