Skolem constant in existential instantiation for first order logic

For any sentence $\alpha$, variable $v$, and constant symbol $k$ that does NOT appear elsewhere in KB: $$\dfrac{\exists \nu. \alpha}{\mathsf{subst}(\{ \nu / k \},\alpha)}.$$ E.g., $∃x. \mathrm{Crown}(x) \wedge \mathrm{OnHead}(x, \mathrm{John})$ yields

$\mathrm{Crown}(C_1) \wedge \mathrm{OnHead}(C_1, \mathrm{John})$

Provided $C_1$ is a new constant symbol (aka Skolem constant)

Can someone clarify the Skolem constant concept?

• '...elsewhere in KB'. What is KB? – Anton Trunov Apr 1 '16 at 12:16
• I don't understand anything in your question before "Can someone clarify." Is that a quote from somewhere? A definition? Something that you believe to be true? Could you add some context to explain what's going on? Or is everything before that last sentence redundant? In that case, you should look up the concept in a textbook. – David Richerby Apr 1 '16 at 20:03
• @Anton KB means knowledge base... I came across what I think was the "inspiration" for that question : divms.uiowa.edu/~tinelli/classes/145/Fall05/notes/… – dader Jun 17 '18 at 12:20

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.