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érateur | introduction | élimination |
---|---|---|
∧ | ||
∨ | ||
→ | ||
¬ | ||
∀ | ||
∃ |
La notation [p]...q
désigne un arbre dont
la racine est q
et dont l'une des feuilles
est p
.
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 ».
La conjonction ∧ a deux règles d'élimination :
p∧q⊦p
et p∧q⊦q
.
La disjonction ∨ a deux règles d'introduction :
p⊦p∨q
et q⊦p∨q
.
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.
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.
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.
La règle d'élimination de → est appelée modus ponens.
Elle est notée p,p→q⊦q
.
La règle d'introduction de la négation est p→⊥⊦¬p
.
Gentzen l'appelle démonstration de ¬p par l'absurde.
La négation ¬ a deux règles d'élimination :
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.
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)
:
C'est un exemple de Gentzen (début années 1940) :
De P(x)
où 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
.
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.
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.
S'il existe un x
vérifiant le prédicat
P
, et si P(a)⊦q
alors on
considère q
comme prouvé.
Les exemples suivants sont de Gentzen.