# Need alternative proof to $\exists x (k(x) \rightarrow t)$ entails $\forall x (k(x)) \rightarrow t$

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

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