Le mot le plus employé dans une copie de mathématiques est probablement « donc ». C’est aussi celui qu’on n’explique jamais. On corrige les calculs, on sanctionne les erreurs de signe, mais on laisse dans l’ombre la question centrale : à quelle condition a-t-on le droit d’écrire « donc » ?

La logique du premier ordre répond avec une précision déconcertante. Cet article poursuit la série ouverte par Syntaxe et sémantique, dont il reprend les notations.

1. Ce qu’est une démonstration

Définition. Soit un ensemble de formules. Une démonstration de à partir de est une suite finie de formules telle que et que chaque soit, au choix, un axiome logique, un élément de , ou le résultat de l’application d’une règle de déduction à des formules qui la précèdent dans la suite.

Trois traits de cette définition méritent qu’on s’y arrête. Elle est finie : une démonstration a un dernier mot. Elle est linéaire : chaque ligne ne dépend que de celles qui la précèdent. Et surtout elle est purement syntaxique : nulle part il n’est question de vérité, de modèle, ni de sens. On écrit lorsqu’une telle suite existe.

2. Les règles

On pourrait croire qu’il en faut beaucoup. Il en suffit de deux.

Modus ponens, ou règle de détachement. De et de , on déduit .

Généralisation. De , on déduit , pourvu que ne soit libre dans aucune hypothèse utilisée.

La restriction sur la généralisation n’est pas un détail technique. Sans elle, de l’hypothèse «  est pair » on déduirait « tout entier est pair ». C’est la formalisation exacte du « soit quelconque » que l’on écrit en tête de démonstration : est quelconque précisément parce qu’aucune hypothèse ne le contraint.

Tout le reste — la logique propositionnelle entière — tient dans trois schémas d’axiomes, valables pour toutes formules , , :

Deux règles, trois schémas. Toute démonstration mathématique, si longue soit-elle, se ramène en principe à cet assemblage. En principe seulement : personne n’écrit ainsi, pas plus qu’on ne rédige un logiciel en code machine.

3. Le théorème qui autorise « supposons »

Pour démontrer une implication, tout le monde écrit : supposons — alors… — donc ; par conséquent . Ce geste, si naturel qu’on ne le remarque plus, n’est pas une règle primitive. C’est un théorème.

Théorème de la déduction. Si , alors .

Il se démontre par récurrence sur la longueur de la démonstration, et les deux premiers schémas d’axiomes y jouent exactement le rôle pour lequel ils ont été choisis. Sans ce théorème, l’écriture mathématique ordinaire serait injustifiable.

4. Ce qui n’est pas une règle

La liste des règles étant close, tout ce qui n’y figure pas est interdit. Deux figures fautives reviennent sans cesse dans les copies, et elles ressemblent toutes deux, de loin, au modus ponens.

L’affirmation du conséquent conclut à partir de et de . Prenons « si est divisible par 4, alors est pair », avec : l’implication est vraie, la conclusion «  est pair » est vraie, et pourtant 6 n’est pas divisible par 4.

La négation de l’antécédent conclut à partir de et de . Même exemple : 6 n’est pas divisible par 4, mais il reste pair.

Dans les deux cas, l’erreur consiste à traiter l’implication comme une équivalence. Elle a un nom en classe — « confondre une proposition et sa réciproque » — mais on la désigne rarement comme ce qu’elle est : l’usage d’une règle de déduction qui n’existe pas.

5. Les règles dérivées, et leur prix

La contraposition, elle, est parfaitement légitime : et sont interdéductibles, le troisième schéma d’axiomes donnant un sens et le théorème de la déduction l’autre.

Le raisonnement par l’absurde demande davantage de soin, car il recouvre deux gestes distincts que l’enseignement confond.

• Pour établir une négation , on suppose et l’on dérive une contradiction. Ce geste ne coûte rien : c’est la définition même de la négation.
• Pour établir une affirmation , on suppose et l’on dérive une contradiction. On conclut alors de à — et ce pas supplémentaire n’est pas gratuit.

Le second repose sur l’élimination de la double négation, équivalente au principe du tiers exclu, lui-même contenu dans le troisième schéma d’axiomes. Les logiques intuitionnistes le refusent, et perdent du même coup les démonstrations d’existence qui n’exhibent aucun objet. C’est une position cohérente, pas une lubie : elle exige seulement que « il existe » signifie « on sait construire ».

Un élève à qui l’on présente le raisonnement par l’absurde comme une évidence perd donc une information : il utilise, sans le savoir, le seul axiome de la liste qui soit discutable.

6. Vérifier est facile, trouver ne l’est pas

Puisqu’une démonstration est une suite finie de formules dont chacune est justifiée par un critère mécanique, contrôler une démonstration est une opération décidable. Une machine y suffit, et c’est ce que font les assistants de preuve.

En trouver une est d’une autre nature. Church et Turing ont établi en 1936 qu’aucun algorithme ne peut décider, pour un énoncé quelconque du premier ordre, s’il est démontrable. On peut certes énumérer mécaniquement toutes les démonstrations possibles, si bien qu’une démonstration existante finira par apparaître ; mais rien ne permet de savoir, devant un énoncé qui résiste, s’il faut chercher encore ou renoncer.

Cette asymétrie explique une expérience familière à tout élève : une démonstration, une fois lue, paraît limpide, et l’on ne comprend pas de ne pas l’avoir trouvée. Ce n’est pas un défaut d’intelligence. Lire et chercher ne sont pas la même opération, et la seconde n’a pas de méthode.

---

Le prochain article de la série propose cinq raisonnements, dont un seul est correct, et invite à nommer la règle violée dans chacun des autres. Les règles de déduction et leurs conditions d’emploi sont exposées au chapitre 2 du Discours formel sur les mathématiques pour le secondaire.