Prueba de deducción natural de $(\forall x.P(x))\land(\forall y.P(y) \implies Q(y)) \vdash \forall z.Q(z)$

Question

Mi intento

1. $(\forall x.P(x))\land(\forall y.P(y) \implies Q(y))$ [premisa]
2. $\forall y.P(y) \implies Q(y)$ [ $\land$ elim 1]
3. $\forall x.P(x)$ [ $\land$ elim 1]
4. $a, P(a)$ [ $\forall$ elim 3]
5. $a, P(a) \implies Q(a)$ [ $\forall$ elim 2]
6. $Q(a)$ [ $\implies$ elim 4,5]
7. $\forall z.Q(z)$

Creo que los pasos 4-5 no son correctos, porque utilizamos a para dos expresiones diferentes. Tampoco estoy muy segura de si es correcto el paso 6-7. ¿Alguien podría decirme si lo que hice es correcto y si no cómo debería arreglarlo?

Answer 1

Puede eliminar cualquier universal con cualquier término que desee, por lo que no es necesario introducir $a$ en la línea 4 o 5.

Sin embargo do necesidad de introducir el $a$ para establecer la regla de Introducción Universal. Es decir, básicamente tienes que decir: "que $a$ sea un objeto arbitrario. En $\forall x P(x)$ se deduce que $P(a)$ y por $\forall y (P(y) \rightarrow Q(y))$ se deduce que $P(A) \rightarrow Q(a)$ . Por lo tanto, tenemos $Q(a)$ . Pero como $a$ era arbitraria, se deduce que $\forall z Q(z)$ "

No sé cómo se formaliza exactamente esa prueba en el sistema que estés utilizando, pero aquí tienes una hecha en Fitch:

Answer 2

Yo justificaría tus pasos 4 y 5 con "instanciación universal" y escribiría que $a$ en el paso 5 es el mismo $a$ como en el paso 4. (Si el paso 2 es cierto para todo $y$ entonces es ciertamente cierto con la asignación $y = a$ para el mismo $a$ como en el paso 4). Luego el paso 6 es modus ponens sobre los pasos 5 y 4. (No todo es eliminación.) Luego el paso 7 es generalización universal aplicada al 6.

Pero por lo demás, esto parece estar bien.

Answer 3

La eliminación universal ( $\forall\textsf {Elim}$ ) los pasos son que : Si la declaración $S(w)$ es válido para cualquier entidad $w$ del dominio, entonces $S(a)$ se cumple para un valor arbitrario $a$ del dominio. $$\forall w~S(w)~\vdash~ S(a)$$

La introducción universal ( $\forall\textsf{Intro}$ ) paso es igualmente que : Si la declaración $S(a)$ se cumple para un valor arbitrario $a$ del dominio, entonces $S(z)$ es válida para todos los valores $z$ del dominio. $$S(a)~\vdash~\forall z~S(z)$$

El criterio clave es que no debe violar la naturaleza arbitraria de la variable libre $a$ entre supuesto(s) y alta. Sin embargo, está bien que dos eliminaciones universales asuman el mismo valor arbitrario; y no hay ningún problema con que las variables ligadas utilicen fichas diferentes. Todos los pasos están bien.

---

$$\dfrac{\dfrac{\dfrac{\dfrac{\forall x~P(x)~\wedge~\forall y~(P(y)\to Q(y))}{\forall y~(P(y)\to Q(y))}{\wedge\textsf E}}{P(a)\to Q(a)}{\forall\textsf E,a}\quad\dfrac{\dfrac{\forall x~P(x)~\wedge~\forall y~(P(y)\to Q(y))}{\forall x~P(x)}{\wedge\textsf E}}{P(a)}{\forall\textsf E,a}\quad}{Q(a)}{{\to}\textsf E,a}}{\forall z~Q(z)}{\forall\textsf I,\not a}$$