Voir la source de Interprétation (logique)

{{homonyme|Interprétation}}
{{ébauche| logique| mathématique|informatique théorique| date=2 juin 2017}}
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 [[Syntaxe|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 (logique)|sémantique formelle]].

== Introduction ==
Pour plus de commodité, nous allons nous restreindre aux logiques formelles les plus souvent étudiées, à savoir, la [[Calcul des propositions|logique propositionnelle]], la [[Calcul des prédicats|logique des prédicats]] et la [[logique modale]]. Une ''interprétation'' est une [[Fonction (mathématiques)|fonction]] qui a pour domaine un langage formel et pour cible un modèle.

Si le modèle contient les [[booléen]]s, une interprétation [[logique classique|classique]] affecte à chaque {{page h'|Proposition|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 (logique mathématique)|structure]] de la proposition.

== Langages formels ==
{{section à recycler|date=juin 2017}}
Un langage formel est une collection de ''propositions'' (aussi appelés'' [[Formule logique|formules]]''), composé à partir d'un ensemble de ''lettres'' ou de ''symboles''. Cet ensemble de lettres est appelé l'''{{Lien |langue=en |trad=Alphabet (formal languages)|fr=Alphabet (langages formels)| texte=alphabet}}''. 

La [[logique propositionnelle]] est un langage formel dont l'alphabet est divisé en deux ensembles : les [[connecteur]]s 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#Sémantique de la logique intuitionniste|Logique intuitionniste]].''

Une ''valuation'' associe à chaque proposition une valeur de vérité qui soit ''Vrai'', soit ''Faux''. Les propositions qui sont vraies pour une valuation sont dites ''[[Satisfaisabilité|satisfaite]]'' par cette valuation.

Une proposition n'est ''[[Cohérence (logique)|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 ''[[Déduction logique|conséquence logique]]'' de ψ).

=== Connecteurs logiques ===

Les connecteurs de la logique propositionnelle classique sont interprétés comme suit :
* ¬Φ est Vrai [[Équivalence logique|si et seulement si]] Φ est Faux.
* (Φ ∧ Ψ) est Vrai si et seulement si Φ est Vrai et Ψ est Vrai.
* (Φ ∨ Ψ) est Vrai si et seulement si Φ est Vrai ou Ψ est Vrai (ou les deux).
* (Φ → Ψ) est Vrai si et seulement si Φ est Faux ou Ψ est Vrai (ou les deux).
* (Φ ↔ Ψ) est Vrai si et seulement si (Φ → Ψ) est Vrai et (Ψ → Φ) est Vrai.
Donc, en vertu d'une interprétation donnée de toutes les variables propositionnelles des propositions Φ 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.
{| class="wikitable" style="text-align:center; margin: 1em auto;"
|+ 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 [[Calcul des propositions|logique propositionnelle]] se compose de formules construites à partir de symboles propositionnels et de connecteurs logiques.
=== Interprétation classique ===
L'interprétation [[logique classique|classique]] de la logique propositionnelle se fait à partir de fonctions (les valuations) qui associent, à chaque symbole propositionnel, l'une des [[Valeur de vérité|valeurs de vérité]] ''vrai'' ou ''faux''. 

Pour un langage avec ''n'' variables propositionnelles distinctes, il y a 2<sup>''n''</sup> valuations classiques possibles distinctes. Pour toute variable ''a'', par exemple, il y a 2<sup>1</sup>=2 valuations possibles : 1) ''a'' est affecté ''vrai'', ou 2) ''a'' est affecté ''faux''. Pour la paire ''a'', ''b'' il y a 2<sup>2</sup>=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 [[logique intuitionniste|intuitionniste]] se fait par les [[Sémantique de Kripke|modèles de Kripke]].

== Logique classique du premier ordre ==
Chaque langage de premier ordre est défini par une [[Signature (logique)|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 de constante, 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<sup>n</sup>'' → ''D'').
* Pour chaque symbole de relation ''n''-aire, une relation ''n''-aire sur D en tant que son interprétation (qui est un sous-ensemble de ''D<sup>n</sup>'').
Un objet portant cette information est connu comme une [[Structure (logique mathématique)|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 [[Variable libre|variables libres]]. La valeur de vérité d'une proposition arbitraire est alors définie par [[induction (logique)|induction]] à l'aide du schéma-T, qui est une définition des sémantiques du premier ordre développée 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 {{nobr|∀ ''x'' φ(''x'')}} et {{nobr|∃ ''x'' φ(''x'')}}. L'idée est que la proposition {{nobr|∀ ''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 {{nobr|∃ ''x'' φ(''x'')}} est satisfaite s'il existe au moins un élément ''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'{{Pas clair|date=juin 2022}}, 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 intentionnelles.

=== Exemple d'une interprétation classique de premier ordre ===
Considérons un langage '''L''' dont la signature contient uniquement trois symboles de constante a, b et c, quatre symboles de prédicats unaires F, G, H et I, un symbole de prédicat binaire J, et trois variables x, y et z.

Un exemple d'interprétation <math>\mathcal{I}</math> de ce langage '''L''' 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 [[Domaine du discours|univers du discours]]. La raison de cette exigence est de garantir que les équivalences telles que
:: <math>(\phi \lor \exists x \psi) \leftrightarrow \exists x (\phi \lor \psi)</math>,
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
: <math>[\forall y (y = y) \lor \exists x ( x = x)] \equiv \exists x [ \forall y ( y = y) \lor x = x]</math>
é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<ref>Mates, Benson (1972), Elementary Logic, Second Edition, New York: [[Oxford University Press]], p. 56, {{ISBN|0-19-501491-X}}</ref>.

== Logique d'ordre supérieur ==
{{Section vide ou incomplète}}

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 du discours|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 formel|Système logique]]
* [[Théorème de Löwenheim-Skolem]]
* [[Logique modale]]
* [[Théorie des modèles]]
* [[Satisfaisabilité]]
* [[Vérité]]

== Références ==
<references />théorie de la démonstration

== Liens externes ==
* [http://mathworld.wolfram.com/FormalLanguage.html mathworld.wolfram.com: FormalLanguage] (langage formel)
* [http://mathworld.wolfram.com/Connective.html mathworld.wolfram.com: Connective] (connecteur logique)
* [http://mathworld.wolfram.com/Interpretation.html mathworld.wolfram.com: Interpretation] (interprétation)
* [http://mathworld.wolfram.com/PropositionalCalculus.html mathworld.wolfram.com: Propositional Calculus] (calcul des propositions)
* [http://mathworld.wolfram.com/First-OrderLogic.html mathworld.wolfram.com: First Order Logic] (logique du premier ordre)

{{Portail|logique}}

[[Catégorie:Langage formel]]
[[Catégorie:Théorie des modèles]]
[[Catégorie:Philosophie du langage]]
[[Catégorie:Philosophie de l'esprit]]
[[Catégorie:Sémantique]]
[[Catégorie:Syntaxe]]