• La logique formelle
  les formalismes des fondemants des mathématiques
  La logique classique
  La logique des prédicats
  Les logiques multivalentes
• Volume de l'hypersphère
  pourquoi les banquiers n'ont pas de lingots sphériques
  
• L'axiome du choix
  polémiques et paradoxes
  
• Fonctions continues sans dérivées
  les monstres qui effrayaient Charles Heremite
• Les géométries non euclidiennes
  D'Euclide à Poincaré, la saga des figures étranges
  
• 1+2+3+... = -1/12
  vu dans "Ciel et Espace" N0 238 page 32
  
• Le nombre pi
  décimales et algorithmes
  
• Termes inversibles en Lambda calcul
  mémoire de DEA
  
• Mathématiques pour un anniversaire
  curieuses formules
  
• Mes bouquins de maths préférés
  de saines lectures pour les soirées d'hiver
  
• Liens et autres sites
  un petit tour chez les collègues
  

Introduction.

La logique des propositions que l'on vient de voir traite les propositions comme un tout. La célèbre phrase de Socrate Tout homme est mortel peut être analysée plus finement à l'aide du prédicat être mortel, et de la variable d'individu x qui représentera génériquement l'homme.
Dans le petit exposé qui suit on va décrire le système formel du calcul des prédicats, son utilisation, les problemes de complétude et de décision des EBF.

Le formalisme de la logique des prédicats.

Le système formel correspondant contient la logique de propositions à laquelle on y ajoute un autre ensemble d'objets appelé variables des individus, et un ensemble de prédicats portant sur les individus. De manière un peu plus précise voici le langage correspondant à la logique des prédicats. L'ensemble suivant est le vocabulaire terminal:

{C,N,a,b,c,...} { } { } {}

C et N sont les deux connecteurs de base de la logique des proposition: implication et négation.

{a,b,c,d,.....} sont les variables propositionnelles.

{} sont les variables d'individus.

{} sont les prédicats de poids 1, c'est-à-dire portant sur une seule variable d'individu.

{} sont les prédicats de poids 2, c'est-à-dire portant sur 2 variables d'individu.

{} sont les prédicats de poids n, c'est-à-dire portant sur n variables d'individu.

est le quantificateur universel.

Les constructions des EBF sont données par la grammaire suivante:

Soit {V, W, P1, P2, ... Pn, F, E} le vocabulaire auxiliaire. E étant le point d'entrée de la grammaire.

Cette grammaire contient une infinité de règles.

Avant d'exposer les règles de déduction, il nous faut définir un nouveau concept portant sur les variables d'individu, le concept de variable libre et de variable liée. On détermine l'ensemble des variable liées d'une EBF en appliquant la fonction V ci-dessous récursivement à l'EBF:

V({x}) =
V(x X) = V(X){x}
V(CXY) = V(X)V(Y)
V(NX) = V(X)
V(P) =

On détermine l'ensemble des variable libres d'une EBF en appliquant la fonction W ci-dessous récursivement à l'EBF:

W({x}) = {x}
W(x X) = W(X)\{x}
W(CXY) = W(X)W(Y)
W(NX) = W(X)
W(P) = {}

Les termes X et Y représentent des EBF du calcul des prédicats, et P un prédicat de poids quelconque.

Ceci étant précisé, on ajoute aux règles de substitution et de détachement concernant du calcul des propositions les deux règles suivantes concernant l'usage du quantificateur :

Si on désigne par L une EBF du calcul des prédicats

CfxL --> CxfxL Règle [R4]
CLfx --> CLxfx Règle [R5], à la condition que x ne figure pas libre dans L.

La règle de substitution du calcul des propositions doit être légèrement modifiée:

On peut subsituer une EBF du calcul des prédicats à une variable propositionnelle à la condition que l'EBF ne contienne pas des variables d'individu liées dans l'expression générale.

En ce qui concerne les définitions, on conserve les mêmes que pour le calcul des proposition, à savoir E, K, A, D, et en plus un nouveau symbole avec la définition:

NxN --> x

Aux axiomes du calcul des propositions on ajoute les deux axiomes suivants:

1. xf(x) ==> f(r)
2. f(r) ==> xf(x)

Soufflons un peu

La présentation très formelle que l'on vient de faire est due à Prior.

L'interprétation des termes et est celle bient connue des symboles et (le quel que soit et le il existe)

Si on reprend l'exemple de l'introduction Tout homme est mortel, cette phrase de Socrate était analysée comme un tout susceptible d'être vrai ou faux en calcul des propositions. En calcul des prédicats on va pouvoir en analyser plus finement les composants à l'aide du prédicat à une place être mortel et d'une variable d'individu représentant l'homme. Cette phrase se traduira en termes du calcul des prédicats:

