Deduzione naturale con predicati con più variabili

[cellkurt1]

Per la prima volta in un esercizio dove bisogna provare una tautologia mi sono trovano nella situazione di dover gestire dei predicati con due variabili, ma non so come usare le regole di deduzione naturale per gestire questo caso

\(\displaystyle (\exists x:(P x)) => ((\forall x:((P x) => (Qx x)))=> (\exists x:(\exists y:(Qx y)))) \)

Questo è il tentativo che ho fatto:
http://i57.tinypic.com/2u8xxc9.jpg
(Scusate la mia scrittura orribile )

Come andare avanti?

[cellkurt1]

up

[cellkurt1]

up

[Pappappero1]

Non conosco il metodo con cui stai risolvendo questo esercizio. Ti spiego la procedura con cui personalmente risolverei questo esercizio (e l'unica che conosco). Non spieghero' la teoria che c'e' dietro, limitandomi a fornire link alle pagine di wikipedia che potrebbero dare almeno in parte le informazioni necessarie.

Prima di tutto scioglierei le implicazioni usando che $A \to B$ e' equivalente a $\neg A \vee B$. Poi porterei tutti i quantificatori davanti, portando la formula in PNF, facendo attenzione a dare nomi diversi a tutte le variabili vincolate (cioe' quantificate) e portando l'interno della formula in CFN. Infine eliminerei i quantificatori esistenziali usando il processo di skolemizzazione. A questo punto quello che resta e' semplicemente una CNF vincolata, che puo' essere risolta con la procedura di Davis Putnam (associata magari ad istanziazioni successive).