Buenas, llegué a la siguiente derivación, pero esta contiene errores en las restricciones, los cuales marqué con rojo.
Hay una hipótesis que no usé, lo cual esta claro que tendría que usarla ,pero no me doy cuenta como ni en donde.
Que correcciones tendría que hacer en la derivación?
gracias.
Buenas:
La idea de las dos eliminaciones de existe con φ₂ está bien orientada.
Te sugiero usar usar la hipótesis (∀x)(∀y)(P₃(x,y) ↔ P₂(x,y)).
La idea es derivar ¬P₃(x,y) por introducción de la negación.
Tendrías que armar algo así:
[P₃(x,y)]⁽¹⁾
⋮
¬P₂(x,y) P₂(x,y)
————————————————————————
⊥
——————————— I¬⁽¹⁾
¬P₃(x,y)
̌ ⋮
Donde ¬P₂(x,y) sale de las dos eliminaciones del ∃. La derivación de P₂(x,y) es muy fácil de obtener usando la hipótesis que se agrega a Γ.