I am trying to use existential elimination to derive Brillig(a) & Tove(a). how would I do this? I have tried to do separate sub proofs to prove both Brillig(a) & Tove(a) but that doesn't work either. Can someone point me in the right direction?enter image description here

  • You may not derive that. Why do you want to? Commented Jun 9, 2020 at 1:50
  • Sorry I posted the answer to this proof as a reply to my post. I didn't need to use the first premise which through me off.
    – Samaritna
    Commented Jun 9, 2020 at 18:16

2 Answers 2


The reason you are having trouble doing that, is that that can not be done.

It is not a valid derivation. The conjunction of two existences does not entail an existence of a conjunction.

Neither do the other two premises enable it to be derived.

PS: Existential Elimination requires an existential statement, and the assumption of a witness for that existence, under which is derived a statement that does not freely contain the witness variable.

i|  Ǝx T(x)      Derived or Premised
j|  |_ [a] T(a)  Assumption (of a witness for i)
 |  |  :
k|  |  S         Derived Somehow; S does not contain the witness variable
 |  S            Ǝ Elimination i,j-k

I figured it out for people that stumble across this again. For the solution I found statement 1 isn't needed.enter image description here

Not the answer you're looking for? Browse other questions tagged .