I tried to derive $\forall x (P(x) \to Q(x)) \to (\exists x P(x) \to \exists x Q(x))$ using deduction lemma but without Godel's Theorem, but I stucked.

My attempt. Let's use deduction lemma and add $\forall x (P(x) \to Q(x))$ to our axioms. Now we have to derive $\exists x P(x) \to \exists x Q(x)$. Okay, let's use deduction lemma one more time and now add $\exists x P(x)$ to our axioms. Finally we have to prove $\vdash \exists x Q(x)$. From $\forall x (P(x) \to Q(x))$ we can obtain $\vdash P(x) \to Q(x)$, but it seems useless. From second formula using modus ponens one can obtain $\vdash \exists x Q(x) \to \exists x P(x)$ but it also seems extremely useless. Unfortunately, Bernays rules are not applicable to $\forall x (P(x) \to Q(x))$. For sure I have to use some tautology but I'm confused.

Edit. I can use:

  1. Special cases of tautologies.
  2. $A(t) \to \exists u A(u)$.
  3. $\forall u A(u) \to A(t)$.
  4. Modus ponens.
  5. Bernays rule 1.
  6. Bernays rule 2.
  7. Deduction lemma.
  • 1
    $\begingroup$ I assume that you are not licensed to use Natural Deduction ... What are the axioms and rules of your proof system ? $\endgroup$ – Mauro ALLEGRANZA Mar 3 '15 at 19:56
  • $\begingroup$ @MauroALLEGRANZA 1. Special cases of tautologies 2. $A(t) \to \exists u A(u)$ 3. $\forall u A(u) \to A(t)$ 3. Modus ponens 4, 5. Bernays rules. $\endgroup$ – Jihad Mar 3 '15 at 19:59

Assuming the equivalence between $\forall$ and $\lnot \exists \lnot$, here is a proof sketch...

1) $∀x(P(x)→Q(x))$ --- premise

2) $P(x)→Q(x)$ --- from 1) by quantifier axiom : $∀u A(u) → A(t)$ and modus ponens

3) $\lnot Q(x) → \lnot P(x)$ --- from 2) by tautological implication

4) $\forall x \lnot Q(x)$ --- assumed [a]

5) $\lnot Q(x)$ --- from 4) by quantifier axiom

6) $\lnot P(x)$ --- from 3) and 5) by mp

7) $\forall x \lnot Q(x) \to \lnot P(x)$ --- from 4) and 6) by Deduction Theorem, discharging assumption [a]

8) $\forall x \lnot Q(x) \to \forall x \lnot P(x)$ --- using Bernays' rule : if $C \to A(x)$, then $C \to \forall x A(x)$, provided that $x$ is not free in $C$

9) $\lnot \forall x \lnot P(x) \to \lnot \forall x \lnot Q(x)$ --- from 8) by tautological implication

10) $\exists x P(x) \to \exists x Q(x)$ --- from 9) by equivalence between quantifiers.

We can avoid the equivalence between quantifiers ...

To do this, we need a "derived rule", the so-called $\exists$-elimination rule, easily proved with Bernays' rule : if $\Gamma, A(x) \vdash C$, then $\Gamma, \exists x A(x) \vdash C$, with $x$ not free in $C$ nor in $\Gamma$.

1)-2) as above

3) $\exists xP(x)$ --- assumed [a]

4) $P(x)$ --- assumed [b]

5) $Q(x)$ --- from 2) and 4) by mp

6) $\vdash Q(x) \to [(\lnot R \lor R) \to Q(x)]$ --- tautology : $A \to (B \to A)$

7) $(\lnot R \lor R) \to Q(x)$ --- from 5) and 6) by mp

8) $(\lnot R \lor R) \to \forall x \ Q(x)$ --- by Bernays' rule

9) $\vdash \lnot R \lor R$ --- tautology

10) $\forall x \ Q(x)$ --- from 9) and 8) by mp

From 4)-10) we have : $P(x) \vdash \forall x \ Q(x)$; we apply the $\exists$-elimiantion rule ($x$ is not free in $\forall x \ Q(x)$, nor in the premise 1)) to derive :

11) $\exists x \ P(x) \vdash \forall x \ Q(x)$

12) $\exists x \ P(x) \vdash \exists x \ Q(x)$ --- from 11) by the quantifier axioms and mp

13) $\exists x \ P(x) \to \exists x \ Q(x)$ --- from 12) by Deduction Th.

  • $\begingroup$ Nice, my thanks! $\endgroup$ – Jihad Mar 3 '15 at 20:13

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.