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 as long as `y` does not already occur in `Q(b)`
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.| | ∃x Q(x) ∃I, 7 as long as `x` does not already occur in `Q(b)`
9.| ∃x Q(x) ∃E, 1, 2-8
Note: we are not required to use the same bound variable, and may choose to use a different one; .
1.| ∀x ∀y [Likes(x,y) → Likes(y,x)]
2.|_ ∃x ∀y Likes(x,y)
3.| |_ [a] ∀y Likes(a,y) A a is a witness for 2
4.| | ∀y [Likes(a,y) → Likes(y,a)] ∀E 1 [x\a]
5.| | |_ [b] A b is an arbitrary entity
6.| | | Likes(a,b) ∀E 3 [y\b]
7.| | | Likes(a,b) → Likes(b,a) ∀E 4 [y\b]
8.| | | Likes(b,a) →E 6,7
9.| | | ∃y Likes(b,y) ∃I 8 since a exists in context
10.| | ∀x ∃y Likes(x,y) ∀I 5-9 since b is arbitrary
11.| ∀x ∃y Likes(x,y) ∃E 2,3-10 since a does not occur in 10