# First Order Logic (deduction proof in Hilbert system) [duplicate]

Possible Duplicate:
First order logic proof question

I need to prove this: ⊢ (∀x.ϕ) →(∃x.ϕ)

Using the following axioms:

The only thing I did was use deduction theorem: (∀x.ϕ) ⊢(∃x.ϕ)

And then changed (∃x.ϕ) into (~∀x.~ϕ), so: (∀x.ϕ) ⊢ (~∀x.~ϕ)

How can I continue with this? I cannot use soundness/completeness theorems.

EDIT: ∀* means it is a finite sequence of universal quantifiers (possible 0)

-

## marked as duplicate by Henning Makholm, Srivatsan, J. M., Asaf Karagila, t.b.Nov 16 '11 at 17:30

Similarly, if your language has a constant symbols $c$, then from $\forall x \varphi(x)$ you may deduce $\varphi(c)$, and from $\forall x\neg\varphi(x)$ you can deduce $\neg\varphi(c)$, and so putting things together you may deduce $\neg\forall x\neg\varphi(x)$, which is what you want. – JDH Nov 16 '11 at 5:07