# Formal Proofs: $\vdash Py \land \exists x Qx \rightarrow \exists x (Py \land Qx)$

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.

• Is $\exists$ short for something? There no axioms which include $\exists$. – Git Gud Nov 18 '14 at 1:21
• Yes $\exists x$ is short for $\neg \forall x \neg$ – Bobby Lee Nov 18 '14 at 3:19

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)$

7) $\vdash Py∧∃xQx → ∃x(Py∧Qx)$ --- by Deduction Theorem.