Pruebas de lógica relacional de predicados - ¡Pregunta difícil!

Question

Llevo cuatro horas y media trabajando en este problema y creo que simplemente se me ha escapado algo. Necesito la ayuda de mis compañeros. Las reglas que puedo utilizar son las reglas básicas de inferencia (MP, MT, HS, Simp, Conj, DS, Add, Dil.), las reglas de sustitución (DN, Comm, Assoc, Dup, DeM, BE, Contrap, CE, Exp, Dist.), CP, IP, y EI, UI, EG, UG.

He aquí el problema:

1. (x)[(y)Rxy --> (y)Ryx]
2. Rab / (x)(y)Rxy

Mi profesor nos dio la pista de usar la premisa 1 dos veces.

Me siento muy tonta porque sé que se me ha escapado algo sencillo (como siempre) pero necesito un segundo par de ojos. Por favor y gracias por vuestra ayuda.

Answer 1

Sus premisas son:

$1.\quad \forall x(\exists yRxy \to \forall yRyx)$

$2. \quad Rab$

Instanciar el primer universal con $a$ (¿qué más?) para conseguir

$3. \quad \exists yRay \to \forall yRya$

Dado un condicional, siempre hay que ver si se puede obtener el antecedente y utilizar el modus ponens. Y ¡sí! Por supuesto que se puede. Por generalización existencial en $b$ (2) te da el antecedente de (3), así que podemos usar el modus ponens para llegar a

$4. \quad \forall yRya$ .

¿Pero ahora dónde? Si vamos a llegar a una conclusión cuantificada universalmente, sabemos que vamos a necesitar obtenerla de algún wff donde los únicos parámetros sean arbitrarios (no una constante fija como $a$ ), por lo que podemos generalizar sobre ellos. Así que vamos a necesitar algo más que $4$ . Hmmmm. Ok, vamos a utilizar el puramente general (1) y instanciar con un nuevo parámetro (nombre arbitrario, variable libre, como te gusta pensar en si) $v$ . Eso es sólo fuerza bruta, pero ¿qué otra cosa podemos hacer? Es la única opción. Eso nos da

$5. \quad \exists yRvy \to \forall yRyv$

Pero, ¡ajá! Otro condicional. ¿Podemos conseguir el antecedente? Pero es inmediato que (4) nos da $Rva$ y por lo tanto $\exists yRvy$ así que el modus ponens nos da de nuevo

$6 \quad \forall yRyv$

Y ahora el final está a la vista.

Pero, ¡demonios! No podemos cuantificar eso tal cual (o mejor dicho, podemos pero entonces n obtendríamos $\forall x\forall yRyx$ que tiene las cosas al revés). Para poner los cuantificadores al revés, tenemos que dar otro paso. Instanciar (6) con un nuevo parámetro $u$ para obtener

$7 \quad Ruv$ .

Pero $u$ y $v$ eran arbitrarias, así que puedes cuantificar universalmente dos veces (¡hazlo en el orden correcto!) y obtendrás, he aquí,

$8 \quad \forall x\forall yRxy$ .

[Afortunadamente, esto es lo que a veces se llama una prueba "Just Do It", es decir, que en cada paso haces lo único sensato y todo sale bien].

Answer 2

Este es un comentario "largo" sobre la "equivalencia" de las restricciones sobre la norma UG.

En "estándar" deducción natural sistemas, tenemos que :

en $\forall$ -I la variable $x$ no puede darse gratuitamente en ninguna hipótesis en la que $\varphi(x)$ depende, es decir, una hipótesis no cancelada [véase, por ejemplo, Dirk van Dalen, Lógica y estructura (5ª ed. - 2013), página 86].

Con esta restricción, podemos demostrar, la Lema :

$\forall x (\varphi(x) \rightarrow \psi(x)) \vdash \forall x \varphi(x) \rightarrow \forall x \psi(x)$

de la siguiente manera :

1) $\forall x (\varphi(x) \rightarrow \psi(x))$ --- Suposición

2) $\varphi(a) \rightarrow \psi(a)$ --- $\forall$ -E (o UI)

3) $\forall x \varphi(x)$ --- Suposición

4) $\varphi(a)$ --- de 3) por IU

5) $\psi(a)$ --- formulario 3) y 4) por MP

6) $\forall x \psi(x)$ --- de 5) por $\forall$ -I (o UG) : $a$ no es gratis en los Supuestos

7) $\forall x \varphi(x) \rightarrow \forall x \psi(x)$ --- de 6) por $\rightarrow$ -intro, "descargando" la Asunción en 3) (por favor, compruébalo en tu libro de texto : creo que es CP).

Ahora, la "otra manera".

Me referiré a Daniel Bonevac, Deducción. Introducción a la lógica simbólica (2ª ed. - 2003), página 215 para Prueba universal (cómo demostrar una conclusión universal) y el ejemplo de la página 216, donde la restricción es que :

Generalización universal requiere que la variable sea completamente nueva en la prueba.

Procedemos como sigue :

1) $\forall x (\varphi(x) \rightarrow \psi(x))$ --- Suposición

2) $\forall x \varphi(x)$ --- Suposición

3) (queremos) Mostrar : $\forall x \psi(x)$

4) $| \quad$ a Mostrar $\psi(a)$ suponemos la constante $a$ nuevo a la prueba

5) $| \quad \varphi(a)$ --- de 2) por IU

6) $| \quad \varphi(a) \rightarrow \psi(a)$ --- de 1) por IU

7) $| \quad \psi(a)$ --- de 6) y 5) por MP

habiendo demostrado que un arbitraria objeto $a$ "es $\psi$ ", podemos concluir :

8) $\forall x \psi(x)$ ("crossig" el Mostrar ).

Por último, aplicamos $\rightarrow$ -intro (o CP) para obtener :

9) $\forall x \varphi(x) \rightarrow \forall x \psi(x)$ , cumpliendo el supuesto 2).

Espero que pueda ayudar ...