I tried to prove $ \exists x (k(x) \rightarrow t)$ entails $\forall x (k(x)) \rightarrow t $ as;

  1. $ \exists x (k(x) \rightarrow t)$

  2. $ \exists x (\neg k(x) \lor t)$

  3. $ \exists x (\neg k(x)) \lor \exists x(t)$

  4. $ \neg \forall x (k(x)) \lor \exists x(t)$

  5. $ \neg \forall x (k(x)) \lor t$

  6. $ \forall x (k(x)) \rightarrow t$

Also tried elimination and introduction on $ \forall$ and $ \exists$ operators, but couldn't find a smarter way out. I guess there should be a much more simpler way, any ideas?


We assume that : $x$ is not free in $t$.

Thus :

$∃x(k(x)→t)$ --- premise

1) $k(x)→t$ --- assumed [a] for $\exists$E

2) $∀xk(x)$ --- assumed [b]

3) $k(x)$ --- from 2) by $\forall$E

4) $t$ --- from 1) and 3) by $\rightarrow$E

5) $∀xk(x) \rightarrow t$ --- from 2) and 4) by $\rightarrow$I, discharging assumption [b]

We have derived $∀xk(x) \rightarrow t$ from assumption [a] : $k(x)→t$. Due to the fact that $x$ is not free in $t$, we have that $x$ is not free in $∀xk(x) \rightarrow t$; thus the proviso for $\exists$E is fulfilled and we can derive :

6) $∀xk(x) \rightarrow t$ --- from 1) and 5) by $\exists$E, discharging assumption [a].

Thus, we have proved :

$∃x(k(x)→t) \vdash ∀xk(x) \rightarrow t$.

  • $\begingroup$ Could you explain what FV(t) is? $\endgroup$ – Cnqt Nov 3 '14 at 7:18
  • $\begingroup$ @Cnqt - $x \notin FV(t)$ means : "variable $x$ is not free in formula $t$" ... $\endgroup$ – Mauro ALLEGRANZA Nov 3 '14 at 7:36
  • 1
    $\begingroup$ Should it be "-> introduction" instead of "-> elimination" on row 5? $\endgroup$ – Cnqt Nov 3 '14 at 20:16

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.