Calcul des prédicats

Un article de Wikipédia, l'encyclopédie libre.
Aller à : navigation, rechercher

Le calcul des prédicats du premier ordre, ou calcul des relations, ou logique du premier ordre, ou tout simplement calcul des prédicats est une formalisation du langage des mathématiques proposée par les logiciens[Qui ?] de la fin du XIXe siècle et du début du XXe siècle. En logique du premier ordre, on peut raisonner sur des énoncés comme « Tout x est gentil » et « Il existe un x tel que pour tout y, x est ami avec y » en symboles :

\forall x ~gentil(x) et \exists x \forall y~ amis(x, y).

Les traits caractéristiques de la logique du premier ordre sont :

  • l'utilisation de variables comme x, y, etc. pour dénoter des éléments d'un ensemble ;
  • l'utilisation de prédicats (ou relations) sur les éléments ;
  • l'utilisation de connecteurs logiques (et, ou, etc.) ;
  • l'utilisation de deux quantificateurs, l'un "universel" (« Quel que soit », « pour tout » noté ) et l'autre "existentiel" (« il existe au moins un … tel que », noté ).

Le calcul des prédicats du premier ordre égalitaire adjoint au calcul des prédicats un symbole de relation, l'égalité, dont l'interprétation est obligée : c'est l'identité des éléments du modèle, et qui est axiomatisée en conséquence. Suivant le contexte, on peut parler simplement de calcul des prédicats pour le calcul des prédicats égalitaire.

On parle de logique du premier ordre par opposition aux logiques d'ordre supérieur, où l'on peut aussi quantifier sur les prédicats ou les fonctions en plus des variables.

Histoire[modifier | modifier le code]

Emmanuel Kant croyait à tort que la logique de son temps, celle d’Aristote, était une science complète et définitivement achevée (préface de la seconde édition de la critique de la raison pure, 1787). Les logiciens du XIXe siècle se sont rendu compte que la théorie d’Aristote ne dit rien ou presque sur la logique des relations. Gottlob Frege et beaucoup d'autres ont comblé cette lacune en définissant le calcul des prédicats au premier ordre.

Kurt Gödel a démontré en 1929 (dans sa thèse de doctorat) que le calcul des prédicats est complet, au sens où on peut donner un nombre fini de principes (axiomes logiques, schémas d'axiomes logiques et règles de déduction) qui suffisent pour déduire de façon mécanique toutes les lois logiques (voir le théorème de complétude de Gödel). Il y a équivalence entre la présentation sémantique et la présentation syntaxique du calcul des prédicats. Tout énoncé universellement valide (c'est-à-dire vrai dans tout modèle du langage utilisé) est un théorème (c'est-à-dire qu'il peut être déduit d'un calcul, un système de règles logiques et d'axiomes, de façon équivalente un système à la Hilbert, la déduction naturelle, ou le calcul des séquents), et réciproquement. La logique du premier ordre est donc achevée au sens où le problème de la correction logique des démonstrations y est résolu. Elle continue cependant à faire l’objet d’importantes recherches : théorie des modèles, théorie de la démonstration, mécanisation du raisonnement

Syntaxe[modifier | modifier le code]

Définition[modifier | modifier le code]

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 : x, y, z, etc.
  • un ensemble de symboles appelés constantes, éventuellement vide : a, b, c, etc.
  • un ensemble de symboles de fonctions ː f, g, h, etc.
  • un ensemble de symboles de prédicats : P, Q, R, etc.

Chaque symbole de prédicat a une arité, le nombre d'arguments ou d'objets auxquels il est appliqué. Par exemple, le prédicat B pour « est bleu(e) » a une arité d'un (on dit qu'il est unaire ou monadique), tandis que le prédicat J pour « joindre » a une arité de deux (on dit qu'il est binaire ou dyadique).

  • les symboles \forall (quel que soit) et \exists (il existe), appelés quantificateurs
  • les symboles \lnot (non), \land (et), \lor (ou) et \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 \forall et de deux connecteurs logiques \lnot et \land en définissant les autres connecteurs et quantificateur à partir de ceux-ci. Par exemple \exists x \; P est défini comme \lnot (\forall x \; \lnot P).

Les formules du calcul des prédicats du premier ordre sont définis par induction ː

  • P(t_1, \dots, t_n) si P un symbole de prédicats d'arité n et t1, ...tn sont des termes (une telle formule est appelée un atome ou une formule atomique)
  • ¬e si e est une formule.
  • (e1e2) si e1 et e2 sont des formules.
  • (e1e2) si e1 et e2 sont des formules.
  • (e1e2) si e1 et e2 sont des formules.
  • \forall x \; e si e est une formule.
  • \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).

Exemples[modifier | modifier le code]

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 est une formule close.

Prédicats, formules closes, formules polies, variables libres, variables liées[modifier | modifier le code]

Lorsqu’une variable x appartient à une sous-formule précédée d’un quantificateur, \forall x ou \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, \exists x (x < y) est identique à \exists z (z < y) mais pas à \exists x (x < z) et encore moins à \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, \forall x \exists y (x < y) est une formule close du langage de l'arithmétique. \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).

Article détaillé : Variable libre.

Sémantique[modifier | modifier le code]

Voici un modèle pour la logique du premier ordre. Le domaine a trois éléments ː un bonhomme de neige, un oiseau et une cerise. Le modèle permet d'interpréter un prédicat binaire aime ː le bonhomme de neige aime l'oiseau, l'oiseau aime tout le monde (y compris lui-même) et la cerise n'aime personne.

La théorie de la vérité des formules du calcul des prédicats a été appelée par Tarski sa sémantique[réf. nécessaire]. Elle est présentée ici et aussi dans l'article Théorie des modèles.

