Substitution de variable en calcul des prédicats

[sunyata]

Bonjour,

Dans un cours de logique formelle, en logique des prédicats, on fait appel à des changements de variables.
https://fr.wikipedia.org/wiki/Calcul_des_s%C3%A9quents

La notation �[�/�] désigne la formule � dans laquelle la variable � est remplacée par un terme �, toutefois ce remplacement doit être sain : � ne doit pas contenir de sous-formule ∀�.� ou ∃�.� où � serait une variable libre de � apparaissant dans le terme �. Par exemple, [�/�] n'est pas une substitution saine dans ∀�∃�.�(�,�,�) car après remplacement de � par �, on obtient : ∀�∃�.�(�,�,�), une variable (ici �) du terme remplaçant � s'est fait capturer par le quantificateur ∃�.

Je ne comprends pas les tenants et les aboutissants de ces substitutions, ni leur utilité. C'est utilisé notamment en calcul des séquents, notamment lorsqu'on manipule des quantificateurs.
y/t signifie que je remplace y par t....


Si quelqu'un peut éclaircir le sujet, car je bloque sur ce point.

Cordialement,
-----

[GBZM]

Bonsoir,

Le sens me paraît assez clair : si l'on démontre quelque chose sous l'hypothèse , alors on l'a démontré sous l'hypothèse . En déduction naturelle, si on a démontré , alors on a démontré .
Et si on démontre alors on démontre .