Calcul des prédicats

Le calcul des prédicats, ou logique du premier ordre, est une théorie formelle (au sens où il s’agit de manipuler des formules) qui modélise le raisonnement mathématique.

Des exemples de théories mathématiques modélisables en logique du premier ordre sont les entiers naturels (via les axiomes de Peano) ou les mathématiques entières (via les axiomes de Zermelo-Fraenkel). Il existe cependant des limitations bien connues à la possibilité de réaliser ces modélisations, comme l’a démontré Gödel avec ses théorèmes d’incomplétude.

Définitions

On fait comme d’habitude une distinction entre syntaxe et sémantique. Si la première est à peine plus complexe que la syntaxe du Calcul des propositions, la deuxième est beaucoup plus riche, car n’importe quelle structure mathématique peut faire de modèle à la logique du premier ordre.

Syntaxe

La logique du premier ordre a été conçue pour décrire n’importe quelle structure mathématique, comme par exemple les nombres naturels. Avant de pouvoir énoncer des propriétés (i.e., des théorèmes) d’une structure mathématique, nous devons définir quel est son langage, i.e. quelles sont les façons légitimes de combiner les objets de la structure.

Un langage, ou signature, est la donnée des éléments suivants (tous en quantité pas nécessairement finie):

Par exemple, le langage de l’arithmétique est constitué de:

On peut combiner les symboles d’un langage pour former des termes. Pour cela, nous nous donnons un ensemble dénombrable de variables . alors un terme est

Par exemple

sont des termes, mais

n’en sont pas. Un terme qui ne contient pas de variables est dit clos.

Remarque: ni les parenthèses ni le point ne font pas partie du langage. Ils sont simplement là pour rendre les termes non-ambigus, i.e. pour indiquer dans quel ordre les fonctions ont été appliquées pour obtenir le terme. Voir du bon usage des parenthèses.

Une formule atomique est un prédicat du langage de arité appliqué à termes. Par exemple

sont des formules atomiques, mais

n’en sont pas (même si certaines d’entre elles sont des raccourcis communément utilisés).

Finalement nous sommes prêts à définir la syntaxe de la logique du premier ordre. Nous nous donnons les connecteurs logiques suivants

Une formule du premier ordre (ou formule bien formée) est:

Voici des exemples de formules:

et des non-exemples:

(même si la première est un raccourci courant).

Variables libres et liées

Une variable est dite libre si elle n’est quantifiée par aucun quantificateur (dans son sous-arbre syntaxique). Elle est dite liée sinon. Par exemple, dans le prédicat

la variable est liée, tandis que est libre. De façon moins évidente, dans le prédicat

la première occurrence de la variable est liée, tandis que la deuxième est libre (en effet, le quantificateur ne porte pas sur elle, car il est dans un sous-arbre différent).

Une formule sans variables libres est dite close. Une formule de variables libres est parfois notée lorsque l’on veut indiquer clairement les noms de ses variables libres. Ceci est intéressant, par exemple, lorsque l’on forme un prédicat plus long à partir de , comme par exemple

Priorité des opérateurs

Les règles de priorité des opérateurs sont les mêmes que pour le Calcul des propositions. Les quantificateurs on par convention la priorité la plus basse, ainsi

est à lire comme

et non pas comme

On omet aussi les parenthèses lorsque plusieurs quantificateurs se suivent. Ainsi, la seule façon d’interpréter

est

Autres conventions

En dehors du cadre de la logique, le calcul des prédicats est utilisé pour exprimer de façon succincte des énoncés mathématiques. Pour avoir plus de souplesse et de maniabilité, l’on accepte dans ce cas d’autres raccourcis de notation qui ne sont pas standard dans la théorie de la logique du premier ordre.

Les raccourcis les plus courants sont

Ces raccourcis peuvent être utilisés, par exemple, pour écrire

Une autre convention courant consiste à utiliser le symbole pour l’implication, à la place du symbole qui a déjà trop d’utilisations en algèbre.

Dans la suite de ce cours, nous allons rigoureusement éviter d’utiliser ces raccourcis.

Sémantique

Comme en Calcul des propositions, donner une sémantique au calcul des prédicats revient à attacher une interprétation à chaque symbole, et ensuite à chaque prédicat. Les choses sont rendues plus complexes par le fait que le calcul des prédicats permet de modéliser toutes les mathématiques, et que donc le nombre d’interprétations possibles est infini (alors que, rappelons-le, dans une proposition avec formules atomique a seulement modèles distincts).

La première chose à fixer pour interpréter le calcul des prédicats est un domaine du discours, en général un ensemble (par exemple les entiers), dans lequel on va interpréter tous les termes.

Une fois le domaine du discours fixé, on définit un modèle (ou interprétation, ou structure du premier ordre) comme l’assignation

Par exemple, si le langage est celui de l’arithmétique, un modèle possible sera l’assignation

Remarque : Tout ceci peut paraître une inutile lapalissade, car on donne à chaque symbole la signification qu’on lui attribue déjà ordinairement. Gardez à l’esprit, toutefois, qu’un même symbole peut être interprété de plusieurs façons différentes : les chiffres peuvent représenter des nombres en base deux, les opérations arithmétiques peuvent être faites modulo un entier, etc. La théorie du calcul des prédicats s’intéresse aux metathéorèmes qu’on peut démontrer indépendemment de la façon d’interpréter le langage ; il est donc naturel de monter à ce niveau d’abstraction, afin de pouvoir attacher des modèles exotiques au calcul des prédicats.

