Computer Science Stack Exchange is a question and answer site for students, researchers and practitioners of computer science. It only takes a minute to sign up.
Sign up to join this community
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?
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.
Another, more informal way to look at it is that by introducing a skolem constant you extend the language of your logic. You start by defining a language with a fixed store of constant symbols, each bound to a semantic value. Then you quantify existentially using variable v in an open sentence and find some (unknown, indeterminate) semantic value that satisfies the form in which v appears, turning it into a proposition. So you extend the language by adding a fresh constant and binding it to that value. Now you can write a proposition using that symbol.
