Les diapositives mises ici ont servi de support dans les années
2003-2007 pour un cours d'initiation au raisonnement logique, basé sur
la déduction naturelle.

La logique est souvent présentée en démarrant par les fameuses "tables
de vérité". Il s'agit en réalité pas de raisonnement, mais de
techniques de calcul basées sur une algèbre particulière, l'algèbre
booléenne. Elles sont utiles à l'ingénieur qui conçoit des circuits
logiques ou cherche à simplifier des expressions booléennes.
Cependant :
- elles ne correspondent pas au raisonnement ordinaire
- elles ne s'appliquent pas aux formules comportant
  des quantificateurs (∀, "pour tout" et ∃, "il existe")
- elles s'appliquent encore moins aux formes de raisonnement
  plus élaborées comme la récurrence et ses variantes.

Au contraire, on utilise ici la déduction naturelle qui a l'avantage
de coller au raisonnement tel qu'il est pratiqué quotidiennement par
tout un chacun, avec des schémas emblématiques comme les raisonnement
par cas ou le modus ponens, un syllogisme connu depuis l'antiquité
grecque (de A et A => B, déduire B). Toutes les formes de raisonnement
que l'on rencontre s'expriment facilement sous forme de règles de
déduction naturelle. Et ce n'est pas un hasard si les logiciels
modernes appelés "assistants à la preuve" comme Coq s'appuient sur
la déduction naturelle.

JF Monin, septembre 2018