Using existential generalization repeatedly.

Question

The statement I'm trying to prove:

$\exists x\left[R\left(x,\:x\right)\right]\:^{\:}\wedge \:\left[\forall x\exists y\left[R\left(x,\:x\right)\rightarrow P\left(x,y,y\right)\right]\right]\rightarrow \exists x\exists y\exists z\left[P\left(x,y,z\right)\right]$

We can start with:

$1. \exists \:x\left[R\left(x,\:x\right)\right] (Premise)$

$2. \forall \:x\exists \:y\left[R\left(x,\:x\right)\rightarrow \:P\left(x,\:y,\:y\right)\right] (Premise)$

$3. R(a,a)$ $(1, Existential Instantiation)$

$4. \exists \:y\left[R\left(a,\:a\right)\rightarrow \:P\left(a,\:y,\:y\right)\right]$ (2, Universal Instantiation)

$5. R\left(a,\:a\right)\rightarrow \:P\left(a,\:b,\:b\right)$ (4, Existential Instantiation)

$6. P(a,b,b) (3,5,Modus Ponens)$

And from this point I'm not sure how I should carry on, I assume that if I'll be using existential generalization then I'll have to replace all free occurrences of the constant with the variable (As mentioned in Wikipedia) which doesn't make it possible for me to reach the conclusion.

Answer 1

Consider the formula $\exists z P(a,b,z)$.

Here we have that $Q(z)$ is $P(a,b,z)$ and $P(a,b,b)$ is obtained replacing all free instances of $z$ in $P(a,b,z)$.

Thus, applying the rule, we get:

$P(a,b,b) \to \exists z P(a,b,z)$.

The rule does not say that you have to replace all occurrences of $a$ in $Q(a)$ with $x$ to get $Q(x)$, but says that you have to start for (the suitable) $Q(x)$ and get $Q(a)$.