Sémantique

2 Sémantique

Comme dans le cas propositionnel, la sémantique de la logique du premier ordre est décrite par une interprétation. Cependant le langage de la logique du premier ordre est plus riche, et de nouvelles définitions sont nécessaires :

Définition 5 [Interprétation] Une interprétation I est un ensemble non vide D_I, appelé le domaine de l'interprétation, muni d'une application I(f) de D_I^m vers D_I pour chaque symbole de fonction f d'arité m, et d'une application I(P) de D_I^m vers B pour chaque symbole de prédicat P d'arité m.

Une affectation r est une application de V vers D_I. Soit A=V® D_I l'ensemble de toutes les affectations.

Intuitivement, une interprétation fournit un ensemble de valeurs D_I que nous décrivons à l'aide des termes, un ensemble d'opérations I(f) sur ces valeurs, et un ensemble de propriétés de base I(P) sur des m-uplets de valeurs.

Contrairement au cas propositionnel, les interprétations et les affectations sont des objets différents : une affectation donne une valeur à chaque variable, alors qu'une interprétation décrit le domaine des valeurs et la sémantique des symboles de fonctions et de prédicats.

Les interprétations nous permettent de définir la sémantique des termes du premier ordre (comme des valeurs dans D_I) et des formules (comme des valeurs de vérité dans B) :

Définition 6 [Sémantique] Pour toute affectation r, soit r[v/x] l'affectation envoyant chaque variable y autre que x vers r(y), et x vers v.

Dans une interprétation I, et modulo l'affectation r, la sémantique des termes et des formules est définie par :

[x]Ir=r(x);
[f(t₁, ..., t_m)]Ir= I(f)([t₁]Ir, ..., [t_m]Ir);
[P(t₁, ..., t_m)]Ir= I(P)([t₁]Ir, ..., [t_m]Ir);
[¬ F]Ir= non [F]Ir;
[FÚ F']Ir= [F]Ir ou [F']Ir;
[FÙ F']Ir= [F]Ir et [F']Ir;
[FÞ F']Ir= [F]Ir imp [F']Ir;
[" x· F]Ir= Ù_{vÎ
D_I}[F]I(r[v/x]);
[$ x· F]Ir= Ú_{vÎ
D_I}[F]I(r[v/x]);

où Ù est la conjonction distribuée et Ú et la disjonction distribuée, et non , et , ou et imp sont les fonctions booléennes usuelles.

Une formule est valide si elle est vraie dans toute interprétation et toute affectation; sinon, elle est invalide. Une formule est insatisfiable is elle est fausse dans toute interprétation et toute affectation; sinon, elle est satisfiable.

Une interprétation dans laquelle une formule F est satisfaite est appelée un modèle de F. Un modèle d'une théorie est un modèle de toutes les formules qu'elle contient. Si F est une formule ou une théorie, nous notons I|= F la relation ``I est un modèle de F.''

La notion de conséquence sémantique, notée aussi |=, lie une théorie (resp. une formule) F à une autre théorie (resp. formule) F' : F|= F' si tout modèle de F est aussi un modèle de F'.