I. Motivation

Pour montrer qu'une formule est une tautologie, on peut calculer sa table de vérité... mais elle a lignes pour variables : c'est un coût exponentiel. Et en mathématiques, on ne démontre pas un théorème en essayant toutes les valeurs possibles : on fait un raisonnement, en enchaînant des étapes simples.

La déduction naturelle formalise ces raisonnements : on se donne des règles, et une preuve est un assemblage de règles.

II. Séquents et règles

La règle de base est l'axiome : on peut toujours conclure une de ses hypothèses.

III. Les règles de la déduction naturelle

Pour chaque connecteur, on a des règles d'introduction (pour prouver une formule qui a ce connecteur) et d'élimination (pour utiliser une hypothèse qui a ce connecteur).

a) Conjonction

Pour prouver " et ", on prouve les deux. Si on sait " et ", on sait chacune des deux.

b) Implication

Pour prouver "si alors ", on suppose et on prouve . La règle d'élimination est le modus ponens.

c) Disjonction

L'élimination de la disjonction est le raisonnement par cas : si on sait " ou ", et qu'on peut prouver dans les deux cas, alors on a .

d) Négation et absurde

On note l'absurde (une contradiction). La négation se comporte comme :

Enfin, le raisonnement par l'absurde :

IV. Arbres de preuve

Exemple 1 : le modus ponens .

Exemple 2 : le syllogisme barbara . On note .

On lit la preuve de bas en haut : pour prouver , on suppose ; de et , on déduit ; de et , on déduit .

Exemple 3 : . On note .

V. Correction

Exercices