# 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. is back., Asaf Karagila, t.b.Nov 16 '11 at 17:30

This question has been asked before and already has an answer. If those answers do not fully address your question, please ask a new question.

## 1 Answer

If the asterisks in your axioms mean that the axioms are to be fully universally quantified, so that they become sentences, and if your language has no constant symbols, then it will not be possible to make the desired deduction in your system. The reason is that since all the axioms are fully universally quantified, they are (vacuously) true in the empty structure, and your rule of inference is truth-preserving for any structure including the empty structure. But your desired deduction is not valid for the empty structure, since the hypothesis is vacuously true there, but the conclusion is not. So it would actually be unsound for you to able to make that deduction. Your desired validity is only valid in nonempty domains, and so you need a formal system appropriate for reasoning in nonempty domains.

-
But perhaps by the asteriskses you don't mean to have only sentential axioms, in which case you will be able to make the deduction by a use of axiom 5, to instantiate the universal quantifier by a term and thereby gain existential import. –  JDH Nov 16 '11 at 4:40
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
∀* means it is a finite sequence of universal quantifiers (possible 0) I should have pointed this out :\ –  DillPixel Nov 16 '11 at 5:26