Formal Proofs: $\vdash \exists x (Py \land Qx) \rightarrow Py \land \exists x Qx$ I wish to show $\vdash \exists x (Py \land Qx) \rightarrow Py \land \exists x Qx$  using the Hilbert System in First-Order Logic with the following 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$.
  

Here is my attempt to show $\vdash \exists x (Py \land Qx) \rightarrow Py \land \exists x Qx$:


*

*$\exists x (Py \land Qx) \rightarrow Py$ (Tautology)

*$\exists x (Py \land Qx)$ (Assumed)

*$Py$ (Modus ponens)


We have shown that $\exists x (Py \land Qx) \vdash Py$.


*

*$\exists x (Py \land Qx) \rightarrow \exists x Qx$ (Tautology)

*$\exists x (Py \land Qx)$ (Assumed)

*$\exists x Qx$ (Modus ponens)


We have shown that $\exists x (Py \land Qx) \vdash \exists x Qx$. By Rule T, $\exists x (Py \land Qx) \vdash Py \land \exists x Qx$. And by the Deduction Theorem,  $\vdash \exists x (Py \land Qx) \rightarrow Py \land \exists x Qx$.
Is this correct?
 A: Step 1 : $∃x(Py∧Qx)→Py$ (tautology) is not correct : it is not a tautology (in the sense of propositional logic).
See in Enderton [page 114] the discussion about tautologies :

Axiom group 1 consists of generalizations of formulas to be called tautologies. These are the wffs obtainable from tautologies of sentential logic (having only the connectives ¬ and →) by replacing each sentence symbol by a wff of the first-order language.

Of course it is valid, but to use it in a formal proof according to Enderton's proof system, we have to prove it ...

We can to "mimick" the proof of the previous post.
1)  $∃x(Py∧Qx)$ --- assumed
2) $\lnot \forall x \lnot(Py∧Qx)$ --- abbreviation
3) $\lnot \forall x (Py \rightarrow \lnot Qx)$  --- with the tautology : $¬(α∧β)↔(α→¬β)$
4) $\lnot (Py \rightarrow \forall x \lnot Qx)$ --- by EXAMPLE (Q2A) [page 121] : if $x$ does not occur free in $α$, then $⊢(α→∀xβ)↔∀x(α→β)$ : $x$ is not free in $Py$.
5) $Py \land \lnot \forall x \lnot Qx$ --- with the tautology : $(α∧¬β)↔¬(α→β)$
6) $Py \land \exists Qx$ --- abbreviation


7) $∃x(Py∧Qx) \rightarrow Py \land \exists Qx$ --- by Deduction Theorem.



Note
To be "formal", in step 3) we apply a tautological transformation "inside" the universal quantifier; it must be understood as a "shorthand" for the sub-proof :
$2)$ $\lnot \forall x \lnot(Py∧Qx)$ 
$2_A)$ $\forall x(Py \rightarrow \lnot Qx)$ --- assumed [a]
$2_B)$ $(Py \rightarrow \lnot Qx)$ --- by Ax.2 and modus ponens
$2_C)$ $\lnot(Py∧Qx)$  --- with the tautology : $(α→¬β)↔¬(α∧β)$
$2_D)$ $\forall x\lnot(Py∧Qx)$ --- by Gen Th : $x$ is not free in $2_A$
$2_E)$ $\forall x(Py \rightarrow \lnot Qx) \rightarrow \forall x \lnot (Py \land Qx)$ --- from $2_A)$ and $2_E)$ by Deduction Theorem, discharging [a]
$2_F)$ $\lnot \forall x \lnot (Py \land Qx) \rightarrow \lnot \forall x(Py \rightarrow \lnot Qx)$ --- from $2_E)$ with the tautology : $(α→β)↔(¬β→¬α)$
$3)$ $\lnot \forall x (Py \rightarrow \lnot Qx)$  --- from $2)$ and $2_F$ by modus ponens.


Addendum
We can prove : $∃x(Py∧Qx) → Py$ from the tautology : $(Py∧Qx) → Py$.
1) $\vdash (Py∧Qx)→Py$ --- tautology
2) $\vdash \lnot Py \rightarrow \lnot (Py∧Qx)$ --- from $(α→β)↔(¬β→¬α)$ by modus ponens
3) $\vdash \forall x [\lnot Py \rightarrow \lnot (Py∧Qx)]$ --- by Gen Th [page 117] : $\Gamma = \emptyset$
4)  $\vdash \lnot Py \rightarrow \forall x \lnot (Py∧Qx)$ --- by EXAMPLE (Q2A) [page 121] : $x$ is not free in $Py$, and mp
5) $\vdash \lnot \forall x \lnot (Py∧Qx) \rightarrow Py$ --- as in 2) and using double negation

6) $\vdash \exists x (Py∧Qx) \rightarrow Py$ --- abbreviation.


In the same way, we can prove $∃x(Py∧Qx) → ∃xQx$ from the tautology : $(Py∧Qx) → Qx$; in this case we need Ax.3.
