Symbolic Logic, Irving M. Copi, Prentice Hall, 1979, 5th edition, Part II, exercise 8, p.134

Old man Copi has left a number of quirky brain teasers in his Symbolic Logic (1979), which has been the core of college level logic courses in some universities. Professor Peter Suber, from Earlham College, posted answers to many of them in his course hand-outs for the academic year 1996-97: http://www.earlham.edu/~peters/courses/log/loghome.htm At one point though, he gives up saying: 'I haven't had time to finish this set of exercises. I hope to do soon ...' (Polyadic Predicate Logic). When I last emailed him, he said he had retired. He left off at what is in my edition Part II, exercise 8, p. 134. Symbolize the following argument and construct a formal proof of validity:

There is a professor who is liked by every student who likes at least one professor. Every student likes some professor or other. Therefore, there is a professor who is liked by all students.

1. (∃x){Px • (y){[Sy • (∃z)(Pz • Lyz)] ⊃Lyx]}
2. (y)[Sy ⊃(∃x)(Px • Lyx)]
3. ∴(∃x)[Px • (y)(Sy ⊃Lyx)]
4. Pa • (y){[Sy • (∃z)(Pz • Lyz)] ⊃Lya] / 1EI
5. Pa / 4Simp
6. (y){[Sy • (∃z)(Pz • Lyz)] ⊃Lya] / 4Simp
7. * Sy / ACP
8. * Sy ⊃(∃x)(Px • Lyx) / 2UI
9. * (∃x)(Px • Lyx) / 7,8MP
10. * Pm • Lym / 9EI
11. * (∃z)(Pz • Lyz) / 10EG
12. * Sy • (∃z)(Pz • Lyz) / 7,11Conj
13. * [Sy • (∃z)(Pz • Lyz)] ⊃Lya / 6UI
14. * Lya / 12,13MP
15. Sy ⊃Lya / 7-14CP
16. (y)(Sy ⊃Lya) / 15UG
17. Pa • (y)(Sy ⊃Lya) /5,16Conj
18. (∃x)[Px • (y)(Sy ⊃Lyx)] / 17EG

The least obvious strategy here perhaps involves a change of variable, from 'x' on line 9 to 'z' on line 11 by first instantiating it to a constant, other than 'a', by Existential Instantiation and then generalising it back to a variable by Existential Generalisation.