Esercizio di Logica - deduzione in N

[Sk_Anonymous]

Sono date le seguenti ipotesi:

1-$\forall x(p(x)vvd(x))$
2- $\not\existsx(p(x)^^^d(x))$
3- $\forallx(p(x)->p(x*x))$
4 - $forallx(d(x)->d(x*x))$

dedurre $\forallx(p(x)\equivp(x*x))$ da 1-4.

Al di là dell'estrema banalità del ragionamento (:-D), il mio docente vuole la deduzione sviluppata per bene, usando solo le regole del sistema di deduzione naturale (non basta un'argomentazione a parole, quindi). La prima cosa da fare, ovviamente, è eliminare i quantificatori universali (usando l'apposita regola di eliminazione secondo cui da $\forallx(A(x))$ deduco $A(a)$). Da $p(a)$ e $p(a)->p(a*a)$ deduco immediatamente $p(a*a)$. Adesso devo dedurre $p(a)$ da $p(a*a)$, usando solo le ipotesi sopra scritte. Qualche suggerimento?

EDIT: errore di digitazione.

[fields1]

Supponi per assurdo $\not p(a)$. Da 1. ottieni $p(a)\vee d(a)$. Ora usi la regola di eliminazione or rispetto a $p(a)\vee d(a)$, deducendo $d(a)$ da $p(a)$ e deducendo $d(a)$ da $d(a)$; ottieni allora $d(a)$. Di qui e' in discesa...

[Sk_Anonymous]

Ok, adesso quadra. Grazie per l'aiuto