Satisfiabilité
La satisfiabilité et la validité sont des concepts élémentaires de la sémantique. Une formule est satisfiable s'il est possible de trouver une interprétation (modèle) qui la rend vraie. Une formule est valide si toutes les interprétations la rendent vraie.
Les contraires de ces concepts sont l’insatisfaisabilité et l’invalidité, c’est-à-dire qu’une formule est insatisfiable si aucune des interprétations ne rend la formule vraie et invalide si une telle interprétation rend la formule fausse. Ces quatre concepts sont liés les uns aux autres d'une manière exactement analogue à Aristote de la place de l’opposition.
Les quatre concepts peuvent être levés pour s’appliquer à des théories entières : une théorie est satisfiable (valide) si l’une (toutes) des interprétations donne la vérité à chacun des axiomes de la théorie, et une théorie est non satisfaisante (invalide) si toutes les interprétations rendent faux chacun des axiomes de la théorie.
Il est également possible de ne considérer que les interprétations qui rendent vrais tous les axiomes d’une seconde théorie.
Cette généralisation est communément appelée théorie de la satisfiabilité.
La question de savoir si une phrase dans la logique propositionnelle est satisfaisable est un problème décidable. En général, la question de savoir si les phrases de la logique du premier ordre sont satisfaisables n'est pas décisive. En algèbre universelle et en théorie équationnelle, les méthodes de réécriture de termes, de fermeture de congruence et d’unification servent à déterminer la satisfiabilité. Que la théorie articulaire soit décidable ou non dépend de son absence de variable ou d'autres conditions
