Universal introduction - how exactly does it work? How does universal introduction work? 
I have tried something like this :
1) $\exists x: p(x) \Rightarrow p(x) $ 
I'm using this rule and I'm getting something like this:
2) $\exists x: p(x) \Rightarrow \forall x: p(x) $
Next someone on this forum once said that this is wrong, could you explain why?
Next I have tried doing something like this:
Now I 'm using Existential instantiation which gets me:
3) $ p(a) \Rightarrow \forall x: p(x) $
Here Universal instantiation which leads me to :
4) $p(a) \Rightarrow p(a) $
What don't I understand in those rules?
 A: (A) The basics. Informally, the idea is this. If you have established $\phi(a)$ for some arbitrarily chosen object $a$ in the domain and relying on no special "inside knowledge" about $a$ in particular, then you are entitled to infer $\forall x\phi(x)$. 
So we get a UI rule like this: given you have established $\phi(a)$, where the parameter ("temporary name") $a$ doesn't appear in the premisses you've ultimately used [that ensures that you are indeed using no special knowledge about $a$!], then you can infer $\forall x\phi(x)$. NB the introduced quantifier has to go right at the front! You are saying $\phi$ applies to this, but this is an arbitrary example, so everything is $\phi$.
Now, some presentations of first-order logic recruit variables $x$ to serve double duty as parameters. Don't let that confuse you. Use different letters for free and bound variables if that helps. In this sort of presentation, the rule will be that if you have established $\phi(x)$ where the unbound-variable-$x$-used-as-a-parameter doesn't appear in any premiss that you rely on [and that will be guaranteed if you insist that premisses can't have free variables!], then you can infer $\forall x\phi(x)$. NB, to repeat, the introduced quantifier has to go right at the front!

(B)Turning to the first example. What is the wff here? In unambiguous notation is it


*

*$\exists x(Px \to Px)$

*$(\exists xPx \to Px)$


If (1), then the sentence $\exists x (Px \to Px)$ hasn't got any parameters/free variables in it: both occurrences of $x$ inside the bracket are already bound by the initial quantiser. So, on one standard story [the best sort!] you can't apply universal quantifier introduction at all. If on the other hand your system allows vacuous quantification, then you are always allowed to infer $\forall y\exists x (Px \to Px)$ or even $\forall x\exists x (Px \to Px)$ with the useless dangling quantifier that does no work. But NB, the added vacuous universal quantifier, if allowed, has to go right at the front, as it is the whole wff that is quantified in a move of UI.
If (2) then the second $x$ is free. But that still does NOT by itself mean that you can apply UI. It will depend on what premisses you have used to in getting as far as (2) in your proof! Does the parameter occur free in a premiss? If it does, you are in trouble! IN particular, you can't apply UI to (2) if (2) is your only premiss!!!
But if you've got (2) from premisses which don't contain $x$ free, then you can infer $\forall y(\exists xPx \to Py)$ or, if you insist, $\forall x(\exists xPx \to Px)$ by UI. NB the quantifier is at the front! And then by further steps  we can infer $(\exists xPx \to \forall x Px)$: but note that takes more work and further rules.
Is that last result weird? No! You'll only be able to infer (2) $(\exists xPx \to Px)$ with its free variable from some generalization about all $x$! So not such a surprise that you can go on to recover a generalization about all $x$! 
