Adjunto un pdf con esas nuevas reglas que se añaden (11_12_PredDeduccionNatural.pdf). Mi duda está en las restricciones que se piden para los cuantificadores. Cada vez que aplicamos una regla que involucra a un cuantificador, nos exigen poner un asterisco (o algún tipo de referencia) para después abajo de la derivación hacer la justificación que corresponda. En el pdf dice que sin las restricciones, las reglas dadas permitirían construir derivaciones para razonamientos incorrectos. Y pone dos ejemplos. Pero aún así no me queda del todo clara esa parte

. ¿Me lo podrían explicar?
Esas condiciones formalizan restricciones que aplicas poco menos que inconscientemente cuando razonas "de verdad". Por ejemplo, para eliminar un cuantificador existencial

te exigen que la variable x ligada por el cuantificador no esté libre ni en las hipótesis que supones hasta el momento ni en la consecuencia

a la que llegues.
Eso lo haces tú todos los días: si tienes que

y, por otra parte, tienes que

, tú quitas normalmente el cuantificador diciendo "tomemos un x que cumpla

, pero no lo harías como yo lo estoy haciendo aquí, sino que dirías: pero ojo, no podemos llamar x a ese número real, porque ya estamos llamando x a otra cosa, a saber, a un cierto número entero. Si siguieras adelante sin tener esto en cuenta, llegarías a que

, lo cual es una contradicción, una contradicción que no viene de tus hipótesis, sino de haber llamado x a dos cosas distintas, al número del que ya estabas hablando, y el que resulta de eliminar el cuantificador.
Lo correcto, si en una demostración ya estás tratando con un

y quieres eliminar el cuantificador en

, es decir "tomemos un y tal que

, donde y es una variable nueva.
En tu sistema deductivo, si ya estás usando x y quieres eliminar el cuantificador de

, tienes que usar que
![\exists x\phi\rightarrow \exists y \phi[y/x]](/foros/Sources/latexrender/pictures/a74ca94e101bdfb2f55807b3e0193f35.png)
, lo cual se demuestra suponiendo

, pasando a

y de ahí a
![\exists y\phi[y/x]](/foros/Sources/latexrender/pictures/34f066529054bd25d45c1e8719aa8f3c.png)
, todo aplicando directamente tus reglas.
Entonces, una vez tienes
![\exists y\phi[y/x]](/foros/Sources/latexrender/pictures/34f066529054bd25d45c1e8719aa8f3c.png)
, donde y es una variable nueva, ya puedes eliminar el cuantificador y escribir
![\phi[y/x]](/foros/Sources/latexrender/pictures/fa5aa82722a013460e9f7943821e1c03.png)
sin violar la condición de que la variable y no esté libre en tus hipótesis.
La otra condición, a saber, que la variable liberada del cuantificador no esté libre en la conclusión, es necesaria porque, en principio, una variable libre puede ligarse con un "para todo", pero eso no sería legítimo si la variable está libre porque le has quitado un "existe" de delante.
Por ejemplo, si partimos de

(sin más hipótesis donde x pudiera estar libre), de ahí puedo pasar legítimamente a tomar un x tal que

, pero esto mismo no es válido como consecuencia lógica de mi premisa, pues, si lo fuera, como x no está libre en mi hipótesis, podría aplicar la regla de introducción del "para todo" y concluir que

, lo cual es absurdo: cuando razonas "de verdad" siempre tienes en la memoria si un x del que hablas es un x arbitrario o, por el contrario, es un x concreto que has escogido entre los que cumplen algo (proviene de eliminar un "existe"). Cuando tienes un x del segundo tipo, para acabar la demostración tienes que volverlo a ligar con un "existe", pues si no lo ligas de ningún modo sería legítimo entender que puede ligarse con un "para todo", y eso no sería correcto.
Volviendo al ejemplo: si partes de

, puedes pasar a

. Esto es correcto, pero lo que has escrito NO es una consecuencia de tu premisa. De ahí puedes a su vez seguir razonando y llegar, por ejemplo, a

, lo cual será correcto, pero esto NO es consecuencia de tu premisa, porque la x no puede estar libre en ninguna consecuencia desde el momento en que has quitado el "existe". Ahora bien, de ahí puedes pasar a

y esto SÍ que es consecuencia de tu premisa, porque ahora x no está libre en ella.
En otras palabras, si le quitas un "existe" a una variable, tienes que comprometerte a volvérselo a poner al final, si es que x aparece en la conclusión de tu razonamiento. (Si no aparece, pues nada.) De no hacerlo así, otro podría continuar tu razonamiento poniéndole un "para todo" a tu x, y eso sería incorrecto.
Con la condición para introducir un "para todo" pasa lo mismo. Imagina que parto de

. De ahí puedo pasar a

, pero esto pasa a ser una hipótesis no cancelada de una subdeducción. En esas condiciones, no puedo pasar a

. Con ello, de la existencia de un número entero pasaría a deducir que todo x es un número entero, lo cual es falso. Para introducir un "para todo" sobre una variable x, es necesario que la variable x no tenga una hipótesis de partida ni en particular que provenga de haber eliminado un "existe".
No hay problema, en cambio, si proviene de eliminar un "para todo".
Por ejemplo, si tenemos que

, de aquí puedes poner

justo debajo. Esto no es la hipótesis de una subdeducción, por lo que x no está como variable libre en ninguna hipótesis no cancelada y puedes volver a ligarla con un "para todo" cuando quieras.
Si, por ejemplo, supones

y a partir de ahí deduces

, en este momento no puedes pasar a

, porque la x está como variable libre en la hipótesis no cancelada

, y, en efecto, no puedes afirmar que todo x es un número complejo, pero puedes cancelar la hipótesis escribiendo

, con lo que ahora x ya vuelve a ser arbitrario. El x que cumple

no es un x arbitrario, sino un x con la condición particular

. En cambio, el x que cumple

sí que es un x arbitrario (esa afirmación la cumple todo x del universo), y formalmente eso se refleja en que x no está libre en ninguna hipótesis no cancelada. Por eso, ahora sí que puedes cuantificar y concluir

.
No sé si me explico.