Une fois le modèle fixé, on peut passer à définir l’interprétation des prédicats. On commence par se donner une affectation des variables , c’est à dire une fonction qui à chaque variable associe un élément du domaine.

On peut maintenant définir l’interprétation d’un terme. L’interprétation d’un terme , sous l’affection est définie inductivement par

Par exemple, si le terme est , en supposant que , son interprétation sous est

On peut finalement définir l’interprétation d’un prédicat sous une affectation . L’interprétation d’un prédicat ne va plus être un élément du domaine, mais plutôt une valeur de vérité (vrai ou faux).

Exemple : on fixe et . La formule est fausse car il existe un , par exemple , , qui diffère de seulement en et qui rend fausse. Au contraire, si on prend et , la même formule devient vraie (sous l’affectation ). On observe que la valeur de ne change rien à la vérité de la formule, car y est liée.

Lorsque la formule ne contient pas de variable libre, sa valeur de vérité ne dépend pas de l’affectation initiale , et on dit simplement que est vraie ou fausse dans le modèle.

Exemple : est fausse dans les entiers. En effet, pour n’importe quelle affectation initiale, il suffit de prendre et pour voir qu’il n’existe pas de choix pour qui vérifie . Par contre le même prédicat est vrai dans les rationnels, il existe en effet toujours un nombre rationnel compris entre deux nombres rationnels distincts. On voit ici que, même si la vérité d’un prédicat clos ne dépend pas de l’affectation, elle peut bien dépendre du modèle choisi.

Un prédicat clos qui est vrai dans un modèle est dit satisfaisable, un prédicat qui est vrai dans tout modèle est dit valide. Ceci est analogue aux définitions de satisfaisabilité et de tautologie en Calcul des prédicats.

Puisque ces notions ne sont bien définie que pour les prédicats clos, on s’intéresse par la suite principalement à ceux-ci. Une convention courrante pour traiter les prédicats non-clos consiste à convenir que toutes les variables libres sont universellement quantifiées. Ainsi lorsque l’on s’interroge sur la validité du prédicat

il est sous-entendu qu’on parle de la validité de

Théorie des modèles

Comme pour le Calcul des propositions, nous nous intéressons aux équivalences entre prédicats qui sont valides indépendemment de la façon dont on interprète les variables. Lorsque un prédicat est valide on note

Si et sont deux prédicats, et si tout modèle qui rend vrai rend aussi vrai , on dit que est une conséquence logique (ou sémantique) de et on note

Si et on dit que et sont équivalentes et on note

En général ces équivalences sont indépendantes du langage employé. Ainsi les équivalences qu’on peut espérer démontrer ressembleront plutôt à

pour tout prédicat .

Exercice : Montrer que cette équivalence est bien vérifiée.

-rennomage

Une des méthodes les plus simples pour obtenir des équivalences consiste à renommer certaines variables sans altérer la sémantique du prédicat. Ce procédé s’appelle -renommage (ou -conversion).

Si est une formule, contenant une variable liée, on peut remplacer toutes les occurrences liées de par une nouvelle variable (en faisant attention à ce que ne soit pas déjà employée et libre dans ), sans altérer la sémantique de .

Par exemple, si est la formule

elle peut être changée en

sans en altérer la sémantique. Lorsque l’on procède à un -renommage il faut faire attention à ce que la nouvelle variable ne soit pas déjà libre dans la formule ; en effet la formule

n’est pas équivalente à (en effet, n’y est plus libre).

Il est aussi possible de renommer les variables libres, par exemple dans la formule précédente, mais dans ce cas il ne fait pas beaucoup de sens de parler d’équivalence, car la formule n’est pas close. Par exemple, la formule

n’est pas équivalente à , néanmoins on peut noter cette nouvelle formule. En général, si est une formule de variable libre , on notera ou encore la même formule dans laquelle toutes les occurrences libres de ont été remplacées par .

Forme normale prénexe

La forme normale prénexe est une technique permettant de transformer un prédicat quelconque en un prédicat équivalent sous une forme standard. Un prédicat est dit en forme normale prénexe (en anglais, PNF) s’il est de la forme

où les sont des quantificateurs ou , et est un prédicat sans quantificateurs. Pour tout prédicat il existe un prédicat sémantiquement équivalent (en logique classique) en PNF ; ce prédicat peut être obtenu à l’aide de quelques transformations élémentaires, que nous listons ci-dessous.

Les équivalences remarquables du calcul des propositions :

Les équivalences remarquables du calcul des prédicats :

Moyennant un -rennomage de la variable , ces quatre dernières règles peuvent être appliquées en toute circonstance.

D’autres règles de transformation, notamment concernant le connecteur , peuvent être déduites à partir de celles-ci.

Exercice : Prouver les équivalences remarquables ci-dessus.

Théorie de la preuve

La Théorie de la preuve de la logique du premier ordre n’est pas plus compliquée que celle du Calcul des propositions: en effet les systèmes de preuve sont les mêmes, après ajout de quelques règles d’inférence pour les quantificateurs. Voir Théorie de la preuve.

Fork me on GitHub