# How Can I Get This Quantification Deduction?

This is a question in my logic class.

Premises:

1. $(\exists x)(Px \land Lxa)$
2. $(y)(Py \supset Lay)$
3. $(x)(y)[(Lxa \land Lay) \supset Lxy]$

Deduce:

• $(\exists x)[Px \land (y)(Py \supset Lxy)]$

So far what occurs to me is that EI 1,

$$Pu \land Lua$$ then UI 2,

$$Pu \supset Lau$$

Through MP I can get $$Lau$$ Since I have $Lau$ and $Lua$, So I can UI 3 and get $$Luv$$ Here's where I'm stuck at. Since $u$ showes up in a EI line, I can't use UG to get $$(y)(Py\supset Lxy)$$

Any idea? By the way, is there any general tips to these questions? Thanks!

-

If I follow your proof outline, I think that in your second step you should consider instantiating premise 2 with a different individual, say $c$, than the one, say $b$, that you chose as an existential witness for 1. That way, you can apply universal generalization over $c$ and then use existential elimination with $b$. Here's an outline in a proof system that's a little bit different than the one you seem to be working in. It should be close enough to get you going, though.

1. $(\exists x)(Px \land Lxa)$ Given.
2. $(y)(Py \supset Lay)$ Given.
3. $(x)(y)[(Lxa \land Lay) \supset Lxy]$ Given.
• $Pb \land Lba$ existential witness for 1.
• $Pc$ Assume.
• $\dots$
• $Lbc$
• $(y)(Py \supset Lby)$ by conditional universal introduction with 5–7.
• $\dots$
• $(\exists x)(Px \land (y)(Py \supset Lxy))$
4. $(\exists x)(Px \land (y)(Py \supset Lxy))$ by existential elimination with 1 and 4–10.
-
Got it. Thank you –  YankeeWhiskey Apr 30 '13 at 22:55

In yet a different proof system+format+notation, that of Feijen/Dijkstra/Gries/etc., we are given that

1. $\langle \exists x : P.x : L.x.a \rangle$
2. $\langle \forall y : P.y : L.a.y \rangle$
3. $\langle \forall x,y : L.x.a \land L.a.y : L.x.y \rangle$

and we are asked to prove

• $\langle \exists x : P.x : \langle \forall y : P.y : L.x.y \rangle \rangle$

The proof is a simple calculation: \begin{align} & \langle \exists x : P.x : \langle \forall y : P.y : L.x.y \rangle \rangle \\ \Leftarrow & \;\;\;\;\;\text{"weaken using 3 -- this is the only thing we know about L.x.y"} \\ & \langle \exists x : P.x : \langle \forall y : P.y : L.x.a \land L.a.y \rangle \rangle \\ \equiv & \;\;\;\;\;\text{"logic: simplify by taking L.x.a, which does not contain y, outside of \forall y"} \\ & \langle \exists x : P.x : L.x.a \land \langle \forall y : P.y : L.a.y \rangle \rangle \\ \equiv & \;\;\;\;\;\text{"logic: simplify by taking \forall y, which does not contain x, outside of \forall x"} \\ & \langle \exists x : P.x : L.x.a \rangle \land \langle \forall y : P.y : L.a.y \rangle \\ \equiv & \;\;\;\;\;\text{"using 1 and 2"} \\ & \textrm{true} \end{align}

-