Interprétation (logique)

En logique, une interprétation est une attribution de sens aux symboles d'un langage formel. Les langages formels utilisés en mathématiques, en logique et en informatique théorique ne sont définis dans un premier temps que syntaxiquement; pour en donner une définition complète, il faut expliquer comment ils fonctionnent et en donner une interprétation. Le domaine de la logique qui donne une interprétation aux langages formels s'appelle la sémantique formelle.

Introduction

Pour plus de commodité, nous allons nous restreindre aux logiques formelles les plus souvent étudiées, à savoir, la logique propositionnelle, la logique des prédicats et la logique modale. Une interprétation est une fonction qui a pour domaine un langage formel et pour cible un modèle.

Si le modèle contient les booléens, une interprétation classique affecte à chaque proposition une valeur de vérité. Si pour une interprétation donnée, la fonction affecte la valeur vrai à une proposition, l'interprétation est appelée la structure de la proposition.

Langages formels

Un langage formel est une collection de propositions (aussi appelés formules), composé à partir d'un ensemble de lettres ou de symboles. Cet ensemble de lettres est appelé l'alphabet (en). 

La logique propositionnelle est un langage formel dont l'alphabet est divisé en deux ensembles : les connecteurs et les variables propositionnelles.

Propriétés générales des interprétations de la logique classique

Cette section traite de la logique classique. Pour d'autres approches, voir par exemple Logique intuitionniste.

De nombreuses interprétations couramment étudiées associent chaque proposition dans un langage formel avec une seule valeur de vérité, soit Vrai ou Faux. Les propositions qui sont vraies pour un valuation sont dites satisfaite par cette valuation.

Une proposition n'est cohérente que si elle est vraie dans au moins une interprétation ; sinon, elle est incohérente. Une proposition φ est dite être logiquement valide si elle est satisfaite par toutes les interprétations (si φ est satisfaite par toute interprétation qui satisfait ψ alors φ est dit être une conséquence logique de ψ).

Connecteurs logiques

Les connecteurs de la logique propositionnelle classique sont interprétés comme suit :

• ¬Φ est Vrai ssi Φ est Faux.
• (Φ ∧ Ψ) est Vrai ssi Φ est Vrai et Ψ est Vrai.
• (Φ ∨ Ψ) est Vrai ssi Φ est Vrai ou Ψ est Vrai (ou les deux).
• (Φ → Ψ) est Vrai ssi Φ est Vrai ou Ψ est Vrai (ou les deux).^{[Information douteuse]}
• (Φ ↔ Ψ) est Vrai ssi (Φ → Ψ) est Vrai et (Ψ → Φ) est Vrai.

Donc, en vertu d'une interprétation donnée de toutes les variables propositionnelles de la proposition Φ et Ψ, nous pouvons déterminer les valeurs de vérité de toutes les formules. Le tableau suivant montre à quoi ce genre de chose ressemble. Les deux premières colonnes montrent les valeurs de vérité des lettres. Les autres colonnes montrent les valeurs de vérité des formules construites à partir de ces lettres.

Connecteurs logiques

Interprétation	Φ	Ψ	¬Φ	(Φ ∧ Ψ)	(Φ ∨ Ψ)	(Φ → Ψ)	(Φ ↔ Ψ)
#1	V	V	F	V	V	V	V
#2	V	F	F	F	V	F	F
#3	F	V	V	F	V	V	F
#4	F	F	V	F	F	V	V

Maintenant, il est plus facile de voir ce qui rend une formule logique valide.

Interprétations pour la logique propositionnelle

Le langage formel de la logique propositionnelle se compose de formules construites à partir de symboles propositionnels et de connecteurs logiques.

Interprétation classique

L'interprétation classique de la logique propositionnelle se fait à partir de fonctions (les valuations) qui associent, à chaque symbole propositionnel, l'une des valeurs de vérité vrai ou faux. 

Pour un langage avec n variables propositionnelles distinctes, il y a 2ⁿ valuations classiques possibles distinctes. Pour toute variable a, par exemple, il y a 2¹=2 valuations possibles: 1) a est affecté vrai, ou 2) a est affecté faux. Pour la paire a, b il y a 2²=4 valuations possibles: 1) les deux sont affectés vrai, 2) les deux sont affectés faux, 3) a est affecté vrai et b est affecté faux, ou 4) a est affecté faux et b est affecté vrai.

Interprétation intuitionniste

Une interprétation intuitionniste se fait par les modèles de Kripke.

Logique classique du premier ordre

Chaque langage de premier ordre est défini par une signature. Dans le cas des symboles fonctionnels et prédicats, une arité est également attribuée. L'alphabet du langage formel se compose de constantes logiques, du symbole de relation de l'égalité =, de tous les symboles de la signature et d'un ensemble infini de symboles connus comme des variables.

Interprétations classiques d'un langage du premier ordre