Modèle[modifier | modifier le code]

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. Un modèle donne une valeur de vérité (vrai ou faux) à toute formule close du langage. Par exemple, dans le modèle à droite ː

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

Formule satisfaisable[modifier | modifier le code]

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

Formule valide[modifier | modifier le code]

On dit qu'une formule F du langage est un formule valide si cette formule est vraie dans tout modèle du langage, ce qu'on note \vDash F. Par exemple, la formule \exists x \forall y~ aime(x,y) \to \forall y \exists x~ aime(x,y) est une formule valide. Dans un modèle M, si \exists x \forall y~ aime(x,y) est vraie alors, il existe un élément d dans le domaine qui aime tout le monde. Mais alors tout le monde est aimé et donc la formule \forall y \exists x~ 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 \forall y \exists x~ aime(x,y) \to \exists x \forall y~ aime(x,y) n'est pas valide. En effet, dans un modèle avec deux éléments {a, b} et où aime est interprété par a n'aime que a et b n'aime que b, la formule \forall y \exists x \; ~ aime(x,y) est vraie alors que \exists x \forall y \; ~ aime(x,y) est fausse. L'implication est donc fausse dans le modèle et la formule n'est pas valide.

Système de déduction[modifier | modifier le code]

Dans le calcul des prédicats, on peut également déduire des formules au moyen de déductions relevant d'un calcul. Une déduction consiste à partir d’hypothèses, ou d’axiomes, à progresser par étapes logiques jusqu’à une conclusion selon des règles prédéfinies. Il existe plusieurs présentations possibles de ces axiomes et de ces règles.

  • La déduction naturelle. Les principes logiques y sont présentés d’une façon aussi proche que possible des raisonnements naturels. Elle consiste en une liste de treize règles. Elles pourraient être réduites à un plus petit nombre, mais l'évidence des principes serait moins naturelle.
  • Le calcul des séquents.
  • La résolution.
  • Les axiomes logiques. Plusieurs systèmes d’axiomes équivalents peuvent être proposés. Cette approche, adoptée par presque tous les logiciens depuis les Principia Mathematica de Whitehead et Russell, a une grande importance à la fois métamathématique et historique. L'un des systèmes d'axiomes le plus court est constitué du triplet suivant :
    Les axiomes du calcul des propositions
    f \to (g \to f)
    (f \to (g \to h)) \to ((f \to g) \to (f \to h))
    (\lnot f \to g) \to ((\lnot f \to \lnot g) \to f)
    les axiomes relatifs au quantificateur \forall
    \forall x( f \to g(x)) \to (f \to \forall x g(x))x n'est pas libre dans f
    \forall x f(x) \to f(a)x n'a pas d'occurrence libre dans une partie bien formée de f de la forme \forall a, h (ceci pour éviter une substitution embarrassante si par exemple, f(x) est de la forme \exists a, a < x).
    La règle du modus ponens
    si on a prouvé f \to g et f, alors on a prouvé g
    La règle de généralisation
    si on a prouvé f(x), alors on a prouvé \forall x f(x) (puisque le x de la première preuve joue un rôle arbitraire).

Mais si la recherche de systèmes d'axiomes minimaux met en évidence les principes élémentaires sur lesquels peuvent s'appuyer tous les raisonnements, elle ne montre pas le caractère d’évidence naturelle des principes logiques plus généraux.

Quelle que soit la présentation abordée, les axiomes et règles peuvent être codés de façon à ce qu'une machine puisse vérifier la validité ou non d'une déduction conduisant à une formule F. Si la déduction est correcte, la formule F est appelé théorème. On dit aussi qu'elle est prouvable, ce qu'on note \vdash F.

Propriétés[modifier | modifier le code]

Complétude[modifier | modifier le code]

Le théorème de complétude dit que \vDash F est équivalent à \vdash F, c'est à dire qu'une formule est valide si, et seulement 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.

Indécidabilité[modifier | modifier le code]

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 cette affectation ne peut pas se faire en temps « raisonnable ».
  • 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ème 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).

Compacité[modifier | modifier le code]

Voir théorème de compacité.

Expressivité[modifier | modifier le code]

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

Théorème de Löwenheim-Skolem[modifier | modifier le code]

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

Incomplétude[modifier | modifier le code]

En un sens différent, les théories « raisonnables[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).

Variantes[modifier | modifier le code]

Le calcul des propositions est un fragment syntaxique de la logique du premier ordre où il n'y a pas de variables et où tous les prédicats sont d'arité 0[réf. nécessaire].

La logique modale propositionnelle et la logique de description sont des fragments syntaxiques de la logique du premier ordre[réf. nécessaire]. D'ailleurs, toute formule du premier ordre qui est invariante par bisimilation est équivalente à une formule de la logique modale ː c'est le théorème de Van Benthem[réf. nécessaire]. La logique du premier ordre a aussi été étendu à la logique modale du premier ordre[réf. nécessaire]. La logique de la dépendance[réf. nécessaire] (dependence logic) est une généralisation de la logique du premier ordre où les dépendances entre variables sont explicitement décrites dans le langage.

Notes[modifier | modifier le code]

  1. Récursivement axiomatisables et cohérentes.

Voir également[modifier | modifier le code]

Bibliographie

  • Stephen Kleene, logique mathématique, Armand Colin, 1971 ou Gabay 1987, (ISBN 2-87647-005-5)
  • R. David, K. Nour et C. Raffalli, Introduction à la logique. Théorie de la démonstration. Cours et exercices corrigés, Dunod, 2001, (ISBN 2-10-006796-6)