Théorie de la preuve

La théorie de la preuve est la branche de la logique mathématique qui s’intéresse à la modélisation du raisonnement mathématique. Développée au début du siècle par Hilbert, Gödel, et les autres pionniers de la logique formelle, elle revenue à la mode à partir des années ‘50 grâce au développement de l’informatique et de l’intelligence artificielle ; elle est en effet à la base des preuves assistées par ordinateur et de la certification de code.

Normalement on présente la théorie de la preuve du Calcul des prédicats, car c’est de cette théorie qui découlent les résultats les plus intéressants. Néanmoins dans ce cours nous mettons l’accent sur la théorie de la preuve du Calcul des propositions, qui constitue un sous-ensemble de la précédente.

Calcul des propositions

En Calcul des propositions, les notions de modèle et de vérité permettent de vérifier aisément (et en temps fini) si une formule donnée est valide ou pas. Néanmoins, quand un mathématicien veut montrer un théorème il ne commence pas par énumérer toutes les possibilités et vérifier que son énoncé reste vrai pour n’importe quel choix. C’est pour modéliser la façon de raisonner du mathématicien qu’on a développé le concept de preuve formelle.

La méthode de démonstration universellement acceptée en mathématiques est la méthode axiomatique. Un ensemble de vérités élémentaires, appelées axiomes, est initialement établi et accepté comme vrai sans aucune preuve. En général sont choisis comme axiomes des énoncés qui paraissent évidents et consensuels, comme par exemple “deux droites parallèles ne se rencontrent en aucun point”.

À partir des axiomes, le mathématicien s’autorise à déduire des théorèmes en appliquant un nombre restreint et universellement accepté de formes de raisonnement appelées règles d’inférence ou de déduction. La preuve est donc une opération purement syntaxique qui transforme des formules vraies en d’autres formules vraies indépendamment de la notion sémantique de vérité.

On appelle système de déduction (ou de preuve) le choix d’un ensemble d’axiomes et de règles d’inférence. Pour tout système formel ce choix n’est pas unique, et plusieurs systèmes de preuve différents vont aboutir aux mêmes théorèmes.

Définitions et notations

Un système de preuve pour le calcul propositionnel est la donne d’un ensemble (éventuellement infini ou même vide) de formules appelées axiomes, et d’un nombre fini de règles d’inférence. Une règle d’inférence est constitué d’une ou plusieurs prémisses et d’une conséquence.

On dit qu’une formule est un théorème

La suite des applications des règles d’inférence qui permettent de dériver un théorème est appelée une preuve de . Si on a une preuve de , on dit aussi qu’on a démontré .

Si une formule est un théorème on écrit

Si est un ensemble de formules, et si en ajoutant aux axiomes on peut démontrer une formule , on dit que est dérivable de (ou que est une conséquence syntaxique de ) et on écrit

On dit qu’un système de preuve est

Déduction naturelle

Il y a plusieurs systèmes de preuve corrects et complets pour le calcul des propositions. Parmi eux, nous nous intéressons principalement à la déduction naturelle, car plus proche de la façon naturelle de penser.

La déduction naturelle se caractérise par un ensemble d’axiomes vide et par des règles d’inférence qui sont généralement notées à l’aide de séquents, c’est à dire des expressions de la forme

Par exemple, la règle d’introduction de la conjonction

est à interpréter comme

« si on peut démontrer à partir de et si on peut démontrer à partir de , alors on peut démontrer à partir de . »

Voici la liste complète des règles de la déduction naturelle

Hypothèse
Tiers exclus
Affaiblissement
Élimination du faux
Introduction du et
Élimination du et
 
Introduction du ou
 
Élimination du ou
Modus ponens
Déduction

Exemple de preuve

Une preuve en déduction naturelle est une suite d’applications des règles d’inférence. L’écriture sous forme de séquents permet de représenter une preuve par un arbre de preuve. Par exemple, la preuve de (sous les hypothèses , et on peut prouver ) a la forme suivante :

Exercice : Prouver le théorème .

Exercice : Prouver .

Règles dérivées

La liste des règles d’inférence de la déduction naturelle est assez restrictive, et elle ne contient pas certaines formes de raisonnement très courantes comme par exemple

Cependant, il est pratique d’isoler certains enchaînements courants de règles pour en faire des règles dérivées. On peut ainsi réutiliser ces nouvelles règles dans des preuves complexes sans avoir à réécrire toute la preuve.

Par exemple, de l’extrait de preuve suivante

on déduit la règle de réduction à l’absurde

Exercice : Indiquer quelles règles ont été utilisées dans la preuve ci-dessus.

Exercice : Donner des preuves pour les deux règles dérivées

Exercice : La liste de règles non dérivées donnée dans la section précédente n’est pas la seule possible. Montrer que la règle du tiers exclus est dérivable de la réduction à l’absurde et des autres règles.

