Logica dei Predicati - Calcolo della deduzione naturale

[Howard_Wolowitz]

Innanzitutto buon giorno.
Ho cercato di svolgere i seguenti esercizi di dimostrazione della logica del primo ordine con il calcolo della deduzione naturale:
1)[tex]\vdash\neg \forall q(\chi(q) \wedge (\chi(q) \rightarrow \exists t \neg \chi(t))[/tex]
2)[tex]\forall x(\phi(x) \rightarrow \neg \psi(x))\vdash \neg \exists x (\phi(x) \wedge \psi(x))[/tex]
3)[tex]\vdash \exists x (A(x) \rightarrow B) \Leftrightarrow (\forall x A(x) \rightarrow B)[/tex]
4)[tex]\vdash \exists x (A(x) \rightarrow B(x)) \Leftrightarrow (\forall x A(x) \rightarrow \exists x B(x))[/tex]
Svolgimento
1)

2)

3)Riesco a dimostrare l'andata ma non capisco come dimostrare il ritorno

4)Come per la precedente non riesco a dimostrare il ritorno

Vi chiedo se cortesemente potete dare un'occhiata alle dimostrazioni fatte, e dirmi se sono corrette, e darmi qualche delucidazione in merito a quelle che non sono riuscito a risolvere completamente(3 e 4).
Grazie mille in anticipo e a presto!!

[perplesso1]

Ciao, non sono espertissimo, comunque per 3) e 4) ho pensato a questo

mentre la 1) e la 2) mi sembrano corrette.