No entiendo la parte "pero en la definición de sustitución de una variable por un término en una variable necesitamos considerar el caso en que la variable sea la variable a sustituir o que sea otra distinta". ¿Esto significa que cuando tenemos \( \forall xy \), debemos tratar por separado los casos \( x=y \) y \( x\neq y \)?
No veo qué relación puedes ver entre lo uno y lo otro. En el párrafo que citas he puesto un ejemplo con $$\forall xy$$ que no tiene nada que ver con el concepto de sustitución. Lo que quería recordar ahí es que el hecho de que usemos letras distintas para representar las variables normalmente lleva implícito que son dos variables distintas, pero no siempre podemos suponerlo así, y en ese párrafo aclaro que la definición de sustitución es uno de esos casos en los que, si tenemos una variable $$x$$ y otra $$y$$ no podemos dejar de considerar la posibilidad de que sean la misma variable.
No estoy seguro de que estés situado: si escribo $$x=x$$, entonces seguro que a ambos lados del igual está la misma variable, pero si escribo $$x=y$$ entonces, con los convenios usuales,
debemos entender que la variable \( x \) es distinta (y nunca igual) a la variable \( y \).Si esto te sorprende, es que no estás situado. No hay contradicción en decir que $$x=y$$ y, al mismo tiempo, decir que la variable $$x$$ no es la misma que la variable $$y$$, que son dos signos distintos del lenguaje formal considerado. Pero esto es menos obvio de lo que podría parecer porque es habitual entender que "$$x$$'' no es en realidad ninguna variable, sino el nombre de una variable, de modo que, aunque "$$x$$" e "$$y$$" sean, sin duda, dos nombres distintos de variables, nada impide a priori que ambos nombren a la misma variable, de modo que $$x=y$$ podría ser $$x_0 = x_0$$ si resulta que $$x\equiv x_0\equiv y$$, aunque el convenio habitual es que si usamos nombres distintos, éstos hacen referencia a variables distintas.
Sin embargo, cuando tenemos que definir la sustitución $$S_x^ty$$, tenemos que contemplar la posibilidad de que la variable $$y$$ sea la misma que la variable $$x$$ o que sea otra, y según el caso la sustitución se calcula de una forma o de otra.
En caso afirmativo, ¿cómo debería tratarse algo como \( \forall abc\exists de\forall f \) considerando cada caso?
¿Pero tratarse para hacer qué?
Ejemplo:
\( \forall xy\in\Bbb{Z}(\text{\(x+y\) es múltiplo de \(4\)}\to\text{\(x+y\) es par}) \)
es verdadero. Demostración:
Si \( x+y \) es múltiplo de 4 existe \( k\in\Bbb{Z} \) tal que \( x+y=4k \). Entonces, \( x+y=2(2k) \) y como \( 2k\in\Bbb{Z} \), hemos probado que \( x+y \) es múltiplo de 2, o sea es par.
Aquí no entiendo (y es una duda que me surgió luego de leer esa observación), dónde he usado que \( x\neq y \) o que \( x=y \).
En ningún sitio. Lo que sí que has supuesto tácitamente es que las variables $$x$$ e $$y$$ son distintas (que no tiene nada que ver con suponer que $$x\neq y$$).
El teorema que has demostrado es uno, y éste sería otro mucho más tonto:
\( \forall xx\in\Bbb{Z}(\text{\(x+x\) es múltiplo de \(4\)}\to\text{\(x+x\) es par}) \)
Si te piden demostrar lo que tú has puesto pero demuestras lo que he puesto yo, estás haciendo trampa, porque mi enunciado es trivial (seguro que $$x+x$$ es par sin necesidad siquiera de la hipótesis). Pero, en principio, si no suponemos tácitamente que $$x\not\equiv y$$, tu enunciado podría ser una forma de escribir el mío, pero nadie lo entenderá nunca así.