Here is the question from Language, Proof and Logic (LPL). Problem 13.30:
1. | Likes(carl, max) 2. | ∀x [∃y (Likes(y, x) ∨ Likes(x, y)) → Likes(x, x)] |––– ...| ?? | ∃x Likes(x, carl)
I haven't had an issue with any of the other questions in this chapter, but this one is really throwing me for a loop. I suppose my issues are caused by carl and max (not nice guys, apparently). I tried finding hints and solutions on the internet, but I couldn't find a solution nor something helpful enough anywhere. According to Trinity University, it requires not a single subproof. I tried this many ways, but always ended up at a dead-end. My most recent attempt was to add this:
3. | Likes(max, carl) ∨ Likes(carl, max) ∨ Intro, 1 4. | ∃y (Likes(y, carl) ∨ Likes(carl, y)) ∃ Intro, 3
But that didn't get me anywhere… Fitch tells me that I may not use that to deduce that
Likes(carl, carl) through
→ Elim. I tried to introduce
∀x first, but this did not help either. This is a very confusing problem for me.