De la logique antique à la "déduction naturelle"¶
Grèce antique : Aristote (~350 av JC)¶
 |
philosophe grec qui s'intéressa à toutes les connaissances de son époque un des penseurs les plus influents du monde occidental la logique comme outil pour faire progresser les autres domaines (politique, réthorique, physique, biologie ...) |
| Aristote |
Deux Prémisses : Tous les hommes sont mortels + Socrate est un homme
Une Conclusion : Socrate est mortel
Culturel¶
Aristote classifie les syllogismes selon la nature des prémisses et de la conclusion :
A : affirmative universelle : « Tous les hommes sont mortels »
E : négation universelle : « Aucun homme n'est mortel »
I : affirmation particulière : « Au moins un homme est mortel »
O : négation particulière : « Au moins un homme est immortel »
NB : cf logique du 1er ordre ($\forall$, $\exists$)
Syllogismes "barbara", "celarent", "darii", "ferio" ...¶
Astuce mnémotechnique des moines du Moyen-Age pour retenir différents types de raisonnement
 |
philosophe, logicien du Moyen-Âge |
bArbArA :¶
AAA trois affirmations universelles
Tous les animaux sont mortels, or les hommes sont des animaux, donc les hommes sont mortels
est un syllogisme "barbara" :
Tous les animaux sont mortels, (prémisse1 : A)
or les hommes sont des animaux, (prémisse2 : A)
donc les hommes sont mortels (conclusion : A)
cElArEnt :¶
EAE une négation universelle, une affirmation universelle, une négation universelle
"Aucun véhicule n'est autorisé à passer, or toute trotinette est un véhicule, donc aucune trotinette n'est autorisée à passer"
est un syllogisme "celarent" :
Aucun véhicule n'est autorisé à passer, (prémisse1 : E)
or toute trotinette est un véhicule, (prémisse2 : A)
donc aucune trotinette n'est autorisée à passer (conclusion : E)
dArII, fErIO ...
Logique moderne : George Boole (~1850)¶
 |
mathématicien, logicien anglais |
| G. Boole |
OU : 0+0=0; 0+1=1; 1+0=1; 1+1=1
ET : 0x0=0; 0x1=0; 1x0=0; 1x1=1
NB: 1+1=1 : l'algèbre de Boole n'est pas $\mathbb{Z}/2\mathbb{Z}$ !
Conséquences majeures :¶
logique booléenne : calcul des propositions
informatique pratique : circuits électroniques
informatique théorique : théorie de l'information
Les limites du calcul des propositions ...¶
Remarque 1 : le lien entre "logique" et "mathématique" n'est pas évident ...¶
LOGIQUE : $\varphi = a \rightarrow b$¶
$\varphi$ formule logique qui peut être vraie ou fausse, selon la valuation choisie
MATHEMATIQUES : Prop : $\mathcal{A} \Rightarrow \mathcal{B}$¶
cette propriété désigne une implication vraie (si $\mathcal{A}$ vraie, alors $\mathcal{B}$ vraie)
En mathématiques, on s'intéresse aux formules logiques vraies (tautologies) ou supposées comme telles¶
Remarque 2 : montrer qu'une formule logique est une tautologie, et faire une démonstration mathématique, ça n'a rien à voir ...¶
Vérifier qu'une formule est une tautologie ? :¶
- pour toutes les valuations possibles ... (table de vérité, algo Quine modifié)
- coût exponentiel, très mécanique
Etablir une preuve mathématique ? :¶
on établit des faits avérés, par déduction, jusqu'à atteindre la conclusion
nature arborescente de la preuve mathématique (étude de cas, raisonnements imbriqués, lemmes ...)
Comment réconcilier LOGIQUE et MATHEMATIQUES ?¶
 |
vous vous souvenez de moi ? |
| David Hilbert |
~1930 : Gerhard Gentzen - Calcul des séquents / Déduction naturelle¶
 |
propose un nouveau formalisme pour raisonner "mathématiquement" sur des formules logiques |
| Gerhard Gentzen |
Interprétation : si les formules $H_1$, ... $H_n$ sont vraies, alors la formule $\varphi$ est vraie
Interprétation : si les formules de $\Gamma$ sont vraies, alors la formule $\varphi$ est vraie
NB lien avec la notion de conséquence logique (en logique booléenne)
Interprétation 2 : en supposant $\Gamma$, on peut déduire $\varphi$
Règle de déduction¶
Interprétation : si en supposant $\Gamma$ on peut déduire $\varphi \rightarrow \psi$, ET en supposant $\Gamma$ on peut déduire $\varphi$ alors, en supposant $\Gamma$, on peut déduire $\psi$
Interprétation 2 : en supposant les séquents du haut vrais, on peut déduire le séquent du bas
NB : UNE étape de raisonnement¶
Arbre de preuve¶
