Propriété d'une formule ou d'un ensemble de formules selon laquelle il existe au moins une interprétation, un modèle ou une affectation de valeurs de vérité rendant chaque formule de l'ensemble vraie.

Principe

Une formule ou une théorie est satisfaisable si et seulement s'il existe un modèle dans lequel toutes ses phrases s'évaluent à vrai selon la sémantique du logique considérée.

Démonstration

En logique propositionnelle, l'ensemble de clauses {p ∨ q, ¬p} est satisfaisable parce que l'affectation p = faux, q = vrai rend les deux clauses vraies ; en logique du premier ordre, une théorie contenant ∃x P(x) est satisfaisable s'il existe une interprétation où au moins un élément satisfait P.

Mauvaise application

Confondre la démontrabilité syntaxique à partir d'axiomes avec la satisfaisabilité : un ensemble peut être cohérent au sens de la preuve mais insatisfaisable dans certaines sémantiques non standard, ou réciproquement être satisfaisable sans être déductible par un système de preuve restreint.

Conséquence

Si un ensemble est satisfaisable, on peut exhiber ou raisonner sur au moins un modèle concret ; la satisfaisabilité permet des méthodes basées sur les modèles comme la recherche de contre‑exemples et la vérification.

Inversion

La négation de la satisfaisabilité est l'insatisfaisabilité (absence de modèle) ; par contraste, la validité n'est pas simplement la négation de la satisfaisabilité mais une condition de vérité universelle sur tous les modèles.

Limite

La satisfaisabilité est sémantique et dépend de la logique et des modèles admis ; certaines logiques non classiques modifient ce qui compte comme modèle, et l'existence de modèles finis ou infinis peut différer.

Tension sémantique

Satisfaisabilité vs démontrabilité : la satisfaisabilité porte sur l'existence de modèles, tandis que la démontrabilité traite des dérivations syntaxiques — les théorèmes de complétude relient les deux mais n'éliminent pas les différences pratiques.

Synthèse

La satisfaisabilité indique l'existence d'une interprétation rendant toutes les phrases vraies ; c'est une assertion sémantique fondamentale qui soutient la construction de modèles, la recherche de contre‑exemples et de nombreux outils de raisonnement automatisé.