Creo que ya lo entiendo, aunque en esa deducción también podría ser causa del error que se introduzca una variable que estuvo anteriormente en la deducción.
Pues ese "aunque" me hace sospechar que todavía no lo acabas de tener claro, porque da a entender que piensas que lo que va después es "otra causa del error" distinta, cuando es la misma.
Tu pregunta inicial era por qué en el enunciado de la regla de eliminación del particularizador no aparece explícito que la variable "liberada" sea distinta de todas las anteriores, y lo que te trato de explicar es que la restricción que realmente hace falta imponer es que la variable "liberada" sea una variable respecto de la que no está prohibido generalizar. En tu último mensaje me pedías un ejemplo en el que se viera qué puede fallar si "liberas" una variable respecto a la que no se puede generalizar, y eso te he puesto y, claro, para eso tiene que ser una variable que ya aparecía antes en la deducción. No es "otra causa" si no "la causa" del error.
Pero, técnicamente, lo que importa no es si la variable estaba antes o no, si no si estaba prohibido generalizar respecto de ella o no. Por ejemplo, este razonamiento es correcto, aunque a un matemático le chirriará un poco porque se aparta de "sus costumbres":
\( \begin{array}{lll}
(1)&\forall x\,Px&\mbox{Hipótesis}\\
(2)&\exists y\,Qy&\mbox{Hipótesis}\\
(3)& Pz&\mbox{EG 1}\\
(4)&Qz&\mbox{EP 2}\\
(5)&Pz\land Qz&\mbox{IC 3, 4}\\
(6)&\exists z(Pz\land Qz)&\mbox{IP 5}
\end{array} \)
La eliminación de particularizador con la variable \( z \), que ya aparecía en la línea anterior, es correcta, porque no está prohibido generalizar respecto a ella. Como digo, a un matemático le chirriará esa eliminación, pero se convencerá de que es válida en cuanto se dé cuenta de que podríamos haber escrito la línea (4) antes de la (3), en cuyo caso "todo está en orden". Pero incluso en el orden en que las he puesto, la deducción es formalmente correcta. La condición de liberar variables de cuantificadores existenciales con variables nuevas evita el problema de elegir una inadmisible, pero no es necesaria técnicamente, siempre y cuando nos aseguremos de que no hay problema en generalizar respecto a la variable elegida.
Otra cosa que noto es que la condición \( y\equiv x \) tiene mas peso que la restricción que afirma que no se debe introducir variables anteriores en la deducción, supongo que se debe a que afirmar \( \exists x\alpha \) es lo mismo que afirmar que \( \alpha\ \) se cumple para un \( x \) particular, lo que afirmamos al hacer la sustitución
No sé qué sentido tengo que darle a lo de "tiene más peso". Es algo independiente. La variable "liberada" \( y \) no tiene que estar libre en la fórmula salvo que sea la propia variable \( x \) que estaba ligada en ella, pero en cualquier caso, tanto si es la misma \( x \) o si es otra, es necesario que sea una variable respecto a la que no esté prohibido generalizar. Que tomes \( x \) como variable "liberada" no te exime de cumplir esta condición. Por ejemplo, en la deducción de la respuesta #4, en la línea (4) se cumple \( y\equiv x \), pero la deducción es incorrecta porque a partir de (3) ya no se puede generalizar respecto de \( x \).
