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:
Tautologies
$\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=x$
- $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.
In your comment there is the key to the solution : $\exists x$ in Enderton's proof system is an abbreviation for $\lnot \forall \lnot$.
1) $Py∧∃xQx$ --- assumed
2) $Py \land \lnot \forall x \lnot Qx$ --- abbreviation
3) $\lnot (Py \rightarrow \forall x \lnot Qx)$ --- with the tautology : $(\alpha \land \lnot \beta) \leftrightarrow \lnot (\alpha \rightarrow \beta)$
4) $\lnot \forall x(Py \rightarrow \lnot Qx)$ --- by EXAMPLE (Q2A) [page 121] : if $x$ does not occur free in $\alpha$, then $\vdash (α → ∀xβ) ↔ ∀x(α → β)$ : $x$ is not free in $Py$.
5) $\exists x \lnot (Py \rightarrow \lnot Qx)$ --- by abbreviation
6) $\exists x (Py \land Qx)$ --- with the tautology : $(\alpha \land \beta) \leftrightarrow \lnot (\alpha \rightarrow \lnot \beta)$