Previous Next Contents

4  Pouvoir d'expression

Les logiques d'ordre un sont beaucoup plus expressives que les logiques propositionnelles correspondantes, et en particulier la logique classique du premier ordre est beaucoup plus expressive que la logique propositionnelle classique.

D'abord, la logique du premier ordre peut exprimer des propriétés sur des domaines infinis. En logique propositionnelle, pour exprimer des propriétés sur des valeurs, nous ne pouvions que coder ces dernières sur un nombre fini de variables propositionnelles. Ceci ne permet qu'un nombre fini de valeurs, puisqu'il n'y a qu'un nombre fini d'affectations portant sur les variables propositionnelles libres dans une formule propositionnelle. En logique du premier ordre, nous pouvons construire des formules comme :
  " x,y,z· x<yÙ y<zÞ x<z
Ù " x,y· x<yÞ$ z· P(x,z)Ù¬ P(y,z)
Ù " x·$ y· x<y
où P et < sont deux symboles de prédicat binaires, < étant écrit en notation infixe. Cette formule est satisfiable : interprétons < comme la relation ``strictement plus petit que'' sur les entiers, et P comme la relation ``plus petit ou égal à''. Mais ses modèles sont tous infinis : < doit dénoter un ordre partiel strict de par les deux premières lignes, et ne peut pas avoir de borne supérieure par la troisième.

Nous pouvons fabriquer des théories plus utiles. Par exemple, prenons un symbole de prédicat (infixe) binaire <, et disons qu'il représente un ordre strict, c'est-à-dire qu'il est irréflexif :
" x· ¬ x<x
et transitif :
" x· " y· " z· x<yÙ y<zÞ x<z

L'égalité = est un peu plus difficile à axiomatiser, car nous voulons pouvoir remplacer les termes par des termes égaux, autrement dit si a= b est vrai, alors s[a/x]= t[a/x] est vrai aussi pour tous termes s et t; aussi, F[a/x] doit être logiquement équivalent à F[b/x]. L'astuce pour axiomatiser l'égalité est de d'abord fixer le langage sur lequel nous travaillerons, autrement dit l'ensemble des symboles de fonctions et de prédicats dont nous aurons besoin, et de produire un axiome par symbole pour exprime que chacun préserve l'égalité. Ceci mène à la théorie suivante : Supposons que nous souhaitions prouver une formule. Son langage est fini, donc nous n'avons besoin que d'un nombre fini d'axiomes pour =. Si nous devons étendre ce langage, par exemple par l'introduction de nouveaux symboles de fonction (comme des symboles de Skolem, voir Section 5.1), nous devrons alors ajouter les axiomes de congruence correspondants.

Grâce à de telles constructions, nous pouvons traduire les logiques modales, ainsi que la logique intuitionniste en terme de logique classique du premier ordre, en exprimant leur sémantique de Kripke. Ceci est cependant une mauvaise idée en général, car les procédures de recherche de preuve spécialisées pour les logiques modales ou intuitionniste sont en général plus efficaces que les procédures générales pour la logique du premier ordre.

Une grande partie des mathématiques peut être formalisée en logique du premier ordre avec égalité. Par exemple, la théorie des groupes étend celle de l'égalité en ajoutant les axiomes suivants sur le langage 0 (constante), + (fonction binaire) :
" x· 0+x= xÙ x= x+0 (0 est élément neutre)
" x· " y· " z· x+(y+z)= (x+y)+z (associativité)
" x·$ y· x+y= 0Ù y+x= 0 (inverse)
La théorie des anneaux ajoute de nouveaux symboles de fonction 1 (constante), * (fonction binaire) et les axiomes :
" x· " y· x+y= y+x (commutativité de +)
" x· 1*x= xÙ x= x*1 (1 est neutre pour *)
" x· " y· " z· x*(y*z)= (x*y)*z (associativité)
" x·" y·" z· x*(y+z)= x*y+x*z  
" x·" y·" z· (y+z)*x= y*x+z*x (distributivité)
Les corps ajoutent l'axiome :
" x· x¹ 0Þ$ y· x*y= 1Ù y*x= 1
Nous pouvons de même développer des théories des corps commutatifs, des modules, des espaces vectoriels, et ainsi de suite.

