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: