[Solved]: Using natural deduction, show that: ∀x.(P (x) → Q(x)), ∃x.P (x) ⊢N ∃x.Q(x)

Problem Detail: 

1. How I would show: ∀x.(P (x) → Q(x)), ∃x.P (x) ⊢N ∃x.Q(x) using Natural Deduction?

2. Would I not need to know what P(x) and Q(x) are to prove soundness and completeness?

Asked By : JollyGr33nGiant

Answered By : Andrej Bauer

We would like to prove $(\forall x . P(x) \to Q(x)), (\exists y . P(y)) \vdash \exists z . Q(z)$.

Let us first do it in plain language, but still in natural deduction. We have hypotheses

1. $(\forall x . P(x) \to Q(x))$
2. $\exists y . P(y)$

We use hypothesis 2: there is $a$ such that $P(a)$. We use hypothesis 1 applied to the case $x := a$ to obtain:

3. $P(a) \to Q(a)$.

We already know that $P(a)$, therefore we can use 3 to get $Q(a)$. We therefore conclude that $\exists z . Q(z)$. QED.

I am not going to draw boxes because you can get them on the web:

• go to ProofWeb and in the section called "Proof assistants on the web" login as guest and select the Coq proof assistant.
• under the "Display menu option select "Fitch style box proofs" or "Gentzen-style tree proofs"

• type the following code into the left-hand window:

  Parameter A : Set. Parameter P : A -> Prop. Parameter Q : A -> Prop.  Lemma foo: (forall x, P(x) -> Q(x)) -> (exists y, P(y)) -> exists z, Q(z). Proof.   intros H1 H2.   destruct H2 as [a H2'].   exists a.   apply (H1 a).   exact H2'. Qed.​ 

• Now move down line by line with the "down" arrow in the upper-left corner. Watch the proof unfold in the lower-right text area.

Best Answer from StackOverflow

Question Source : http://cs.stackexchange.com/questions/50151

 Ask a Question

 Download Related Notes/Documents