Théorème de lecture unique

Attribuons à chaque symbole un poids : $1$ pour une variable ou une constante, $1 - n$ pour un symbole de fonction d'arité $n$. Le poids $p(w)$ d'un mot est la somme des poids de ses symboles.

Lemme. Si $t$ est un terme, alors $p(t) = 1$, et tout préfixe propre non vide de $t$ est de poids au plus $0$.

Par récurrence sur la construction de $t$ : c'est clair pour une variable ou une constante. Pour $t = f\, t_1 \cdots t_n$, on a $p(t) = (1 - n) + n = 1$. Un préfixe propre non vide de $t$ s'écrit $f\, t_1 \cdots t_k\, w$, avec $k < n$ et $w$ un préfixe propre de $t_{k+1}$, éventuellement vide ; son poids vaut $$(1 - n) + k + p(w) \leqslant 1 - n + k \leqslant 0,$$ puisque $p(w) \leqslant 0$ par hypothèse de récurrence.

Il en résulte qu'aucun terme n'est un préfixe propre d'un autre terme, puisque leurs poids diffèrent.

Supposons alors $f\, t_1 \cdots t_n = g\, u_1 \cdots u_m$. Les premiers symboles donnent $f = g$, donc $n = m$. Les mots $t_1 \cdots t_n$ et $u_1 \cdots u_n$ sont égaux ; $t_1$ et $u_1$ sont deux termes dont l'un est préfixe de l'autre, donc $t_1 = u_1$. On efface ce préfixe commun et l'on recommence, ce qui donne $t_i = u_i$ pour tout $i$.

Pour les formules, écrites elles aussi en notation préfixée, on prend le poids $1$ pour une lettre propositionnelle, $1 - n$ pour un symbole de relation d'arité $n$, $-1$ pour $=$ et pour $\to$, $0$ pour $\neg$, et $0$ pour le bloc $\forall x$, compté comme un seul symbole. La même démonstration s'applique mot pour mot.