Esercizietto di logica

[Sk_Anonymous]

Qualcuno mi dà una mano con questo esercizio di logica?
Tutti i professori simpatici sono pericolosi. Esistono professori simpatici. Dedurre che esistono professori pericolosi.

Devo svolgere questo esercizio usando un albero. Ho formalizzato le assunzioni in questo modo: $\forallx(s(x)\rightarrowp(x))$ e $\existsx(s(x))$. Non riesco a dedurre, però, $\existsx(p(x))$. Qualche suggerimento?

EDIT: sicuramente è necessario applicare la regola di eliminazione dell'operatore $\forall$: il primo assunto diventa pertanto $s(a)\rightarrowp(a)$.

[TomSawyer1]

$Sz \vdash Sz \quad\quad Pz \vdash Pz$
$\Sz \to Pz, Sz \vdash \Pz$
$\forall x(Sx \to Px), Sz \vdash \exists xPx$
$\forall x(Sx \to Px), \exists xSx \vdash \exists xPx$
$\forall x(Sx \to Px) \wedge \exists x Sx \vdash \exists xPx$

Devi solo stare attento all'ordine con cui fai la sostituzione delle variabili, eliminando i quantificatori. In questo caso, conviene operare per prima la sostituzione $\exists x Sx = Sz$, perché è l'unica che ti impone delle restrizioni.

EDIT: ho letto ora che devi farlo con un albero. In che modo?