Déduction naturelle

I/ Théorie de Gentzen

L'idée de départ de Gentzen a été qu'une déduction ne se rédige pas comme une liste de propositions découlant les unes des autres, mais comme un arbre. La racine de l'arbre (conventionnellement placée en bas) est déduite des arbres qui la surmontent. Les feuilles de l'arbre sont des hypothèses.

On construit l'arbre en assemblant des arbres de hauteur 1 que Gentzen classe en deux catégories 

Chaque opérateur a sa propre règle d'introduction et sa propre règle d'élimination.

opérateurintroductionélimination
%3 f1 p r p∧q f1--r f2 q f2--r %3 f1 p∧q r p f1--r f2 p∧q s q f2--s
%3 f1 p r p∨q f1--r f2 q s p∨q f2--s %3 f1 p∨q r r f1--r f2 [p]...r f2--r f3 [q]...r f3--r
%3 f1 [p]...q r p→q f1--r %3 f1 p r q f1--r f2 p→q f2--r
¬ %3 f1 [p]...⊥ r ¬p f1--r %3 f1 p r f1--r f2 ¬p f2--r f3 s q f3--s
%3 f1 P(x) r ∀x,P(x) f1--r %3 f1 ∀x,P(x) r P(a) f1--r
%3 f1 P(a) r ∃x,P(x) f1--r %3 f1 ∃x,P(x) r q f1--r f2 [P(a)]...q f2--r

La notation [p]...q désigne un arbre dont la racine est q et dont l'une des feuilles est p.

1) Conjonction ∧

a) Introduction

La règle d'introduction se note aussi p,q⊦p∧q. Cette notation, que Gentzen dit avoir empruntée à Frege, s'appelle un séquent. Gentzen convient que, avant le ⊦ (qui désigne la déduction), la virgule représente un « et » et après le ⊦ la virgule représente un « ou ».

b) Élimination

La conjonction ∧ a deux règles d'élimination : p∧q⊦p et p∧q⊦q.

2) Disjonction ∨

a) Introduction

La disjonction ∨ a deux règles d'introduction : p⊦p∨q et q⊦p∨q.

b) Élimination

La règle d'élimination de ∨ est p∨q,[p]...r,[q]...r⊦r signifie que si on a prouvé

alors on considère r comme prouvé. Gentzen appelle cela raisonnement par disjonction des cas.

3) Implication →

Hilbert notait l'implication (une descendance moderne de ce symbole est promu par Bourbaki), et Gentzen notait également l'implication. Mais l'interprétation fonctionnelle de l'implication amène à préférer la notation . C'est ce qu'on fera ici.

a) Introduction

La règle d'introduction de → est celle qui donne le nom de « déduction naturelle » au système de Gentzen : si, en supposant p, on arrive à en déduire q, on considère p→q comme prouvé. Avec la notation des séquents, on passe de p⊦q à ⊦p→q.

b) Élimination

La règle d'élimination de → est appelée modus ponens. Elle est notée p,p→q⊦q.

4) Négation ¬

a) Introduction

La règle d'introduction de la négation est p→⊥⊦¬p. Gentzen l'appelle démonstration de ¬p par l'absurde.

b) Élimination

La négation ¬ a deux règles d'élimination :

II/ Exemples

1) Chaînage arrière

On veut montrer que (p→q) → ¬(p∧¬q). Pour trouver comment on peut construire l'arbre de preuve, on regarde la forme du succédent : c'est une implication. Donc la racine de l'arbre est une implication et la seule manière de faire grandir l'arbre, c'est par introduction de →. On va donc, pour l'instant, regarder ⊦(p→q) → ¬(p∧¬q) comme (p→q) ⊦ ¬(p∧¬q). On cherche donc pour l'instant à construire un nouvel arbre ayant ¬(p∧¬q) pour racine et dont une des feuilles est p→q. Le tout, récursivement.

¬(p∧¬q) est une négation, donc on regarde comment introduire une négation : il faut partir de p∧¬q et aboutir à une contradiction ⊥. À ce stade on sait que l'arbre aura au moins une feuille portant p→q et une feuille portant p∧¬q et on a un sous-arbre de racine . On peut maintenant continuer par chaînage avant : on part des feuilles et on utilise les règles d'élimination pour chercher la contradiction.