xfx (dans le formalisme de Lukasiewicz - Prior)

xf(x) (dans le formalisme de Russell)

Ici f représente le prédicat être mortel, prédicat de poids 1. On remarque que la grammaire du calcul des prédicats est faite de telle sorte que les prédicats ne s'appliquent qu'aux variables d'individus et pas à d'autres prédicats. On appelle parfois un tel système la logique du premier ordre. Une logique du second ordre contiendrait des prédicats s'appliquent à des prédicats jouant le rôle de variable. On peut remarquer dans ce contexte que le calcul des propositions peut être vu comme un calcul des prédicats d'ordre 0, où les prédicats seraient de poids nul et donc confondus avec les constantes. On appelle parfois le calcul des propositions la logique d'odre zéro.

Des exemples

Donnons quelques exemples d'EBF du calcul des prédicats dans le formalisme de Luksiewicz et dans celui de Russell:

formalisme de Lukasiewicz	formalisme de Russel
Cxyfxyyxfxy	(xyf(x,y)) ==> (yxf(x,y))
CxCpfxCpxfx	x((p) ==> (f(x))) ==> ((p) ==> (xf(x)))
CxCfxgxCxfxxgx	x(f(x) ==> g(x)) ==> (x(f(x)) ==> x(g(x)))

signalons au passage que ces trois exemples sont des thèses du calcul des prédicats et peuvent être démontrées formellement.

Aspect sémantique: la notion de validité

Comme en calcul des propositions, on peut interpréter les EBF du calcul des prédicats et définir la notion de validité. Mais cela est moins simple qu'en calcul des propositions car pour une valeur (vraie ou fausse) d'une EBF il va falloir examiner les valeurs des variables d'individus qui la composent.
En plus des tables de vérité du calcul des propositions pour C et N il faut rajouter une interprétation pour les EBF faisant intervenir les quantificateurs. Ainsi pour une expression de la forme xf(x) on dira qu'elle est vraie si f(a) est vraie pour tout individu a pris dans un ensemble de valeurs donnant un sens au prédicat f, et pour une expression de la forme xf(x) on dira qu'elle est vraie si f(a) est vraie pour au moins une valeur a du modèle.

Par exemple soit l'expression dans le formalisme de Russel:

g(y) V x(g(x) ==> q)

Cette expression est valide sur un domaine à un élément D={a}, mais pas sur un domaine à deux éléments et plus. En effet sur le domaine à un élément cette expression devient: g(a) V (g(a) ==> q) si g(a) est vraie alors l'expression est vraie, si g(a) est fausse alors (g(a) ==> q) est vraie et donc la proposition est vraie. Pour un domaine à deux éléments {a,b} il suffit d'avoir g(a) faux, g(b) vraie et q faux pour pour avoir un contre-exemple. On dira que cette expression est 1-valide.On peut fabriquer des expressions 1-valides, 2-valides et pas 3-valides, et même des expressions n-valides et pas (n+1)-valides. L'expression ci-dessous

~[xyf(x,y) ^ x ~f(x,x) ^ xyz((f(x,y) ^ f(y,z)) ==> (f(x,z)))]

est n-valide pour tout n, mais n'est pas valide sur un domaine infini.

On voit que l'on peut définir des tables de vérité des EBF du calcul des prédicats à la condition que les domaines de valeur des variables d'individu soient finis, et cela donnerait des tables gigantesques. Dans le cas des domaines infinis il faut d'autres techniques pour définir la validité des EBF. C'est l'objet du chapitre suivant.

Les méthodes de déduction

Il existe plusieurs méthodes de déduction, dites aussi méthodes de déduction naturelles. Dans la méthode de démonstration formelle il n'y a aucun moyen au vue de la thèse à déduire de trouver la suite des expressions constituant la démonstration aboutissant à la thèse. C'est en ce sens qu'une démonstration formelle n'est pas naturelle. Une méthode de déduction naturelle au contraire déduit la thèse au vue de la thèse. Il existe de nombreuses telles méthodes qu'il serait fastidieux de passer en revue. Signalons toutefois qu'il existe une méthode principale mais pas de méthode générale. Parmi les méthodes connues signalons la méthode principale de Quine, la méthode de Gentzen, et nous examinerons d'un peu plus près la méthode de Schutte-Ackermann.

Cette méthode, applicable au calcul des propositions comme au calcul des prédicats consite dans un premier temps à écrire l'EBF en forme normale disjonctive c'est-à-dire sous une forme où il n'y a que le symbole de négation et de disjonction qui interviennent. C'est facile puisque l'implication ((p) ==> (q)) peut s'écrire ((p) V (~q)). On applique donc un certain nombre de règles permettant de nous rammener à une telle forme normale disjonctive, dont en particulier:

