Les conditions de bord des quantificateurs

${\forall }_i$ sans sa condition. On partirait de l'axiome $P(x)⊢P(x)$ et l'on conclurait

$$\frac{\frac{}{P(x)⊢P(x)}\text{ax}}{P(x)⊢\forall yP(y)}{\forall }_i\text{ (interdit)}.$$

Le modèle qui réfute : domaine $\{a,b\}$, $P$ vraie en $a$ et fausse en $b$, et $x$ interprétée par $a$. L'hypothèse $P(x)$ est satisfaite, la conclusion $\forall yP(y)$ ne l'est pas. La condition — $x$ n'est libre dans aucune hypothèse de $\Gamma$ — l'interdit ici, puisque $x$ est libre dans l'hypothèse $P(x)$.

Ce que la condition traduit. C'est le « soit $x$ quelconque » des mathématiques. On ne généralise que sur un objet dont on n'a rien supposé. Dès qu'une hypothèse parle de $x$, cet $x$ n'est plus quelconque : il a été choisi.

${\exists }_e$ sans sa condition. On démontrerait

$$\exists xP(x),\exists xQ(x)⊢\exists x(P(x)\wedge Q(x)).$$

La « preuve » : appliquer ${\exists }_e$ à la première hypothèse, ce qui met $P(x)$ dans le contexte ; puis ${\exists }_e$ à la seconde, ce qui y met $Q(x)$ ; puis ${\wedge }_i$ et ${\exists }_i$. Le second ${\exists }_e$ est interdit : sa condition demande que $x$ ne soit libre ni dans $\Gamma$ ni dans la conclusion, et $x$ est désormais libre dans l'hypothèse $P(x)$ que le premier ${\exists }_e$ vient d'introduire.

Le modèle qui réfute : domaine $\{1,2\}$, $P$ vraie seulement en $1$, $Q$ vraie seulement en $2$. Les deux hypothèses sont satisfaites, et $\exists x(P(x)\wedge Q(x))$ ne l'est pas.

L'erreur, dite en français : « il existe un $x$ tel que $P$ ; il existe un $x$ tel que $Q$ ; donc il existe un $x$ tel que $P$ et $Q$ » revient à réutiliser le même nom pour deux objets qui n'ont aucune raison d'être le même. La condition de bord est le mécanisme qui l'interdit : elle force à prendre un nom frais pour chaque témoin.

Et le parallèle informatique est exact. Un compilateur qui substituerait une variable sans vérifier qu'elle n'est pas déjà liée dans la portée d'accueil produirait la même faute — c'est la capture de variable, le défaut classique des macros non hygiéniques. Les conditions de bord de ${\forall }_i$ et ${\exists }_e$ sont la version logique du renommage que fait tout compilateur avant de substituer, et le chapitre chap:logique l'annonçait en distinguant variables libres et liées.