%3 f2 p∧¬q p p f2--p f1 p→q w q f1--w p--w f3 p∧¬q v ¬q f3--v z w--z v--z u ¬(p∧¬q) z--u t (p→q) → ¬(p∧¬q) u--t

2) Contraposition

On raisonne par chaînage avant : on part de ¬q→¬p et on regarde où on peut aller. C'est-à-dire qu'une des feuilles de l'arbre de preuve portera ¬q→¬p. C'est une implication donc on regarde comment éliminer l'implication : on introduit (autre feuille) ¬q et on a donc ¬p. On constate alors qu'il est possible d'éliminer ¬p en introduisant p (nouvelle feuille de l'arbre), ce qui permet d'utiliser la première règle d'élimination de ¬. On a alors un nouveau nœud dans l'arbre, portant . Et on regarde comment on peut éliminer ⊥ : la seconde règle d'élimination de ¬ convient. On choisit alors q comme subséquent puisqu'il n'est dans aucune feuille de l'arbre.

Comme on a un arbre de racine q (pour l'instant) et dont une feuille est p, on peut le greffer sur une nouvelle racine p→q par introduction de →.

Et comme on a un arbre dont une feuille est ¬q→¬p et dont la racine est p→q (pour l'instant), il s'agit d'un arbre de preuve de (¬q→¬p) → (p→q) :

%3 f1 ¬q→¬p t ¬p f1--t f2 ¬q f2--t z t--z f3 p f3--z q q z--q s p→q q--s r (¬q→¬p) → (p→q) s--r

3) Transitivité de l'implication

%3 H0 (p→q)∧(q→r) i1 p→q H0--i1 H1 (p→q)∧(q→r) i2 q→r H1--i2 f1 p f2 q f1--f2 i1--f2 r r f2--r i2--r i3 p→r r--i3 s (p→q)∧(q→r)→(p→r) i3--s

4) Distributivité de ∨ par rapport à ∧

C'est un exemple de Gentzen (début années 1940) :

%3 e1 q∧r q q e1--q e2 q∧r r r e2--r p1 p o1 p∨q p1--o1 p2 p o2 p∨r p2--o2 o3 p∨q q--o3 o4 p∨r r--o4 e3 (p∨q)∧(p∨r) o1--e3 o2--e3 e4 (p∨q)∧(p∨r) o3--e4 o4--e4 e5 (p∨q)∧(p∨r) e3--e5 e4--e5 H p∨(q∧r) H--e5 s p∨(q∧r) → (p∨q)∧(p∨r) e5--s

III/ Quantificateurs

1) Quantificateur universel ∀

a) Introduction

De P(x)P est un prédicat, et x une variable non couverte par un quantificateur, on déduit ∀x,P(x). L'idée est que si on n'a besoin d'aucune hypothèse sur x, ce qu'on a prouvé sur P(x) est valable pour toute valeur de x.

b) Élimination

De ∀x,P(x) on déduit P(a). Par exemple, une fois qu'on sait que tout carré est positif, on n'a plus besoin de prouver que 25 est positif.

2) Quantificateur existentiel ∃

a) Introduction

De P(a) on déduit que ∃x,P(x). Par exemple, une fois qu'on a constaté que 6 est pair, on en déduit qu'il existe un nombre pair.

b) Élimination

S'il existe un x vérifiant le prédicat P, et si P(a)⊦q alors on considère q comme prouvé.

3) Exemples

Les exemples suivants sont de Gentzen.

a) Exemple 1

%3 f1 ∀y,P(a,y) v P(a,b) f1--v u ∃x,P(x,b) v--u t ∀y,∃x,P(x,y) u--t f2 ∃x,∀y,P(x,y) s ∀y,∃x,P(x,y) f2--s t--s r ∃x,∀y,P(x,y)→∀y,∃x,P(x,y) s--r

b) Exemple 2

%3 f2 P(a) v ∃x,P(x) f2--v z v--z f1 ¬∃x,P(x) f1--z u ¬P(a) z--u t ∀y,¬P(y) u--t s ¬∃x,P(x)→∀y,¬P(y) t--s

Logithèque