Intérêt des preuves sous forme d'arbres

Théorème : si M = N alors il existe une suite de termes M₀,…,M_k telle que :

M ≡ M₀ :=: M₁ :=: … :=: M_k ≡ N

où :=: désigne soit := soit =:

Plus clairement, si deux termes sont égaux, il existe une suite d’expansions et de réductions reliant le premier au deuxième

Démonstration. Elle se fait par récurrence sur la hauteur de l’arbre. Comme il n’existe pas d’axiome décrivant une égalité, il n’existe pas d’arbre de preuve de hauteur 0. La récurrence commence donc à 1.

Pour un arbre de hauteur 1

Un arbre de hauteur 1 est un ou plusieurs axiomes suivi de l’application d’une règle qui fournit la conclusion
M = N.
Seules trois règles permettent une conclusion de la forme M=N : (fe), (rf), (te).
Les hypothèses des règles (rf) et (te) ne peuvent être des axiomes puisque ce sont des égalités. La dernière règle est donc (fe).
La preuve de hauteur 1 est donc :

où M := N est un axiome.
Le résultat est alors évident.

Pour un arbre de hauteur k+1

On examine la dernière règle utilisée dans la preuve. C’est une règle dont la conclusion est de la forme M=N.
Il ne peut s’agir que de l’une des règles (fe), (rf) ou (te).
Si la dernière règle est (fe), le résultat est trivial.
Si la dernière règle est (rf), l’hypothèse de récurrence s’applique à la formule N=M. Il existe donc une suite de réduction et d’expansions allant de N à M. En inversant cette suite, on en obtient une qui va de M à N.
Si la dernière règle est (te), l’hypothèse de récurrence s’applique aux hypothèses M=L et L=N. Il existe donc deux suites d’expansions et de réductions, l’une entre M et L et l’autre entre L et N. En les mettant bout à bout, on en obtient une de M à N.

La technique de l’examen de la dernière règle est un classique…