Déduction naturelle ?
Existe-t-il un
outil mathématique capable de reproduire les étapes du
raisonnement humain ?
La vision « commune » d'une « démonstration » est basée sur le modèle de la
géométrie euclidienne : quelques axiomes « clairs » à partir desquels un raisonnement strict permet d'établir les théorèmes nécessaires. Pourtant, le souci de réduire le nombre d'axiomes « fondateurs » a produit des « sytèmes formels » dans lesquels les formules obtenues peuvent sembler plus « évidentes » que les axiomes qui permettent de les établir (systèmes «
à la Hilbert » par exemple).
En réaction,
Gerhard Gentzen (1909 - 1945) a proposé la
déduction naturelle (1934) puis le
calcul des séquents.
Principe de la déduction naturelle
Dans l'écriture verticale, on commence par les
prémisses/hypothèses pour arriver, étape par étape, à la
conclusion (sous la barre).
| p
q | hypothèse p étapes conclusion q |
p p ⇒ q
q | Modus ponens |
Quelques règles
Conjonction | Introduction (1) ( ∧ I ) | p q
p ∧ q |
Élimination (2) ( ∧ E ) | p ∧ q
p | p ∧ q
q |
Disjonction | Introduction (3) ( ∨ I ) | p
p ∨ q | q
p ∨ q |
Implication | Introduction (4) ( ⇒ I ) | [p]
q
p ⇒ q |
Élimination (5) ( ⇒ E ) | p p ⇒ q
q |
Règles du Faux | (6) |
p | ( RAA ) reductio ad absurdum (7) | [¬p]
p |
Remarques :
(1) : Si on a démontré p ainsi que q, alors ( p ∧ q ) est démontré.
(2) : Si on a démontré ( p ∧ q ), alors p ainsi que sont démontrés.
(3) : Si on a démontré p ou bien q, alors ( p ∨ q ) est démontré.
(4) : Si l'hypothèse p permet de démontrer q, alors ( p ⇒ q ) est démontré. p est « déchargée » par la règle (écriture [p]), on peut l'enlever de l'ensemble des hypothèse.
(5) est le
Modus ponens.
(6) exprime que du faux on peut déduire n'importe quelle proposition. La règle peut être vue comme une élimination du connecteur
.
(7) est la régle du
raisonnement par l'absurde.
Exemples copiés chez ...
A/ Démontrer que
{ p ⇒ ( ¬q ⇔ ( r ∨ s ) ) , ¬s } ( p ∧ ¬q ) ⇒ r
1 2 3 4 5 6 7 8 9 10 11 |
p⇒(¬q⇔(r∨s)) ¬s | p∧¬q | p | p⇒(¬q⇔(r∨s)) | ¬q⇔(r∨s) | ¬q | r∨s | ¬s | r (p∧q)⇒r |
Prémisse 1 Prémisse 2 hyp,1 ∧E,3 réut,1 ⇒E,4-5 ∧E,3 ⇔E,6-7 réut,2 ∨E,8-9 ⇒I,3-10 |
Axiomes Hypothèse du raisonnement Élimination de ∧ en 3 Réutilisation de 1 Élimination de ⇒ entre 4 et 5 Élimination de ∧ en 3 Élimination de ⇔ entre 6 et 7 Réutilisation de 2 Élimination de ∨ entre 8 et 9 Introduction de ⇒ à partir de 3 - 10
|
B/ Démontrer que
{ p ⇒ ( ¬q ⇔ ( r ∨ s ) ) , ¬s } ( p ∧ ¬q ) ⇒ r
1 2 3 4 5 6 7 8 9 10 11 |
p⇒(¬q⇔(r∨s)) ¬s | p∧¬q | p | p⇒(¬q⇔(r∨s)) | ¬q⇔(r∨s) | ¬q | r∨s | ¬s | r (p∧q)⇒r |
Prémisse 1 Prémisse 2 hyp,1 ∧E,3 réut,1 ⇒E,4-5 ∧E,3 ⇔E,6-7 réut,2 ∨E,8-9 ⇒I,3-10 |
Axiomes Hypothèse du raisonnement Élimination de ∧ en 3 Réutilisation de 1 Élimination de ⇒ entre 4 et 5 Élimination de ∧ en 3 Élimination de ⇔ entre 6 et 7 Réutilisation de 2 Élimination de ∨ entre 8 et 9 Introduction de ⇒ à partir de 3 - 10
|
Commentaire
théorème de complétude et d'imcomplétude (essayer de le trouver)
bla bla
Le calcul des séquents
Système de Gentzen, déduction naturelle et calcul des séquents
re bla bla
Autres logiques
capable de
ou
variable propositionnelle est une phrase à laquelle il est possible d'attribuer une valeur Vrai ou Faux.
La déduction et la logique naturelle
Hilbert
Gentzen
Les autres logiques
règle du modus (ponendo) ponens manière qui affirme (en affirmant) A implique B or A donc B
on pose l'antécédent d'une traitement si alors et on conclut sa conséquence
si p => q
p
.. q
implication
non-q
si p=>q
.. non-p
on nie la conséquence d'un traitement si-alors et on nie son antécédent.
modus tollendo tollens manière qui nie
contraposée