How Can I Get This Quantification Deduction?

Question

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!

Answer 1

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.
4. • $Pb \land Lba$ existential witness for 1.
5. • • $Pc$ Assume.
6. • • $\dots$
7. • • $Lbc$
8. • $(y)(Py \supset Lby)$ by conditional universal introduction with 5–7.
9. • $\dots$
10. • $(\exists x)(Px \land (y)(Py \supset Lxy))$
11. $(\exists x)(Px \land (y)(Py \supset Lxy))$ by existential elimination with 1 and 4–10.

Answer 2

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