Deducción natural prueba de $\forall x (\exists y (P(x) \vee Q(y))) \vdash \exists y (\forall x (P(x) \vee Q(y)))$

Question

Estoy tratando de hacer una prueba de Fitch

$$ \forall x\existe y (P(x) \vee Q(y))) \vdash \existe y (\forall x (P(x) \vee Q(y))) $$

Editar: usar sólo los axiomas en http://www.proofwiki.org/wiki/Category:Natural_Deduction_Axiomsjunto con universal y existencial de generalización/creación de instancias

La siguiente es mi primer intento.

$$ \begin{array}{lll} 1 & \begin{array}{l}\forall x (\exists y (P(x) \vee Q(y))) \\ \hline \end{array} & \text{asunción} \\ 2 & \existe y (P(v) \vee Q(y)) & \text{$\forall$E, 1} \\ 3 & \begin{array}{ll} & \begin{array}{l} P(v) \vee Q(w) \\ \hline\end{array} \end{array} & \text{asunción} \\ 4 & \begin{array}{ll} & \forall x (P(x) \vee Q(w)) \end{array} & \text{$\forall$I, 3} \\ 5 & \forall x (P(x) \vee Q(w)) & \text{$\exists$E, 2, 3, 4} \\ 6 & \existe y (\forall x (P(x) \vee Q(y))) & \text{$\exists$I, 5} \\ \end{array} $$

Edit: sé que esta prueba es incorrecta, ya que la sustitución de $P(x) \vee Q(y)$ $R(x, y)$ produciría el resultado $$ \forall x\existe y (R(x, y)) \vdash \existe y (\forall x (R(x, y))) ,$$ que claramente no es cierto en general.

No estoy seguro exactamente en la línea de la falla. Agradecería si alguien podría señalar que, y explicar por qué está mal.

Sospecho que estoy supone que el uso de la distributividad de $\exists$ $\vee$ para este. Pero no sé cómo justificar formalmente este distributividad, y no puedo encontrar una deducción natural de la prueba.

Edit: creo que he logrado lo demostró, basándose en @ZevChonoles la respuesta. Aquí está una captura de pantalla:

Answer 1

Usted no puede salir del paso 3 al paso 4. Para el particular, $v$ elige, usted sabe que usted puede encontrar $w$ tal que $P(v)\vee Q(w)$. Si $Q(w)$ es verdadera, entonces, ciertamente, $P(x)\vee Q(w)$ es cierto para todos los $x$, pero si $Q(w)$ es falso que no hay ninguna razón por qué debe ser el caso de que $P(x)\vee Q(w)$ todos los $x$.

---

No sé cómo escribir esto en el Fitch formato, pero la idea esencial es justo que cualquiera de las $Q(y)$ es cierto para algunos $y$ o $Q(y)$ es falsa para todas las $y$.

Si $Q(v)$ es cierto para algunos en particular $v$, $P(x)\vee Q(v)$ es cierto para todos los $x$, y así tenemos que $\exists y(\forall x(P(x)\vee Q(y)))$; el $y$ lo que existe es sólo $y=v$.

Si $Q(y)$ es falsa para todas las $y$,$P(x)\vee Q(y)\iff P(x)$, lo $\forall x(\exists y(P(x)\vee Q(y)))$ implica que el $P(x)$ es cierto para todos los $x$, y, por tanto,$\exists y(\forall x(P(x)\vee Q(y)))$; cualquier $y$ todo el trabajo.

Answer 2

Universal introducción la condición de que el nombre de la carta generalizada, no puede ocurrir en ningún supuesto, todavía en vigor (lo que es equivalente, no puede producirse en cualquier suposición en la hipótesis de conjunto). No importa si aparecieron en cualquier otro lugar, la regla sólo dice que no puede aparecer en ningún supuesto, todavía en vigor. En el paso 3 usted tiene el nombre de las letras "v" y "w". Así, no se puede generalizar en v para llegar a la línea 4. Este se comporta como las siguientes:

1 | (Fa $\lor$ Gb) asunción

2 | $\forall$x(Fx $\lor$ Gb) 1 universal introducción (no válido!)

3 ((Fa $\lor$ Gb)$\implies$$\forall$x(Fx $\lor$ Gb)) 1-2 introducción condicional

Answer 3

Como muchos principiantes, el OP parece estar teniendo algunos problemas para el seguimiento de las dependencias entre las variables-las dependencias que se crean existencial (especificación de eliminar la $\exists$) o algún equivalente de la regla. Tales dependencias no parecen ser un problema en matemáticas libros de texto. Aquí es una alternativa sencilla para el seguimiento de estas dependencias que parece que la mayoría de los autores de los libros de texto de matemáticas de seguir instintivamente:

1. Introducir variables libres sólo por una premisa o existencial (especificación de eliminar la $\exists$).

2. La conclusión a cada premisa no debe contener libre de las variables introducidas en la premisa o en cualquier otra declaración. La conclusión puede requerir algunos universal o existencial generalizaciones para deshacerse de cualquier "nueva" variables libres. (Hacer existencial generalizaciones (introducir $\exists$) antes de generar conclusión.)

Esta no es una nueva forma de lógica. Más bien, puede ser visto como un conjunto de directrices para la redacción formal de pruebas matemáticas análoga a la programación estructurada directrices en CS.

Ejemplo de uso de CC a Prueba de 2.0 a http://www.dcproof.com/ConclusionExample.htm