La relation formelle |= (ou ⊧) entre une structure (ou modèle), une affectation de variables (le cas échéant) et une formule, qui est vérifiée exactement lorsque la formule est vraie dans cette structure sous cette affectation selon les règles sémantiques du langage.

Principe

La satisfaction se définit de façon inductive sur la structure des formules : les formules atomiques s'évaluent en appliquant l'interprétation de la structure aux termes et aux relations ; les connecteurs booléens combinent les valeurs de vérité de la manière habituelle ; les quantificateurs quantifient sur les éléments du domaine via la mise à jour des affectations ; les opérateurs modaux et autres utilisent les primitives sémantiques pertinentes (par ex. l'accessibilité pour la sémantique de Kripke).

Démonstration

En logique du premier ordre, pour une structure M et une affectation g, M,g |= ∃x P(x) ssi il existe un élément a du domaine de M tel que M,g[x↦a] |= P(x). En sémantique propositionnelle de Kripke, M,w |= □φ tient si et seulement si pour tout v tel que wRv on a M,v |= φ.

Mauvaise application

Prendre la relation de satisfaction pour synonyme de la démontrabilité syntaxique (confondre |= avec ⊢), ignorer le rôle des affectations pour les variables libres, ou appliquer des clauses de satisfaction d'une logique à une autre sans adapter les primitives sémantiques.

Conséquence

La relation de satisfaction fonde des notions de la théorie des modèles telles que conséquence logique, conséquence, validité, équivalence élémentaire et transfert de propriétés entre structures ; elle constitue le pont formel entre syntaxe et vérité sémantique.

Inversion

La démontrabilité (⊢) est l'inverse : c'est une relation syntaxique entre formules (et éventuellement prémisses) et conclusions au sein d'un système déductif, et non une évaluation dans des modèles et affectations ; les théorèmes de complétude relient les deux mais restent des concepts distincts.

Limite

S'applique uniquement lorsqu'une interprétation sémantique précise est définie (structures, valuations, domaines) ; elle ne couvre pas les notions informelles de vérité, les interprétations pragmatiques ou les processus de recherche de preuve sauf si ceux-ci sont formalisés comme structures et relations.

Tension sémantique

Tension entre la satisfaction modèle‑théorique et la conséquence proof‑théorique : la satisfaction est sémantique et préserve la référence, tandis que la démontrabilité est syntaxique et fondée sur des règles ; la confusion pratique survient quand des outils confondent vérification dans un modèle et démonstration d'un théorème.

Synthèse

La relation de satisfaction est le prédicat sémantique défini par induction qui précise exactement quand une formule est satisfaite dans une structure sous une affectation, servant de fondement à la théorie des modèles et aux énoncés précis sur vérité, conséquence et équivalence.