[Parcial 2013 - Ejercicio 2.b.I] Error en YODA

[Parcial 2013 - Ejercicio 2.b.I] Error en YODA

de Javier Agustin Sanchez Burgos -
Número de respuestas: 0

Buenas tardes, en la clase de consulta correspondiente al día de hoy 29 de junio de 2015 comente el siguiente problema a los profesores Romina Romero y Fernando Carpani quienes me pidieron que lo haga publico para discutir en eva.

"b. Demuestre o refute las siguientes afirmaciones.
    I. |= (All x)(P(f(x)) ^ (Exi y)¬P(y)) \/ ((Exi x)(All y)(x=y)->(All x)x=f(x))."

Para justificar esta afirmación nos paramos por completitud en una derivación, por una introducción del OR 2 pensamos en probar ((Exi x)(All y)(x=y)->(All x)x=f(x).
El problema radica en la introducción del universal, ya que tenemos (por la eliminación del existencial) la hipótesis (All y)x=y, con x libre en dicha hipótesis. Por lo tanto no se debería permitir hacer esa introducción del universal.
Adjunto la derivación en YODA:
errorjoda(IAll)