m V ~~a V n se transforme en m V a V n - règle [~~]
m V ~(a V b) V n se transforme en m V ~a V n et m V ~b V n - règle [~V]
xA se transforme en ~ x ~A
m V ~xA(x) V n se transforme en m V ~ A(y) V n où y est une variable libre - règle [~].
m V x A(x) V n se transforme en m V x A(x) V A(y) V n où y est une variable libre de l'expression de départ, et de plus A(y) ne doit pas figurer comme expression dans m ou dans n - règle [].

Dans les expressions ci-dessus m et n sont des EBF pouvant ne pas exister. Voyons cette méthode sur un exemple simple:

Soit à montrer x(p ==> f(x)) ==> (p ==> xf(x))

x(p ==> f(x)) ==> (p ==> xf(x))
~x(~p V f(x)) V (~p V x f(x)) mise en forme normale disjonctive
~x(~p V f(x)) V ~p V x f(x) suppression des parenthèses
~(~p y f(y)) V ~p V x f(x) règle [~]
~~p V ~p V xf(x) | ~f(y) V ~p V xf(x) règle [~v]
p V ~p V xf(x) | ~f(y) V ~p V xf(x) V f(y) règle [~~] et règle []

On constate qu'on obtient un arbre à deux branches dont les feuilles sont des expressions valides puisque composées de disjonctions du type A V ~A.

Quand on applique cette méthode il peut se produire plusieurs situations:

1. L'arbre se termine et les feuilles sont des expressions valides. Dans ce cas l'expression analysée est valide.
2. L'arbre se termine et au moins une des feuilles ne donne pas une expression valide. Dans ce cas l'expression analysée n'est pas valide.
3. L'arbre ne se termine pas et contient au moins une branche infinie. Dans ce cas on ne peut pas conclure car il se peut que par une autre méthode on ait pu conclure.

On constate qu'avec une telle méthode on n'a pas interprété les EBF du calcul des prédicats par des tables de vérité mais par un arbre. Le fait que l'arbre puisse devenir infini (comme les tables)montre qu'il faut une méthode planifiée de déduction.

Chaque ligne de la déduction est appelée séquence de disjonctés. Appelons u0,u1,....,up les variables libres figurant dans la séquence de départ. Nous y ajoutons les varaibles libres a1,a2,....., on obtient le domaine infini D={u0,u1,.....,up,a0,a1,.....}. A une certaine séquence on a libéré un certain nombre de variables et sur chaque chemin on groupe les étapes de la manière suivante:

1. on effectue une étape lorsqu'on applique les règles de déduction successivement à chaque disjoncté si possible de la séquence initiale de l'étape.
2. chaque règle s'applique au plus une fois exceptée la règle [] que l'on applique autant de fois qu'il y a de variables libérées.

Cette méthode planifiée a l'inconvénient de donner parfois des arbres de décision très longs. La présence d'arbre infini montre que le calcul des prédicats n'est pas décisoire, c'est-à-dire qu'il n'existe pas de méthode générale pour décider si une expression est valide ou non. On sait par contre classer les EBF afin de savoir si la méthode aboutira ou non à un arbre infini. Mais avant d'être plus précis il nous faut dire quelques mots sur les formes prénexes.

Les formes prénexes

Il est possible de modifier dans une EBF du calcul des prédicats l'ordre et la position des quantificateurs de manière à les regrouper en début d'expression sans changer la valeur de l'EBF.
Par exemple:

x[y(f(x) ^ g(y)) V yf(y)] ^ x(f(x) V g(x))

peut aussi s'écrire quitte à renommer des variables:

xyzw[((f(x) ^ g(y)) V f(z)) ^ (f(w) V g(w))]

On peut aussi l'écrire:

xy[(f(x) ^ g(y)) V f(y)] ^ (f(x) V g(x))

Ce qui montre que la mise en forme prénexe d'une formule du calcul des prédicats n'est pas chose simple.

On peut donner, pour conclure le paragraphe précédent, les classes de formule pour lesquels il y a un procédé de décision:

• Si la formule ne contient que des prédicats monadiques.
• Si la formule en forme prénexe ne contient que des quantificateurs universels
• Si la formule en forme prénexe ne contient que des quantificateurs existentiels
• Si la formule en forme prénexe ne contient que des quantificateurs universels suivi de quantificateurs existentiels.

Par contre si la formule en forme prénexe contient des quantificateurs existentiels suivis de des quantificateurs universels, alors elle n'est pas décisoire.

Consistance et complétude

Le calcul des prédicats, comme le calcul des propositions est un système consistant c'est-à-dire que l'on ne peut pas montrer à la fois qu'une expression est une thèse ainsi que sa négation.

