How Can I Get This Quantification Deduction? This is a question in my logic class.
Premises:


*

*$(\exists x)(Px \land Lxa)$

*$(y)(Py \supset Lay)$

*$(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!
 A: 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.


*

*$(\exists x)(Px \land Lxa)$ Given.

*$(y)(Py \supset Lay)$ Given.

*$(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))$


*$(\exists x)(Px \land (y)(Py \supset Lxy))$ by existential elimination with 1 and 4–10.

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


*

*$\langle \exists x : P.x : L.x.a \rangle$

*$\langle \forall y : P.y : L.a.y \rangle$

*$\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}
$$
