Take the 2-minute tour ×
Mathematics Stack Exchange is a question and answer site for people studying math at any level and professionals in related fields. It's 100% free, no registration required.

This is a question in my logic class.


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


  • $(\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!

share|improve this question
add comment

2 Answers 2

up vote 2 down vote accepted

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.
share|improve this answer
Got it. Thank you –  YankeeWhiskey Apr 30 '13 at 22:55
add comment

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

share|improve this answer
add comment

Your Answer


By posting your answer, you agree to the privacy policy and terms of service.

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