Prove $\forall_x(P(x)\rightarrow Q(x))\rightarrow (\exists_x P(x)\rightarrow \exists_x Q(x))$ is a tautology

first-order-logiclogicpredicate-logic

I need to prove or disprove whether $\forall_x(P(x)\rightarrow Q(x))\rightarrow (\exists_x P(x)\rightarrow \exists_x Q(x))$ is a tautology. I've determined that this is indeed a tautology, because if $P(x)$ is false for every $x$ then the formula is true, and if $\forall_x(P(x)\rightarrow Q(x))$ is true and there is at least one $x$ for which $P(x)$ is true and $Q(x)$ is true then both $\forall_x(P(x)\rightarrow Q(x))$ and $(\exists_x P(x)\rightarrow \exists_x Q(x))$ are true.

My problem is formulating the formal proof. I have the 3 tautology axioms from Hilbert system

  1. $[\varphi\rightarrow (\psi \rightarrow \varphi)]$
  2. $([\varphi\rightarrow (\psi \rightarrow \theta)]\rightarrow [(\varphi\rightarrow \psi)\rightarrow (\varphi\rightarrow \theta)])$
  3. $[(\neg \varphi \rightarrow\neg\psi )\rightarrow (\psi\rightarrow\varphi )]$

and the inference rules are $\frac{\varphi , (\varphi\rightarrow\psi)}{\psi}$ and $\frac{\varphi}{\forall_x\varphi}$. As the second rule doesn't seem relevent here I tried to prove some $\varphi$ and $\varphi\rightarrow \forall_x(P(x)\rightarrow Q(x))\rightarrow (\exists_x P(x)\rightarrow \exists_x Q(x))$ then use modus ponens to prove what's needed but I can't get to anything remotely close to that so I tried to prove that $\{\forall_x(P(x)\rightarrow Q(x))\}\vdash (\exists_x P(x)\rightarrow \exists_x Q(x))$ and then by deduction $\vdash \forall_x(P(x)\rightarrow Q(x))\rightarrow (\exists_x P(x)\rightarrow \exists_x Q(x))\Longrightarrow \models \forall_x(P(x)\rightarrow Q(x))\rightarrow (\exists_x P(x)\rightarrow \exists_x Q(x))$ but here too I'm never able to get only the needed formulae for proving that it is a tautology

EDIT: I can get rid of $\exists$ as I don't have an inference rule for this quantifier
$\forall_x(P(x)\rightarrow Q(x))\rightarrow (\exists_x P(x)\rightarrow \exists_x Q(x))\equiv\forall_x(P(x)\rightarrow Q(x))\rightarrow (\neg\forall_x \neg P(x)\rightarrow \neg\forall_x \neg Q(x))$

Best Answer

Hint

Without rules and axioms for $\exists$ you have to consider it an abbreviation for $\lnot \forall \lnot$.

Thus, you have to prove $\lnot \exists x Qx \to \lnot \exists x Px$ and then use the third propositional axioms.

This is equivalent to: $\forall x \lnot Qx \to \forall x \lnot Px$ that derives from $\forall x (Px \to Qx)$ by Instantiation and Contraposition and Generaliztion using $\forall x (\alpha \to \beta) \to (\forall x \alpha \to \forall x \beta)$.

Related Question