Pour attribuer un sens à toutes les propositions du langage du premier ordre, les informations suivantes sont nécessaires :

• Un univers du discours D.
• Pour chaque symbole, un élément de D en tant qu'interprétation.
• Pour chaque symbole de fonction n-aire, une fonction n-aire de D à D en tant que son interprétation (qui est une fonction Dⁿ → D).
• Pour chaque symbole n-aire, une relation n-aire sur D en tant que son interprétation (qui est un sous-ensemble de Dⁿ).

Un objet portant cette information est connu comme une structure (de la signature σ, ou la structure-σ, ou comme un "modèle").

Les informations spécifiées dans l'interprétation fournissent suffisamment d'informations pour donner une valeur de vérité à toute formule atomique, après chacune de ses variables libres. La valeur de vérité d'une proposition arbitraire est alors définie par induction à l'aide du schéma-T, qui est une définition des sémantiques du premier ordre développées par Alfred Tarski. Le schéma-T interprète les connecteurs logiques à l'aide d'une table de vérité. Ainsi, par exemple, φ & ψ est satisfait si et seulement si φ et ψ sont satisfaits.

Reste encore la question de savoir comment interpréter les formules de la forme ∀ x φ(x) et ∃ x φ(x). L'idée est que la proposition ∀ x φ(x) est vraie en vertu d'une interprétation lorsque chaque substitution de φ(x), où x est remplacé par un élément du domaine, est satisfaite. La formule ∃ x φ(x) est satisfaite s'il existe au moins un élément de d du domaine tel que φ(d) est satisfaite.

Certains auteurs admettent aussi des variables propositionnelles dans la logique du premier ordre, qui doivent alors aussi être interprétées. Une variable propositionnelle peut se 'tenir debout', comme une formule atomique. L'interprétation d'une variable propositionnelle est l'une des deux valeurs de vérité vrai et faux.

Parce que les interprétations de premier ordre décrites ici sont définies dans la théorie des ensembles, elles n'associent pas chaque symbole de prédicat avec une propriété (ou une relation), mais plutôt avec l'extension de cette propriété (ou relation). En d'autres termes, ces interprétations de premier ordre sont extensionnelles, et non intensionnelles.

Exemple d'une interprétation classique de premier ordre

Un exemple d'interprétation ${\mathcal {I}}$ du langage L décrit ci-dessus est comme suit.

• Domaine : Un jeu d'échecs
• Constantes individuelles : a: Le Roi blanc, b: La Reine noire, c: Le pion du Roi blanc
• F(x) : x est une pièce
• G(x) : x est un pion
• H(x) : x est noir
• I(x) : x est blanc
• J(x, y) : x peut prendre y

• les données suivantes sont vraies : F(a), G(c), H(b), I(a) J(b, c),
• les suivantes sont fausses : J(a, c), G(a).

Univers non-vide

Comme indiqué plus haut, une interprétation de premier ordre est généralement nécessaire pour spécifier un ensemble non-vide comme univers du discours. La raison de cette exigence est de garantir que les équivalences telles que

$(\phi \lor \exists x\psi )\leftrightarrow \exists x(\phi \lor \psi )$,

où x n'est pas une variable libre de φ, sont logiquement valides. Cette équivalence tient dans toutes les interprétations avec un univers non-vide, mais ne tient pas toujours lorsque les univers vides sont autorisés. Par exemple, l'équivalence

$[\forall y(y=y)\lor \exists x(x=x)]\equiv \exists x[\forall y(y=y)\lor x=x]$

échoue dans une structure avec un univers vide. Ainsi, la théorie de la démonstration de la logique du premier ordre devient plus compliquée lorsque les structures vides sont autorisées.

Logique d'ordre supérieur

Un langage formel pour la logique d'ordre supérieur ressemble beaucoup au langage formel dédié à la logique du premier ordre. La différence est qu'il y a beaucoup de variables de types différents. Certaines variables correspondent à des éléments de l'univers, comme dans la logique du premier ordre. D'autres variables correspondent à des objets de type supérieur: sous-ensembles de l'univers, fonctions de l'univers, fonctions prenant un sous-ensemble de l'univers et renvoyant une fonction à partir de l'univers des sous-ensembles de l'univers, etc. Tous ces types de variables peuvent être quantifiés.

Voir aussi

• Variable libre
• Système logique
• Théorème de Löwenheim-Skolem
• Logique modale
• Théorie des modèles
• Satisfiasabilité
• Vérité

Références

théorie de la démonstration

Liens externes

• mathworld.wolfram.com: FormalLanguage (langage formel)
• mathworld.wolfram.com: Connective (connecteur logique)
• mathworld.wolfram.com: Interpretation (interprétation)
• mathworld.wolfram.com: Propositional Calculus (Calcul des propositions)
• mathworld.wolfram.com: First Order Logic (Logique de première ordre)