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 \(x,y,z,\ldots\). alors un terme est

Par exemple

\[0+1,\qquad x-3,\qquad (y+5)\times 6\]

sont des termes, mais

\[-5,\qquad x=y,\qquad ++3, xy\]

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é \(n\) appliqué à \(n\) termes. Par exemple

\[x=y,\qquad (2+y) = x,\qquad (0 + 1) = (3 - 2)\]

sont des formules atomiques, mais

\[2+3,\qquad 2 + (y=x), \qquad y=x=z, 0\le 1\le 2\]

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:

\[\forall x.(x\le 0\vee x=0),\qquad (\exists x.x+2=0)\wedge(\exists y.z=2)\]

et des non-exemples:

\[\forall x\le 0. x=y,\qquad \exists x.x,\qquad (\exists x.x=y)+1\]

(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

\[\forall x. (P(x) \vee Q(y))\]

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

\[(\forall x. P(x)) \vee Q(x)\]

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

Une formule sans variables libres est dite close. Une formule \(\phi\) de variables libres \(x,y,\dots\) est parfois notée \(\phi(x,y,\dots)\) 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 \(\phi\), comme par exemple

\[\forall x.\exists y.\phi(x,y).\]

Priorité des opérateurs

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

\[\forall x. P(x) \vee Q(x)\]

est à lire comme

\[\forall x. (P(x) \vee Q(x))\]

et non pas comme

\[(\forall x. P(x)) \vee Q(x)\]

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

\[\forall x. \exists y. P(x,y)\]

est

\[\forall x. (\exists y. P(x,y))\]

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

\[\forall x,y \in \mathbb{N}. x + y \ge 0.\]

Une autre convention courant consiste à utiliser le symbole \(\Rightarrow\) pour l’implication, à la place du symbole \(\to\) 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 \(n\) formules atomique a seulement \(2^n\) 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 \(\mu\), c’est à dire une fonction \(\mu(x)\) qui à chaque variable \(x,y,\dots\) associe un élément du domaine.

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

Par exemple, si le terme est \(x+1\), en supposant que \(\mu(x)=3\), son interprétation sous \(\mu\) est

On peut finalement définir l’interprétation d’un prédicat \(\phi\) sous une affectation \(\mu\). 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 \(\mu(x) = 2\) et \(\mu(y) = 1\). La formule \(\forall x.(x>0)\to(x>y)\) est fausse car il existe un \(\mu'\), par exemple \(\mu'(x)=1\), \(\mu'(y)=1\), qui diffère de \(\mu\) seulement en \(x\) et qui rend \((x>0)\to (x>y)\) fausse. Au contraire, si on prend \(\mu(x)=2\) et \(\mu(y)=0\), la même formule devient vraie (sous l’affectation \(\mu\)). On observe que la valeur de \(\mu(x)\) ne change rien à la vérité de la formule, car \(x\) y est liée.

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

Exemple : \(\forall x.\forall y.\exists z. (x < z < y)\) est fausse dans les entiers. En effet, pour n’importe quelle affectation initiale, il suffit de prendre \(\mu'(x)=0\) et \(\mu'(y)=1\) pour voir qu’il n’existe pas de choix pour \(z\) qui vérifie \(x<z<y\). 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

\[\forall x. x < y\]

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

\[\forall y. \forall x. x < y\]

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 \(\phi\) est valide on note

\[\models \phi\]

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

\[\phi\models\psi\]

Si \(\phi\models\psi\) et \(\psi\models\phi\) on dit que \(\phi\) et \(\psi\) sont équivalentes et on note

\[\phi\equiv\psi \quad\text{ou}\quad \phi\Leftrightarrow\psi \quad\text{ou}\quad \phi=\psi\]

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 à

\[\neg(\forall x. \psi) \equiv \exists x.\neg\psi\]

pour tout prédicat \(\psi\).

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

Fork me on GitHub