Logique (mathématiques)/Déduction naturelle
La déduction naturelle est une façon d'exposer les principes de la logique mathématique pour les rendre aussi proches que possible des façons naturelles de raisonner.
Les origines de la déduction naturelle modifier
L’histoire des théories de la déduction a suivi un cheminement curieux. De nombreux logiciens dont Bertrand Russell et Alfred North Whitehead avec leurs Principia Mathematica ont développé la logique sous une forme axiomatique. Les lois logiques sont déduites à partir d’axiomes logiques, d’une façon qui ressemble à la méthode euclidienne, au moins aux yeux de ceux qui faisaient ces déductions. Cette méthode pouvait sembler relativement naturelle tant qu’on choisissait comme axiomes des lois dont la vérité logique était évidente. Mais le souci de formuler des systèmes d’axiomes aussi réduits que possible a conduit parfois à des formalismes où l’on déduit des vérités logiques évidentes à partir d’autres qui ne le sont pas. Les méthodes des logiciens permettaient de justifier tous les raisonnements dont la validité était reconnue mais elles étaient très éloignées de l’idéal d’évidence naturelle que l’on attend de la logique.
Gerhard Gentzen est le premier à avoir développé des formalismes qui redonnent à la logique le caractère d’un cheminement naturel. La principale idée de départ de Gentzen était simple : pas d’axiomes logiques, mais uniquement des règles de déduction et autant qu’il en faut pour reproduire toutes les formes élémentaires et naturelles de raisonnement. Pour réaliser cette idée, Gentzen a développé un formalisme où les déductions ne sont pas des suites de phrases mais des arbres, faits de colonnes de phrases qui se rejoignent jusqu’à la conclusion. Cette méthode est très suggestive pour l’intuition et elle a conduit Gentzen à faire de belles découvertes, mais elle nuit à l’idée originale qui était de reproduire les formes naturelles de raisonnement. Frederic Brenton Fitch a modifié la méthode de Gentzen en renonçant aux déductions arborescentes. Les déductions de Fitch ne sont cependant pas de simples suites de phrases. Pour donner à une déduction un caractère naturel, il faut faire apparaître des relations de dépendance entre les phrases. Au lieu d’une forme arborescente, la méthode de Fitch se sert seulement de barres verticales. Une assertion dépend des phrases qui sont au-dessus d’elle sauf de celles qui sont décalées sur la droite par ces barres. Cette règle simple permet de faire des déductions à la fois formelles et naturelles. Dans ce cours, il n’y aura pas de barres verticales, mais seulement de suites de ronds « °°°°° » pour décaler les phrases vers la droite. Une phrase dépendra de toutes les hypothèses qui sont au-dessus d’elle sauf de celles qui sont décalées vers la droite. Les hypothèses sont des axiomes ou des hypothèses provisoires. Elles seront indiquées avec la mention (hyp) ou (axiome).
Les règles de déduction pour les quatre opérateurs booléens fondamentaux modifier
Les règles de déduction permettent d’enchainer logiquement les phrases, c’est-à-dire introduire de nouvelles phrases comme conséquences logiques de ce qui a été dit auparavant. À chacun des opérateurs logiques fondamentaux sont associées deux règles de déduction.
La règle du détachement modifier
Pour l’opérateur d’implication, la règle du détachement, ou du modus ponens énonce que, des deux phrases « P » et « si P alors Q », on peut déduire « Q ». Elle permet de passer de conditions déjà connues, P, à des conditions nouvelles, Q, pourvu qu’il y ait une loi qui l’autorise, si P alors Q.
Formellement, on note : .
La règle de l'abandon d’une hypothèse provisoire modifier
L’autre règle pour l'opérateur d'implication est elle aussi très naturelle mais elle est plus difficile à formuler. Lorsqu’on veut démontrer une implication de la forme « si P alors Q », on procède souvent de la façon suivante : on pose P comme une hypothèse provisoire, on fait alors des déductions à partir de toutes les phrases antérieures plus P en vue d’atteindre Q. On a alors démontré Q sous l’hypothèse P ainsi que sous toutes les autres hypothèses. On peut alors en déduire « si P alors Q ». Insistons sur un point : Q est démontrée sous l’hypothèse P mais pas « si P alors Q », qui elle ne dépend que des prémisses antérieures. Avec la méthode de Fitch, on peut introduire n’importe quand dans une déduction une hypothèse provisoire: il suffit de la décaler vers la droite par rapport aux autres prémisses, et tout ce qui est déduit sous une hypothèse provisoire doit être sous elle ou sur sa droite mais jamais sur sa gauche. La deuxième règle de déduction pour l’implication postule donc que si on a déduit Q sous l’hypothèse provisoire P alors on peut déduire si P alors Q sans cette hypothèse, on peut donc décaler si P alors Q sur la gauche par rapport à P, mais pas par rapport aux autres prémisses utilisées dans la démonstration de Q. On l’appellera la règle de l’abandon d’une hypothèse provisoire.
Montrons qu’avec ces deux règles on peut déduire si P alors R à partir des deux phrases si P alors Q et si Q alors R :
1 si P alors Q (hyp)
2 si Q alors R (hyp)
3 P (hyp provisoire)
4 Q (Modus.Ponens entre la ligne 1 et 3)
5 R (Modus.Ponens entre la ligne 4 et 2)
6 si P alors R
Les lignes 1 et 2 sont les prémisses. 3 introduit une hypothèse provisoire. 4 est déduit à partir de 1 et 3 en vertu de la règle de détachement, de même pour 5 à partir de 2 et 4. 6 est la conclusion. Elle est obtenue à partir de 3 et 5 en vertu de la règle de l’abandon d’une hypothèse provisoire.
Les règles de l'analyse et de la synthèse modifier
Pour la conjonction, les règles sont très simples : à partir de la phrase (A et B) on peut déduire les deux phrases A et B prises séparément (règle de l'analyse), et à partir des deux phrases A et B on peut déduire la phrase (A et B) (règle de la synthèse). Ces règles permettent d’assembler ou au contraire de séparer des assertions qui sont toutes considérées comme vraies. C’est la forme logique de la capacité de la raison à analyser le monde, c’est-à-dire à étudier ses parties séparément, et à le synthétiser, c’est-à-dire à rassembler les éléments d’une étude en un tout. C’est pourquoi ces règles sont ici appelées les règles de l’analyse et de la synthèse.
Les règles de disjonction des hypothèses et de l'affaiblissement d’une thèse modifier
Les deux règles de déduction pour la disjonction sont :
- la règle de la disjonction des hypothèses : à partir des deux phrases, si P alors R et si Q alors R on peut déduire si (P ou Q) alors R;
- la règle de l’affaiblissement d’une thèse : à partir de la phrase P on peut déduire les deux phrases (P ou Q) et (Q ou P) quelle que soit la phrase Q.
La règle de disjonction des hypothèses sert quand on examine plusieurs cas possibles qui conduisent à la même conclusion. On peut aussi la formuler d’une façon équivalente : si on a démontré R une fois sous l’hypothèse provisoire P, une autre fois sous l’hypothèse provisoire Q, alors on peut en déduire si (P ou Q) alors R. La règle de l’affaiblissement d’une thèse, quant à elle, peut sembler peu intéressante mais elle est en vérité très importante. Parfois il est avantageux de prouver (P ou Q) après avoir prouvé P.
Le principe du raisonnement par l'absurde modifier
Le principe du raisonnement par l’absurde est une règle de déduction pour la négation. Si on démontre une contradiction à partir d’une hypothèse alors celle-ci est nécessairement fausse et donc sa négation est vraie. Plus formellement, si dans une déduction sous l’hypothèse provisoire P on a trouvé une contradiction (Q et non Q) alors on peut déduire nonP à partir de toutes les prémisses antérieures sauf P. On décale donc non P sur la gauche par rapport à P.
(…)
°°°°° P (hyp)
°°°°° (…)
°°°°° Q et non Q
non P
Ici on suppose que (Q et non Q) a été démontrée à partir de P et des autres prémisses antérieures.
On peut aussi formuler une règle équivalente et plus simple : quelle que soit la phrase Q, on peut déduire nonP à partir de si P alors (Q et nonQ).
La règle de la suppression de la double-négation modifier
La seconde règle pour la négation est la règle de la suppression de la double négation. De non nonP on peut déduire P. Quand on considère que toute phrase est nécessairement ou bien vraie ou bien fausse, la validité de cette règle est évidente. Elle est caractéristique de la logique dite classique, qui est présentée ici. Elle est acceptée par la grande majorité des scientifiques. Elle a pourtant été contestée à cause d’un problème important, celui des preuves d’existence par l’absurde. Il arrive que l’on puisse prouver qu’un problème a une solution sans être capable de la trouver. Pour cela il suffit de prouver que l’absence de solution conduit à une contradiction. Le raisonnement par l’absurde permet alors de conclure qu’il n’est pas vrai que le problème n’a pas de solution : non non (le problème a une solution). Il faut alors supprimer la double négation pour en conclure que le problème a une solution. Certains mathématiciens et logiciens, dont Brouwer, ont contesté cette méthode et se sont opposés à Hilbert qui la défendait et qui l’avait brillamment mise à profit. Ils estimaient qu’une preuve d’existence n’a pas de sens tant qu’on ne peut pas effectivement montrer ce qui existe. On pourrait dire qu’ils ne croient que ce qu’ils voient.
La grande majorité des travaux mathématiques sont effectués dans le cadre de la logique classique, mais il y a aussi des mathématiques intuitionnistes.
On peut introduire d’autres règles pour les autres opérateurs booléens, notamment l’opérateur d’équivalence, mais ce n’est pas nécessaire, parce que ces opérateurs peuvent être définis à partir des précédents et que leurs règles de déduction peuvent être alors déduites à partir des règles précédentes. (P équivaut à Q) est défini par ( (si P alors Q) et (si Q alors P) ) .
L’usage des noms de variable dans les théories du premier ordre modifier
Les règles de déduction pour les opérateurs universels et existentiels gouvernent l’usage des noms de variable. Cet usage donne à une théorie la puissance de la généralité, c’est-à-dire la possibilité de connaître non chaque individu pris isolément mais tous les individus d’un même genre, en une seule phrase.
Les règles d’usage des variables précisent à quelles conditions on peut introduire des noms de variable et ce qu’on peut alors dire à leur sujet. Ces règles sont naturelles mais il y a quelques difficultés techniques à propos des notions de terme, d’occurrence libre ou liée d’une variable, de substitution d’un terme aux occurrences d’une variable et de substitution d’une variable aux occurrences d’un terme.
Pour qu’une théorie puisse utiliser la logique du premier ordre, il faut avoir défini un domaine d’objets et il faut que les prédicats attribués par la théorie à ses objets ne soient pas eux-mêmes des objets de la théorie.
La signification d’un nom de variable d’objet, c’est de représenter un objet quelconque de la théorie : soit x un nombre. Souvent on introduit un nom de variable dans des prémisses qui déterminent des conditions générales sur cet objet. x est un objet quelconque de la théorie pourvu seulement qu’il satisfasse à ces conditions : soit x un nombre premier… Une théorie contient en général des noms pour ses objets. La théorie des nombres entiers contient par exemple des noms pour tous les nombres : 0, 1, 2…, -1, -2…
Les termes peuvent être simples ou composés. Ce sont les noms d’objet, les noms de variable d’objet, et toutes les expressions composées que l’on peut former à partir d’eux en appliquant les opérateurs d’objets de la théorie. Par exemple, 1, x, x+1et (x+x)+1 sont des termes de la théorie des nombres.
Rappelons d’abord la très importante distinction entre les variables liées par un opérateur et les autres, les variables libres. Les occurrences d’un nom de variable dans une phrase sont tous les endroits où ce nom apparait. Une occurrence peut être libre ou liée. Quand un opérateur existentiel ou universel en x est appliqué à une phrase complexe, toutes les occurrences de x deviennent liées par cet opérateur. Toutes les occurrences qui ne sont pas ainsi liées sont libres.
Si une phrase contient plusieurs opérateurs existentiels et universels, il est souhaitable que ces opérateurs portent tous sur des noms de variable différents. Cette règle n’est pas indispensable. Elle n’est pas respectée lorsque l’on met le calcul des prédicats sous la forme d’une algèbre cylindrique (une algèbre cylindrique est une algèbre de Boole complétée par des lois particulières aux opérateurs universels et existentiels). Mais elle est toujours respectée en pratique parce qu’elle permet d’éviter des confusions.
Une phrase est obtenue à partir d’une autre par substitution d’un terme t aux occurrences d’une variable x lorsque toutes les occurrences libres de x ont été remplacées par t. Par exemple, (le père de x est humain et le père de x est honnête) est obtenu par substitution du terme le père de x à la variable y dans la formule (y est humain et y est honnête).
Ces préliminaires permettent de formuler les règles de déduction pour les opérateurs universels et existentiels.
La règle de singularisation modifier
À partir d’une phrase de la forme (pour tout x) P(x) , on peut déduire P(t) pour n’importe quel terme t dont les variables ne sont pas liées dans P(x). P(x) désigne une phrase quelconque qui contient x comme variable libre, P(t) désigne la phrase obtenue à partir de P(x) en y substituant t à toutes les occurrences libres de x. La règle de singularisation consiste simplement à appliquer une loi universelle à un cas singulier.
La règle de généralisation modifier
De P(x) on peut déduire (pour tout x)P(x) pourvu que le nom de variable x n’apparaisse jamais dans les hypothèses dont P(x) dépend. x peut avoir été introduit avec la règle de singularisation, dans une hypothèse provisoire qui a ensuite été écartée par la règle d’abandon, ou avec la règle d’affaiblissement.
Très souvent on introduit des variables dans des hypothèses provisoires. On raisonne ensuite sur elles comme si elles étaient des objets. On peut alors en déduire des lois générales, parce que ce qu’on a déduit est vrai pour tous les objets qui vérifient les mêmes hypothèses. Ce sont les règles d’abandon d’une hypothèse provisoire et de généralisation qui permettent de conclure.
La règle des preuves directes de l’existence modifier
À partir de la phrase P(t) on peut déduire il existe un x tel que P(x) pour toute variable x qui n’apparait pas dans P(t) et pour tout terme t dont les noms de variables ne sont pas liés dans P(t).
P(t) désigne une phrase quelconque qui contient au moins une fois le terme t. P(x) est obtenue à partir de P(t) en substituant x à t à une ou plusieurs de ses occurrences. Dans cette règle il n’est pas nécessaire de substituer x à toutes les occurrences de t.
La règle des conséquences de l’existence modifier
La phrase il existe un x tel que P(x) peut avoir du sens même quand on ne connait pas ce x, parce qu’elle a des conséquences. Pour les déduire on introduit une nouvelle hypothèse provisoire P(y) où y est un nom de variable qui n’a jamais été utilisé auparavant et où P(y) est obtenu à partir de P(x) en substituant y à toutes les occurrences de x. On peut alors raisonner sous cette hypothèse. La règle des conséquences de l’existence permet alors de conclure mais elle est un peu compliquée à énoncer :
De la phrase il existe un x tel que P(x) on peut déduire R lorsque R a été déduit sous l’unique hypothèse provisoire supplémentaire P(y) et qu'y n’apparait ni dans les prémisses antérieures à P(y) ni dans R.
y est une sorte d’être hypothétique. Il ne fait que servir d’intermédiaire dans une déduction mais il n’apparait ni dans ses prémisses, ni dans sa conclusion.
À ces douze règles, ou quatorze, si on compte qu’il y a deux règles d’analyse et deux règles d’affaiblissement, il faut en ajouter une quinzième, très simple, la règle de répétition : on peut toujours répéter une thèse antérieure, sauf si elle dépend d’une hypothèse qui a été abandonnée. On peut donc répéter toutes les thèses tant qu’on ne les décale pas sur la gauche. Cette règle est nécessaire quand on veut répéter une prémisse dans une conclusion ou quand on a besoin d’une thèse antérieure dans le corps d’une déduction sous hypothèse provisoire pour appliquer une règle.
Ces quinze règles suffisent pour faire toutes les déductions dont on a besoin dans les sciences. Même les théories des ensembles peuvent utiliser la logique du premier ordre.
Pour chaque opérateur, il y a une règle d’introduction et une règle d’élimination, sauf pour la règle de la disjonction des hypothèses. Mais on peut éliminer une disjonction, en passant de (PouQ) à R à l’aide de si P alors R , de si Q alors R et de la règle de disjonction des hypothèses. Introduction et élimination sont nécessaires pour pouvoir démonter et remonter des formules. La recherche d’une déduction logique consiste justement à analyser les prémisses, c’est-à-dire à les démonter, et à réassembler les morceaux pour faire des formules que l’on peut enchainer logiquement jusqu’à la conclusion. On croit parfois qu’il est très difficile de faire des preuves mathématiques, mais dans son principe, ce n’est pas très différent d’un jeu de construction avec des cubes.
Comment vérifier la correction d’un raisonnement ? modifier
La liste des quinze règles précédentes est complète au sens où elle suffit pour faire toutes les déductions correctes. Kurt Gödel a prouvé, (Théorème de complétude du calcul logique, 1929) pour un système logique différent, mais équivalent à celui qui vient d’être présenté, qu’il suffit pour formaliser toutes les déductions correctes du calcul des prédicats du premier ordre.
Les déductions correctes sont d’abord toutes celles qui respectent rigoureusement ces règles fondamentales. Toutes les phrases doivent être ou bien des axiomes, ou bien des hypothèses provisoires, ou bien des conséquences des phrases qui les précèdent en vertu de l’une des quinze règles. On peut élargir la classe des déductions correctes en autorisant l’usage de règles dérivées. Une règle dérivée est correcte lorsqu’on peut montrer que tout ce qui peut être déduit avec elle peut aussi être déduit sans elle avec seulement les règles fondamentales. En pratique les règles logiques dérivées sont utilisées de façon implicite. C’est pourquoi il faut étudier un peu de logique, au-delà de la seule connaissance des règles fondamentales, pour savoir reconnaitre si un raisonnement est correct. Mais les règles couramment utilisées sont peu nombreuses et cette étude peut être assez rapide.
Tant que les déductions sont formalisées, il est toujours possible de reconnaitre si oui ou non une déduction est correcte parce que les règles de déduction sont en nombre fini, quinze si l’on se contente des règles fondamentales, et qu’il est toujours possible de vérifier en un temps fini si oui ou non une formule est la conséquence d’une ou plusieurs autres en vertu de l’une de ces règles. Même un ordinateur peut savoir reconnaitre si une déduction est correcte. La méthode est opératoire, effective, efficace. Elle marche toujours. Elle réalise une partie du programme appelé parfois finitaire proposé par David Hilbert pour résoudre les problèmes des fondements des mathématiques. Hilbert cherchait une méthode efficace, éventuellement très compliquée à mettre en pratique, qui permette de décider pour tout énoncé mathématique si oui ou non il est un théorème, c’est-à-dire une vérité mathématique. Le calcul des prédicats permettait de ramener le problème à la question de savoir si oui ou non une formule est une loi logique. On sait aujourd’hui, depuis le Théorème d'incomplétude de Gödel (1931), que ce programme finitaire de Hilbert n’est pas complètement réalisable. S’il était complètement réalisable, on pourrait programmer un ordinateur pour le rendre capable de discerner la vérité mathématique dans tous les cas. On peut le faire pour certaines théories mathématiques importantes, mais pas pour la théorie des nombres. En revanche, le théorème de complétude montre qu’il est toujours possible de savoir si oui ou non une déduction formelle est correcte.
La vérification de la correction des déductions dans la langue courante pose davantage de difficultés. Il faut d’abord traduire les phrases familières dans une langue formalisée du calcul des prédicats. Cette étape pose parfois problème si on a des doutes sur la fidélité de la traduction. Mais la plus grosse difficulté vient de ce que les déductions courantes font en général une large place à l’implicite. Même les relations de dépendance par rapport à une hypothèse ne sont pas toujours explicitées. Les déductions formelles au contraire ne laissent rien dans l’ombre. Celles qui sont ici proposées sont très semblables aux déductions courantes sauf qu’elles explicitent tout. Les méthodes formelles ne suffisent pas en pratique pour savoir toujours reconnaître si les raisonnements d’autrui sont corrects, parce qu’elles requièrent l’explicitation de tout ce qui est implicite. C’est pourquoi souvent il faut beaucoup étudier et connaître tout l’implicite avant de savoir si un raisonnement est correct.
Les lois logiques sont des vérités anhypothétiques modifier
Pour les méthodes de déduction naturelle, il n’y a pas d’axiomes logiques. Mais cela n’empêche pas de prouver la validité des lois logiques. Celles-ci sont des conclusions de déductions sans hypothèses, sans axiomes. C’est possible parce qu’on est libre d’introduire des hypothèses provisoires que l’on abandonne par la suite. Toutes les lois logiques peuvent être ainsi déduites :
- le principe de non-contradiction. Pour toute phrase P, non(P et nonP) est vrai,
- le principe du tiers exclu. Pour toute phrase P, (P ou nonP) est vrai,
et beaucoup d’autres en nombre infini.
On ne sait pas toujours reconnaître si une formule est oui ou non une loi logique. Quand on n’a pas trouvé de déduction anhypothétique d’une formule, on n’est pas toujours sûr qu’il n’en existe pas. Dans de nombreux cas on peut montrer qu'oui la formule n’est pas une loi logique, mais il n’y a pas de méthode universelle qui marche dans tous les cas. On peut déduire des théorèmes d’incomplétude qu’une telle méthode ne peut pas exister. Quand il est impossible de trouver une méthode qui permette de répondre dans tous les cas à une question générale, on dit qu’il s’agit d’une question indécidable. Cela ne veut pas dire qu’on ne trouve jamais de réponse mais seulement qu’on ne peut pas espérer les trouver toutes. La question si une formule est une loi logique est une des nombreuses questions dont l’indécidabilité a été démontrée.
Au point de vue formel, il faut distinguer une règle de déduction et une loi logique bien qu’elles soient deux notions très voisines. Une règle de déduction énonce qu’il est correct de déduire une phrase à partir de phrases antérieures. Une loi logique est une formule qui énonce une vérité universelle, vraie dans tous les mondes possibles. Il n’y a que quinze règles fondamentales de déduction naturelle alors que les lois logiques sont en nombre infini. Mais la séparation entre loi logique et règle de déduction n’est tout de même pas très nette. Aux règles fondamentales on peut joindre des règles dérivées et celles-ci sont en nombre infini. Pour chaque règle de déduction, on peut définir des lois logiques qui disent essentiellement la même chose : si les conditions sont vraies, la conclusion l’est aussi. Inversement on peut se servir des lois logiques pour introduire des règles dérivées, parce que la preuve d’une loi logique peut être utilisée dans la preuve de dérivation. Les lois logiques et les règles de déduction sont deux aspects différents d’une même technique logique. Les Principia Mathematica mettaient l’accent sur les lois logiques, la déduction naturelle insiste au contraire sur les règles de déduction, mais les résultats obtenus sont finalement les mêmes. La déduction naturelle a quand même un avantage. Elle est plus facile à apprendre, à enseigner, et à appliquer.