En ce qui concerne la complétude, c'est un petit peu plus délicat que pour le calcul des propositions. On rappelle ici les définitions de la complétude:

Complétude forte ou syntaxique.Un système formel est dit complet si, en utilisant ses axiomes et ses règles, on peut montrer de n'importe quelle EBF, soit qu'elle est une thèse du système, soit que jointe au système elle le rend contradictoire.

Complétude faible ou sémantique.Un système formel est dit complet si, en utilisant ses axiomes et ses règles, on peut établir comme thèses toutes les EBF valides.

Le calcul des prédicats ne remplit pas la condition de complétude syntaxique. Il est en effet possible de rajouter au système d'axiomes du calcul des EBF non thèses sans le rendre contradictoire. Par exemple l'expression f(x) V ~f(y) qui contient deux variables libres n'est pas une thèse mais rajoutée au système elle ne conduit pas à une contradiction. Si on prend un domaine de validité à un élément {a}, on obtient f(a) V ~f(a) qui est valide dans ce domaine.

On s'aperçoit que la validité des expressions dépend des domaines. Une expression du calcul des prédicats sera valide si elle l'est sur tout domaine. Godel a démontré en 1930 la complétude sémantique du calcul des prédicats.

Signalons aussi le célèbre théorème de Löwenheim-Skolem: si une EBF est valide sur un domaine infini dénombrable alors elle est valide sur tout domaine.

Le calcul des pédicats avec identité

Le calcul des prédicats que l'on vient de définir est souvent appelé calcul des prédicats pur. Il ne permet pas d'identifier deux variables d'individu et est tout à fait inapte à décrire les mathématiques. Ici nous allons l'enrichir très légèrement avec le concept nouveau d'identité. Nous définirons ce que l'on pourrait appeler un calcul restreint en ce sens que l'identité ne va porter que sur des variables d'individus et pas sur des prédicats.

L'idée est de pouvoir formaliser des concepts d'identité d'individus comme par exemple:

Napoléon = Napoléon (identité triviale)
Napoléon = Vercingétorix (égalité fausse)
Napoléon = Bonaparte (identité ni triviale ni fausse)
7+5 = 12 (identité vraie mais non triviale)

Pour ce faire on va particulariser un prédicat particulier qui sera l'identité. Le prédicat correspondant f(x,y) sera noté x = y. Ce prédicat est caractérisé par deux axiomes supplémentaires:

1. x(x = x)
2. xy[(f(x) ^ (x = y)) ==> f(y)]

Le second axiome traduit la transitivité de la relation d'égalité; il suffit de remplacer le prédicat f(x) par l'égalité z = x pour obtenir

xy[((z = x) ^ (x = y)) ==> (z = y)]

Si on prend maintenant le prédicat f(t): t = x alors on obtient:

xy[((x = x) ^ (x = y)) ==> (y = x)]

c'est-à-dire la symétrie de la relation d'égalité.

Pour pouvoir utiliser les méthodes de déduction naturelle avec ces nouveaux axiomes, il faut modifier légèrement les règles et introduire une nouvelle règle:

m V ~(y = x) V A(y) V n devient m V A(x) V n règle [~=]

avec y ne figurant pas dans m ou dans n. En effet on peut dire que ~(y = x) V A(y) a la même valeur de vérité que A(x).

Le calcul des prédicats permet de traiter des notions nouvelles comme par exemple:

xy[((x est un dieu) ^ (y est un dieu)) ==> (x = y)]

qui signifie il y a au plus un dieu alors que l'expression suivante:

x[(x est un dieu) ^ y[(y est un dieu) ==> (x = y)]]

signifie qu'il y a exactement un dieu. Enfin l'expression

xy[f(x) ^ f(y) ^ ~(x = y)]

exprime qu'il y a au moins deux éléments qui vérifient le prédicat f.

Naturellement le calcul des prédicats avec égalité restreinte est aussi complet.

Conclusions

Nous venons de passer rapidement en revue le calcul des prédicats pur qui est le système à la base de toutes les théories mathématiques un peu évoluées. Ce système est trop simple pour fonder les mathématiques. Il ne contient que des prédicats d'ordre 1, que le mathématicien appellerait des relations. Il ne contient pas de constructeurs permettant de construire une nouvelle variable d'individu à partir d'autres, comme la fonction successeur par exemple. Il ne permet pas de raisonner sur les prédicats eux-mêmes.

Si on introduit des prédicats d'ordre supérieur prenant comme variables d'autres prédicats, on aboutit à la théorie des types de Bertrand Russell. On peut y définir le concept de nombre et de classe et démarrer une théorie des ensembles.

On sait depuis les célèbres travaux de Godel qu'une théorie formelle contenant l'arithmétique n'est pas complète et qu'elle contient des enoncés vrais indémontrables dans le système.