Ces théories décrivent les notions mathématiques correspondantes de façon adéquate. Cependant, il existe des notions qui ne peuvent pas être capturées précisément par aucune théorie du premier ordre récursivement énumérable. Nous disons que de telles notions ne sont pas axiomatisables au premier ordre. (Trivialement, toute notion mathématique peut être capturée par une théorie du premier ordre, à savoir celle qui liste tous les énoncés valides portant sur la notion; mais cette théorie n'est pas forcément récursivement énumérable.) Par exemple, il n'y a pas de théorie du premier ordre axiomatisable dont les modèles sont tous les groupes finis, et seulement les groupes finis. (Bien que nous puissions décrire les groupes de cardinal p, pour tout entier p fixé.) Nous ne pouvons pas traduire le µ-calcul modal en logique du premier ordre fidèlement non plus, autrement dit nous ne pouvons pas axiomatiser les constructions de la logique en logique du premier ordre. C'est parce que les règles de point fixe du calcul ne peuvent pas être traduites fidèlement en logique du premier ordre. Pour la même raison, il n'y a pas d'axiomatisation au premier ordre dont le seul modèle soit l'ensemble N des entiers naturels muni des opérations arithmétiques usuelles.

Nous pouvons quand même construire une forme d'arithmétique appelée arithmétique de Peano du premier ordre PA1, mais il nous faudra un nombre infini d'axiomes, et elle ne décrira pas complètement l'arithmétique, bien qu'elle en décrive une bonne partie. Le langage de PA1 consiste en la constante 0, la fonction unaire s (successeur), les fonctions binaires + et * (addition et multiplication, que nous écrivons en infixe), les relations binaires = et £ (égalité et relation ``inférieur ou égal à'', écrites en infixe; nous les notons en rouge pour les distinguer des affirmations d'égalité et d'inégalité = et £). Les axiomes de PA1 --- les éléments de la théorie PA1 --- sont : Le schéma de récurrence est une collection infinie d'axiomes. Nous voudrions écrire à la place :
" P· P(0)Ù (" x· P(x)Þ P(s(x)))Þ " x·F
où P est une variable de prédicat. (Ceci est l'axiome de récurrence du second ordre.) Nous ne pouvons pas le faire en logique du premier ordre, puisque nous ne pouvons quantifier que sur les variables, et les variables dénotent des valeurs, pas des prédicats sur les valeurs. Mais les dommages sont limités : bien que PA1 ait une infinité d'axiomes, l'ensemble de ses axiomes est récursif, ce qui signifie que nous pouvons décider par algorithme si une formule donnée est un axiome de PA1 ou non.

Un modèle de PA1 est le modèle souhaité : l'ensemble N des entiers naturels, où la constante 0 est interprétée comme zéro, s est interprétée comme l'application envoyant n vers n+1, + est interprétée comme l'addition, * comme la multiplication, = comme l'égalité et £ comme l'ordre naturel £ vérifie tous les axiomes. Il s'agit du modèle standard de PA1.

Mais PA1 a d'autres modèles, les modèles non standard de l'arithmétique [Rob66], comme on s'y attendait au su du fait que l'arithmétique de Peano n'est pas axiomatisable en logique du premier ordre. Ceci est une limitation inhérente à la logique du premier ordre, et peut être expliqué dans ce cas par le théorème de Löwenheim-Skolem, que nous présenterons en section 5.2.

La logique du premier ordre peut non seulement exprimer cette forme faible d'arithmétique, mais elle est encore assez expressive pour formaliser la théorie des ensembles, par exemple au moyen des axiomes de Zermelo et Frænkel, sur laquelle toutes les mathématiques peuvent être fondées (à l'exception de quelques points n'intéressant que les logiciens). Voir [Joh92] pour une discussion de la théorie des ensembles de Zermelo-Frænkel, de ses concepts et résultats fondamentaux.



Previous Next Contents