Recherchez sur tout Techno-Science.net
       
Techno-Science.net : Suivez l'actualité des sciences et des technologies, découvrez, commentez
Catégories
Techniques
Sciences
Encore plus...
Techno-Science.net
Partenaires
Organismes
 CEA
 ESA
Sites Web
Photo Mystérieuse

Que représente
cette image ?
 A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | +
Calcul des prédicats

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 du début du XXe siècle.

Le trait caractéristique de la logique (La logique (du grec logikê, dérivé de logos (λόγος), terme inventé par Xénocrate signifiant à la fois raison, langage, et raisonnement) est dans une première...) du premier ordre est l'introduction d'un ensemble (En théorie des ensembles, un ensemble désigne intuitivement une collection d’objets (les éléments de l'ensemble), « une multitude qui peut être comprise comme un tout »,...) de symboles désignant des variables, d'un ensemble de symboles désignant des fonctions, d'un ensemble de symboles désignant des prédicats, ainsi que des connecteurs logiques et deux symboles \forall et \exists appelés quantificateurs. Cela permet ainsi de formuler des énoncés tels que, " Tout x est P " et " Il existe un x tel que pour tout (Le tout compris comme ensemble de ce qui existe est souvent interprété comme le monde ou l'univers.) y xRy ", en symboles, \forall x (Px) et \exists x \forall y (x R y).

Les formules logiques déduites de ce calcul des prédicats (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...) ont pour but de s'appliquer à n'importe quel modèle, c’est-à-dire n'importe quel ensemble dans lequel les variables, les fonctions, les prédicats du calcul représentent respectivement des éléments de l'ensemble, des fonctions de cet ensemble dans lui-même, et des parties de cet ensemble. Les prédicats représentent des qualités, s’ils sont à une place (unaires), ou des relations n-aires, entre n individus de cet ensemble. Ces notions seront précisées dans la suite de cet article.

Le calcul des propositions (Le calcul des propositions ou calcul propositionnel, dont le fondateur fut le logicien allemand Frege, version moderne de la logique stoïcienne, est une théorie...) est une version réduite du calcul des prédicats, sans les quantificateurs \forall et \exists. Il est très utile notamment en informatique (L´informatique - contraction d´information et automatique - est le domaine d'activité scientifique, technique et industriel en rapport avec le...) mais ne suffit pas pour formaliser tous les raisonnements.

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

Formation d'une formule du calcul des prédicats du premier ordre

Syntaxe

Cette section donne une brève présentation de la grammaire du calcul des prédicats dans un langage formel (Dans de nombreux contextes (scientifique, légal, etc.) l'on désigne par langage formel un mode d'expression plus formalisé et plus précis (les deux n'allant pas nécessairement de pair) que le langage de tous les jours (voir langage...) couramment utilisé en logique classique par la plupart des mathématiciens. Mais le calcul des prédicats n’est pas limité aux théories purement mathématiques (Les mathématiques constituent un domaine de connaissances abstraites construites à l'aide de raisonnements logiques sur des concepts tels que les nombres, les figures, les structures et les transformations. Les...). L’article Prédicat (Les prédicats d’une théorie sont les formules qui contiennent des variables libres.) donne une présentation moins formelle, dans un langage semi-naturel, qui montre plus clairement pourquoi la grammaire des prédicats est universelle.

On se donne un langage L défini par :

  • V un ensemble de symboles appelés variables, toujours infini (Le mot « infini » (-e, -s ; du latin finitus, « limité »), est un adjectif servant à qualifier quelque chose qui n'a pas de limite en nombre ou en taille.).
  • C un ensemble de symboles appelés constantes, éventuellement vide (Le vide est ordinairement défini comme l'absence de matière dans une zone spatiale.).
  • P un ensemble de symboles de prédicats
  • F un ensemble de symboles de fonctions, éventuellement vide.

Chaque symbole de prédicat ou de fonction a une arité (un entier strictement positif) qui détermine le nombre (La notion de nombre en linguistique est traitée à l’article « Nombre grammatical ».) d'arguments ou d'objets auxquels il est appliqué.

  • 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 les connecteurs logiques du 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).

On appellera termes les formules composées ainsi :

  • x, élément de V , est un terme,
  • x, élément de C , est un terme,
  • si f est un symbole de fonction n-aire et t_1,t_2,\dots,t_n sont des termes, alors f(t_1,t_2,\dots,t_n) est un terme.

Un terme est clos s'il ne contient pas de nom de variable (En mathématiques et en logique, une variable est représentée par un symbole. Elle est utilisée pour marquer un rôle dans une formule, un prédicat ou un algorithme. En statistiques, une...).

Les termes ont pour but de représenter les objets sur lesquels vont s'appliquer des prédicats. Appelons T l'ensemble des termes.

Les énoncés ou formules du calcul des prédicats du premier ordre sont les suivants, et uniquement les suivants (appelons E l'ensemble des énoncés) :

  • p(t_1,t_2,\dots,t_n) si (t_1,t_2,\dots,t_n)\in T^n, p\in P et p est n-aire (une telle formule est appelée un atome ou une formule atomique)
  • (e_1\land e_2) si e_1,e_2\in E
  • (e_1\lor e_2) si e_1,e_2\in E
  • (e_1\to e_2) si e_1,e_2\in E
  • \lnot e si e\in E
  • \forall x \; e si e\in E et x\in V
  • \exists x \; e si e\in E et x\in V

Les énoncés ont pour but de représenter des propositions susceptibles d'être vraies ou fausses.

Exemples

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 (Une relation binaire est un concept mathématique qui systématise des notions comme « ... est supérieur ou égal à ... » en arithmétique, ou « ... est élément de l’ensemble ... » en...) =, alors le langage utilisé peut être interprété comme étant celui de la théorie (Le mot théorie vient du mot grec theorein, qui signifie « contempler, observer, examiner ». Dans le langage courant, une théorie est une idée ou une connaissance spéculative,...) 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, variables libres, variables liées

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 (voir Prédicat). Ainsi, \forall x \exists y (x < y) est une formule close du langage de l'arithmétique (L'arithmétique est une branche des mathématiques qui comprend la partie de la théorie des nombres qui utilise des méthodes de la géométrie algébrique et...). \forall x (x < z) est un prédicat portant sur la variable z.

But du calcul des prédicats

Comme le calcul des propositions, le calcul des prédicats se donne pour but de définir quels sont les énoncés qui sont valides et quels sont ceux qui ne le sont pas. Et comme pour le calcul des propositions, il existe deux façons d'aborder cette question, l'aspect sémantique et l'aspect syntaxique. Un théorème (Un théorème est une proposition qui peut être mathématiquement démontrée, c'est-à-dire une assertion qui peut être établie comme vraie au travers d'un raisonnement logique construit...) de complétude (On parle de complétude en mathématiques dans des sens très différents. On dit d'un objet mathématiques qu'il est complet pour exprimer que rien ne peut lui...) montre l'équivalence entre ces deux aspects.

Sémantique du calcul des prédicats du premier ordre

La théorie de la vérité des formules du calcul des prédicats a été appelée par Tarski sa sémantique. Elle est présentée dans l'article Théorie des modèles (La théorie des modèles est une théorie de la vérité mathématique. Elle consiste essentiellement à dire qu’une théorie est mathématiquement valide si on peut définir un univers dans lequel elle est vraie.). Un modèle d'un langage du premier ordre est un ensemble dans lequel on donne un sens (SENS (Strategies for Engineered Negligible Senescence) est un projet scientifique qui a pour but l'extension radicale de l'espérance de vie humaine. Par une...) aux symboles du langage. On peut alors attribuer une valeur de vérité (La notion de valeur de vérité consiste à attribuer aux énoncés des valeurs numériques au travers de fonctions dont il faudra définir les règles de composition : c'est le principe de compositionnalité nécessaire pour calculer les...) (vrai ou faux) aux formules du langage dans ce modèle. On dit qu'une formule F du langage est un théorème si cette formule est vraie dans tout modèle du langage, ce qu'on note \vDash F. Par exemple, si P désigne un prédicat binaire, la formule \exists x \forall y P(x,y) \to \forall y \exists x P(x,y) est un théorème. En effet, tout modèle M sera un ensemble non vide dans lequel le prédicat P sera représenté par un ensemble A de M × M. Les variables x et y se verront affectées comme valeur des éléments de M, et dire que P(x,y) est vrai signifiera que (x,y) est élément de A. Il y a alors deux cas.

Ou bien il existe un élément a de M tel que \{(a,y), y \in M\} \subset A et, dans ce cas, les deux propositions \exists x \forall y \; (x,y) \in A et \forall y \exists x \; (x,y)\in A sont vraies (il suffit de prendre x = a), et l'implication est vraie.
Ou bien un tel a n'existe pas et la proposition \exists x \forall y \; (x,y) \in A est fausse. Mais alors, quelle que soit la valeur de vérité de \forall y \exists x \; (x,y)\in A, l'implication sera vraie.

L'implication étant vraie dans tout modèle, la formule est valide.

Par contre, la formule \forall y \exists x P(x,y) \to \exists x \forall y P(x,y) n'est pas valide. Il suffit pour cela de prendre pour modèle un ensemble à deux éléments {a,b} et de modéliser P par l'égalité. Dans cette structure, la phrase \forall y \exists x \; (x=y) est vraie alors que \exists x \forall y \; (x=y) est fausse. L'implication est donc fausse et la formule est invalide.

Syntaxe du calcul des prédicats

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, et à progresser par étapes logiques jusqu’à une conclusion selon des règles prédéfinies. Il existe plusieurs présentation possible de ces axiomes et de ces règles.

  • La déduction naturelle (La déduction naturelle est une façon d'exposer les principes de la logique du premier ordre pour les rendre aussi proches que possible des façons naturelles de raisonner). 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.
  • 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 consiste en :
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 \forall 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 (La joue est la partie du visage qui recouvre la cavité buccale, fermée par les mâchoires. On appelle aussi joue le muscle qui sert principalement à ouvrir et fermer la bouche et à...) un rôle arbitraire).

Mais si la recherche (La recherche scientifique désigne en premier lieu l’ensemble des actions entreprises en vue de produire et de développer les connaissances scientifiques. Par extension métonymique,...) 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.

  • La logique du dialogue (Le dialogue est une communication entre deux ou plusieurs personnes ou groupes de personnes. Il doit y avoir au minimum un émetteur et un récepteur. Une donnée émise, c'est le message. Un...) apporte également un autre éclairage sur la nature des lois logiques.
  • Voir aussi correspondance (La correspondance est un échange de courrier généralement prolongé sur une longue période. Le terme désigne des échanges de courrier personnels plutôt...) de Curry-Howard.

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 dite prouvable, ce qu'on note \vdash F.

Se pose alors la question suivante : y a-t-il équivalence entre la présentation sémantique et la présentation syntaxique ? \vDash F est-il équivalent à \vdash F ? Autrement dit :

Toute formule prouvable est-elle un théorème ? Si la validité de F est attestée par un calcul syntaxique, F est-elle valide dans tout modèle du langage utilisé ?
Réciproquement, si F est un théorème, valide dans tout modèle, peut-on montrer sa validité à la suite d'un calcul syntaxique ?

C'est à cette question que répond le théorème de complétude qui suit.

Complétude et indécidabilité (En logique mathématique, le terme décidabilité recouvre deux concepts liés : la décidabilité logique et la décidabilité algorithmique.)

Emmanuel Kant croyait à tort que la logique de son temps (Le temps est un concept développé par l'être humain pour appréhender le changement dans le monde.), celle d’Aristote, était une science (La science (latin scientia, « connaissance ») est, d'après le dictionnaire Le Robert, « Ce que l'on sait pour...) complète et définitivement achevée (préface de la seconde ( Seconde est le féminin de l'adjectif second, qui vient immédiatement après le premier ou qui s'ajoute à quelque chose de nature identique. La seconde est une unité de mesure du temps....) édition de la critique de la raison pure, 1787). Les logiciens du dix-neuvième siècle (Un siècle est maintenant une période de cent années. Le mot vient du latin saeculum, i, qui signifiait race, génération. Il a ensuite indiqué la durée d'une génération humaine et faisait 33 ans 4 mois (d'où peut être...) se sont rendus 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 prouvé en 1929 (dans sa thèse (Une thèse (du nom grec thesis, se traduisant par « action de poser ») est l'affirmation ou la prise de position d'un locuteur, à l'égard du sujet ou...) 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 (Dans le langage courant, la mécanique est le domaine des machines, moteurs, véhicules, organes (engrenages, poulies, courroies, vilebrequins, arbres de...) 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. Toute tautologie (propriété vraie dans tout modèle du langage utilisé) est un théorème c'est-à-dire qu'elle peut être déduite d'un calcul, soit au moyen de la déduction naturelle, soit au moyen des axiomes logiques, 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 (De manière générale, le mot objet (du latin objectum, 1361) désigne une entité définie dans un espace à trois dimensions, qui a une fonction précise, et qui...) d’importantes recherches : théorie des modèles, algèbres cylindriques, mécanisation du raisonnement... On notera qu'il existe d'autres théories qui ne sont pas complètes. Ainsi, Gödel a prouvé en 1930 que les théories des ensembles et, plus généralement, toutes les théories mathématiques qui contiennent certaines vérités arithmétiques élémentaires, ne sont pas complètes, au sens où elles ne permettent pas de prouver toutes les vérités qu'elles permettent pourtant d'énoncer (voir théorème d'incomplétude (On parle de complétude en mathématiques dans des sens très différents. On dit d'un objet mathématiques qu'il est complet pour exprimer que rien ne peut lui être ajouté, en un sens qu'il faut préciser dans chaque contexte. Dans le...) de Gödel).

Le calcul des prédicats est semi-décidable, dans le sens où une machine peut dresser, les uns après les autres, la liste des théorèmes (Liste des théorèmes par ordre alphabétique.) de cette logique. Mais, contrairement au calcul des propositions, il n'est pas décidable (En logique mathématique, le terme décidabilité recouvre deux concepts liés : la décidabilité logique et la décidabilité algorithmique.) dans le sens où, si on se donne une formule F, il n'est pas possible de décider si F est un théorème ou non, si on ne dispose pas de sa preuve. En effet, 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, 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. Par contre le calcul des prédicats monadiques (n'ayant que des symboles de propositions unaires et pas de symbole de fonction) est décidable.

Source: Wikipédia publiée sous licence CC-BY-SA 3.0.

Vous pouvez soumettre une modification à cette définition sur cette page. La liste des auteurs de cet article est disponible ici.