First order logic, Hilbert's System. For those familiar with Enderton's Introduction to Mathematical Logic, I am allowed the same axioms. For those unfamiliar, I can use these axioms:
$\forall x \alpha \rightarrow \alpha_t^x$, where $t$ is substitutable for $x$ in $\alpha$.
$\forall x (\alpha \rightarrow \beta)\rightarrow(\forall x \alpha \rightarrow \forall x \beta)$
$\alpha \rightarrow \forall x \alpha$, where $x$ does not occur free in $\alpha$
And if the language includes equality,
- $x=y \rightarrow (\alpha \rightarrow \alpha')$, where $\alpha$ is atomic and $\alpha'$ is obtained from $\alpha$ by replacing $x$ in zero or more places by $y$.
The problem is $\vdash Py \land \exists x Qx \rightarrow \exists x (Py \land Qx)$. I'm really stuck on this problem. I mean, intuitively it makes sense ... $Py$ doesn't rely on $x$ and we know that there is an $x$ that satisfies $Qx$... thus it is intuitively obvious that $\exists x (Py \land Qx)$. The thing is, I can't figure out a sequence of deductions to arrive there (formally). Can somebody give me a hand? I've been staring at this problem for too long now.