Éléments de logique
- 3 -
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
ConjonctionIntroduction (1)
( ∧ I )
p       q

p ∧ q
Élimination (2)
( ∧ E )
p ∧ q

p
p ∧ q

q
DisjonctionIntroduction (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  
Retour au menu