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
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.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 ∃�
.
y/t signifie que je remplace y par t....
Si quelqu'un peut éclaircir le sujet, car je bloque sur ce point.
Cordialement,
-----