Satisfaisabilité

Un article de Wikipédia, l'encyclopédie libre.
Aller à : navigation, rechercher

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) qui rend la formule vraie. Une formule est valide si pour toutes les interprétations la formule est vraie. Les concepts opposés sont l'insatisfaisabilité et la non-validité, ainsi, une formule est insatisfaisable si aucune de ses interprétations 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: Une théorie est satisfaisable (valide) si une (toutes) interprétations rend chacun des axiomes de la théorie vraie, et la théorie est insatisfaisable (non-valide) si toutes (une) interprétation rend chacun des axiomes de la théorie fausse.[réf. souhaitée]

La satisfaisabilité dans la théorie des modèles[modifier | modifier le code]

Dans la théories des modèles, une formule atomique est satisfaisable s'il existe des éléments d'une structure qui rende la formule vraie[1]. Si A est une structure, φ une formule, et a une collection d'éléments pris à partir de la structure, qui satisfont φ, alors on note

A ⊧ φ [a]

Si φ n'a pas de variable, alors, si φ est une formule atomique, et qui est satisfaite par A, alors on écrit

A ⊧ φ

Dans ce cas, on peut aussi dire que A est un modèle pour φ, ou que φ est vrai dans A. Si T est un ensemble de formules atomiques (une théorie en somme) satisfaite par A, on écrit

A ⊧ T

Voir aussi[modifier | modifier le code]


Notes et références[modifier | modifier le code]

  1. (en) Wilifrid Hodges, A Shorter Model Theory, Cambridge University,‎ 1997, 12 p. (ISBN 0521587131)