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.
Don't be confused by their use of $[x]$. The important issue is that whatever letter is used, it is the instantiation variable.
Here it is $a$ that is the instantiation variable. Since this $a$ does not occur free in any line preceding the instantiation, you may use existential generalisation on anything where it occurs consequent of the instantiation.
Further, since $a$ does not even occur in the conclusory $Dx$, existential generalisation is not required.
$${\vdots\\(\forall x)(\forall y)(Cxy\to Dx)\text{ here}\\\quad{\mid\quad{Ax\hspace{34ex}\text{Assumption (arbitrary $x$ occurs free)}\\\vdots\\(\exists!y)Cyx\\(\exists y)(Cxy\wedge(\forall z)(Cxz\to z=y))\hspace{5ex}\text{A Definition of uniqueness}\\\quad{ Cx\color{red}a\wedge(\forall z)(Cxz\to z=\color{red}a)\hspace{9ex}\text{Existential Instance (witnessed by }\color{red}a)\\Cx\color{red}a\hspace{31ex}\text{Simplification}\\Cx\color{red}a\to Dx\hspace{24ex}\text{Universal Instantiation}}\\Dx\hspace{34ex}\textit{Modus Ponens}\text{ ($a$ no longer occurs)}}\\Ax\to Dx}\\(\forall x)(Ax\to Dx)}$$
[It is helpful to use indentation to identify where an instantation variable occurs, to ensure the rules are cleanly followed. This is optional.]