# Logic – Deductive proof with quantifiers (Fitch/LPL 13.30)

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.

• @zagadka. In case the line "?? | Exists y(x, carl)" does not contains a typo: What is meant? – Jo Wehler Aug 11 '15 at 18:38
• @jowehler I meant that the "??" represents whatever number that line happens to be, since I do not know that number. It is nothing important. I did miss "Likes" after the y, however. I fixed that. – zagadka314 Aug 11 '15 at 18:53
• Now remains my question why this line contains y and x? I suppose it should read either x or y. – Jo Wehler Aug 11 '15 at 19:05
• @jowehler Ah! Sorry about that, it looks like there was a single lingering PEBCAK error ;-) – zagadka314 Aug 11 '15 at 19:27