Satisfaisabilité
En logique mathématique, la satisfaisabilité ou satisfiabilité et la validité sont des concepts élémentaires de sémantique. Une formule est satisfaisable s'il est possible de trouver une interprétation (modèle), une façon d'interpréter tous les éléments constitutifs de la formule, qui rend la formule vraie. Une formule est universellement valide, ou en raccourci valide si, pour toutes les interprétations, la formule est vraie. Les concepts opposés sont la non satisfaisabilité ou insatisfaisabilité et la non-validité : une formule est insatisfaisable si aucune de ses interprétations ne rend la formule vraie et non valide s'il existe une interprétation qui rend la formule fausse.
Les quatre concepts peuvent être appliqués aux théories. Ainsi une théorie est satisfaisable s'il existe une interprétation qui rend chacun des axiomes de la théorie vrai, non satisfaisable si toute interprétation rend l'un des axiomes faux.
La satisfaisabilité en théorie des modèles
En théorie des modèles (de la logique du premier ordre), une formule écrite dans un certain langage, défini par une signature, s'interprète dans une structure sur cette même signature. Une formule peut contenir des variables libres. On dit alors qu'une formule est satisfaisable dans une structure s'il existe des éléments de l'ensemble de base de cette structure qui, substitués à ses variables libres, rendent la formule vraie. Une formule est satisfaisable quand elle est satisfaisable dans une certaine structure.
Si A est une structure, φ une formule, et a une collection d'éléments de l'ensemble de base de cette structure, qui satisfont φ, alors on note
- A ⊧ φ [a].
Si φ est une formule close satisfaite par A, c'est-à -dire qu'elle n'a pas de variable libre, alors on écrit simplement :
- A ⊧ φ[1].
Dans ce cas, on peut aussi dire que A est un modèle pour φ, ou que φ est vraie dans A. Si T est un ensemble de formules (une théorie en somme) satisfaite par A, on écrit
- A ⊧ T.
La définition formelle de la satisfaction d'une formule dans une structure, pour une certaine interprétation des variables libres dans cette formule, procède récursivement à partir de la définition de la satisfaction des formules atomiques.
Notes et références
- (en) Wilfrid Hodges, A Shorter Model Theory, Cambridge, Cambridge University, , 310 p. (ISBN 0-521-58713-1, lire en ligne), p. 12,24.
Bibliographie
- René Cori et Daniel Lascar, Logique mathématique I. Calcul propositionnel, algèbres de Boole, calcul des prédicats [détail des éditions] (chapitre 1 : Calcul propositionnel, chapitre 3: Calcul des prédicats)