Lógica: Ejercicio 7 Parte e

Hola, no estoy pudiendo resolver esta parte sigo los siguientes paso(en particular no puedo derivar $\varphi$ )

Introduccion del para todo
Introduccion del si solo si
A la derecha me queda $\varphi$
Intento aplicar la regla $RI_4 *$
A la izquierda me queda $y =´ x$ y a la derecha $\varphi [y/x]$ y de ahi no se que hacer
Intento aplicar eliminación del implica o la regla $RI_2$ pero se empiezan a repetir las derivacion

Saludos
Diego

Re: Ejercicio 7 Parte e

de Guillermo Calderon - InCo - jueves, 1 de junio de 2023, 11:57

Hola:

En la derivación de la derecha, la clave está en encontrar la sustitución apropiada para la eliminación del para todo con la hipótesis $\forall y (x =' y \to \varphi[y/x])$ .

Aquí te recomiendo que busques un término $t$ para sustituir la $y$ de manera que te quede algo así:

$x ='t \to \varphi[t/x]$

donde:

$x =' t$ se pueda derivar sin hipótesis
$\varphi[t/x]$ sea igual $\varphi$

Con eso sale fácil.