Cuando lo añadas, si puedes, avísame, que me gustaría ver los enunciados concretos con esta variante para asegurarme que no se me está escapando nada de momento.
Ahora mismo no es buen momento para hacer cambios en mi libro de lógica, porque estoy escribiendo otro sobre la formalización de la metamatemática, empezando en la Aritmética Recursiva Primitiva y usando teorías más potentes según va siendo necesario hasta llegar a teorías aritméticas de segundo orden cuya consistencia es "controlable" en cierto sentido (es equivalente a la de la Aritmética de Peano o más débil, en casi todas ellas).
Luego, mi idea es eliminar de mi libro de lógica los resultados que no son realmente necesarios para profundizar en la teoría de conjuntos, remitiendo al nuevo libro para los de interés puramente lógico.
Así, una posibilidad es demostrar los teoremas necesarios sobre relativización de fórmulas en el caso particular de la teoría de conjuntos en el libro de Lógica en lugar de remitir al teorema general sobre interpretaciones, que pasaría al nuevo, aunque no sé si será eso lo que decida finalmente.
De todos modos, creo que hay una forma muy sencilla de trabajar en una situación totalmente general:
En la definición 3.28 de mi libro de Lógica se exige que una interpretación de una teoría \( S \) sobre un lenguaje \( \mathcal L_S \) en otra teoría \( T \) sobre un lenguaje \( \mathcal L_T \) asigne a cada variable \( x \) de \( \mathcal L_S \) una variable \( \bar x \) de \( \mathcal L_T \).
Luego, al introducir la fórmula \( x\in M \) de \( \mathcal L_T \), basta exigir que no tenga variables libres de la forma \( \bar y \), para ninguna variable \( y \) de \( \mathcal L_S \) (que la variable \( x \) sea o no de la forma \( \bar y \) es irrelevante, porque luego sólo vamos a usar fórmulas de la forma \( \bar x\in M \), es decir, cambiando la variable \( x \) por imágenes de variables de \( \mathcal L_S \), pero las demás variables posibles de \( x\in M \) nunca se van a sustituir por otras.) Actualmente, lo que se pide es que no haya más variables libres, que es un caso particular de pedir que no haya más variables libres asociadas a variables de \( \mathcal L_S \).
Lo mismo con los demás apartados de la definición: si \( c \) es una constante de \( \mathcal L_S \), no hace falta que \( c \) sea un designador de \( \mathcal L_T \). Basta con que sea un término cuyas variables libres no sean de la forma \( \bar y \). Si \( f \) es un funtor \( n \)-ádico, el término \( \bar f(x_1,\ldots, x_n) \) puede tener más variables libres a condición de que no sean de la forma \( \bar y \), etc.
Con esta definición, no hay que cambiar nada ni añadir ninguna hipótesis a los teoremas 3.29 y 3.30, y las demostraciones valen sin cambio alguno.
Para cada expresión \( \theta(x_1, \ldots, x_n) \), la traducción \( \bar \theta(\bar x_1, \ldots, \bar x_n) \) es otra expresión que, si tiene otras variables libres, no serán de la forma \( \bar y \), para ninguna variable \( y \) de \( \mathcal L_S \), y eso basta para que funcionen todos los argumentos sin cambio alguno. Simplemente, las posibles variables adicionales "no molestan", "no interfieren". De hecho, como no se hace nada con ellas, se tratan siempre como si fueran constantes y, si lo fueran, estaríamos en el caso en el que no hay más variables libres.