I'm considering a particular argument while working through Hurley's Concise Introduction:
1. (x)(Ax -> Bx) 2. (x)(Bx -> (E!y)Cxy) 3. (x)(Cxy -> Dx) / (x)(Ax -> Dx)
I verified the validity of this argument using truth-trees. However, moving on to actually deriving the conclusion, my current strategy is to use conditional proof:
1. (x)(Ax -> Bx) 2. (x)[Bx -> (E!y)Cxy] 3. (x)(y)(Cxy -> Dx) 4. | Ax 5. | Bx 6. | (E!y)Cxy 7. | ? 8. | Dx 9. Ax -> Dx 10. (x)(Ax -> Dx)
My first thought would be to use existential instantiation:
1. (x)(Ax -> Bx) 2. (x)[Bx -> (E!y)Cxy] 3. (x)(y)(Cxy -> Dx) 4. | Ax 5. | Bx 6. | (E!y)Cxy 7. | Cxa 8. | Cxa -> Dx 9. | Dx 10. Ax -> Dx 11. (x)(Ax -> Dx)
However, this seems to be a violation of the restriction on universal generalization: according to Hurley, "UG must not be used if the instantial variable [x] is free in any preceding line obtained by EI."
By the time the conditional is discharged at line 10, the instance variable x is free in a line resulting from existential instantiation, line 7.
Given that this argument is valid, what other intuitive ways might you approach this problem? Am I misunderstanding the restriction on universal generalization?
I do want to stress that this is not an assignment.