I have been working on this problem for over an hour and I think I have simply missed something. I need some help. I don't see how this is supposed to work out
Here are the premises:
Here is the goal: ∀x ∃yLikes(x,y)
I can see we will need to use existential elimination and introduction, but I do not understand why these rules are the way they are.
The problem is to derive the following using natural deduction:
Here are the premises:
- ∀x ∀y[Likes(x,y) → Likes(y,x)]
- ∃x ∀yLikes(x,y)
Here is the goal: ∀x ∃yLikes(x,y)
Using Klement's proof checker associated with the forallx textbook referenced below, this can be completed in 10 lines. The proof checker associated with the textbook you are using may require different syntax although the basic idea would be to use existential elimination and introduction with modus ponens (conditional elimination).
The real problem is understanding why the existential elimination rules work the way they do. It is relatively easy to manipulate a proof checker (or manually follow steps) to reach the correct result. It is not easy to understand why those specific steps should lead to a valid derivation. This takes studying the logic textbook itself describing existential elimination.
In forallx, existential elimination is covered in section 32.5. Given the premise ‘∃xFx’ as their example, the authors make the observation: (page 246)
Suppose we know that something is F. The problem is that simply knowing this does not tell us which thing is F. So it would seem that from ‘∃xFx’ we cannot immediately conclude ‘Fa’, ‘Fe23’, or any other substitution instance of the sentence. What can we do?
Note that, unlike universal elimination where we can substitute any name for the variable 'x' since everything in the domain is that predicate, we don't know which thing actually is F. All we know by the premise is that something in the domain is F.
After providing a proof on page 247 which is a simplification of your exercise, they make the following observation about what they did:
Breaking this down: we started by writing down our assumptions. At line 3, we made an additional assumption: ‘Fo’. This was just a substitution instance of ‘∃xFx’. On this assumption, we established ‘∃xGx’. Note that we had made no special assumptions about the object named by ‘o’; we had only assumed that it satisfies ‘Fx’. So nothing depends upon which object it is. And line 1 told us that something satisfies ‘Fx’, so our reasoning pattern was perfectly general. We can discharge the specific assumption ‘Fo’, and simply infer ‘∃xGx’ on its own.
This leads to the rules.
We must pick a name, 'o' in the case of this example, that was not previously used in an undischarged assumption nor in the line containing the existential quantifier we are eliminating. This is to make sure there are "no special assumptions about the object named by ‘o’".
We can discharge the assumption closing the subproof if we can derive a line that does not use that name so we don't take the name outside the subproof. An easy way to do that is to use existential introduction, but we also want some line that will help us complete the proof. For this example, existential introduction is all we need.
References
Kevin Klement's JavaScript/PHP Fitch-style natural deduction proof editor and checker http://proofs.openlogicproject.org/
P. D. Magnus, Tim Button with additions by J. Robert Loftis remixed and revised by Aaron Thomas-Bolduc, Richard Zach, forallx Calgary Remix: An Introduction to Formal Logic, Winter 2018. http://forallx.openlogicproject.org/
