Formalisation des démonstrations

Formaliser les démonstrations revient à définir mathématiquement la notion de « être démontrable », avec des critères purement syntaxiques. Nous retrouvons l’idée de ramener le raisonnement à un calcul sur des signes qui était déjà le but de Leibniz (voir section 1.2.2 dans la première partie). Bien sûr, on veut que cette idée de démontrabilité préserve la vérité, c’est-à-dire que si la proposition B est démontrable à partir d’une proposition A, alors lorsque A est vraie, B est vraie 1. La première formalisation achevée est celle de Frege (voir la section 1.3.2 dans la première partie). Elle repose sur le principe suivant : on se donne un ensemble d’axiomes logiques et des règles permettant d’en déduire d’autres « lois logiques ». Dans un tel système axiomatique, une démonstration formelle est une suite finie de propositions (écrites dans une langue formelle) telle que chaque proposition est soit un axiome, soit obtenue par l’application d’une règle de déduction à partir de propositions qui se trouvent précédemment dans la suite. La dernière proposition est la proposition à démontrer. Cette approche est ensuite développée par Whitehead et Russell, puis par Hilbert.G. Gentzen n’est pas satisfait par de tels systèmes axiomatiques, et il veut « édifier un formalisme qui reflète le plus exactement possible les raisonnements logiques qui sont réel- lement utilisés dans les démonstrations mathématiques » (Gentzen, 1955, p. 17). Il propose alors un système qu’il appelle la déduction naturelle et dans lequel il n’y a pas d’axiomes : « la déduction naturelle ne part pas, en général, de propositions logiques fondamentales, mais d’hypothèses, auxquelles viennent se rattacher des déductions logiques. Grâce à une déduction ultérieure, le résultat est alors rendu indépendant des hypothèses 2 » (Gentzen, 1955, p. 19). Dans le système qu’il propose, les règles régissent le comportement des connecteurs et des quantificateurs. Elles sont de deux types : les règles d’introduction et les règles d’élimination.

Preuves dans le calcul des propositions

Dans la suite, je vais présenter le système de Hilbert et Ackermann (exposé dans Grundzüge der theoretischen Logik, 1928) pour le calcul des propositions et la déduction naturelle de Gentzen (exposée dans Recherches sur la déduction logique, 1934) pour le calcul des pro- positions et des prédicats. On peut trouver une présentation relativement simple (parfois d’ailleurs un peu trop sim- plifiée) de ces deux systèmes dans le livre Logique et raisonnement de M. Freund (Freund, 2011), et une présentation plus approfondie dans Logique. Méthodes pour l’informatique fondamentale de P. Gochet et P. Gribomont (Gochet & Gribomont, 1990). Comme dans le chapitre précédent, le but ici n’est pas de faire une présentation théorique, mais de mettre ces systèmes formels en relation avec les pratiques, notamment langagières, utilisées en mathématiques pour la rédaction des démonstrations. La déduction naturelle cherche à être plus proche du raisonnement naturel. Elle ne fonc- tionne qu’avec des règles, mais qui sont de nature plus générale que celles que l’on utilise dans les systèmes à la Hilbert, qui n’agissent que sur des propositions : les règles de la déduction naturelle agissent sur les démonstrations.

Une démonstration est un objet que l’on peut voir comme un texte composé de proposi- tions et de règles, mais il n’est pas nécessaire de définir explicitement cet objet. Le tout est de savoir qu’une démonstration possède des hypothèses : une suite finie de propositions, et une conclusion : une seule proposition. Une règle de déduction permet de construire une nouvelle démonstration à partir d’autres démonstrations. Une règle prend ainsi en argument des démonstrations, que l’on peut voir comme des textes déjà écrits, en ne te- nant compte que de la conclusion et des hypothèses de ces démonstrations. C’est à partir de ces démonstrations que la règle permet de poursuivre en produisant une nouvelle dé- monstration, avec toujours une nouvelle conclusion, et éventuellement une modification de la liste des hypothèses.On indique dans ce qui suit comment représenter graphiquement une démonstration : cette représentation donne à voir les règles qui ont permis, à partir des démonstrations élémentaires, d’arriver à la démonstration.