1
$\begingroup$

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?

$\endgroup$
  • 2
    $\begingroup$ '...elsewhere in KB'. What is KB? $\endgroup$ – Anton Trunov Apr 1 '16 at 12:16
  • 1
    $\begingroup$ 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. $\endgroup$ – David Richerby Apr 1 '16 at 20:03
  • 2
    $\begingroup$ @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/… $\endgroup$ – dader Jun 17 '18 at 12:20
3
$\begingroup$

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.

$\endgroup$
1
$\begingroup$

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.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.