Autres systèmes de preuve

La déduction naturelle n’est pas le seul système de preuve correct et complet, ni historiquement premier.

Systèmes à la Hilbert

Les systèmes à la Hilbert se caractérisent par l’emploi de la seule règle du modus ponens, exprimée par le séquent

On remarquera que la notation est simplifiée par rapport à la déduction naturelle à cause de la disparition du symbole , inutile dans ce contexte.

D’un autre côté, les systèmes à la Hilbert possèdent un nombre relativement grand d’axiomes (de trois jusqu’à la dizaine). Voici un exemple de système d’axiomes à la Hilbert dû à Frege:

  1. ,
  2. ,
  3. ,
  4. ,
  5. ,
  6. .

Un exemple de preuve dans le système de Frege est le suivant:

où les deux prémisses du modus ponens sont obtenues par instanciation des axiomes 2 et 1 respectivement. On conclut que

Comme dans la déduction naturelle, on peut démontrer dans un système à la Hilbert des résultats conditionnels où un théorème est dérivable d’une ou plusieurs hypothèses. Par exemple on montre qu’à partir des hypothèses et on peut prouver (ce qui est un peu bête, admettons); en symboles:

La preuve procède ainsi (par convention, on met une barre au dessus des prémisses qui ne sont pas des axiomes, comme si on avait utilisé la règle en déduction naturelle):

Théorème de déduction

La principale différence entre les systèmes à la Hilbert et la déduction naturelle est le manque de la règle de déduction

On peut cependant prouver un méta-théorème, dit théorème de déduction qui permet de simplifier grandement les preuves. Ce théorème affirme que si et sont deux formules on peut prouver

dans un système à la Hilbert si et seulement si on peut prouver

Si passer de la deuxième preuve à la première revient juste à appliquer une fois le modus ponens, la construction explicite qui permet de passer de la première preuve à la deuxième est assez longue et compliquée, mais il est important (et confortant) de savoir qu’elle existe et est automatique. Ceci est à comparer avec la déduction naturelle, où les deux passages sont immédiats.

On remarque que la règle et le théorème de déduction donnent un fondement formel à une technique de preuve utilisée largement en mathématiques: pour prouver un énoncé de la forme , on commence par supposer et on démontre .

Système de Łukasiewicz

Łukasiewicz démontre que les trois schémas d’axiomes suivants

  1. ,
  2. ,
  3. ,

avec le modus ponens sont suffisants à définir un système de preuve complet (et correct). Dans les Exercices on peut trouver quelques questions autour de systèmes similaires à celui de Łukasiewicz.

Extensions conservatives des systèmes à la Hilbert

Par souci de coincision, il est classique de présenter les systèmes à la Hilbert en utilisant seulement les symboles et . Il est bien évidemment possible d’étendre ces systèmes en ajoutant les symboles , etc. Pour cela, il suffit d’ajouter quelques axiomes de plus; par exemple:

  1. ,
  2. ,
  3. ,
  4. .

Séquents de Gentzen

Voir http://fr.wikipedia.org/wiki/Calcul_des_séquents.

Calcul des prédicats

La théorie de la preuve du Calcul des prédicats est à peine plus riche de celle du calcul des propositions. Il s’agit, en effet, d’ajouter simplement les règles d’inférence concernant les quantificateurs. Comme pour les autres connecteurs logique, chacun des quantifieurs et va avoir une règle d’introduction et une règle d’élimination.

On rappelle qu’une variable dans un prédicat est dite libre si elle n’est pas quantifiée, et liée sinon. Si est libre dans et si est une nouvelle variable, on note le prédicat obtenu en remplaçant toutes les occurrences libres de par . De la même façon, si est un terme, on note le prédicat obtenu en remplaçant toutes les occurrences libres de par . Voir aussi la syntaxe du Calcul des prédicats.

Voici finalement les règles pour et . Dans ces règles et sont des variables, et est un terme quelconque. La variable ne doit pas apparaître libre dans ou dans  ; de façon équivalente, les règles et ne doivent pas contenir la variable libre dans les conclusions.

Généralisation
Spécialisation
Introduction de l’existentiel
Élimination de l’existentiel

Intuitivement, la règle de généralisation dit que si on peut prouver sans faire d’hypothèses sur , alors est vrai pour tout . Par exemple, si on peut prouver sans faire d’hypothèse sur , alors on peut conclure . L’élimination de l’existentiel a une interprétation similaire.

L’introduction de l’existentiel dit que si on peut prouver pour un terme spécifique , alors on peut conclure qu’il existe un terme qui rend vrai . Par exemple, si on peut démontrer que , alors on peut conclure que . La règle de spécialisation a une interprétation similaire.

Excercice : donner des exemples concrets de dérivations utilisant la règle de spécialisation ou la règle d’élimination de l’existentiel.

Bibliographie

Fork me on GitHub