# Language Proof and logic Chapter 13 problem 31

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:

• ∀x ∀y[Likes(x,y) → Likes(y,x)]
• ∃x ∀yLikes(x,y)

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.

• I made an edit to add what I think is the issue to avoid this question being closed. You may roll this back if I misrepresented your concern. – Frank Hubeny Dec 4 '18 at 14:55

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.

Existential Introduction is easy. [Just avoid scope collisions when binding a term to the existential quantifier.]

``````: | : :
7.| |  Q(b)
8.| |  ∃y Q(y)    ∃I, 7
``````

If a predicate is true for a term that does exist in the context, then in that context there exists some term which makes the predicate true.

Thus we "introduce" an existential statement.

Existential Elimination is slightly more involved.

Having derived a predicate in a context that makes an assumption that is a witness for an existential statement (outside the context), and the predicate does not include the assumed term, then that assumption may be discharged to deduce the predicate outside that context.

``````1.|  ∃y P(y)                   an existential statement about a predicate
2.|  |_ [b] P(b)               an assumed witness for that predicate
: |  |  :
8.|  |  R                      R does not include b as a free term
9.|  R           ∃E, 1, 2-8
``````

We "eliminate" the existential in line `1`, to derive the conclusion of the sub-proof in lines `2-8`.

These are often combined. Existential Introduction is used to derive a predicate that does not include the term for the witness, so that Existential Elimination may be employed.

``````1.|  ∃y P(y)
2.|  |_ [b] P(b)
: |  |  :
7.|  |  Q(b)
8.|  |  ∃y Q(y)    ∃I, 7
9.|  ∃y Q(y)       ∃E, 1, 2-8
``````

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.