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?
-
You may not derive that. Why do you want to?– Graham KempJun 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.– SamaritnaJun 9, 2020 at 18:16
Add a comment
|
2 Answers
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.