4
$\begingroup$

Edit: answerers keep finding (valid!) problems with my example. I'll try again. The older version is below the horizontal line. Thanks to Klaus below for pointing out the last problem.

My question is how to unify skolemizations that have differing numbers of arguments. As he points out, there is rarely any need for this. For example, if the statements are

Some homes are blue.
There is a home with two stories.

The skolemizations here should not unify, because we can't know from this if a blue home is two-storied.

If we're going to ever need to unify one skolemization with another, we'll need to know we're talking about the same home. This would do it:

Jane's and Mark's home is blue (their only home).
Jane's home has two stories (her only home).

Here it is in FOPC:

$$ \exists x: has(Jane,x) \wedge has(Mark,x) \wedge home(x) \wedge blue(x) \wedge $$ $$ (\forall y: has(Jane,y) \wedge home(y) \implies x=y) \wedge $$ $$ (\forall y: has(Mark,y) \wedge home(y) \implies x=y) $$ and $$ \exists x: has(Jane,x) \wedge home(x) \wedge twoStories(x) \wedge (\forall y: (has (Jane,y) \wedge home(y) \implies x=y) $$

Converting to conjunctive normal form with skolemization gives us this set:

$$ has(Jane,skolem1(Jane,Mark)) $$ $$ has(Mark,skolem1(Jane,Mark)) $$ $$ home(skolem1(Jane,Mark)) $$ $$ blue(skolem1(Jane,Mark)) $$ $$ \neg has(Jane,y) \vee \neg home(y) \vee skolem1(Jane,Mark) =y $$ $$ \neg has(Mark,y) \vee \neg home(y) \vee skolem1(Jane,Mark)=y $$

$$ home(skolem2(Jane)) $$ $$ twoStories(skolem2(Jane)) $$ $$ \neg has (Jane,y) \vee \neg home(y) \vee skolem2(Jane)=y $$

Now, if I want to reason about whether there's a blue house with two stories -- which I should be able to start by resolving the first and last clauses in the set -- I can't, because the two skolemizations can't unify: they have different numbers of arguments.

Is there a good protocol of picking arguments to prevent this problem -- other than applying human intelligence after the mismatch is noticed?

Here is the old version. It's significantly different, but as Klaus pointed out, the old version simply doesn't give us a skolemization problem (or even a skolem for the first statement):

"Everybody who has a home pays utilities on it," encoded as

$$ \forall x: has(x,skolem1(x)) \wedge home(skolem1(x)) \implies paysUtilsOn(x, skolem1(x)) $$
or $$ \bar has(x, skolem1(x)) \vee ~home(skolem1(x)) \vee paysUtilsOn(x, skolem1(x)) $$ and "Jane and Mark have a home," encoded as $$ has(Jane,skolem2(Jane,Mark)) \wedge has(Mark,skolem2(Jane,Mark)) \wedge home(skolem2(Jane,Mark)) $$ or $$ has(Jane,skolem2(Jane,Mark)) $$ $$ has(Mark,skolem2(Jane,Mark)) $$ $$ home(skolem2(Jane,Mark)) $$

I want to use resolution to prove Jane pays utilities. The problem is that skolem1 has 1 argument and skolem2 has 2 arguments, so they don't unify.

I'm not sure if this matters -- could I just refer to skolem1 and skolem2 and forget the arguments entirely? If it does matter, how do I resolve the problem so that skolem1 and skolem2 can unify, and resolution can work? Not by finding a way around the problem, but by truly using skolemization correctly. The issue is what to do with skolems that have different argument lists if they seem to occur naturally.

Improve this question
$\endgroup$
7
  • 3
    $\begingroup$ Some editing comments: 1. Don't assume everyone knows what FOPC means (although we're all fans of the Fair Oaks Presbyterian Church ;) ). 2. The statements in the first sentence don't match the ones you formalise. 3. You can use LaTeX markup ($\forall x \ldots$) to make the formulae clearer. 4. What are skolem1 & skolem2? The Skolemization of their arguments (aren't they already quantifier free)? $\endgroup$
    – Luke Mathieson
    Mar 5, 2015 at 22:20
  • 1
    $\begingroup$ Also, is there something preventing you just using equality and avoiding skolem2 entirely? E.g. $has(\text{Jane},skolem_{1}(\text{Jane})) \wedge has(\text{Mark},skolem_{1}(\text{Mark})) \wedge skolem_{1}(\text{Jane}) = skolem_{1}(\text{Mark})\ldots$ etc. $\endgroup$
    – Luke Mathieson
    Mar 5, 2015 at 22:54
  • $\begingroup$ What I can find on skolemization suggests that skolemizations have, or may have, arguments. Russell & Norvig encodes "Everyone has a heart" as forall x, Person(x)->Heart(F(x))^Has(x,F(x)), so that we are "applying to each person a function that maps from person to heart." It also says "the existentially quantified variable is replaced by a term that consists of a Skolem function applied to the variables universally quantified outside the existential quantifier in question. $\endgroup$
    – Alpha Ralpha Boulevarde
    Mar 6, 2015 at 19:40
  • $\begingroup$ If I don't need arguments to a skolemization, good riddance to them. But if it's logically necessary, at least sometimes, I want to use them correctly. ...Your suggested edits are now applied (thanks), except the one I didn't understand, #4. Skolem1 and skolem2 are Skolem functions. If I'm doing them wrong, do tell me! Thanks-- $\endgroup$
    – Alpha Ralpha Boulevarde
    Mar 6, 2015 at 19:42
  • $\begingroup$ Do you just have to start with the English sentences, and produce any FO sentence that expresses them? Or do you have restrictions (e.g. you're given a starting FP sentence and have to Skolemize it)? Skolemization is just to move existential quantifiers from the inside of the sentence (by introducing a function), so if you don't have existential quantifiers in the middle somewhere, you don't need Skolemization. $\endgroup$
    – Luke Mathieson
    Mar 7, 2015 at 7:25

2 Answers 2

Reset to default
2
$\begingroup$

"Everyone has a heart" gets first encoded first as $\forall x. \text{Person}(x) \Rightarrow \exists y. \text{Hart}(y) \wedge \text{Has}(x,y)$. Then you get the Skolemization (that you found in RN) from that.

Now "Everybody who has a house pays utilities" is just $\forall x. \text{Houseower}(x) \Rightarrow \text{PaysUtilities}(x)$ because there is no assertion that anything exists in this statement. However, if you want to spell out what houseowner means, $\forall x.\text{Houseowner}(x) \Leftrightarrow (\text{Person}(x)\wedge\exists y.\text{House}(y) \wedge Has(x,y))$. And you can skolemize that... but it's not even needed for what you want to infer.

As to "Jane and Mark have a house", it's actually a bit ambiguous. Do they have the same house? But that's an irrelevant detail if you just encode $\text{Houseower}(\text{Jane}) \wedge \text{Houseower}(\text{Mark})$. From that it immediately follows that $\text{Houseower}(\text{Jane})$ and using $\forall x. \text{Houseower}(x) \Rightarrow \text{PaysUtilities}(x)$ it follows that $\text{PaysUtilities}(\text{Jane})$ with the obvious unification $x=\text{Jane}$.

As you can see, the definition of houseowner (which asserts the existence of a house etc.) is completely irrelevant to the inference you wanted. In general, not every "has" in the English language gets translated into a binary predicate, unless it's relevant to what you want to prove. Nobody managed to invent a rigorous way to formally and universally translate all of English (or any other natural language) into first-order logic. While there are some guidelines, a translation of a problem statement from natural language to FO ultimately uses a problem-specific encoding method.

Also note that your first sentence "Everybody who has a house pays utilities" bears some resemblance to a donkey sentence, but it's not actually one; you'd have to say "Everybody who has a house pays utilities on it" to get a donkey sentence.

Improve this answer
$\endgroup$
3
  • $\begingroup$ And translating some statements/problems in the opposite direction, from FO to natural language can result in "paradoxes" or [more more appropriately said] in sentences that are rather non-intuitive; a typical example is the "drinker paradox" which was actually conceived for this purpose. $\endgroup$
    – Fizz
    Mar 8, 2015 at 7:52
  • $\begingroup$ So: should Skolemizations ever have multiple arguments? Or is it more a matter of "work it out however it'll work? ...Or are arguments irrelevant, and you can always just say skolem1(), skolem2(), etc., omitting arguments entirely, because it doesn't matter? $\endgroup$
    – Alpha Ralpha Boulevarde
    Mar 15, 2015 at 19:51
  • $\begingroup$ Maybe that donkey sentence would be a better way of encoding the question. I will make appropriate changes above. $\endgroup$
    – Alpha Ralpha Boulevarde
    Mar 20, 2015 at 14:30
1
$\begingroup$

One issue with your example is that it doesn't say what you seem to think it says. Recall that skolemization is used to eliminate an existentially quantified variable by replacing it with a function depending on whatever universally quantified variables are in scope. Then your initial formula would be the skolemization of

$\forall x\exists y:(has(x,y)\wedge house(y))\Rightarrow paysUtilsOn(x,y)$.

This says that for all $x$ there is some $y$ such that, if $y$ is a house owned by $x$, then $x$ pays utilities on it. This formula is trivially satisfiable by always picking a non-house (or something not owned by $x$) for $y$. The following makes more sense:

$\forall x\forall y:(has(x,y)\wedge house(y))\Rightarrow paysUtilsOn(x,y)$,

i.e. a person pays utilities for every house they own. No existential quantifiers to skolemize away here, though. As for your second statement, Jane and Mark are specific people, so

$\exists y:has(Jane,y)\wedge has(Mark,y)\wedge house(y)$

simply skolemizes to

$has(Jane,s0())\wedge has(Mark,s0())\wedge house(s0())$

(note the complete absence of universally quantified variables).This would change if you had a property like

$\forall x\forall y: partners(x,y)\Rightarrow\exists z:has(x,z)\wedge has(y,z)\wedge house(z)$.

This becomes

$\forall x\forall y:partners(x,y)\Rightarrow has(x,s2(x,y))\wedge has(y,s2(x,y))\wedge house(s2(x,y))$,

and then from $partners(Jane,Mark)$ you could conclude $has(Jane,s2(Jane,Mark))$ and $paysUtilsOn(Jane,s0(Jane,Mark))$.

Improve this answer
$\endgroup$
2
  • $\begingroup$ Your criticism is valid. I'll try to think of a way to repair the example. Of course, the question of unification is still there... but we'll see if we can limit it. $\endgroup$
    – Alpha Ralpha Boulevarde
    Mar 27, 2015 at 14:20
  • $\begingroup$ Regarding the unification: if you get two skolem functions for separate formulas, these corresponds to two separate requirements like "for all x there is a y such that...". There is a priori no reason why these two y should be the same, which is also why unification should usually fail. $\endgroup$
    – Klaus Draeger
    Mar 27, 2015 at 17:36

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

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