Skolemization with multiple arguments -- how to unify 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.
"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.