Calcul des prédicats

Exemple d'une formule de la logique du premier ordre. Le schéma montre les quantificateurs, les occurrences des symboles de fonctions et des symboles de prédicats.

Cette section donne une brève présentation de la syntaxe du langage formel du calcul des prédicats.

On se donne pour alphabet :

• un ensemble de symboles appelés variables, toujours infini : ${\displaystyle x}$, ${\displaystyle y}$, ${\displaystyle z}$, etc. ;
• un ensemble de symboles appelés constantes, éventuellement vide : ${\displaystyle a}$, ${\displaystyle b}$, ${\displaystyle c}$, etc. ;
• un ensemble de symboles de fonctions : ${\displaystyle f}$, ${\displaystyle g}$, ${\displaystyle h}$, etc. ;
• un ensemble de symboles de prédicats : ${\displaystyle P}$, ${\displaystyle Q}$, ${\displaystyle R}$, etc.

Chaque symbole de fonction et chaque symbole de prédicat a une arité : il s'agit du nombre d'arguments ou d'objets auxquels il est appliqué. Par exemple, le prédicat ${\displaystyle B}$ pour « est bleu(e) » a une arité égale à 1 (on dit qu'il est unaire ou monadique), tandis que le prédicat ${\displaystyle amis}$ pour « être amis » a une arité de deux (on dit qu'il est binaire ou dyadique).

• Les symboles ${\displaystyle \forall }$ (quel que soit) et ${\displaystyle \exists }$ (il existe), appelés quantificateurs.
• Les symboles ${\displaystyle \lnot }$ (non), ${\displaystyle \land }$ (et), ${\displaystyle \lor }$ (ou) et ${\displaystyle \to }$ (implique), qui sont des connecteurs que possède aussi le calcul des propositions.
• Les symboles de ponctuation « ) » et « ( ».

On pourrait se contenter d'un seul quantificateur ${\displaystyle \forall }$ et de deux connecteurs logiques ${\displaystyle \lnot }$ et ${\displaystyle \land }$ en définissant les autres connecteurs et quantificateur à partir de ceux-ci. Par exemple ${\displaystyle \exists x\;P(x)}$ est défini comme ${\displaystyle \lnot (\forall x\;\lnot P(x))}$.

Les formules du calcul des prédicats du premier ordre sont définies par induction :

• ${\displaystyle P(t_{1},\dots ,t_{n})}$ si ${\displaystyle P}$ un symbole de prédicat d'arité n et t₁, …, t_n sont des termes (une telle formule est appelée un atome ou une formule atomique) ;
• ¬e si e est une formule ;
• (e₁∧e₂) si e₁ et e₂ sont des formules ;
• (e₁∨e₂) si e₁ et e₂ sont des formules ;
• (e₁→e₂) si e₁ et e₂ sont des formules ;
• ${\displaystyle \forall x\;e}$ si e est une formule ;
• ${\displaystyle \exists x\;e}$ si e est une formule.

On appelle énoncé une formule dont toutes les variables sont liées par un quantificateur (donc qui n'a pas de variable libre).

Exemple 1

Si on se donne pour constantes les deux symboles 0 et 1, pour symboles de fonctions binaires + et ., et pour symboles de prédicats binaires les symboles = et <, alors le langage utilisé peut être interprété comme étant celui de l'arithmétique. x et y désignant des variables, x+1 est un terme, 0+1+1 est un terme clos, x<y+1 est une formule, 0+1+1<0+1+1+1 est une formule close.

Exemple 2

Si on se donne un ensemble de variables quelconque, une constante notée e, un symbole de fonction binaire noté *, un symbole de fonction unaire notée ^-1, un symbole de relation binaire =, alors le langage utilisé peut être interprété comme étant celui de la théorie des groupes. Si x et y désignent des variables, x*y est un terme, e*e est un terme clos, x=y*y est une formule, e=e*e^-1 et (e^-1 * e)^-1 = (e^-1)^-1 sont des formules closes.

Lorsqu’une variable ${\displaystyle x}$ appartient à une sous-formule précédée d’un quantificateur, ${\displaystyle \forall x}$ ou ${\displaystyle \exists x}$, elle est dite liée par ce quantificateur. Si une variable n’est liée par aucun quantificateur, elle est libre.

La distinction entre variable libre et variable liée est importante. Une variable liée ne possède pas d'identité propre et peut être remplacée par n'importe quel autre nom de variable qui n'apparaît pas dans la formule. Ainsi, ${\displaystyle \exists x(x<y)}$ est identique à ${\displaystyle \exists z(z<y)}$ mais pas à ${\displaystyle \exists x(x<z)}$ et encore moins à ${\displaystyle \exists y(y<y)}$.

Une formule close est une formule dont toutes les variables sont liées. Un prédicat est une formule qui contient une ou plusieurs variables libres. On peut considérer les prédicats comme des concepts. Ainsi, ${\displaystyle \forall x\exists y(x<y)}$ est une formule close du langage de l'arithmétique. ${\displaystyle \forall x(x<z)}$ est un prédicat portant sur la variable z.

Une formule est dite polie lorsque d'une part aucune variable n'y a à la fois d'occurrences libres et d'occurrences liées et que d'autre part aucune variable liée n'est soumise à plus d'une mutification (on dit qu'un signe est mutificateur lorsqu'il permet de confirmer l'hypothèse d'une variable liée)..

Un modèle M d'un langage du premier ordre est une structure : c'est un ensemble d'éléments (appelé domaine) dans lequel on donne un sens aux symboles du langage. Généralement, si le langage possède un prédicat binaire pour le symbole d'égalité =, alors son interprétation dans la structure est l'égalité.

Un modèle donne une valeur de vérité (vrai ou faux) à toute formule close du langage. Les conditions de vérité sont définis par induction structurelle sur les formules. Par exemple, dans le modèle ci-contre :

• ${\displaystyle \exists x\forall y~\mathrm {aime} (x,y)}$ est vraie dans le modèle M car il existe un élément (l'oiseau) qui aime tout le monde ;
• ${\displaystyle \exists x\forall y~\lnot \mathrm {aime} (x,y)}$ est vraie dans le modèle M car il existe un élément (la cerise) qui n'aime personne.

Une formule est satisfaisable s'il existe un modèle M qui la rend vraie. Par exemple ${\displaystyle \exists x\forall y~\mathrm {aime} (x,y)}$ est satisfaisable.

On dit qu'une formule F du langage est une formule valide si cette formule est vraie dans tout modèle du langage, ce qu'on note ${\displaystyle \vDash F}$. Par exemple, la formule ${\displaystyle \exists x\forall y~\mathrm {aime} (x,y)\to \forall y\exists x~\mathrm {aime} (x,y)}$ est une formule valide. Dans un modèle M, si ${\displaystyle \exists x\forall y~\mathrm {aime} (x,y)}$ est vraie alors, il existe un élément ${\displaystyle x}$ dans le domaine qui aime tout le monde. Mais alors tout le monde est aimé et donc la formule ${\displaystyle \forall y\exists x~\mathrm {aime} (x,y)}$ est vraie dans le modèle M. L'implication étant vraie dans tout modèle M, la formule est valide.

Par contre, la formule ${\displaystyle \forall y\exists x~\mathrm {aime} (x,y)\to \exists x\forall y~\mathrm {aime} (x,y)}$ n'est pas valide. En effet, dans un modèle avec deux éléments {a, b} et où ${\displaystyle \mathrm {aime} }$ est interprété par a n'aime que a et b n'aime que b, la formule ${\displaystyle \forall y\exists x\;~\mathrm {aime} (x,y)}$ est vraie alors que ${\displaystyle \exists x\forall y\;~\mathrm {aime} (x,y)}$ est fausse. L'implication est donc fausse dans le modèle et la formule n'est pas valide.

On dit que F est conséquence sémantique d'une théorie T si, tout modèle qui satisfait toutes les formules de T satisfait aussi F.

Le théorème de complétude dit que F est valide est équivalent à F est prouvable. Mieux, on parle de complétude forte : si F est conséquence sémantique d'une théorie T alors F est prouvable à partir de T.

Tous les systèmes logiques ne sont pas décidables, autrement dit bien qu'ils soient parfaitement définis, il n'existe pas toujours un algorithme pour dire si une formule est oui ou non un théorème. D'ailleurs historiquement la théorie de la calculabilité s'est construite pour démontrer précisément leur indécidabilité. Avant de développer ces résultats, voici résumé ce qu'on sait sur la décidabilité et l'indécidabilité des systèmes logiques.

• Calcul propositionnel : décidable et complet. Pour la décidabilité, il y a donc une procédure effective pour décider si une formule du calcul propositionnel est satisfaisable, c'est-à-dire que l'on peut affecter aux variables propositionnelles des valeurs de vérité qui la rende vraie, mais le problème, nommé problème SAT, est NP-complet, c'est-à-dire que tous les algorithmes déterministes connus de recherche d'une solution sont en temps exponentiel par rapport au nombre de variables (voir l'article Problème SAT).
• Calcul des prédicats du premier ordre monadique, c'est-à-dire réduit aux relations unaires et sans fonctions : décidable et complet, par réduction au calcul propositionnel.
• Calcul des prédicats du premier ordre : réductible au calcul des prédicats dyadique, soit avec au plus des prédicats binaires (comme il en est en théorie des ensembles n'ayant que l'appartenance et l'égalité comme symboles primitifs) : semi-décidable et complet.
• Calcul des prédicats de deuxième ordre : [quid sur sa décidabilité], et théorème de complétude partiel sur une sous-classe de formules^{[réf. souhaitée]}.
• Calcul des prédicats d'ordre supérieur :

Le calcul des prédicats est semi-décidable, dans le sens où une machine peut énumérer les théorèmes les uns après les autres. Mais, contrairement au calcul des propositions, il n'est pas en général décidable dans le sens où il n'existe pas de moyen « mécanique » qui, si on se donne une formule F, permette de décider si F est un théorème ou non. La semi-décidabilité ne permet pas de conclure : la confrontation de F avec la liste des théorèmes se terminera si F est effectivement un théorème, mais dans l'attente de la terminaison, a priori on ne sait pas si le calcul des théorèmes n'a pas été mené assez loin pour identifier F comme théorème ou si ce calcul ne se terminera pas parce que F n'est pas un théorème.

Cela dépend cependant du langage utilisé, en particulier du choix des symboles primitifs (la signature). Le calcul des prédicats égalitaire monadique (n'ayant que des symboles de prédicats unaires et pas de symbole de fonction) est décidable. Le calcul des prédicats égalitaire pour un langage comportant au moins un symbole de prédicat binaire est indécidable (algorithmiquement).

Des fragments syntaxiques sont décidables comme la logique monadique du premier ordre ou la classe de Bernays-Schönfinkel.

Voir théorème de compacité.

Une application intéressante du théorème de compacité est qu'il n'existe pas de formules qui exprime « le domaine est infini ».

Voir théorème de Löwenheim-Skolem.

En un sens différent, les théories « raisonnables »[note 1] qui permettent de formaliser suffisamment l'arithmétique intuitive, comme l'arithmétique de Peano, ou la théorie des ensembles ne sont pas complètes : il existe un énoncé non démontrable dont la négation est également non démontrable (voir théorème d'incomplétude de Gödel).

• Calcul des propositions
• Théorie des modèles
• Skolémisation
• Langage formel mathématique
• Théorème de Lindström
• Langage informatique Prolog
• Déduction naturelle
• Signature (logique)
• Structure (logique mathématique)
• Théorème d'interpolation de Craig
• Théorème de Trakhtenbrot