Mathematics Stack Exchange is a question and answer site for people studying math at any level and professionals in related fields. Join them; it only takes a minute:

Sign up
Here's how it works:
  1. Anybody can ask a question
  2. Anybody can answer
  3. The best answers are voted up and rise to the top

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)

share|cite|improve this question

marked as duplicate by Henning Makholm, Srivatsan, J. M., 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.

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.

share|cite|improve this answer
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

Not the answer you're looking for? Browse other questions tagged or ask your own question.