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?

  • $\begingroup$ $\checkmark$ Looks good. $\endgroup$ – Graham Kemp Nov 25 '14 at 1:31

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.


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.


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.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.