Skolem constant in existential instantiation for first order logic
Perhaps it will help to discuss this in a broader context, so let me explain this concept with regard to the resolution principle, which is used to check if some formula is unsatisfiable.
Resolution for propositional logic's formulae is rather straightforward and is based on the Conjunctive Normal Form.

We want to apply resolution to first-order formulae, i.e. sort of reduce FOL to propositional logic. One way to do that is to convert the original formula via Skolemization into a formula of the form
$$\forall x_1x_2...x_nM,$$
where $M$ (called 'matrix') is a formula without quantifiers and in CNF. To do this conversion we must get rid of existential quantifiers. The rule you provided does that in the special case where the current existential quantifier is not in scope of any universal quantifiers.

The intuition here is if it is known there exists some $\nu$ for which $\alpha$ holds, then why don't we "pretend" we know that $\nu = k$, where $k$ is some fresh constant. It needs to be 'fresh' in order not to introduce any dependencies between unrelated things. 
And the reason we are allowed to "pretend" we know $\nu$ is that there is a theorem which claims that Skolemization preserves unsatisfiability.

Note: recall that we only want to check if a formula is satisfiable/unsatisfiable, so the skolemized formula is not necessarily equivalent to the original one.