Calcul des prédicats

Le trait caractéristique de la logique du premier ordre est l'introduction d'un ensemble de symboles appelés variables d’objet, d'un autre ensemble de symboles représentant des prédicats fondamentaux, ainsi que de deux symboles \forall et \exists appelés quantificateurs, permettant ainsi de formuler des énoncés tels que, «Tout X est P» et «Il existe un x tel que pour tout y xRy», en symboles, \forall x (Px) et \exists x \forall y (x R y) .

Ici les variables représentent des valeurs d'un certain ensemble d'objets de base donné (par exemple, les entiers naturels). On appelle cet ensemble le domaine de quantification, ou d’existence, ou l’univers de la théorie. Les quantifications des variables se rapportent uniquement à 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. est une version réduite du calcul des prédicats, sans les quantificateurs (pour tout x) et (il existe un x). Il est très utile notamment en informatique 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 objets de l'ensemble de base que des prédicats ou des fonctions sur l'ensemble de base.

Sommaire

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

Cette section donne une brève présentation de la grammaire du calcul des prédicats dans un langage formel couramment utilisé par les mathématiciens. Mais le calcul des prédicats n’est pas limité aux théories purment mathématiques. L’article Prédicat 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 :

Chaque symbole de prédicat ou de fonction a une arité (un entier strictement positif), qui détermine le nombre d'arguments, ou d'objets auxquels il est appliqué.

On pourrait se contenter d'un seul quantificateur \forall et de deux connecteurs logiques \neg et \wedge sans perdre en expressivité.

On appellera termes les formules composées ainsi :

Appelons T l'ensemble des termes.

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

Ce système très formel peut s'instancier, par exemple en l'arithmétique en prenant pour constantes (les fonctions 0-aires) les nombres (entiers par exemple) pour fonctions binaires les symboles des opérations « + » et « . » et comme prédicats binaires, les symboles « = » et « < ».

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.

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). Il n’y a pas de sens à dire qu’une formule qui contient des variables libres est vraie ou fausse. Il faut substituer des constantes à toutes les variables libres pour obtenir une formule susceptible d’être vraie ou fausse.

Une formule close est une formule dont toutes les variables sont liées.

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, parce qu'elle est plus couramment nommée ainsi.

La déduction est un calcul

Une déduction consiste à partir d’hypothèses, ou d’axiomes, et à progresser par étapes logiques jusqu’à une conclusion. On peut présenter les principes de la déduction au premier ordre de plusieurs façons.

La logique du dialogue apporte également un autre éclairage sur la nature des lois logiques.

Résultats de complétude et d'incomplétude

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 dix-neuvième siècle 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 ce qu’on appelle aujourd’hui le calcul des prédicats au premier ordre, ou logique du premier ordre.

Kurt Gödel a prouvé en 1929 (dans sa thèse de doctorat) que la logique du premier ordre est une science essentiellement achevée 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 toutes les lois logiques (voir le théorème de complétude de Gödel ). La méthode de déduction naturelle en particulier se contente d’une liste de treize règles qui suffisent pour déduire toutes les lois logiques. Elles pourraient être réduites à un plus petit nombre, mais l'évidence des principes serait moins naturelle.

Il faut entendre que la logique du premier ordre est achevée seulement au sens où le problème de la correction logique des démonstrations y est résolu. Cela ne veut pas dire qu’il n’y a plus de questions à se poser à son sujet. Même après la démonstration du théorème de complétude de Gödel, elle a continué à faire l’objet d’intenses recherches : théorie des modèles, algèbres cylindriques, ...

Gödel a prouvé en 1930 que les théories des ensembles et toutes les théories mathématiques qui contiennent les vérités arithmétiques ne sont pas complètes, au sens où elles ne suffisent pas pour répondre à toutes les questions qu'elles permettent de poser, elles ne permettent pas de prouver toutes les vérités qu'elles permettent pourtant d'énoncer.

Ce premier théorème d'incomplétude a été suivi par de nombreux autres (voir Incomplétude). L'incomplétude des principes mathématiques est étroitement reliée au paradoxe du menteur, aux théorèmes de Cantor sur l'existence des ensembles indénombrables, et à la puissance de l'imagination.

See also: Calcul des prédicats, Alfred Tarski, Aristote, Axiome logique, Calcul des propositions, Déduction naturelle, Emmanuel Kant, Gottlob Frege, Incomplétude, Kurt Gödel