# 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? Commented Apr 1, 2016 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. Commented Apr 1, 2016 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/… Commented Jun 17, 2018 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.