Pour les articles homonymes, voir Interprétation.

Cet article est une ébauche concernant la logique, les mathématiques et l’informatique théorique.

Vous pouvez partager vos connaissances en l’améliorant (comment ?) selon les recommandations des projets correspondants.

Consultez la liste des tâches à accomplir en page de discussion.

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.

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.

Cette section a besoin d'être recyclée (juin 2017).
Une réorganisation et une clarification du contenu sont nécessaires. Améliorez-la ou discutez des points à améliorer.

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.

Cette section traite de la logique classique. Pour d'autres approches, voir par exemple 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 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 ψ).

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

• ¬Φ est Vrai 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.

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

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

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.

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

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.

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ⁿ → 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ⁿ).

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é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 ∀ 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 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], 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.

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 ${\displaystyle {\mathcal {I}}}$ 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).

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

${\displaystyle (\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

${\displaystyle [\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^[1].

Cette section est vide, insuffisamment détaillée ou incomplète. Votre aide est la bienvenue ! Comment faire ?

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.

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

théorie de la démonstration

• 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 du premier ordre)

• Portail de la logique