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

Question

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

1. $\exists x (Py \land Qx) \rightarrow Py$ (Tautology)
2. $\exists x (Py \land Qx)$ (Assumed)
3. $Py$ (Modus ponens)

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

1. $\exists x (Py \land Qx) \rightarrow \exists x Qx$ (Tautology)
2. $\exists x (Py \land Qx)$ (Assumed)
3. $\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?

Answer 1

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.