¿Es un chiste, no? 
No sé cuántas veces más quieres que copie la tablita que tanto trabajo me costó hacerla de este mensaje:
¡Esta vez no iba para ti!
Era para Slaut, para que aclarara a qué reglas se refiere cuando dice
Usar las reglas de inferencia, de reemplazo, de demostración condicional, de demostración indirecta y de la lógica de relaciones
Con tu ayuda creo que he podido resolverlo:
\(
\begin{array}{lll}
1)&\forall x\{Lx\to(\exists w)[Vw\land(\exists z)(Gz\land Bz\land Hwz)\land Rxw]\}&\text{Premisa}\\
2)&\neg (\exists x)(Gx\land\neg Mx)&\text{Premisa}\\
3)&\neg (\exists x)(Vx\land\neg Cx)&\text{Premisa}\\
4)&\neg (\exists x)(Lx\land\neg Nx)&\text{Premisa}\\
5)&(\exists x)Lx&\text{Premisa}\\
6)&La&\text{Particularización existencial 5)}\\
7)&\forall x(\neg Lx\lor Nx)&\text{Equivalencia 4)}\\
8)&\neg La\lor Na&\text{Particularización universal 7)}\\
9)&La\to Na&\text{Equivalencia del condicional 8)}\\
10)&Na&\text{Modus Ponens 6,9)}\\
11)&La\to(\exists w)[Vw\land(\exists z)(Gz\land Bz\land Hwz)\land Raw]&\text{Particularización universal 1)}\\
12)&(\exists w)[Vw\land(\exists z)(Gz\land Bz\land Hwz)\land Raw]&\text{Modus Ponens 6,11)}\\ 13)&Vb\land(\exists z)(Gz\land Bz\land Hbz)\land Rab&\text{Particularización existencial 12)}\\
14)&Vb&\text{Eliminación conjunción 15)}\\
15)&\forall x(\neg Vx\lor Cx)&\text{Equivalencia 3)}\\
16)&\neg Vb\lor Cb&\text{Particularización universal 15)}\\
17)&Vb\to Cb&\text{Equivalencia del condicional 16)}\\
18)&Cb&\text{Modus Ponens 14,17)}\\
19)&(\exists z)(Gz\land Bz\land Hbz)&\text{Eliminación conjunción 13)}\\
20)&Gc\land Bc\land Hbc&\text{Particularización existencial 19)}\\
21)&Gc&\text{Eliminación conjunción 20)}\\
22)&\forall x(\neg Gx\lor Mx)&\text{Equivalencia 2)}\\
23)&\neg Gc\lor Mc&\text{Particularización universal 22)}\\
24)&Gc\to Mc&\text{Equivalencia del condicional 23)}\\
25)&Mc&\text{Modus Ponens 21,24)}\\
26)&Bc&\text{Eliminación conjunción 20)}\\
27)&Hbc&\text{Eliminación conjunción 20)}\\
28)&Mc\land Bc&\text{Introducción conjunción 25,26)}\\
29)&Mc\land Bc\land Hbc&\text{Introducción conjunción 27,28)}\\
30)&(\exists z)(Mz\land Bz\land Hbz)&\text{Generalización existencial 29)}\\
31)&Cb\land(\exists z)(Mz\land Bz\land Hbz)&\text{Introducción conjunción 18,30)}\\
32)&Rab&\text{Eliminación conjunción 13)}\\
33)&Cb\land(\exists z)(Mz\land Bz\land Hbz)\land Rab&\text{Introducción conjunción 31,32)}\\
34)&(\exists w)[Cw\land(\exists z)(Mz\land Bz\land Hwz)\land Raw]&\text{Generalización existencial 33)}\\
35)&Na\land(\exists w)[Cw\land(\exists z)(Mz\land Bz\land Hwz)\land Raw]&\text{Introducción conjunción 10,34)}\\
36)&(\exists x)\{Nx\land(\exists w)[Cw\land(\exists z)(Mz\land Bz\land Hwz)\land Rxw]\}&\text{Generalización existencial 35)}\\
\end{array}
\)
¿Es correcto?
Sí, yo lo veo bien.
Pregunta: Como no trabajo con predicados de más de una variable, me surgió la duda de si tenemos algo del estilo \( Rabcd \) donde \( a,b,c,d \) son constantes, se puede generalizar existencialmente alguna de las variables del medio, por ejemplo \( \exists x\,Rabxd \). ¿Esto es correcto? ¿Cómo puede explicarse que es correcto teniendo en cuenta la regla 9 de las reglas de inferencia de la Tabla que dice \( p(a)\therefore\exists x\,p(x) \)? (Pienso que esa \( x \) es una variable, ¿o puede funcionar como varias variables?)
Sí, es correcto. En la regla 9 puede haber otras variables además de \[ x \] en la fórmula. Es decir, a partir de \[ p(a,b,c,d) \] puedes deducir \[ \exists x p(a,b,x,d) \] (o \[ \exists x p(x,b,c,d) \] o cualquier otra combinación). Iterando, también puedes deducir \[ \exists x \exists y p(x,y,c,d) \], o cualquier otra combinación, hasta \[ \exists x \exists y \exists z \exists t p(x,y,z,t) \] o cualquier combinación de varios existenciales.
En general la mejor estrategia con los cuantificadores (especialmente con los universales) es no eliminarlos hasta justo cuando los necesites.
Muy buena sugerencia .
Gracias.
Este creo que es un consejo útil incluso más allá de los cuantificadores. Es mejor no tocar fórmulas ni aplicar reglas hasta que lo necesites. Pero con los cuantificadores universales es especialmente importante porque muchas veces (como aquí) no sabes a qué variable te interesa particularizar hasta justo antes de que necesites usarlo.
Ahora entiendo un poco más sobre lo que decías de "saber" qué variables eran genéricas y cuáles no, porque en razonamientos como estos, el registro se desvanece más rápidamente. ¿Tienes algún "truco" para eso, como lo de eliminar los universales justo antes de particularizar?
Lo de las variables genéricas es más delicado. La cuestión es que de alguna manera tienes que distinguir a nivel formal una variable como la \[ a \] en \[ La \] del argumento anterior, de variables "genéricas" que te permitan introducir cuantificadores universales. La cuestión es que por ejemplo la inferencia \[ x=x \vdash \forall x (x=x) \] es correcta, pero sin embargo lo que no puedes hacer es pasar de \[ \exists x p(x) \] a \[ p(a) \] (esto es correcto) y de aquí a \[ \forall x p(x) \], porque la deducción \[ \exists x p(x) \vdash \forall x p(x) \] obviamente no es correcta. Por eso debe haber algo en el cálculo que te permita hacer la primera deducción pero no la segunda. Pero esto ya depende de los detalles del cálculo deductivo que se use.
