# Thread: First order logic

1. ## First order logic

Hi, I have no idea how to begin constructing this proof, and I would appreciate any help!

I need to prove the following, and to make matters worse, without soundness or completeness

⊢ (∀x.ϕ) →(∃x.ϕ)

I can use the following axioms/theorems http://img233.imageshack.us/img233/5...11115at824.png Thank you.
Please note that any sort of help to get me started on the proof would be very helpful.

2. ## Re: First order logic

Is ∃x.ϕ defined as ¬∀x.¬ϕ, since the axioms don't mention ∃? Do you have any previously derived theorems about ∃, such as $\phi^x_t\to\exists x.\,\phi$? Also, are you allowed to use the deduction theorem?

3. ## Re: First order logic

Originally Posted by emakarov
Is ∃x.ϕ defined as ¬∀x.¬ϕ, since the axioms don't mention ∃? Do you have any previously derived theorems about ∃, such as $\phi^x_t\to\exists x.\,\phi$? Also, are you allowed to use the deduction theorem?
Thanks,
Yes I believe that $\phi^x_t\to\exists x.\,\phi$ would be okay. And I'm allowed to use the deduction theorem.

Thank you.

4. ## Re: First order logic

The idea is to assume $\forall x.\,\phi$ and $\forall x.\,\neg\phi$, then instantiate both quantifiers to x and derive $\phi\land\neg\phi$. Then by deduction theorem $\forall x.\,\phi\vdash (\forall x.\,\neg\phi)\to\phi\land\neg\phi$, from where one has to derive $\forall x.\,\phi\vdash\neg\forall x.\,\neg\phi$. It would help to first derive $(A\to B\land\neg B)\to\neg A$ for all formulas A and B.